ch:interaction-nets: ch:interaction-nets

Let $\alpha$ have auxiliary ports ${\alpha }_1,{\alpha }_2$, and let $\beta$ have auxiliary port ${\beta }_1$. Join ${\alpha }_2$ to ${\beta }_1$. The three free ports are then the two principal ports ${\alpha }_0,{\beta }_0$ and the remaining auxiliary port ${\alpha }_1$. For example, $$I=({\alpha }_0,{\alpha }_1,{\beta }_0)\text{and}{I}^{\prime }=({\beta }_0,{\alpha }_0,{\alpha }_1)$$ are two interfaces on the same underlying partial matching. They specify different positions at which a surrounding net must reconnect those ports. Joining ${\alpha }_0$ to ${\beta }_0$ creates the active pair $\alpha \bowtie \beta$. That second wire consumes two previously free ports, so the new interface has the single entry $({\alpha }_1)$.

Name the three successor agents of the first addend $S_1,S_2,S_3$, from root to zero, and name the three fresh output tails $s_1,s_2,s_3$. The trace is Each successor interaction inherits an ordered three-port boundary. It is $(y,r_i,x_i)$: $y$ is the unchanged root of $\bar{2}$, $r_i$ is the current result wire, and $x_i$ leads to the predecessor constructor. The final $A\bowtie Z$ interaction has ordered boundary $(y,r_3)$ and splices those two wires. There are three successor interactions and one zero interaction, hence $3+1=4$ steps, as the addition proposition predicts.

Let $$N=C[A(y,r)\bowtie S(x),A(y^{\prime },r^{\prime })\bowtie Z],$$ where the two displayed pairs have disjoint agent occurrences and $C$ is their surrounding wiring context. Contracting the first pair gives $$M_1=C[r=S(s),A(y,s)\bowtie x,A(y^{\prime },r^{\prime })\bowtie Z].$$ The second pair is unchanged, so its contraction gives $$P=C[r=S(s),A(y,s)\bowtie x,y^{\prime }=r^{\prime }].$$ In the other order, The isomorphism $P\cong P^{\prime }$ fixes every old port and sends the one fresh internal name $s$ to $s^{\prime }$. If two rules were allowed for the same unordered symbol pair, the coincident-redex case in theorem 41.9 would no longer imply isomorphic contracta; that is the exact failed line.

The new left side $\mathrm{\Omega }\bowtie \mathrm{\Omega }$ still has a unique rule. For two distinct redexes, disjointness and commutation are unchanged. For the same redex, both reductions use that unique rule and create isomorphic fresh copies. Thus the proof of theorem 41.9 applies verbatim.

Starting from $N_0=\mathrm{\Omega }\bowtie \mathrm{\Omega }$, the rule produces a fresh isomorphic active pair $N_1$, then $N_2$, and so on: $$N_0{⟶}_I{N}_1{⟶}_I{N}_2{⟶}_I\cdots .$$ Hence the system is not strongly normalizing. Confluence asks whether two finite reducts can be joined; here any $N_i,N_j$ join at $N_{max(i,j)}$. Uniqueness of normal forms is conditional on a normal form existing, and this component has none.

The six orders are $$rst,rts,srt,str,trs,tsr.$$ The one-step diamond permits an adjacent swap of distinct residuals: $$rst\leftrightarrow srt\leftrightarrow str\leftrightarrow tsr\leftrightarrow trs\leftrightarrow rts\leftrightarrow rst.$$ Each swap compares the two sides of one commuting square, so all six endpoints are isomorphic. Every sequence has three steps because each initial redex has one residual until contracted.

A redex created by contracting $r$ was not a member of the selected frontier $\{r,s,t\}$. A sequence that also contracts it has more than three steps and is not a development of that set under definition 41.11. The adjacent-swap proof says nothing about whether that new redex exists in schedules where $r$ has not yet been contracted.

