First-order interaction nets

An interaction system in chapter 41 has a finite agent signature with one principal and finitely many ordered auxiliary ports per occurrence. Nets contain finite agent occurrences and finite interval or circular wiring components; ordered free interval ends form the interface. A rule replaces one principal–principal active pair by a net with the same boundary. Each unordered symbol pair has at most one rule. Reduction and equality are taken modulo interface-fixing graph isomorphism and fresh-name renaming.

By lemma 41.5, distinct active pairs share no agent. Coincident redex occurrences select the same agent pair and the unique rule for its unordered symbol pair, hence have the same reduct modulo the stipulated boundary isomorphism; distinct redexes commute. These two cases give the exact one-step diamond in theorem 41.9. The corollary corollary 41.10 gives ordinary confluence and uniqueness of an existing normal form. The omega rule shows that none of these statements implies termination.

For a fixed finite set of active pairs present in the initial net, every complete development contracts exactly those residuals, has the same length, and ends in an isomorphic net by theorem 41.12. The theorem does not schedule redexes created by the development and gives no total-work or space bound.

Unary addition calculates by proposition 41.7. Exactly-once beta simulation for the named map $\mathcal{T}$ is theorem 41.14; the converse redex correspondence is corollary 41.15. The local theorem 41.17 adds a bidirectional root-beta calculation for a finite constructor template and closed constructor-tree argument: one $\mathsf{App}\bowtie \mathsf{Lam}$ interaction is followed by exactly $|U|$, $0$, or $(k-1)|U|$ manager interactions according as the binder multiplicity $k$ is zero, one, or at least two. It is not a general nonlinear lambda translation.

Lafont’s universality result is theorem 41.18. For a finitely presented source system under his reduced-right-side convention, its effective symbol map ${\mathrm{\Phi }}_I$ preserves ordered interfaces and sends each source step to a finite interaction-combinator reduction, modulo interface-fixing isomorphism. It does not assert converse simulation or exact source-step preservation. Lafont’s separate Proposition 4 bounds the simulating combinator steps by source-system-dependent linear constants; this is not an implementation-cost theorem. The eraser/duplicator calculation proposition 41.16 is restricted to finite constructor trees; its external $\mathrm{rb}$ reads only normal unary trees and is not a general lambda readback theorem.

INAMB adds a two-principal-port $\mathsf{amb}$ agent. Its two enabled choices yield the non-isomorphic normal peak of proposition 41.19; deterministic strong confluence is deliberately not transferred. INMPP uses selected-principal terms, multiequations, and polarized Graft typing. The local reconstruction in theorem 41.20 records the mechanisms behind Fernández–Khalil Propositions 4.10 and 4.13, which the source states without proof. The imported shallow translation and operational correspondence are Proposition 4.14 and Definitions 4.15–4.16 with Propositions 4.17–4.18, as delimited by theorem 41.21. Fair merge, the finitary pi-calculus encoding, and claims unique to the later 2003 paper are excluded.

The HVM2 study is pinned at commit 654276018084b8f44a22b562dd68ab18583bfb5b and reports a work-in-progress document and source tree: ten paper-level interaction names, eight C/CUDA dispatcher classes, and seven agent-like node tags plus VAR. The syntax-to-readback map is pinned to src/hvm.rs, lines 147–158 and 860–905, and src/ast.rs, lines 365–429. The paper explicitly flags the CON–SWI table entry as problematic. Source tables are implementation facts, not proofs of confluence or optimality and not wall-clock benchmark evidence.

The Kappa corpus recorded in appendix E checks unary arithmetic, a two normalization schedules, finite-tree erasure/duplication counts, unordered rule-key uniqueness, boundary preservation, the pinned HVM2 count mapping, and both schedules of the two-VOID microbenchmark with work two, span one, and readback zero. It proves none of the metatheorems above.

Lafont’s original paper supplies the interaction-net discipline. The local author copy of his interaction-combinator paper gives the six rule diagrams in §2.1, the construction through §2, and states Theorem 1 on printed p. 8. De Falco’s Definition 5.1, Proposition 5.3, and Corollary 5.4 in the local author copy, pp. 13–14, supply the strong-confluence statement. Fernández–Khalil Definitions 4.1–4.16 and Propositions 4.10, 4.13–4.14, and 4.17–4.18 delimit INAMB/INMPP. HVM2 claims are limited to the pinned work-in-progress artifacts.