Interaction Nets¶

Compute by replacing principal-port-connected pairs of fixed-arity graph agents with interface-preserving local nets under a one-rule-per-agent-pair discipline, so distinct redexes are disjoint and reductions are strongly confluent by construction.

Version: v1 · 2026-08-30 · History
Domain-specific #: 2085
Origin domain: theoretical computer science
Subdomain: graph rewriting and models of computation
Aliases: Interaction net

Core Idea¶

Interaction nets are a restricted graph-rewriting model of computation introduced by Yves Lafont. A program state is a port graph whose vertices are labeled agents. Every agent has exactly one distinguished principal port and a fixed number of auxiliary ports determined by its symbol. Computation occurs only when two agents meet principal port to principal port, forming an active pair. A rule replaces that pair with another net while preserving all connections by which the pair met the surrounding graph.^[1]

The restrictions are the point. There is at most one rewrite rule for each unordered pair of agent symbols. Because an agent has only one principal port, it can belong to at most one active pair at a time. Distinct redexes therefore do not overlap, and their local replacements commute. This yields the one-step diamond, often called strong or uniform confluence: if a net takes two different one-step reductions, the results can be joined by one step on each branch. When a normal form is reachable, it is unique up to graph isomorphism and the chosen naming convention.^[1]^[2]

That guarantee makes interaction nets simultaneously a formal calculus, an intermediate representation, and an implementation discipline. Copying, erasing, sharing, and substitution are not hidden meta-operations; they must be represented by agents and wires. Disjoint active pairs expose semantic parallelism without a global reduction order. Yet confluence does not imply termination, useful parallel width, constant total cost, or synchronization-free hardware. Those are separate program and implementation questions.^[3]

The seed described “typed graph agents.” Agent symbols are sometimes informally called agent types, and Lafont's original paper emphasized a type discipline, but a static type system is not mandatory in the general definition. Typed interaction-net systems are important variants; untyped systems, including universal interaction combinators, remain genuine interaction nets.^[4]

Structural Signature¶

An interaction-net system contains the following roles:

A signature \(\Sigma\): a set of agent symbols with an arity map \(\operatorname{ar}:\Sigma\to\mathbb N\).
Port-bearing agents: an occurrence of \(\alpha\in\Sigma\) has one principal port and \(\operatorname{ar}(\alpha)\) ordered or otherwise distinguished auxiliary ports.
Linear wiring: an edge joins exactly two ports, and a port is incident to at most one edge. Unconnected ports are free ports.
An interface: the free ports expose the net to its context. Internal agents may be replaced without silently changing that external connection boundary.
An active pair: two agents connected through their principal ports form the only shape eligible for an interaction rule.
A rule table \(R\): for each unordered symbol pair \(\{\alpha,\beta\}\), there is at most one rule. Not every pair must have a rule.
An interface-preserving reduct: a rule replaces the active pair with a fixed finite net whose free ports correspond bijectively to the auxiliary-port connections exposed by the removed pair.
Local reduction: the rewrite changes the active pair and its prescribed replacement, then reconnects the preserved interface; unrelated graph regions remain untouched.
A normal or stuck state: no applicable active pair remains. In incomplete systems, a principal–principal connection with no rule can be stuck, so “no active pair” and “no reducible active pair” must not be conflated.

Write an active pair abstractly as

\[ \alpha(x_1,\ldots,x_m)\bowtie\beta(y_1,\ldots,y_n), \]

where the variables name its \(m+n\) connections to the context. A valid rule

\[ \alpha(\vec x)\bowtie\beta(\vec y)\;\Longrightarrow\;N_{\alpha\beta}(\vec x,\vec y) \]

uses the same interface names exactly as prescribed by the port discipline. The right-hand side may create or destroy internal agents, but it cannot duplicate, discard, or merge external wires implicitly. Such resource changes require explicit agents and rules.