For $(\lambda x.x)u$, the translated application and abstraction form $$\mathsf{App}(\mathcal{T}(u),r)\bowtie \mathsf{Lam}(x,x).$$ The interaction splices $\mathcal{T}(u)$ to the unique binder wire $x$ and the body wire $x$ to $r$. Eliminating the resulting wire splice leaves $\mathcal{T}(u)$, which is $\mathcal{T}(x[u/x])$.

For $(\lambda x.\lambda y.xy)u$, the outer rule again connects the argument root to the unique $x$-port, but leaves the inner $\mathsf{Lam}$ and $\mathsf{App}$ agents intact. The result has the translation tree for $$(\lambda y.xy)[u/x]=\lambda y.uy,$$ with the same free-variable interface as $\mathcal{T}(u)$.

The body $xx$ has two free occurrences of $x$. A Lam agent supplies one binder auxiliary port, and a port belongs to at most one wire. It cannot be spliced simultaneously to both occurrences. A full encoding must therefore add explicit duplication agents and their rules; the two-agent linear beta rule alone is insufficient.

Write $\bar{2}=S_1(S_2(Z))$. Erasure is $$E\bowtie S_1(S_2(Z)){⟶}_{I}E\bowtie S_2(Z){⟶}_{I}E\bowtie Z{⟶}_I\mathrm{\varnothing }.$$ Each $E\bowtie S$ redex exposes the single child wire $x$, so both its left and right boundaries are $(x)$. The final $E\bowtie Z$ redex has empty boundary on both sides. There are three agents in $\bar{2}$ and three interactions.

For $\bar{1}=S(Z)$, start with $D(\ell ,r)\bowtie S(x)$. The first rule has ordered boundary $(\ell ,r,x)$ and yields $$\ell =S({\ell }_1),r=S(r_1),D({\ell }_1,r_1)\bowtie Z.$$ The remaining redex has boundary $({\ell }_1,r_1)$ and yields ${\ell }_1=Z,r_1=Z$. The outputs are two disjoint copies $\ell =\bar{1}$ and $r=\bar{1}$. The two original agents account for the two interactions.

The induction in proposition 41.16 decomposes a tree into disjoint child subtrees. In a shared diamond, two child wires can reach the same agent, so separate induction calls would count and copy that occurrence twice. In a cycle there is no finite constructor-tree height on which to induct. Neither graph satisfies the proposition’s hypothesis.

In $(\lambda x.Z)\bar{2}$, the template has $k=0$. The binder is therefore attached to $E$. After the one $\mathsf{App}\bowtie \mathsf{Lam}$ interaction, the manager trace is $$E\bowtie S(S(Z)){⟶}_{I}E\bowtie S(Z){⟶}_{I}E\bowtie Z{⟶}_I\mathrm{\varnothing }.$$ The body root remains $Z$, so the final net is ${\mathcal{T}}_{\mathrm{res}}(Z)$. Since $|\bar{2}|=3$, the manager count is $c(0,\bar{2})=3$.

For $(\lambda x.C(x,C(x,x)))\bar{1}$, choose the fixed left-associated manager tree whose root duplicator feeds the first occurrence directly and a second duplicator; the latter feeds occurrences two and three. The argument has two constructors, $S$ and $Z$. The root manager performs $$D\bowtie S{⟶}_{I}D\bowtie Z{⟶}_I(\bar{1},\bar{1}).$$ One output is installed at the first $x$-port. The other meets the second manager and repeats the same two interactions, producing the copies for the remaining two ports. Thus the four manager interactions produce $${\mathcal{T}}_{\mathrm{res}}(C(\bar{1},C(\bar{1},\bar{1}))),c(3,\bar{1})=(3-1)|\bar{1}|=2\cdot 2=4.$$ The order of the two complete duplicator developments can change, but theorem 41.12 fixes their common endpoint.

A lambda graph is not a closed constructor tree: it may contain binders, sharing, cycles, and manager agents for which the $E/D$ constructor schemas have not been defined. Replacing the argument by such a graph violates the hypothesis rather than extending the theorem.

