Interaction Nets and Interaction Combinators

Prerequisites. Direct starred prerequisites: Chapter 40. No later core chapter depends on this route.

Forget the formula labels on a proof net and retain a finite graph of nodes and connection points. Each node has one distinguished connection point. A local rewrite is triggered only when the distinguished points of two nodes meet. Because a distinguished point has at most one mate, two different redexes cannot share a node.

An interaction net is such a finite port graph, with one distinguished port per node and rewrites triggered where two distinguished ports meet.

The bridge from chapter 40 is literal at the local level. Regard the tensor and par links as binary agents whose formula roots are principal ports: a multiplicative proof-net cut is then the active pair $\otimes \bowtie \mathrm{\wp }$, a pair of agents joined at their distinguished ports, and its two smaller cuts are the two boundary reconnections joining the four exposed ports. The proof-net atomic axiom–cut splice is the corresponding nullary wiring case. Interaction nets retain this principal-port mechanism while discarding the logical formula labels.

Agents, ports, and interfaces

An agent symbol $\alpha$ has an arity $\mathrm{ar}(\alpha )$. An occurrence of $\alpha$ has one distinguished principal port, at which a rewrite may be triggered, and $\mathrm{ar}(\alpha )$ ordered auxiliary ports, which form the rewrite boundary. The arity counts auxiliary ports, not all ports. In diagrams a triangle points toward the principal port: Diagram This picture has arity two. The order $1,2$ is data even though wires may be drawn with different bends.

A wire has no direction and no value moving along it. Its endpoints only record incidence. Ordering the free ports lets a net denote a component with a stable external calling convention. Rewriting may replace its interior, but not reorder, duplicate, or discard that interface.

Diagram

Local rules and reduction

A rule has a left-hand active pair and a right-hand net with the same ordered boundary. If $\alpha$ has arity $m$ and $\beta$ arity $n$, removing the active pair exposes $m+n$ auxiliary wires. The right-hand side must expose exactly those $m+n$ boundary ports, in that order.

These are Lafont’s interaction-net ingredients, with the interface made explicit for the proofs below [Laf90].

The two restrictions do different work. Boundary preservation makes a rule compositional: the context cannot detect which internal representation was used. Uniqueness for a symbol pair prevents two rules from competing for the same active pair.

Proof of Lemma 41.5 — Distinct redexes are disjoint

Proof. An agent has exactly one principal port. If an occurrence belonged to two active pairs, that one port would be matched to the principal ports of two different agents. A partial matching gives it at most one mate. Hence the two active pairs would be the same pair. ◻

A complete arithmetic system

Before considering lambda terms, we calculate in a system small enough to inspect completely. Unary naturals have constructors $Z$ of arity zero and $S$ of arity one. An addition agent $A$ has arity two. Its auxiliary ports are the second addend $y$ and result $r$; its principal port consumes the first addend.

Write $\bar{n}$ for a chain of $n$ successors ending in $Z$.

Proof of Proposition 41.7 — Addition calculates

Proof. Induct on $m$. For $m=0$, the $A\bowtie Z$ rule splices the second addend directly to $r$, in one step. For $m+1$, the $A\bowtie S$ rule creates one output $S$ and leaves $A(\bar{n},s)\bowtie \bar{m}$ behind it. The induction hypothesis takes $m+1$ further steps, so the total is $m+2$, and the output is $S(\overline{m+n})=\overline{m+1+n}$. ◻

The one-step diamond

Ordinary local confluence permits each branch to take several steps before joining. Interaction systems satisfy a sharper property.

Proof of Theorem 41.9 — Strong confluence of interaction systems

Proof. Consider reductions of $N$ at redexes $r_1$ and $r_2$. If the redexes coincide, the unordered pair of symbols determines at most one rule. Fresh names may differ, but the two contracta are isomorphic.

If the redexes are distinct, lemma 41.5 says that their agent occurrences are disjoint. Contracting $r_1$ changes only its local interior and reconnects the same boundary ports, so $r_2$ remains an active pair. Apply the same argument after the exact renaming $r_1\leftrightarrow r_2$: $r_1$ remains after contracting $r_2$. Contract the surviving redex on each branch. Both results replace the same two disjoint subgraphs by fresh copies of the same two right-hand sides, and are therefore isomorphic after renaming fresh internal data. ◻

