Interaction Nets

Origin. Lafont (1990). Graph rewriting for computation. Local interaction rules. Inherently parallel. Linear logic proof net execution.

Models. Agents with ports. Nets connect ports with wires. Interaction: two principal ports connect. Rewrite: replace interacting pair. Deterministic, local, parallel.

Formalism.

Agents: α: agent symbol with arity n. Principal port (one) and auxiliary ports (n-1). Graphical: principal port distinguished.

Net: Graph of connected agents. Wires connect ports. Interface: free ports (boundary).

Active pair: Two agents connected via principal ports. α ⊳ β: interaction rule defined.

Interaction rule: α(x₁,...,xₙ) ⊳ β(y₁,...,yₘ) = N Replace active pair with net N. Auxiliary ports of α, β become interface of N.

Example (natural numbers): Z: zero (arity 1) S: successor (arity 2) Add: addition (arity 3) Add(x, y, r) ⊳ Z(r) = x connects to r Add(x, y, r) ⊳ S(n, r) = Add(x, n, m), S(m, r)

Properties: Deterministic: at most one rule per pair. Strong confluence: any order gives same result. One-step: single interaction per step.

Encoding λ-calculus: Optimal reduction (Lamping). Sharing via explicit duplication.

Symbols.

Symbol	Unicode	Name	Meaning
α, β	—	Agents	Computation nodes
⊳	U+22B3	Interaction	Rewrite rule
—	—	Wire	Connection
●	U+25CF	Principal	Distinguished port

Metatheory. Lafont's design forces strong confluence, and that is the whole point: an agent has exactly one principal port and at most one rule governs any pair of them, so distinct active pairs are disjoint and reducing one cannot create or destroy another. Consequently reduction satisfies the one-step diamond property, every reduction sequence from a net to a normal form has the same length, and the result is independent of the order chosen. Reduction strategies therefore do not exist as a subject here, unlike in the λ-calculus. Lafont (1997) proved a universality result: the three interaction combinators γ, δ and ε suffice to translate every interaction net system, so the formalism has a finite universal basis. The connection to linear logic is that cut elimination on multiplicative proof nets is exactly interaction net reduction. Lamping's optimal reduction algorithm (1990), reformulated by Gonthier, Abadi and Lévy via linear logic, realizes Lévy's optimal λ-reduction as an interaction net system.

Applies to. Optimal λ-reduction. Parallel computation. Proof net execution. Functional programming. Reversible computation.

Limitations. Strong confluence comes from determinism, and the loss is expressiveness: at most one rule may govern a pair of symbols, so nondeterministic choice, races and shared mutable state have no native encoding, and a system that admits agents with several principal ports loses the disjointness argument and with it confluence. Optimality is not efficiency — Asperti and Mairson (1998) proved that the number of parallel beta steps is not a reasonable cost measure, since sharing-graph reduction of a term with a bounded number of such steps can take non-elementary time in the bookkeeping. Encoding the λ-calculus requires explicit duplication and erasure agents together with a read-back procedure that is not itself an interaction net computation. Erasure is local, so discarding a large net costs steps proportional to its size.