Lafont's interaction nets for optimal parallel λ-reduction. Graph rewriting
/plugin marketplace add plurigrid/asi/plugin install asi-skills@asi-skillsThis skill inherits all available tools. When active, it can use any tool Claude has access to.
README.md"The only model where parallelism is not an optimization but the semantics itself."
Interaction nets are a graphical model of computation where:
┌─●─┐ ┌───┐
───┤ ├─── → ───┤ ├───
└─●─┘ └───┘
principal ports result
meet
Lafont's universal basis (3 agents):
ε (eraser) δ (duplicator) γ (constructor)
│ /│\ /│\
● ● │ ● ● │ ●
│ │
● ●
γ ─● ●─ γ → cross-wire (annihilation)
δ ─● ●─ δ → cross-wire (annihilation)
γ ─● ●─ δ → duplication (commutation)
ε ─● ●─ γ → erase both aux ports
ε ─● ●─ δ → erase both aux ports
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 Bend
cargo install hvm
cargo install bend-lang
# Run with parallelism
bend run program.bend -p 8 # 8 threads
│ (bound var)
┌───●───┐
│ λ │
└───●───┘
│ (body)
│ │
●───@───●
│
● (result)
(λx.M) N
│ │
┌───●───┐ ┌───●───┐
│ λ ├───┤ @ │
└───●───┘ └───●───┘
│ │
M N
→ substitutes N for x in M (via wire surgery)
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
Mazza's variant (used in HVM2):
S (symmetry) D (duplication) E (eraser)
/│\ /│\ │
● │ ● ● │ ● ●
│ │
● ●
# Only 6 rules needed for universal computation
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
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
| Linear Logic | Interaction Nets |
|---|---|
| ⊗ (tensor) | Constructor |
| ⅋ (par) | Duplicator |
| ! (of course) | Box/Unbox agents |
| Cut elimination | Reduction |
| 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) |
# 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
| Speaker | Relevance | Repository/Talk |
|---|---|---|
| condret | ESIL graph rewriting | radare2 ESIL |
| thestr4ng3r | CFG reduction graphs | r2ghidra |
| xvilka | RzIL graph IR | rizin |
lambda-calculus - What interaction nets optimizelinear-logic - Logical foundationgraph-rewriting - General theorypropagators - Another "no control flow" model