Diagram

The qualification “modulo isomorphism” matters whenever a rule creates fresh internal names.

Proof of Corollary 41.10 — Confluence

Proof. Pass to interface-fixing isomorphism classes of nets. The isomorphism branch of definition 41.8 becomes equality, and the other branch is a literal one-step diamond. Induct on the length of the first reduction: push its first step across the first step of the other reduction, transport the remaining reduction along the resulting isomorphism, and apply the induction hypothesis to the shorter strip. Lifting the join from isomorphism classes gives representatives $P_1\cong P_2$. If both endpoints are normal, their joining reductions are empty, so the endpoints are isomorphic. ◻

Confluence is not termination. Add a nullary symbol $\mathrm{\Omega }$ and the rule $\mathrm{\Omega }\bowtie \mathrm{\Omega }{⟶}_I\mathrm{\Omega }\bowtie \mathrm{\Omega }$, using a fresh copy of the same two-agent active pair. The resulting system remains strongly confluent but admits an infinite reduction.

Parallel developments

A finite set of initially active pairs may be contracted in any order because those pairs are disjoint.

Because initial active pairs are disjoint, contracting one neither erases nor duplicates another. Each has one unambiguous residual until it is contracted.

Proof of Theorem 41.12 — Independence of developments

Proof. Every development lists each member of $R$ exactly once, through its unique residual, so its contraction order is a permutation of $R$. Any two finite permutations are connected by adjacent transpositions. It is therefore enough to exchange two consecutive contractions $r,s$. Their residual active pairs are disjoint, so the one-step diamond gives $N_{rs}\cong N_{sr}$. An interface-fixing isomorphism carries every remaining agent occurrence, hence every remaining residual, to its mate; the common suffix can therefore be replayed on the other representative. Each adjacent transposition preserves the endpoint up to isomorphism, and a finite chain of them relates any two developments. Since each member has exactly one residual and is contracted once, every development has $|R|$ steps. ◻

Thus an already chosen frontier can execute in parallel. Newly created redexes still require synchronization, and the theorem gives no bound on work to normal form.

A linear lambda fragment

A full untyped lambda encoding must account for weakening and contraction. For exactly-once terms, however, the beta step is represented by wiring alone.

The translation $\mathcal{T}(t)$ has one root interface port and one interface port for each free variable, in a fixed order. A variable is a wire from its free-variable port to the root. A binary $\mathsf{Lam}$ agent has auxiliary ports for the binder and body; a binary $\mathsf{App}$ agent has auxiliary ports for argument and result. The principal ports of $\mathsf{Lam}$ and $\mathsf{App}$ meet precisely when an abstraction is used as a function. Their rule splices argument to binder and body to result: $$\mathsf{App}(\mathcal{T}(u),r)\bowtie \mathsf{Lam}(x,\mathcal{T}(t)){⟶}_{I}x=\mathcal{T}(u),r=\mathcal{T}(t).$$ The displayed names denote the four exposed boundary wires. Exactly-once use ensures that the binder has one endpoint to splice.

Proof of Theorem 41.14 — One beta step

Proof. By construction, the outer application connects the principal port of its $\mathsf{App}$ agent to the principal port of the translated abstraction’s $\mathsf{Lam}$ agent. Their rule removes those agents, connects the root of $\mathcal{T}(u)$ to the unique free-$x$ port of $\mathcal{T}(t)$, and connects the body root to the result. This is exactly the inductive translation of postfix capture-avoiding substitution $t[u/x]$. The free interfaces are disjoint by definition 41.13, so no other wire is changed. ◻

Proof of Corollary 41.15 — Exact beta correspondence

Proof. Induct on $v$. A variable has neither kind of redex. Under an abstraction, both sets are exactly those in the body, so use the induction hypothesis. In an application $tu$, the pairs inside the two disjoint subnet translations correspond to the redexes inside $t$ and $u$ by induction. There is one additional active pair at the application root exactly when $t=\lambda x.w$; that is exactly the additional beta-redex occurrence. Theorem 41.14 proves that contracting this pair yields $\mathcal{T}(w[u/x])$ up to interface-preserving isomorphism. Compatible translation contexts reconnect the same ordered boundary, so an inner contraction also produces $\mathcal{T}(v^{\prime })$. No other pair can appear across the disjoint free-variable interfaces. ◻

