Agent Skills: Interaction Nets Skill

Lafont's interaction nets for optimal parallel λ-reduction. Graph rewriting

UncategorizedID: plurigrid/asi/interaction-nets

Install this agent skill to your local

pnpm dlx add-skill https://github.com/plurigrid/asi/tree/HEAD/plugins/asi/skills/interaction-nets

Skill Files

Browse the full folder contents for interaction-nets.

Download Skill

Loading file tree…

plugins/asi/skills/interaction-nets/SKILL.md

Skill Metadata

Name
interaction-nets
Description
Lafont's interaction nets for optimal parallel λ-reduction. Graph rewriting

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

  1. No evaluation order — unlike λ-calculus, no choice between CBV/CBN
  2. Optimal sharing — work is never duplicated (Lamping's algorithm)
  3. Massively parallel — every independent redex reduces simultaneously
  4. 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

  1. Lafont (1990) - "Interaction Nets" (original paper)
  2. Lamping (1990) - Optimal λ-reduction algorithm
  3. Mazza (2007) - Symmetric Interaction Combinators
  4. 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 optimize
  • linear-logic - Logical foundation
  • graph-rewriting - General theory
  • propagators - Another "no control flow" model