|
| 1 | +# Theory |
| 2 | + |
| 3 | +This project is all about interaction combinators. Interaction |
| 4 | +combinators are a subset of interaction nets, a graphical model of |
| 5 | +computation. Specifically, we have two variadic agents; the constructor |
| 6 | +and duplicator. *Agents* (like nodes in a graph) are connected by |
| 7 | +*wires* (edges). The final graph is called a *net*. In our case, these |
| 8 | +wires are directed (*polarized* - another subset of interaction |
| 9 | +combinators). |
| 10 | + |
| 11 | +Specifically, agents consist of *ports* where one end of a wire is |
| 12 | +connected to. Each port can only be connected to a single port with a |
| 13 | +single wire (linearity). Ports are either positive (+) or negative (-). |
| 14 | +Only positive ports can be connected by wire to negative ports and |
| 15 | +vice-versa. |
| 16 | + |
| 17 | +There exist two port variants: *Principal ports* and *auxiliary ports*. |
| 18 | +Each agent has exactly one principal port and 0-n auxiliary ports. When |
| 19 | +the principal ports of two agents are connected by wire, they can |
| 20 | +*interact*. Interaction is the only kind of net reduction. Through |
| 21 | +interaction, both interacting agents get removed, while the other ends |
| 22 | +of the wires of both agent's auxiliary ports can be rewired arbitrarily |
| 23 | +to each other or to new agents constructed through the interaction. The |
| 24 | +interaction is therefore entirely local, as an interaction can never |
| 25 | +interfere with another interaction. |
| 26 | + |
| 27 | +We write constructors `c` and duplicators `d` using the following |
| 28 | +grammar: |
| 29 | + |
| 30 | + p ::= + | - |
| 31 | + l ::= a, b, abc, ... |
| 32 | + c ::= lp(lp, ..., lp) |
| 33 | + d ::= lp[lp, ..., lp] |
| 34 | + |
| 35 | +For example: |
| 36 | + |
| 37 | + a+(b+, b-) |
| 38 | + a-[c+, c-] |
| 39 | + |
| 40 | +Here, the principal ports `a` of both agents are connected to each |
| 41 | +other, while the auxiliary ports are connected per agent (`b+ -> b-` and |
| 42 | +`c+ -> c-`). |
| 43 | + |
| 44 | +In interaction nets, the interaction *rule* that specifies the precise |
| 45 | +graph rewrite can be chosen arbitrarily by the interpreter (interaction |
| 46 | +system). Due to the restricted set of agents, interaction combinators |
| 47 | +can interact in one of two ways: Commutation (interaction between |
| 48 | +duplicator and constructor), or annihilation (interaction between |
| 49 | +constructor and constructor). |
| 50 | + |
| 51 | +The interaction between two duplicators depends on the desired semantics |
| 52 | +-- for the semantics of the subset of the lambda calculus typable in the |
| 53 | +Elementary Affine Logic (EAL), duplicators must have labels that specify |
| 54 | +whether two interaction duplicators annihilate or commute. To support |
| 55 | +the semantics of the full lambda calculus, you have to additionally |
| 56 | +insert control agents into the net ("bookkeeping", "oracle")\*. In this |
| 57 | +experimental project, we always annihilate two connected duplicators. |
| 58 | + |
| 59 | +*Commutation* of two n-ary agents (ζ = constructor, δ = duplicator): |
| 60 | + |
| 61 | + │⋯│ │ │ |
| 62 | + ╭┴─┴╮ ╭─┴─╮ ╭─┴─╮ |
| 63 | + │ ζ │ │ δ │ ⋯ │ δ │ |
| 64 | + ╰─┬─╯ ╰┬─┬╯ ╰┬─┬╯ |
| 65 | + │ │ ╰───╭───╯ │ |
| 66 | + │ ───────► │ │ │ |
| 67 | + │ │ ╭───╯───╮ │ |
| 68 | + ╭─┴─╮ ╭┴─┴╮ ╭┴─┴╮ |
| 69 | + │ δ │ │ ζ │ ⋯ │ ζ │ |
| 70 | + ╰┬─┬╯ ╰─┬─╯ ╰─┬─╯ |
| 71 | + │⋯│ │ │ |
| 72 | + |
| 73 | +*Annihilation* of two n-ary agents: |
| 74 | + |
| 75 | + │⋯│ │ ⋯ │ |
| 76 | + ╭┴─┴╮ │ │ |
| 77 | + │ ζ │ │ │ |
| 78 | + ╰─┬─╯ ╰─╭─╯ |
| 79 | + │ │ |
| 80 | + │ ───────► │ |
| 81 | + │ │ |
| 82 | + ╭─┴─╮ ╭─╯─╮ |
| 83 | + │ ζ │ │ │ |
| 84 | + ╰┬─┬╯ │ │ |
| 85 | + │⋯│ │ ⋯ │ |
| 86 | + |
| 87 | +Notably it can very well happen that a duplicator interacts with a |
| 88 | +constructor that has different polarities for some of its auxiliary |
| 89 | +ports. In this case, the resulting duplicators (at the top right) turn |
| 90 | +into a variant with different polarizations at their principal ports. A |
| 91 | +common example is the dual of the duplicator (called superposition): |
| 92 | +`x+[x1-, x2-, x3-]` (sup) vs `x-[x1+, x2+, x3+]` (dup). |
| 93 | + |
| 94 | +\*(as interaction combinators are Turing complete: the full lambda |
| 95 | +calculus could also be fully supported without control nodes -- in fact |
| 96 | +there is a lot of literature on that --, but you lose part of the reason |
| 97 | +why you would typically want to translate to interaction nets in the |
| 98 | +first place; this being increased sharing even under abstractions, |
| 99 | +incremental superpositions, "optimal reduction") |
| 100 | + |
| 101 | +## Lambda Calculus |
| 102 | + |
| 103 | +We choose the following translation: |
| 104 | + |
| 105 | + ₚ┌┄┄┄┄┄┄┐ |
| 106 | + ⟦M⟧ = ◯──┤ ⟦M⟧ₚ ┊ |
| 107 | + └┄┄┄┄┄┄┘ |
| 108 | + |
| 109 | + |
| 110 | + p |
| 111 | + ┌┄┄┄┄┄┄┄│┄┄┄┄┄┄┄┄┄┄┄┐ |
| 112 | + ┊ ╭─┴─╮+ ┊ |
| 113 | + ┊ │ ζ │ ┊ |
| 114 | + ┊ +╰┬─┬╯- ┊ |
| 115 | + ⟦λx.M⟧ₚ = ┊ x╭─╯ ╰───╮m ┊ = p+(x+, m-) |
| 116 | + ┊ ┌─┴─┐ ┌┄┄┴┄┄┄┐ ┊ |
| 117 | + ┊ │ δ ╞══╡ ⟦M⟧ₘ ┊ ┊ |
| 118 | + ┊ └───┘ └┄┄╥┄┄┄┘ ┊ |
| 119 | + └┄┄┄┄┄┄┄┄┄┄┄┄║┄┄┄┄┄┄┘ |
| 120 | + fv(λx.M) |
| 121 | + ↑ |
| 122 | + perfectly dual! |
| 123 | + ↓ |
| 124 | + fv(M) |
| 125 | + ┌┄┄┄┄┄┄┄┄║┄┄┄┄┄┄┐ |
| 126 | + ┊ ┌┄┄╨┄┄┄┐ ┊ |
| 127 | + ┊ ┊ ⟦M⟧ₘ ┊ ┊ |
| 128 | + ┊ └┄┄┬┄┄┄┘ ┊ |
| 129 | + ┊ │m ┊ |
| 130 | + ┊ ╭─┴─╮- ┊ |
| 131 | + ⟦M N⟧ₚ = ┊ │ ζ │ ┊ = m-(n-, p+) |
| 132 | + ┊ -╰┬─┬╯+ ┊ |
| 133 | + ┊ n╭─╯ ╰─╮ ┊ |
| 134 | + ┊ ┌┄┄┴┄┄┄┐ │ ┊ |
| 135 | + ┊ ┊ ⟦N⟧ₙ ┊ │ ┊ |
| 136 | + ┊ └┄┄╥┄┄┄┘ │ ┊ |
| 137 | + └┄┄┄┄┄║┄┄┄┄┄│┄┄┄┘ |
| 138 | + fv(N) p |
| 139 | + |
| 140 | +Beware of edge cases in the abstraction translation: If the variable is |
| 141 | +bound once (linearly), no duplicator is required. If it is not bound at |
| 142 | +all, the duplicator is nilary and becomes an eraser. |
| 143 | + |
| 144 | +## Resources |
| 145 | + |
| 146 | +Drawings were done by me (for another project). |
| 147 | + |
| 148 | +We refer to an excellent collection of interaction net resources: |
| 149 | +https://github.com/marvinborner/interaction-net-resources |
| 150 | + |
| 151 | +There's no actually novel theory in this project. |
0 commit comments