The two-occurrence term exposes the failure in symbols. Translating the application in $\lambda x.xx$ would require the one binder endpoint $b_x$ to satisfy $$b_x=u_1\text{and}{b}_x=u_2,u_1\ne u_2,$$ where $u_1,u_2$ are the two variable-interface endpoints. A port belongs to at most one wire, so the second equation cannot be added. The repair must introduce an explicit duplicator whose two outputs meet $u_1,u_2$.

Erasure, duplication, and readback

The obstruction in the last exercise can be made local for finite constructor trees. Add a nullary eraser $E$ and a binary duplicator $D$, whose auxiliary ports are its two outputs. For every constructor symbol $\alpha$ of arity $n$, add the rules $$E\bowtie \alpha (x_1,\dots ,x_n){⟶}_{I}E\bowtie x_1,\dots ,E\bowtie x_n,$$ The first right side is empty when $n=0$. The equations on the second right side attach two fresh copies of the root to the two output wires, then send one duplicator down each child. Both schemas preserve their ordered boundaries. They are finitely many rules only when the constructor signature is finite.

Proof of Proposition 41.16 — Resource-manager calculation

Proof. Induct on $U=\alpha (U_1,\dots ,U_n)$. The root interaction takes one step. Erasure leaves one eraser at each $U_i$; the induction hypotheses erase them in $\sum _i|U_i|$ steps. Duplication creates two roots and one duplicator at each $U_i$; the induction hypotheses create the two copies of every child in the same sum. In either case the total is $1+\sum _i|U_i|=|U|$. Disjointness follows because every right-hand side uses fresh agent occurrences for its two roots. ◻

For unary naturals this proof is visible. Erasing $\bar{2}=S(S(Z))$ takes the three interactions $E\bowtie S$, $E\bowtie S$, and $E\bowtie Z$. Duplicating $\bar{1}=S(Z)$ takes one $D\bowtie S$ step, which leaves two output successors and one new $D\bowtie Z$ redex; contracting that redex is the second and last step and leaves two output zeros.

Define the external readback on a normal unary tree by $$\mathrm{rb}(Z)=0,\mathrm{rb}(S(x))=1+\mathrm{rb}(x).$$ It follows by induction that $\mathrm{rb}(\bar{n})=n$. Thus the arithmetic calculation has an observable result: $$A(\bar{n},r)\bowtie \bar{m}{⟶}_I^{\ast }r=\overline{m+n},\mathrm{rb}(r)=m+n.$$ Readback is a named external function on normal numeral trees, not another interaction rule and not a semantic double-bracket notation.

These agents also give an exact nonlinear calculation on a deliberately finite fragment. A constructor template $B[x_1,\dots ,x_k]$ is a finite constructor tree with distinct variable leaves $x_1,\dots ,x_k$, each occurring once. Let $U$ be a closed finite constructor tree. Define ${\mathcal{T}}_{\mathrm{res}}$ as $\mathcal{T}$ on $\mathsf{Lam}$, $\mathsf{App}$, wires, and constructors, except that the binder of $$(\lambda x.B[x,\dots ,x])U$$ is connected to $E$ when $k=0$, directly to the unique occurrence when $k=1$, and to a fixed full binary tree of $k-1$ duplicators whose ordered leaves feed the $k$ occurrences when $k\ge 2$. The tree shape is part of the translation; it performs no implicit meta-level copying.

Proof of Theorem 41.17 — Finite nonlinear beta simulation and reflection

Proof. The first interaction splices the argument root to the binder resource tree and the body root to the result, exactly as in theorem 41.14. If $k=0$, proposition 41.16 erases $U$ in $|U|$ steps. If $k=1$, the splice already is the translated substitution. For $k\ge 2$, each of the $k-1$ duplicators in the fixed full binary tree meets one complete copy of $U$ along its output path. The proposition gives $|U|$ interactions at each such node and two disjoint output copies; induction over the duplicator tree therefore gives $(k-1)|U|$ interactions and $k$ copies in leaf order. Plugging those copies into the constructor template is precisely postfix simultaneous substitution.