The unordered pairs with repetition from three symbols are $$\{\epsilon ,\epsilon \},\{\epsilon ,\gamma \},\{\epsilon ,\delta \},\{\gamma ,\gamma \},\{\delta ,\delta \},\{\gamma ,\delta \}.$$ Their boundary equations are For the mixed pair, with four fresh wire names, Every old endpoint $a_1,a_2,b_1,b_2$ occurs once on each side. Every $p_{ij}$ occurs twice on the right: once at auxiliary port $i$ of the $j$-th new $\delta$ and once at auxiliary port $j$ of the $i$-th new $\gamma$. Hence the mixed right side is a four-agent grid with no dangling or triply incident wire.

The $\gamma$-self rule crosses intrinsic positions while the $\delta$-self rule preserves them. Transposing only one new agent in the mixed grid changes which two auxiliary ports a $p_{ij}$ joins. Since auxiliary-port order belongs to the signature, that is a different rule even if a reflected drawing looks similar.

Write the two streams as $\alpha (A)$ and $\beta (B)$, where $A,B$ are their tails. With both heads at the principal ports of $\mathsf{amb}$, the first selection has two outcomes: $$\mathsf{AM}(\alpha (A),\beta (B)){⟶}_{\mathrm{A}\mathrm{m}\mathrm{b}-0}\alpha (\mathsf{AM}(A,\beta (B)))$$ or $$\mathsf{AM}(\alpha (A),\beta (B)){⟶}_{\mathrm{A}\mathrm{m}\mathrm{b}-1}\beta (\mathsf{AM}(\alpha (A),B)).$$ The first branch preserves the whole right input $\beta (B)$; the second preserves the whole left input $\alpha (A)$. If $A={\alpha }^{\prime }(A^{\prime })$, the next left selection exposes ${\alpha }^{\prime }$ and leaves $\mathsf{AM}(A^{\prime },\beta (B))$. The symmetric calculation applies to $B$. Thus each selected head recreates the merge state around the two remaining tails.

Nothing requires the next selection to alternate inputs. An infinite run may repeatedly select one ready side, so the calculation is not a fairness proof. The two displayed first steps also expose different root agents when $\alpha \ne \beta$; with terminating tails they give the nonjoinable peak of proposition 41.19. Recursive restoration therefore proves the merge protocol’s shape, not strong confluence.

Suppose $\alpha (\overrightarrow{x}):{\sigma }^{-s}$. Fernández–Khalil’s Example 4.12 assigns $y:{\sigma }^{-s}$, $z:{\sigma }^s$, and $z^{\prime }:{\sigma }^s$. An instance of Graft-amb therefore assigns both principal ports of $\mathsf{amb}(z,z^{\prime })$ the type ${\sigma }^s$. Selecting the first port gives the source’s actual active equation: $$\frac{\begin{array}{c}\mathrm{\Gamma },(-,y)\mathsf{amb}(z,z^{\prime }):{\sigma }^s\\ \mathrm{\Delta },\alpha (\overrightarrow{x}):{\sigma }^{-s}\end{array}}{\mathrm{\Gamma },\mathrm{\Delta },(-,y)\mathsf{amb}(z,z^{\prime })=\alpha (\overrightarrow{x}):\diamond }\mathrm{Cut}.$$ The corresponding rule’s right-hand-side wiring relays $\alpha (\overrightarrow{x})$ to the main output and relays the unselected principal connection through $y$. Selecting the second port uses the other, identically typed conclusion component of Graft-amb; the derivation is the same after exchanging the two principal positions. Thus both rules cut the active type pair ${\sigma }^s,{\sigma }^{-s}$ while preserving the boundary types $y:{\sigma }^{-s}$, $z:{\sigma }^s$, and $z^{\prime }:{\sigma }^s$.

