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. Strong normalization (for typed). Parallelism: independent pairs reduce simultaneously. Linear logic connection. Turing complete.

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

Limitations. Unfamiliar paradigm. Duplication overhead. Debugging complex. Limited tooling.