For reflection, no manager rule creates a $\mathsf{Lam}$ or $\mathsf{App}$, so the outer active pair comes only from the displayed source redex. Manager redexes for distinct constructor subtrees are disjoint. Theorem 41.12 permits adjacent swaps of their steps, and the induction just given fixes the endpoint and count. Hence every complete manager development has the stated result. ◻

This theorem covers weakening and finite multiplicity only when the argument is a closed constructor tree and the body is a constructor template. General lambda graphs may contain binders inside the duplicated argument, sharing, cycles, and resource managers themselves. The theorem is not a full nonlinear lambda encoding and carries no Lévy-optimality claim.

Interaction combinators

Lafont’s interaction combinators form a universal interaction system with three symbols: binary $\gamma$ and $\delta$, and nullary $\epsilon$. Because symbol pairs are unordered, six pair classes suffice. Fix the intrinsic auxiliary order $1,2$ on both binary symbols. If the old boundary of a binary–binary pair is $(a_1,a_2,b_1,b_2)$, five rules have the following exact port equations: The eraser on the right of equation 41.2, equation 41.3 is a fresh nullary agent whose principal port is connected to the named old boundary endpoint. Thus those rows expose the same two boundary wires as their left sides. The $\gamma \bowtie \gamma$ annihilation crosses the intrinsic positions; $\delta \bowtie \delta$ preserves them. A spatially reflected glyph can hide that difference, which is why the equations carry numbered ports.

Diagram

The earlier $\mathsf{App}\bowtie \mathsf{Lam}$ pair uses two different symbols and its own same-position boundary convention; neither symbol is the combinator $\gamma$. Likewise, the later HVM2 table calls a runtime tag “constructor-like” only as a role comparison. It is not an identification of that runtime rule, the linear lambda rule, and equation 41.4. Port order is fixed separately for each signature.

For the sixth, mixed rule, take fresh internal wire names $p_{ij}$ $(i,j\in \{1,2\})$ and set Each equation attaches an old endpoint to the principal port of one fresh agent; each $p_{ij}$ occurs exactly twice and joins auxiliary port $i$ of the $j$-th new $\delta$ to auxiliary port $j$ of the $i$-th new $\gamma$. Thus the mixed right side has four fresh agents and exactly the old ordered boundary.

Diagram

Together, equation 41.1, equation 41.2, equation 41.3, equation 41.4, equation 41.5, equation 41.6 are Lafont’s six diagrams in algebraic port form [Laf97].

The equations compute immediately. Attach nullary ${\epsilon }_1$ to $a_1$ and ${\epsilon }_2$ to $b_2$ in a $\gamma (a_1,a_2)\bowtie \gamma (b_1,b_2)$ pair. Then The first rule crosses intrinsic positions and creates the second active pair; the second removes it. This two-step instance consumes two of the six rules before the general simulation result is invoked.

Proof of Theorem 41.18 — Universality of interaction combinators

Imported proof. This is Lafont’s Theorem 1 in §2 of the local author copy, printed p. 8 [Laf97]. The relation ${⟶}_{\mathrm{IC}}^{\ast }$ permits a reduction of arbitrary finite length, possibly zero. The result is existence and simulation, not a claim that translated programs preserve source step count or asymptotic cost.

The construction proceeds in two layers. First, each source symbol and each source interaction rule is compiled into a finite net with the same free-port interface. Second, Lafont builds the required finite routing, copying, and selection gadgets from $\gamma ,\delta ,\epsilon$, and shows that the net compiled from a source redex reduces to the net compiled from its right-hand side. Closure under contexts then gives the simulation of arbitrary source steps. Reproducing the gadget library would replace this chapter’s local proofs with many pages of source diagrams. We therefore state and use the simulation theorem rather than reconstructing the entire gadget library. Its conclusion is only the forward existence statement $N{⟶}_I{N}^{\prime }$ implies ${\mathrm{\Phi }}_I(N){⟶}_{\mathrm{IC}}^{\ast }{\mathrm{\Phi }}_I(N^{\prime })$; it does not reflect arbitrary target reductions back to source steps. Lafont’s separate Proposition 4 gives constants depending on the finite source system that bound the combinator steps used to simulate an $n$-step source reduction. That bound is not an implementation-cost theorem. ◻

