Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
Rewriting Diagrams
Diagram rewriting replaces a piece of a diagram matching a pattern with another piece, reconnecting the wires. Matching happens on the diagram's hypergraph structure, so rules are insensitive to layout and port naming — formal pattern symbols in port positions bind to whatever wiring the match finds. This tech note builds rewrite rules for algebraic laws and applies them with and .
In[1]:=
<<Wolfram`DiagrammaticComputation`
Structural Rules
A rewrite rule is a between two diagrams whose ports carry patterns. Associativity of a binary operation rewires the parenthesisation of a double application:
f
In[2]:=
associativity=
[f_,{p_,p3_},p4_],
[f_,{p1_,p2_},p_]
[f,{p1,p},p4],
[f,{p2,p3},p]
 | DiagramComposition |
 | Diagram |
| Diagram |
| DiagramComposition |
| Diagram |
| Diagram |
Out[2]=
Coassociativity is the mirror law for a binary cooperation:
In[3]:=
coassociativity=
[f_,p_,{p2_,p3_}],
[f_,p1_,{p_,p4_}]
[f,p,{p3,p4}],
[f,p1,{p2,p}]
| DiagramComposition |
| Diagram |
| Diagram |
| DiagramComposition |
| Diagram |
| Diagram |
Out[3]=
Applying Rules
A tree of binary operations and cooperations to rewrite:
A
B
In[4]:=
diag=
[C,p],
[B,p,{p,p}],
[B,p,{p,p}],
[A,{p,p},p],
[A,{p,p},p],
[p],
[D,p,p]
 | Diagram |
| DiagramRightComposition |
| DiagramProduct |
 | Diagram |
| DiagramComposition |
| Diagram |
| Diagram |
| DiagramComposition |
| Diagram |
| DiagramProduct |
| Diagram |
| IdentityDiagram |
| Diagram |
Out[4]=
enumerates every possible single application of the rule:
In[5]:=
 | DiagramReplaceList |
Out[5]=
Several rules can be tried at once:
In[6]:=
| DiagramReplaceList |
Out[6]=
,
applies the first match only:
In[7]:=
| DiagramReplace |
Out[7]=
In[8]:=
| DiagramNestReplace |
Out[8]=
Interaction-Net Rules
The paclet provides constructors for the standard interaction-net rule schemas. Two facing copy nodes annihilate into parallel wires:
A node commutes past a copy node, duplicating itself:
An eraser propagates through a process, erasing it port by port:
Erasing one branch of a copy leaves a plain wire:
These rules drive lambda-calculus evaluation as interaction nets: beta reduction is an annihilation between a lambda node and an application node, and copy/erase rules implement sharing and garbage collection.
Inspecting the Matcher