First-order interaction nets

Fix a finite signature $\mathrm{\Sigma }$ and $\mathrm{ar}:\mathrm{\Sigma }\to \mathbb{N}$. An occurrence of $\alpha \in \mathrm{\Sigma }$ has one principal port and $\mathrm{ar}(\alpha )$ ordered auxiliary ports. A net is a finite set of agents and finite wiring components: an interval may attach at zero, one, or two agent ports and a circle is a closed wire. Each agent port is incident to at most one component; the ordered free interval ends form the interface. An active pair $\alpha \bowtie \beta$ is a wire between two principal ports.

An interaction rule replaces one active pair by a net with the same ordered boundary. The system supplies at most one rule for each unordered symbol pair. Reduction $$N{⟶}_{I}M$$ replaces a matching active pair by a fresh copy of that right-hand side and reconnects corresponding boundary ports. Net equality in the metatheory is interface-fixing graph isomorphism $N\cong M$, including consistent renaming of fresh internal data.

The chapter’s unary arithmetic instance has nullary $Z$, unary $S$, and binary $A$. Boundary names make its two rules $$A(y,r)\bowtie Z{⟶}_{I}y=r,$$ $$A(y,r)\bowtie S(x){⟶}_{I}r=S(s)\text{with}A(y,s)\bowtie x.$$ Here an equation between boundary names means a wire splice.

For exactly-once lambda terms, the named syntactic translation $\mathcal{T}(t)$ uses binary agents $\mathsf{Lam}$ and $\mathsf{App}$. Its beta interaction is $$\mathsf{App}(\mathcal{T}(u),r)\bowtie \mathsf{Lam}(x,\mathcal{T}(t)){⟶}_{I}x=\mathcal{T}(u),r=\mathcal{T}(t).$$ It realizes $\mathcal{T}((\lambda x.t)u){⟶}_I\mathcal{T}(t[u/x])$ only for the exactly-once fragment. Duplication and erasure require additional agents.

For a finite constructor signature, a nullary eraser $E$ and binary duplicator $D$ may be given one rule against each constructor: $$E\bowtie \alpha (x_1,\dots ,x_n){⟶}_{I}E\bowtie x_1,\dots ,E\bowtie x_n,$$ These rules calculate only on finite constructor trees. Unary-normal-form readback is the external function $\mathrm{rb}(Z)=0$ and $\mathrm{rb}(S(x))=1+\mathrm{rb}(x)$. For a constructor template with $k$ occurrences of its binder, the named translation ${\mathcal{T}}_{\mathrm{res}}$ connects that binder to $E$ for $k=0$, to a wire for $k=1$, and to a fixed full binary tree of $k-1$ duplicators for $k\ge 2$. This is the finite constructor-tree fragment of theorem 41.17, not a general lambda translation.

The interaction-combinator signature has binary $\gamma ,\delta$ and nullary $\epsilon$. With intrinsic binary-port order $1,2$, five of its six exact rules are For the sixth, mixed rule, fresh $p_{ij}$ give Each old boundary name occurs once on each side and every fresh wire name twice on the right. These equations are the six source diagrams in explicit ordered-port form.

The pinned HVM2 document names ten paper interactions: Link, Call, Void, Erase, Commute, Annihilate, Operate1, Operate2, Switch1, and Switch2. The pinned C/CUDA dispatcher uses eight classes: LINK, CALL, VOID, ERAS, COMM, ANNI, OPER, and SWIT. ERA/CON/DUP occupy the $\epsilon /\gamma /\delta$ eraser/constructor/duplicator roles, but this role map does not prove identity of intrinsic auxiliary-port order. The remaining tags and global link state extend the abstract combinator signature. Its two independent ERA–ERA candidates dispatch to VOID; the chapter 41 microbenchmark leaves a numeric-zero root for readback after two interactions.

INAMB and the textual INMPP calculus

The binary-choice agent has two principal ports and two auxiliaries. In the right-hand-side convention of Fernández–Khalil Definition 4.2, its complete rules against any ordinary agent $\alpha$ are $$(-,\ell )\mathsf{amb}(\alpha (\overrightarrow{x}),\ell )\bowtie \alpha (\overrightarrow{x}),(\ell ,-)\mathsf{amb}(\alpha (\overrightarrow{x}),\ell )\bowtie \alpha (\overrightarrow{x}).$$ INMPP terms, multiequations, and configurations are Every name occurs at most twice. Interface terms are INMPP-normal as in Definition 4.3: auxiliary subterms are normal and a principal variable of a term or subterm occurs at most once in the whole term.

Writing $\mathsf{N}(q)$ for the names in $q$, the two basic indirections are Indirection 3 selects one component of a multiequation: If the source rule at principal ports $p,q$ has fresh right-side data $$({\overrightarrow{\ell }}^{\prime },{\overrightarrow{k}}^{\prime },{\overrightarrow{s}}^{\prime },{\overrightarrow{u}}^{\prime },\mathit{eq}),$$ then Interaction is The fresh tuple is alpha-renamed before insertion. The two collection rules are The first requires $x\in \mathsf{N}(\overrightarrow{t})$, INMPP-normal $u$, and no principal variable of $u$ in $\mathrm{\Delta }$; the second has the analogous normality and freshness conditions. Multiset congruence closes these rules under permutation of the equation multiset before and after a step.

With polarized port types ${\sigma }^s$, the structural rules are $$\frac{\phantom{X}}{x:{\sigma }^s,x:{\sigma }^{-s}}\mathrm{Ax}\frac{\begin{array}{c}\mathrm{\Gamma },t:{\sigma }^s\\ \mathrm{\Delta },u:{\sigma }^{-s}\end{array}}{\mathrm{\Gamma },\mathrm{\Delta },t=u:\diamond }\mathrm{Cut},$$ $$\frac{\begin{array}{c}\{{\mathrm{\Gamma }}_i,{\ell }_i:{\sigma }_i^{-s_i}{\}}_{1\le i\le m}\\ \mathrm{\Gamma },\alpha (\overrightarrow{t}):({\sigma }_1^{s_1},\dots ,{\sigma }_m^{s_m})\end{array}}{{\mathrm{\Gamma }}_1,\dots ,{\mathrm{\Gamma }}_m,\mathrm{\Gamma },({\ell }_1,\dots ,{\ell }_m)\alpha (\overrightarrow{t}):\diamond }\mathrm{MultiCut}$$ The selected form exposes one principal port: Every agent contributes a Graft rule. In particular, $$\frac{\mathrm{\Gamma },t_0:{\phi }^s,t_1:{\phi }^s}{\mathrm{\Gamma },\mathsf{amb}(t_0,t_1):({\phi }^s,{\phi }^s)}\mathrm{Graft}-\mathrm{amb}.$$