One agent that breaks the diamond

The proof of theorem 41.9 uses two facts. Distinct active pairs are disjoint, and an active pair determines at most one right-hand side. Multiple principal ports destroy the first fact: one $\mathsf{amb}$ occurrence may belong to two active pairs at once. INAMB’s two interactions with each ordinary agent also abandon the global unique-rule presentation, but the counterexample below fails specifically because its two redexes overlap at $\mathsf{amb}$.

Fernández and Khalil isolate that obstruction in the calculus INAMB. The new agent $\mathsf{amb}$ has two principal ports and two auxiliary ports. We write $$(p_0,p_1)\mathsf{amb}(m,a)$$ for an occurrence, where $p_0,p_1$ are the two possible inputs, $m$ is the main output, and $a$ is the remaining auxiliary connection. For every ordinary agent $\alpha$, there are two rules: an $\alpha$-agent arriving at $p_0$ is relayed to $m$, and an $\alpha$-agent arriving at $p_1$ is relayed to $m$. Fernández–Khalil’s Definition 4.2 writes a rule by displaying its right-hand-side wiring to the left of $\bowtie$. With that convention, the two complete rules are $$(-,\ell )\mathsf{amb}(\alpha (\overrightarrow{x}),\ell )\bowtie \alpha (\overrightarrow{x})\text{and}(\ell ,-)\mathsf{amb}(\alpha (\overrightarrow{x}),\ell )\bowtie \alpha (\overrightarrow{x}).$$ The arguments of each displayed $\mathsf{amb}$ term record the resulting wiring: $\alpha (\overrightarrow{x})$ is exposed at the main output and $\ell$ relays the unselected principal connection to the auxiliary port. The dash marks the principal port chosen for the interaction; it is not a missing term.

Now connect $\alpha (\overrightarrow{x})$ to $p_0$ and $\beta (\overrightarrow{y})$ to $p_1$, with $\alpha \ne \beta$. The two one-step reductions expose different root agents at $m$: $$N{⟶}_{\mathrm{A}\mathrm{m}\mathrm{b}-0}{N}_{\alpha },N{⟶}_{\mathrm{A}\mathrm{m}\mathrm{b}-1}{N}_{\beta }.$$ Choose $\alpha$ and $\beta$ with no rule between their exposed forms. Then neither branch has a one-step reduct joining the other. This is the exact line at which the diamond proof fails. The failure is intentional; INAMB supplies a nondeterministic choice, not a second strongly confluent interaction system.

Proof of Proposition 41.19 — The deterministic hypothesis is necessary

Proof. Choose the two competing agents already displayed to be distinct nullary symbols ${\kappa }_0$ and ${\kappa }_1$, with no rules on either exposed form. Selecting $p_0$ leaves ${\kappa }_0$ at the main output and selecting $p_1$ leaves ${\kappa }_1$. Both results are normal. The agent at that fixed output differs, so no interface-fixing isomorphism carries one result to the other; normality also rules out a one-step join. The competing unordered symbol pairs are distinct, so this counterexample violates the disjoint-redex lemma, not rule uniqueness for either of those two pairs. ◻

Angelic and infinity merge

Let a stream be a chain of unary element agents ending at an interface port. An angelic merge of two streams must produce an infinite output if either input can keep producing; it need not serve both inputs fairly. Every output element is an unaltered input element, and elements from either one input retain their original order. Put the two input heads at the principal ports of $\mathsf{amb}$. When a head $\alpha$ wins, relay $\alpha$ to the output and reconnect the continuation of that input, together with the untouched other input, to a fresh merge agent. Thus the active principal port chooses the next output cell and the same wiring recursively restores the merge. If both heads are ready, the choice is nondeterministic. If only one is ready, that branch remains available.

