Explains Lafont's interaction nets for optimal parallel λ-calculus reduction and graph rewriting. Covers combinators, rules, Bend/HVM examples.
From asi-skillsnpx claudepluginhub plurigrid/asiThis skill uses the workspace's default tool permissions.
README.mdGuides Next.js Cache Components and Partial Prerendering (PPR) with cacheComponents enabled. Implements 'use cache', cacheLife(), cacheTag(), revalidateTag(), static/dynamic optimization, and cache debugging.
Migrates code, prompts, and API calls from Claude Sonnet 4.0/4.5 or Opus 4.1 to Opus 4.5, updating model strings on Anthropic, AWS, GCP, Azure platforms.
Facilitates interactive brainstorming sessions using diverse creative techniques and ideation methods. Activates when users say 'help me brainstorm' or 'help me ideate'.
"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