For the failed cycle, connect the principal outputs of two agents whose Graft conclusions both assign ${\tau }^{+}$ around a directed two-edge cycle. Each edge would require an instance of Cut with premises ${\tau }^{+}$ and ${\tau }^{-}$, but the cycle supplies ${\tau }^{+}$ at both ends. Equating them would require $+=-$, so there is no derivation. Typed deadlock freedom excludes that principal cycle. It says nothing about uniqueness of an enabled rule: a well-typed $\mathsf{amb}$ may still have two simultaneously enabled, type-preserving interactions, which is exactly the peak excluded from the deterministic diamond proof.

Suppose a rule creates a candidate principal wire $p$–$q$ and enqueues it. Before that entry reaches the head, another interaction may consume $p$, reconnecting its former boundary peer elsewhere. On dequeue, either $p$ no longer exists or its current mate is not $q$. Endpoint-existence and mutual-connection validation therefore reject the stale entry before any rewrite. This is the safety part of the invariant.

Initial coverage is a separate base case. If the initial graph contains a live redex $a\bowtie b$ but the initial queue is empty, no rewrite occurs and no rewiring event exists that could enqueue it. Validation and fairness cannot manufacture the missing candidate.

For enqueue preservation, let a rule reconnect two surviving principal ports $a,b$ for which a rule exists, but omit the enqueue operation. If no other queue entry names that wire, the resulting live redex is never presented to the scheduler. Validation cannot recover a candidate it never sees. This violates the inductive completeness step. Finally, an enqueued, valid, permanently live candidate can still starve under an unfair queue that always chooses newer entries; fairness is the separate hypothesis that excludes that execution. Thus initial coverage handles old redexes, enqueue preservation handles new ones, validation supplies safety, and fairness supplies eventual service.

The two many-to-one groupings are $$\{Operate1,Operate2\}\mapsto \mathtt{\text{OPER}},\{Switch1,Switch2\}\mapsto \mathtt{\text{SWIT}}.$$ The other six names map one-to-one to LINK, CALL, VOID, ERAS, COMM, and ANNI. Hence ten paper names occupy eight dispatcher classes.

The tag VAR denotes a wire-level reference. The seven agent-like tags are REF, ERA, NUM, CON, DUP, OPR, and SWI. The pinned syntax parses a root tree and explicit redex bag. At role level, $\epsilon /\gamma /\delta$ correspond to ERA/CON/DUP: eraser/binary pairs dispatch to ERAS, the unequal binary pair to COMM, and equal binary pairs to ANNI. This does not by itself identify the stored auxiliary port order with both distinct Lafont self-annihilations.

The table at src/hvm.rs, lines 147–158, selects a dispatcher class from two tags; lines 860–905 pop, order, dispatch, optionally requeue, and count a redex. The evaluator drains the local bag. The paper’s architecture supplies the CPU work-stealing and CUDA bag-sharing policies. The readback in src/ast.rs, lines 365–429, enters the root and reconstructs the AST by runtime tag.

For 0 & * ~ * & * ~ *, each ERA–ERA pair selects VOID. Call the pairs $r,s$. Both schedules are two-step traces, $$(r,s)⟶(s)⟶(),(r,s)⟶(r)⟶().$$ They have work $2$; because the pairs share no node, the ideal parallel span is $1$. Neither touches the NUM 0 root, so the AST readback is 0. These are finite interaction-count and readback observations, not elapsed-time measurements.

Before applying theorem 41.9, one must at least show that each modeled interaction preserves a fixed port interface and that each unordered agent-symbol pair, including all side-condition cases, selects at most one abstract rule. One must also account for global references or mutable state so that a dispatcher action really denotes a local graph rewrite. In particular, the pinned paper flags CON–SWI as problematic; the current table is source evidence, not a completed confluence proof.

1. Source inspection of the pinned commit establishes that the local rule is present in that program.

2. A mathematical proof over the precisely defined abstract rewrite relation establishes strong confluence.

3. An encoding theorem relating beta families to sharing-graph work establishes Lévy optimality.

4. A reproducible benchmark records a comparative runtime result for its exact builds, machine, workload, and protocol.