The source constructs infinity merge from a nondeterministic natural number generator. The generator uses $\mathsf{amb}$, the ordinary eraser, and duplicator to choose a finite numeral while preserving its interface. An oracle repeatedly chooses $n$, emits exactly $n$ cells from the first input, chooses $n^{\prime }$, and emits exactly $n^{\prime }$ cells from the second. If an input contains fewer than the number just requested, that branch blocks. Nevertheless, if one input is infinite, every cell of the other input eventually appears in the output. This is the source’s infinity-merge guarantee. It is weaker than fairness: INAMB does not implement fair merge. Panangaden and Shanbhogue prove the strict implementation hierarchy: fair merge cannot be implemented by angelic merge, and angelic merge cannot be implemented by infinity merge [PS92]. Fernández and Khalil invoke that result at printed p. 4 and use it to delimit their own constructions of angelic and infinity merge [FK02].

The textual multiple-principal-port calculus

The metatheorems are stated for the paper’s textual calculus INMPP. Fix agents $\alpha$ with auxiliary arity $n$ and a finite number of principal ports. Terms and equations are A name occurs at most twice. One occurrence denotes a free port and two occurrences denote a wire. A dash selects the principal port currently exposed by a term. A multiequation $(\overrightarrow{\ell })\alpha (\overrightarrow{k})$ records all potential principal interactions of one occurrence at once.

A term is INMPP-normal when it is a variable, or a selected-principal term whose auxiliary subterms are INMPP-normal and in which every name used at a principal port of that term or a subterm occurs at most once. This is Fernández–Khalil Definition 4.3; it differs from interaction-net normal form. A configuration $⟨\overrightarrow{t}\mid \mathrm{\Delta }⟩$ has a list of INMPP-normal interface terms and a multiset of equations. No principal name is shared by two interface terms or between the interface and $\mathrm{\Delta }$. The load-bearing nondeterministic rule selects one principal component of a multiequation: The other two indirection rules substitute a name or expose a named principal port. Interaction replaces an explicit active equation by a fresh instance of its rule; collection moves a normal component to the interface; multiset congruence reorders equations. These clauses make the selected principal port visible in the dynamics instead of hiding the nondeterministic choice in a graph picture.

Port types are polarized types ${\sigma }^s$, with $s\in \{+,-\}$, and a wire joins dual polarities. Each agent supplies one user-defined Graft rule typing all its principal ports and auxiliary subnets together. Write $\alpha (\overrightarrow{t}):({\sigma }_1^{s_1},\dots ,{\sigma }_m^{s_m})$ for its Graft conclusion. The structural core contains $$\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}.$$ The rules that close all principal ports or expose exactly port $j$ are $$\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 is All displayed premise contexts are pairwise name-disjoint. These side conditions make the proof below a graph-construction induction. For $\mathsf{amb}$, the Graft rule is $$\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}.$$ Both principal ports consequently have the same type and direction. The two $\mathsf{amb}$ rules are typeable because either selected principal port is cut against the same dual type and the unselected connection is preserved.

Proof of Theorem 41.20 — Typed INMPP safety, reconstructed

Proof. The source states Propositions 4.10 and 4.13 without proofs; we reconstruct the required mechanism. For clause 1, induct on the height of the typing derivation. Ax contributes one wire and no cycle. A Graft instance joins an agent to the pairwise disjoint auxiliary premise nets and leaves its principal ports exposed, so any principal cycle would already occur in a premise. Cut joins the exposed roots of two disjoint premise nets by one edge and therefore cannot close a cycle. MultiCut attaches distinct premise nets to all principal ports of one freshly grafted agent; its incidence graph is a star of disjoint components. Select makes the same attachments except at port $j$, which remains exposed. Exchange changes no incidence. These cases exhaust the derivation and establish absence of principal cycles.

For clause 2, inspect the final dynamic rule while inducting on the height of its typing derivation. Indirection (i) eliminates a name edge by capture-avoiding substitution; indirection (ii) exposes the same named principal port; and indirection (iii) replaces a multiequation by the corresponding Select conclusions and one Cut. Each rearranges the same dual occurrences. Interaction is the load-bearing case: the definition of a typeable rule supplies a derivation of its active equation and a derivation of its right-hand-side equations under exactly the same typed boundary, so replacing the former by a fresh copy of the latter preserves the conclusion. The two collection rules invert Ax or Select and move the resulting INMPP-normal term to the interface. Multiset congruence is exchange. Hence every dynamic rule preserves the interface typing. Clause 3 applies clause 1 to the preserved derivation after each step. ◻