The confluence invariant follows structurally. If \(M\to M_1\) reduces active pair \(p\) and \(M\to M_2\) reduces a distinct pair \(q\), then \(p\) and \(q\) share no agent. Reducing the residual of \(q\) in \(M_1\), or the residual of \(p\) in \(M_2\), yields the same net \(M'\):

\[ M_1\to M'\leftarrow M_2. \]

This proof depends on the single-principal-port, active-pair, unique-rule, and interface-preservation conditions. Relaxing them may sacrifice the diamond property.

What It Is Not¶

Interaction nets are not arbitrary graph rewriting. General graph rules may match large or overlapping subgraphs, inspect context, identify several nodes, or offer competing rules for one match. Interaction nets deliberately restrict the left-hand side to a principal-port pair and preserve a fixed interface. Their confluence is purchased by this loss of pattern freedom.

They are not Petri nets. A Petri net holds a marking of tokens over places, and transitions consume and produce token multisets according to incidence arcs. An interaction net rewrites the graph topology and agents themselves. Both expose concurrency, but their state spaces and enabling rules are different.

They are not simply term-rewriting systems. Ordinary terms are rooted trees, and substitution, copying, and erasure may occur implicitly in a rewrite. Interaction nets admit sharing and cyclic wiring and represent resource operations explicitly. Fernández and Mackie showed systematic relationships with term rewriting, but the graphical port discipline remains a genuine residual rather than notation alone.^[2]

They are not the lambda calculus, although lambda terms can be compiled into them. Beta reduction becomes local graph interaction only after application, abstraction, sharing, duplication, and erasure are encoded. Different interaction-net evaluators make different translation and strategy choices.^[5]^[6]

They are not identical to linear-logic proof nets. Lafont generalized ideas from proof structures, and interaction systems can encode cut elimination. But arbitrary interaction-net signatures and rules need not be proofs of a particular logic, and typing is optional.^[1]^[7]

Finally, they are not the machine-learning interaction network architecture for object-relation reasoning, a social interaction network, or a generic live prime:network. Those share node-edge vocabulary but not the principal-port rewrite discipline.

Scope of Application¶

The core scope is theoretical computer science: graph rewriting, models of computation, declarative programming, functional-language implementation, linear logic, and parallel reduction. Interaction nets can serve as a high-level visual programming formalism or as a low-level target into which another calculus is compiled. Their interface-preserving rules support compositional construction; their explicit resource agents expose copying and erasure; and their local steps map naturally to pointer-rewiring implementations.^[8]^[9]

Lambda-calculus evaluation is the best-established application family. Interaction-net implementations have represented beta reduction, sharing graphs, Lévy-style optimal reduction, and closed reduction. Linear-logic applications encode multiplicative, exponential, and additive cut elimination. Lafont's interaction combinators show that three symbols and six rules suffice for a universal distributed-computation model, establishing that the severe local restriction does not destroy computational universality.^[4]^[7]

The model also supports studies of abstract machines, compilation, in-place graph rewriting, process-network encodings, and parallel execution. These are applications of one formal core, not guarantees that every net runs well on every architecture. Some programs expose many simultaneous active pairs; others generate essentially one at a time. Heap allocation, contention, graph placement, cache locality, and readback can dominate physical performance even though the calculus permits independent semantic steps.^[3]

Clarity¶

A candidate is an interaction-net system only if all of these questions have satisfactory answers:

What is the signature, and what fixed arity belongs to each agent symbol?
Which port is the unique principal port of every agent occurrence?
Are edges linear—at most one edge incident to each port—and which free ports form the interface?
Does rewriting trigger only on principal–principal active pairs?
Is there at most one rule for each unordered pair of agent symbols?
Does each rule preserve the active pair's external interface exactly?
Are copying and erasing explicit rather than silently performed by the meta-language?

If a graph merely carries messages, if nodes update from neighboring state on a global clock, or if rewrite rules match arbitrary neighborhoods, the case is not an interaction net. If rules add nondeterministic choices, multiple principal ports, nested patterns, side effects, or context tests, it is an extension whose confluence must be proved afresh rather than inherited from the standard definition.

The strongest reader trap is the word interaction. Two agents connected auxiliary-to-auxiliary do not reduce merely because they are adjacent. Computation triggers only when their principal ports meet and a rule exists for that symbol pair.

Manages Complexity¶

Interaction nets manage rewriting complexity by making critical overlap impossible at the primitive level. In a general rewrite system, proving confluence may require enumerating and joining critical pairs. Here the one-principal-port restriction prevents one agent from participating in two active pairs, while the one-rule-per-symbol-pair restriction removes ambiguity at a redex. The calculus obtains local diamond behavior from representation design rather than a global theorem proved separately for each program.

They also turn implicit resource behavior into inspectable graph structure. A term calculus can substitute one argument into many occurrences or delete an unused variable as a meta-operation. In an interaction-net encoding, duplication and erasure are realized by agents and local rules. This makes sharing cost, fan propagation, and garbage behavior visible to optimization and implementation.

Free-port interfaces isolate a component's context. A rule can replace an internal active pair while reconnecting the same boundary, so local reasoning does not require traversing the entire graph. Textual interaction calculi then represent the same structure with names, terms, and equations, making operational semantics, strategy, and implementation proofs easier to state than in pictures alone.^[8]

The abstraction does not eliminate complexity; it relocates it. High-level pattern matching must be compiled into binary interactions, large data structures require agent families, and graph management may be expensive. The benefit is that every primitive step has a small, explicit dependency footprint.

Abstract Reasoning¶

Redex-independence inference. If two applicable active pairs are distinct, they share no agent. Their one-step reductions commute. An evaluator may schedule either first or execute both in parallel without changing the joined semantic state.

Unique-normal-form inference. Strong confluence implies at most one normal form when one is reachable. It does not prove that reduction terminates, that a normal form exists, or that a scheduler will reach it under an unfair strategy. Lafont's interaction combinators include universal computation and therefore nontermination.^[4]

Interface-invariance inference. A local rule preserves the number and identity correspondence of external connections. If a proposed replacement adds or loses a boundary wire, it is malformed unless the change is represented inside the net by explicit erasing, duplication, or construction.

Parallel-width inference. The number of simultaneously present active pairs bounds semantic parallelism at that moment. A net with one active pair is sequential even on many processors; a broad active-pair frontier offers potential parallelism. Physical speedup further depends on work per interaction, allocation, locality, contention, and scheduling.^[3]

Cost-locality inference. For a fixed finite rule table, one primitive interaction has a fixed-size pattern and replacement. This supports constant-rule-footprint implementations. It does not imply constant program runtime: a computation may create unboundedly many agents and interactions.

Extension-safety inference. Adding multiple rules for one active pair, context-sensitive matches, side effects, or multi-principal agents invalidates the standard confluence argument. The extension may be useful, but its nondeterminism and synchronization properties need independent analysis.

Encoding-audit inference. To claim that a source calculus is implemented, one must supply a translation, show how source reductions are simulated, preserve an observational or normal-form readback, and account for administrative interactions. A visually suggestive net is not by itself a correct compiler.

Knowledge Transfer¶

Literal transfer occurs among interaction-net systems with different signatures. Arithmetic agents, lambda-calculus agents, linear-logic connectives, universal interaction combinators, process-network nodes, and implementation-oriented instructions preserve the same one-principal-port, active-pair, unique-rule, interface-preserving rewrite skeleton. The domain vocabulary changes while the model of computation remains identical.

Transfer also occurs between graphical and textual presentations. A name can represent a wire, a term can represent an agent tree rooted at a port, and an equation can connect two roots. Fernández and Mackie's interaction calculus gives formal substitution, indirection, strategy, and configuration semantics while denoting the same nets.^[8]

The model transfers into compiler and runtime design as a constrained intermediate representation. Locality suggests pointer rewiring; non-overlap suggests parallel work queues; explicit duplication suggests sharing analyses; and interface preservation suggests modular compilation. These are engineering consequences of the formal structure, not metaphors.

Outside computation and logic, “two components interact locally in a network” is insufficient. Chemical reactions, social networks, neural interaction networks, and cellular automata lack the exact agent-port and rule-table discipline unless deliberately encoded. Their resemblance belongs to generic Network, Interface, and local-rewriting abstractions rather than making Interaction Nets a prime.

Examples¶

A lambda-calculus encoding. An application agent and an abstraction agent can be arranged so their principal ports meet at a beta redex. The interaction rewires the function body and argument locally. If an argument is used several times or not at all, separate duplicator or eraser agents propagate that resource behavior. The full correctness claim depends on the chosen encoding and readback; interaction nets do not make beta substitution disappear for free.^[5]^[6]

Interaction combinators. Lafont's universal system uses three agent symbols—commonly written \(\gamma\), \(\delta\), and \(\varepsilon\)—with arities two, two, and zero, and six local rules. It can simulate arbitrary interaction systems. The example demonstrates the expressiveness tension: an extremely small local vocabulary can support universal behavior, including divergence.^[4]

Linear-logic cut elimination. A translation maps logical proof structure into agents and wires; interacting principal ports represent reducible cuts. Multiplicative, exponential, and additive structures can be encoded using interaction combinators, with cut elimination simulated by local rules. This is a canonical lineage but not the definition of every interaction net.^[7]

Textual interaction calculus. A configuration records interface terms and a multiset of equations. When the roots of two agent terms form a rule-bearing active pair, interaction replaces that equation with equations exposing the rule's right-hand-side wiring; indirection eliminates a wire name by substitution. The calculus supports formal operational reasoning while preserving the graph's linear-name discipline.^[8]

Process-network compilation. A Kahn-style process network can be translated so process state, channels, and messages are represented in one interaction-net substrate. This is an encoding application: the source network's stream semantics and the target net's local rewrites must be related by a correctness argument.^[10]

Negative case. A graph-rewrite engine allows two overlapping three-node patterns and chooses nondeterministically between them. Even if it calls its vertices agents and executes locally, it fails the active-pair and unique-rule restrictions. Its confluence cannot be inferred from interaction-net theory.

Structural Tensions¶

Rule restriction versus expressiveness. Binary principal-port rules are easy to analyze but awkward for high-level nested patterns. Compilers must decompose rich matches into auxiliary agents and multiple interactions. Extensions regain convenience while risking the standard confluence proof.

Confluence versus termination. Reduction order does not change a reachable normal form, but a net may reduce forever. Determinacy of result and existence of result are separate properties.

Semantic parallelism versus realized speedup. Disjoint redexes need no semantic ordering, yet runtimes still allocate nodes, update pointers, arbitrate work, preserve memory safety, and balance load. Some nets expose too little simultaneous work to amortize that machinery.^[3]

Local rules versus global graph cost. Each rule sees a tiny neighborhood, but its data may be scattered in memory. Pointer chasing, cache misses, communication, and readback can make a locally constant rewrite globally expensive.

Explicit resources versus concise programs. Making duplication, erasure, and sharing first-class exposes cost and enables optimization, but expands representations that a lambda term or functional program states implicitly.

Graphical transparency versus formal manipulation. Diagrams make locality and sharing visible; large nets become unreadable and difficult to serialize. Textual calculi improve proofs and implementation but can hide the spatial intuition that motivated the model.

Pure confluence versus effects. Input, output, nondeterministic choice, and external calls are useful, but they introduce order-sensitive observations or rule choices. An effectful extension must state which confluence or equivalence guarantee survives.

Structural–Framed Character¶

Interaction Nets are strongly structural and strongly framed. Their identity is unusually close to a checklist of graph constraints: port cardinality, a unique principal port, active-pair shape, rule uniqueness, interface preservation, and local replacement. From that checklist one derives disjoint redexes and the diamond property.

The framing is nevertheless essential. “Agent,” “port,” “redex,” “rewrite,” “normal form,” “signature,” and “confluence” are formal-computation commitments. Removing them leaves the generic idea that local non-overlapping changes can run in parallel. That broader skeleton already appears in generic Network, Interface, locality, and rewriting concepts and is too weak to identify the Lafont formalism. The candidate therefore passes domain-specific autonomy and fails prime qualification.

Structural Core vs. Domain Accent¶

The portable core is constrain local operations so their write footprints do not overlap, preserve a declared boundary, and remove rule ambiguity; then independent operations commute. This pattern helps reason about parallel transactions, local graph transformations, distributed updates, and modular replacement.

Interaction Nets add a non-negotiable formal accent: fixed-arity symbols, one principal port per agent, linear wiring, principal–principal active pairs, a partial one-rule-per-unordered-pair table, and interface-preserving net replacement. Copying and erasing are graph operations, not silent structural rules. A system that preserves only “local independent work” instantiates the portable core but not this node.

The linear-logic origin is historically and technically important but not an admission criterion. A system need not be typed or directly encode proof nets. Conversely, a graph derived from linear logic is not automatically an interaction net unless it satisfies the port and rewrite discipline.

The proposed direct parent is live prime:network. Every interaction net is a network-like graph of agent occurrences connected by edges, and its interface and rewrite behavior are extra constraints on that genus. The relation is strict specialization, not mere composition: remove the graph connectivity and no interaction net remains, while most networks lack ports and reduction rules.

Live prime:interface is a strong related concept because free ports are precisely the boundary preserved across a local rewrite. It is not a second parent; an interaction net is not a subtype of generic Interface. Live prime:equivalence_preserving_rewriting is related through semantics-preserving compilation and optimization, but ordinary interaction reduction performs computation toward a result rather than necessarily choosing operational forms under an explicit cost criterion. Live prime:determinism captures uniqueness of result, while interaction-net strong confluence is a specific structural route to that property and still permits divergence.

Live prime:interleaving describes sequential schedules of otherwise independent steps. Interaction nets make different redex orders semantically joinable, but the node is not a subtype of Interleaving because physical parallel execution need not serialize the reductions.

Relationships to Other Abstractions¶

Current abstraction Interaction Nets Domain-specific

Parents (1) — more general patterns this builds on

Interaction Nets is a kind of Network Prime

The proposed direct parent is live prime:network.

Hierarchy path (1) — routes to 1 parentless root

Interaction Nets → Network → Reservoir-Flux Network → Conservation Laws → Invariance

Neighborhood in Abstraction Space¶

Interaction Nets sits in a sparse region of the domain-specific corpus (94^th percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Unclustered & Miscellaneous (1565 abstractions)

Nearest neighbors

Computed from structural-signature embeddings · 2026-09-08

Not to Be Confused With¶

Network: a generic node-edge structure; lacks principal/auxiliary ports and rewrite semantics.
Graph-rewriting system: broader family permitting larger, overlapping, context-sensitive, or ambiguous patterns.
Term-rewriting system: tree/term syntax with different copying, sharing, and substitution behavior.
Petri net: token-flow transition system rather than topology-rewriting port graph.
Proof net: graphical proof representation for linear logic; a source and application, not the complete interaction-net genus.
Lambda calculus: source calculus that can be encoded; beta reduction and substitution are not identical to primitive active-pair interaction.
Interaction calculus: textual operational presentation of interaction nets, not a different graphical model.
Interaction combinators: Lafont's particular three-symbol universal interaction system, a strict instance of the broader formalism.
Actor model or process network: communicating-process models that may be compiled to interaction nets but have different native states and semantics.
Machine-learning interaction network: object-relation neural architecture; lexical collision only.
Typed interaction nets: an important subclass; typing is not mandatory for the base identity.
Parallel implementation: an engineering realization. Standard nets expose conflict-free semantic redexes but do not guarantee hardware speedup.

References¶

[1] Yves Lafont, “Interaction Nets,” in Proceedings of the 17^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '90) (1990), 95–108. https://doi.org/10.1145/96709.96718. registry ↩a ↩b ↩c

[2] Maribel Fernández and Ian Mackie, “Interaction Nets and Term-Rewriting Systems,” Theoretical Computer Science 190, no. 1 (1998): 3–39. https://doi.org/10.1016/S0304-3975(97)00082-0. registry ↩a ↩b

[3] Ian Mackie and Shinya Sato, “Parallel Evaluation of Interaction Nets: Case Studies and Experiments,” Electronic Communications of the EASST 73 (2016). https://doi.org/10.14279/tuj.eceasst.73.1034. registry ↩a ↩b ↩c ↩d

[4] Yves Lafont, “Interaction Combinators,” Information and Computation 137, no. 1 (1997): 69–101. https://doi.org/10.1006/inco.1997.2643. registry ↩a ↩b ↩c ↩d

[5] Ian Mackie, “YALE: Yet Another Lambda Evaluator Based on Interaction Nets,” in Proceedings of ICFP '98 (1998), 117–128. https://doi.org/10.1145/289423.289434. registry ↩a ↩b

[6] Ian Mackie, “An Interaction Net Implementation of Closed Reduction,” in Implementation and Application of Functional Languages, LNCS 5836 (2011), 43–59. https://doi.org/10.1007/978-3-642-24452-0_3. registry ↩a ↩b

[7] Ian Mackie and Jorge Sousa Pinto, “Encoding Linear Logic with Interaction Combinators,” Information and Computation 176, no. 2 (2002): 153–186. https://doi.org/10.1006/inco.2002.3163. registry ↩a ↩b ↩c

[8] Maribel Fernández and Ian Mackie, “A Calculus for Interaction Nets,” in Principles and Practice of Declarative Programming (PPDP 1999), LNCS 1702 (1999), 170–187. https://doi.org/10.1007/10704567_10. registry ↩a ↩b ↩c ↩d

[9] Ian Mackie, “Towards a Programming Language for Interaction Nets,” Electronic Notes in Theoretical Computer Science 127, no. 5 (2005): 133–151. https://doi.org/10.1016/j.entcs.2005.02.015. registry ↩

[10] Ian Mackie, “Compiling Process Networks to Interaction Nets,” Electronic Proceedings in Theoretical Computer Science 225 (2016): 5–14. https://doi.org/10.4204/EPTCS.225.3. registry ↩