| name | interaction-nets |
| description | Lafont's interaction nets for optimal parallel λ-reduction. Graph rewriting |
| version | 1.0.0 |
Interaction Nets Skill
"The only model where parallelism is not an optimization but the semantics itself."
Core Concept
Interaction nets are a graphical model of computation where:
- Nodes (agents) have typed ports
- Wires connect ports
- Reduction happens when two principal ports meet
- No global control — all reductions are local and can happen in parallel
┌─●─┐ ┌───┐
───┤ ├─── → ───┤ ├───
└─●─┘ └───┘
principal ports result
meet
Why It's Strange
- No evaluation order — unlike λ-calculus, no choice between CBV/CBN
- Optimal sharing — work is never duplicated (Lamping's algorithm)
- Massively parallel — every independent redex reduces simultaneously
- Linear by default — resources used exactly once (linear logic connection)
Interaction Combinators
Lafont's universal basis (3 agents):
ε (eraser) δ (duplicator) γ (constructor)
│ /│\ /│\
● ● │ ● ● │ ●
│ │
● ●
Reduction Rules
γ ─● ●─ γ → cross-wire (annihilation)
δ ─● ●─ δ → cross-wire (annihilation)
γ ─● ●─ δ → duplication (commutation)
ε ─● ●─ γ → erase both aux ports
ε ─● ●─ δ → erase both aux ports
HVM / Bend Implementation
Bend compiles to HVM (Higher-order Virtual Machine):
# Bend syntax (Python-like, compiles to interaction nets)
def sum(n):
if n == 0:
return 0
else:
return n + sum(n - 1)
# Automatically parallelizes via interaction net reduction
# No explicit parallelism needed!
Install & Run
# Install Bend
cargo install hvm
cargo install bend-lang
# Run with parallelism
bend run program.bend -p 8 # 8 threads
λ-Calculus Encoding
Abstraction (λx.M)
│ (bound var)
┌───●───┐
│ λ │
└───●───┘
│ (body)
Application (M N)
│ │
●───@───●
│
● (result)
β-reduction as Interaction
(λx.M) N
│ │
┌───●───┐ ┌───●───┐
│ λ ├───┤ @ │
└───●───┘ └───●───┘
│ │
M N
→ substitutes N for x in M (via wire surgery)
Optimal Reduction
The key insight: sharing is explicit.
Traditional: (λx. x + x) expensive
→ expensive + expensive (duplicated!)
Interaction: (λx. x + x) expensive
→ shared node, reduces ONCE, result shared
Symmetric Interaction Combinators
Mazza's variant (used in HVM2):
S (symmetry) D (duplication) E (eraser)
/│\ /│\ │
● │ ● ● │ ● ●
│ │
● ●
# Only 6 rules needed for universal computation
Code Examples
Minimal Interaction Net in Julia
abstract type Agent end
struct Eraser <: Agent end
struct Constructor <: Agent
aux1::Union{Agent, Nothing}
aux2::Union{Agent, Nothing}
end
struct Duplicator <: Agent
aux1::Union{Agent, Nothing}
aux2::Union{Agent, Nothing}
end
struct Wire
from::Agent
from_port::Symbol # :principal, :aux1, :aux2
to::Agent
to_port::Symbol
end
function reduce!(net::Vector{Wire})
# Find active pairs (principal-principal connections)
active = filter(w -> w.from_port == :principal &&
w.to_port == :principal, net)
# Reduce all in parallel (no order!)
for wire in active
reduce_pair!(net, wire.from, wire.to)
end
end
function reduce_pair!(net, a::Constructor, b::Constructor)
# Annihilation: cross-connect auxiliaries
# ... wire surgery ...
end
function reduce_pair!(net, a::Constructor, b::Duplicator)
# Commutation: duplicate the constructor
# ... create new nodes ...
end
Bend Example: Parallel Tree Sum
type Tree:
Leaf { value }
Node { left, right }
def sum(tree):
match tree:
case Tree/Leaf:
return tree.value
case Tree/Node:
return sum(tree.left) + sum(tree.right)
# ↑ Both branches computed in parallel automatically!
def main():
tree = Node(Node(Leaf(1), Leaf(2)), Node(Leaf(3), Leaf(4)))
return sum(tree) # → 10, computed in parallel
Relationship to Linear Logic
| Linear Logic | Interaction Nets |
|---|---|
| ⊗ (tensor) | Constructor |
| ⅋ (par) | Duplicator |
| ! (of course) | Box/Unbox agents |
| Cut elimination | Reduction |
Performance
| Metric | Traditional λ | Interaction Nets |
|---|---|---|
| Complexity | Can be exponential | Optimal (no duplication) |
| Parallelism | Sequential (usually) | Maximal |
| Memory | GC needed | Linear (no GC) |
| Sharing | Implicit (hard) | Explicit (easy) |
Literature
- Lafont (1990) - "Interaction Nets" (original paper)
- Lamping (1990) - Optimal λ-reduction algorithm
- Mazza (2007) - Symmetric Interaction Combinators
- Taelin (2024) - HVM2 and Bend language
End-of-Skill Interface
GF(3) Integration
# Trit assignment for interaction net agents
AGENT_TRITS = Dict(
:eraser => -1, # Destruction
:duplicator => 0, # Neutral (copies)
:constructor => 1, # Creation
)
# Conservation: every reduction preserves GF(3) sum
# γ-γ annihilation: (+1) + (+1) → 0 (both gone)
# ε-γ erasure: (-1) + (+1) → 0
r2con Speaker Resources
| Speaker | Relevance | Repository/Talk |
|---|---|---|
| condret | ESIL graph rewriting | radare2 ESIL |
| thestr4ng3r | CFG reduction graphs | r2ghidra |
| xvilka | RzIL graph IR | rizin |
Related Skills
lambda-calculus- What interaction nets optimizelinear-logic- Logical foundationgraph-rewriting- General theorypropagators- Another "no control flow" model