The last clause is conditional twice: the initial configuration must be typeable and every interaction rule used by reduction must satisfy the paper’s typeable-rule definition. It is not progress for arbitrary INAMB nets, and a configuration may still wait for data without containing a principal-port cycle.

Encoding INMPP in INAMB

Before translation, collection and indirection put a configuration into shallow form: its interface contains only names, while each equation contains names or one agent occurrence with named ports. An agent with $m$ principal ports is represented by a chain ${\mathsf{amb}}_m$ of binary $\mathsf{amb}$ agents. A selector records which branch won, duplicators preserve the other boundary data, and clearing agents erase abandoned alternatives. The configuration translation $\theta$ leaves name equations unchanged, splits an explicit active equation through a fresh name, and sends a multiequation $(\overrightarrow{\ell })\alpha (\overrightarrow{t})$ to the selector configuration $$(\overrightarrow{\ell }){\mathsf{Samb}}_m({\alpha }^{\prime }(\overrightarrow{t},g_2,\dots ,g_m),\mathsf{Cl}(g_2),\dots ,\mathsf{Cl}(g_m)).$$ For every source rule between principal port $p$ of $\alpha$ and port $q$ of $\beta$, the target rule connects the selected projections ${\alpha }_q^{\prime }$ and ${\beta }_p^{\prime }$, translates the source rule’s residual equations, and retains the remaining named boundary in reverse order around the selected port. This is the source’s Definitions 4.15 and 4.16, including its selector, labelling, duplicator, eraser, and clearing rules.

Proof of Theorem 41.21 — INMPP–INAMB operational correspondence, imported

Imported proof. Source note. The syntax and dynamics are Definitions 4.1–4.5. Graft typing and its safety results are Definitions 4.7–4.9 and 4.11 and Propositions 4.10 and 4.13. The encoding correspondence is Definitions 4.15–4.16 and Propositions 4.17–4.18 of Fernández and Khalil’s complete 2002 paper [FK02]. Their angelic and infinity merges are Examples 3.1 and the construction on pp. 5–6. The paper rules out fair merge at this signature. Its later process- and term-rewriting encodings, and claims unique to the expanded 2003 article, are outside this chapter. Proposition 4.14 is the shallow-form result used before $\theta$. ◻

A scheduler with a small invariant

A mutable implementation stores an agent tag, its auxiliary-port array, and one peer reference per connected port. Reconnecting a rule touches only the two redex agents, the rule’s fresh agents, and the exposed boundary peers. A work queue may contain candidate principal–principal wires.

The graph store maintains four incidence invariants after every accepted rewrite: every live internal port has exactly one peer; the peer relation is symmetric; every peer names a live agent and an in-range port (or one declared boundary endpoint); and no port of a retired agent remains reachable. A reference reducer may check all four after every interaction. A queue entry is only a candidate address pair, never authority to mutate the graph; the current peer table decides whether it is still a redex.

Call a scheduler enqueue-complete when the initial queue covers every initial redex and every rewrite enqueues every newly created rule-bearing principal–principal wire. Call it validating when dequeue checks that both endpoints are live, mutually connected principal ports with a rule. Call it fair when, for every candidate $c$ and dequeue index $n$, if $c$ remains in the queue after index $n$, then some dequeue with index $m\ge n$ removes $c$. A redex is permanently live after index $n$ when it is never contracted and neither of its principal agents is disconnected after $n$.

Proof of Proposition 41.22 — Queue invariant

Proof. Validation proves safety at the moment of contraction. Initial coverage is the base case for completeness. Thereafter a redex can become newly live only when a rule reconnects a principal port or creates a new agent; the enqueue discipline covers both cases. A duplicate that survives validation contracts the redex once, and all later copies become stale; a candidate that was already stale fails validation before any mutation. Finally, fairness gives a finite dequeue index at which a permanently live candidate reaches the head, where it still passes validation. ◻

Locks or ownership must protect the two active agents and the boundary writes of a rule. Disjoint-redex theory explains why independent critical sections can commute; it does not itself prevent a data race in an unsafe graph store.