Source existence does not establish a universal property of all executions. A confluence proof counts neither beta families nor elapsed time. An optimality theorem is about duplicated semantic work, not a particular machine cost. A benchmark samples implementations and inputs but cannot replace a proof over every net. The four evidence classes are therefore not interchangeable.

There are six unordered pairs with repetition. In intrinsic boundary order $(a_1,a_2,b_1,b_2)$, their complete right sides are and the mixed right side is $$a_1=\delta (p_{11},p_{21}),a_2=\delta (p_{12},p_{22}),b_1=\gamma (p_{11},p_{12}),b_2=\gamma (p_{21},p_{22}).$$ The old names each occur once on the right; each $p_{ij}$ occurs twice. Reading $p_{ij}$ at its two occurrences gives precisely one auxiliary port on a fresh $\delta$ and one on a fresh $\gamma$, so the result is the four-agent grid of Lafont’s Figure 2, §2.1. This wire-by-wire reconstruction is local to the chapter.

The imported map has domain nets over a finitely presented source interaction system $I=(\mathrm{\Sigma },\mathcal{R})$ satisfying the paper’s reduced-right-side convention, and codomain nets over $\{\gamma ,\delta ,\epsilon \}$. For each source $n$-ary symbol, ${\mathrm{\Phi }}_I$ supplies a principal combinator net of arity $n$; compositional extension therefore preserves every ordered free-port interface. Its compatibility clause is $$N{⟶}_{I}M⟹{\mathrm{\Phi }}_I(N){⟶}_{\mathrm{IC}}^{\ast }{\mathrm{\Phi }}_I(M)$$ up to interface-fixing isomorphism. Translation is defined in §1.7 on printed pp. 7–8; universality is Theorem 1 on printed p. 8; the construction is §§2.2–2.7. The gadget construction is not reconstructed here, and no converse is imported. Lafont’s Proposition 4 gives source-system-dependent linear bounds on the number of simulating combinator steps; it is not an implementation-cost theorem.

Write the two disjoint live arithmetic pairs as $r_L,r_R$, and append newly created candidates at the tail. If contracting $r_i$ creates the next arithmetic pair $r_i^{\prime }$, the two initial queue orders are Omit $r_i^{\prime }$ when the zero rule finishes that addition. Disjointness gives an interface-fixing isomorphism $N_{LR}\cong N_{RL}$; repeating the same two rows for the residual pairs enumerates the complete left-first and right-first executions.

After each dequeue, the contracted rule writes both directions of every peer entry, so incidence symmetry is preserved, while the untouched component is unchanged. Initially $[r_L,r_R]$ covers both live pairs. Each rule appends every newly exposed $r_i^{\prime }$, establishing enqueue-completeness inductively. At dequeue, validation checks that the named agents are live, mutually linked at principal ports, and have a rule; any duplicate left after the other schedule contracts its pair is therefore rejected as stale. Finally these queues are finite and FIFO. Every candidate that remains live has only finitely many entries ahead of it, so it is eventually dequeued. This is the fairness condition used in proposition 41.22.

Take distinct nullary agents ${\kappa }_0,{\kappa }_1$ with no rules on their exposed forms, and connect them to the two principal ports of one $\mathsf{amb}$. The two steps are $$N{⟶}_{\mathrm{A}\mathrm{m}\mathrm{b}-0}{N}_0,N{⟶}_{\mathrm{A}\mathrm{m}\mathrm{b}-1}{N}_1.$$ In $N_i$, the agent at the fixed main output is ${\kappa }_i$. Both nets are normal, and an interface-fixing isomorphism cannot change that symbol, so the peak has neither the isomorphism branch nor the one-step-join branch of strong confluence.

If ${\kappa }_i:{\sigma }^{-s}$, Graft-amb gives either selected principal port type ${\sigma }^s$, and Cut types its active equation against ${\kappa }_i$. The interaction’s typeable-rule witness preserves the same boundary on the corresponding right side. Subject reduction says each chosen branch remains typed. It does not assert that the two typed outcomes join, so it is compatible with nondeterminism.