Implementation case study: HVM2

Appendix E records the reproducible implementation evidence. The mathematical object used here is its finite dispatcher table and the work/span calculation below.

The paper-level rule table has ten named interactions:

The C/CUDA dispatcher compresses these into eight tags: LINK, CALL, VOID, ERAS, ANNI, COMM, OPER, and SWIT. Thus “ten paper rules” and “eight dispatcher classes” count different layers and are not contradictory. The implementation’s node tags include VAR, REF, ERA, NUM, CON, DUP, OPR, and SWI; VAR is a wire-level reference rather than one of the seven agent-like constructors.

The closest interaction-combinator role map is On this three-tag subtable, unequal binary tags select COMM, equal binary tags select ANNI, and eraser/binary pairs select ERAS. This is a role-level map, not a proof that the runtime’s one ANNI procedure realizes both intrinsic port permutations in equation 41.4, equation 41.5; that claim would require a separate verification of its stored port orientation. REF, NUM, OPR, SWI, and global-link state are HVM2 extensions, not Lafont combinators.

The evaluator map has three stages. The implementation represents a net as a root tree and a bag of redex equations; nullary ERA/REF/NUM and binary CON/DUP/OPR/SWI are the seven agent-like forms. Dispatch maps the ordered pair of runtime tags to one class, pops one entry from the local redex bag, canonicalizes tag order, calls one of interact_link through interact_swit, requeues a failed claim, and counts successful non-LINK interactions. The evaluator drains that bag; readback follows the runtime root and reconstructs an AST by tag. This gives the concrete $$\begin{array}{c}\text{parsed root/redex bag}\to \text{runtime ports and bags},\\ \text{runtime ports and bags}\to \text{dispatcher interactions},\\ \text{dispatcher interactions}\to \text{AST readback}\end{array}$$ map used by the finite calculation.

One small schedule benchmark can be checked without importing the paper’s performance claims. In the paper’s concrete net syntax, take The root is the number $0$; the bag contains two independent ERA–ERA pairs. The dispatch table sends both to VOID. Left-then-right and right-then-left each perform exactly two counted interactions, while an ideal two-worker frontier has work $2$ and span $1$: work is the total number of interactions, while span is the length of the longest dependency chain under ideal parallel scheduling. Neither interaction touches the root, so the readback code returns 0. This is an interaction-count/readback microbenchmark, not a wall-clock benchmark: it records neither hardware nor throughput. The Kappa companion encodes both schedules and the common readback as finite data.

The preceding strong-confluence theorem applies only after one verifies the interaction-system hypotheses for the modeled rules, including side conditions and state effects. The implementation report itself highlights the CON–SWI entry as problematic and says that either its COMM entry or the SWIT reduction must change. We therefore report the selected table without upgrading its work-in-progress confluence claim to a theorem. A source-code dispatcher table is evidence for what the selected implementation does. It is not by itself a proof of confluence, an optimality theorem, or a speedup claim. Benchmarks, when present, would establish performance only for their recorded hardware, programs, build, and measurement protocol [Hig26].

Executable companion.

The Kappa companion recorded in appendix E executes the unary-addition trace, two finite normalization schedules, unordered rule-key and boundary checks, and the HVM2 dispatcher table. It supplies regression evidence for those examples, but proves none of the confluence, simulation, universality, or optimality results above.

Confluence, simulation, and implementation evidence

For finite first-order interaction systems with at most one rule per unordered symbol pair, theorem 41.9 derives strong confluence from the one-step diamond, and theorem 41.12 proves independence of finite developments. The exact linear and finite constructor-tree simulations are corollary 41.15, theorem 41.17; interaction-combinator universality is theorem 41.18; and the executable scheduler preserves proposition 41.22. These statements establish neither a Lévy-optimal lambda encoding nor a bound comparing graph-reduction work with beta-reduction work: either conclusion requires an explicit encoding and cost relation. For the nondeterministic extension, proposition 41.19 marks the failed deterministic hypothesis, while theorem 41.20, theorem 41.21 delimit typed safety and the INMPP-to-INAMB correspondence. The explicit net framework and one-step diamond argument follow de Falco [dF10].