Interaction Nets examples

An interaction net is a graph you compute with by rewriting it. Each node is an agent with one principal port and some auxiliaries; wherever two principal ports are wired to each other you have an active pair, and a rule says what that pair becomes. Lambda is a ready-made vocabulary of agents — APP, LAM, DUP, DELIM, ERASE, VAR, ROOT, CONST — and Lambda.rules() is a rule book covering it.

Build a net with net { }, wiring ports with to; call relax to let the force-directed layout settle; and hand it to Reducer(Lambda.rules()), whose stepDetailed fires one reaction and returns what changed. Draw it with toFLines, or summarise it as a card with summaryHtml. The single-step examples below each show three cards over a before-and-after drawing; Reference lists the whole API.

Every node also carries an energy, and every rule splits or reduces the energy of the nodes it creates, so a reduction visibly fades as it runs. The energy is there for drawing and does not change what a net computes; it is where the energy figures quoted below come from.

Reducing a λ-term end to end

LambdaTerms.normalise("(\\x. x x) (\\y. y)") parses a term, compiles it to a net, reduces it and reads the answer back as a term. parse accepts \x. x x or λx. x x, with \x y. e as shorthand, and format prints a term that parses back to the same thing. When two DUP fans meet, the fan-fan rule compares their levels: two fans at the same level cancel, and two at different levels pass through each other. erase-erase does the same for two erasers. Pass Reducer(relaxIterations = 0) when nothing will be drawn, so the reduction skips the layout work; the figure below passes 8.

Those are the five stages of (λx. x x) (λy. y), a small term that exercises several kinds of agent. Left to right: the compiled net, 6 agents (ROOT, two APP, two LAM, one DUP — the fan for x, which is used twice); after beta-linear, 4; after dup-lam, 6, with two fans facing each other; after a second beta-linear, 4; and after fan-fan cancels the matched pair, 2 agents holding λa. a. Each panel is scaled to fit its own box, so compare the agent counts rather than the sizes of the drawings.

A term with no normal form never finishes reducing, so normalise takes a maxSteps and leaves Run.finished false when it runs out. Run.steps counts every reaction, fan meetings and erasures included, so it is larger than the number of β-steps.

For the test terms in LambdaTerms.corpus(), the order in which active pairs are chosen changes neither the result nor the amount of work: under every ActivationOrder each term takes the same number of reactions and fires the same rules. A λ-term you can hear measures and draws this.

Reading back a shared answer

The rule book is Lambdascope (van Oostrom, van de Looij and Zwitserlood), an optimal reduction in which each DUP and each DELIM (a scope delimiter) carries a level, so shared structure is handled correctly on every term. On the terms in LambdaTerms.corpus() and on simply-typed terms it gives the same answer as substitution. On a small share of untyped terms, readback cannot tell which copy a shared part of the answer belongs to, and leaves a ⋈ mark in its place.

LambdaTerms.marksOf returns the marks readback left in a result: an empty list means the net read back as an ordinary term, and anything else means the reducer could not give a trustworthy answer. A ? mark means a variable was found outside the body of its binder, so the net no longer describes a term.

Run.finished answers a different question: whether the reduction stopped because nothing was left to fire. Check both: a finished run with marks is still not an answer you should trust.

Beta bridge with swapped pair orientation

APP ⟂ LAM has to reduce the same way whichever order the active pair was connected in, so this net wires it backwards, LAM -> APP, and the rewrite card reports swapped: yes. What beta-linear then does is pure rewiring: the lambda's body is connected to the application's context and its binder to the application's argument, created is none, and APP and LAM are dropped. It is the one rule of the four that attenuates nothing: total energy falls from 5.90 to 3.70, which is exactly the 2.20 the two removed nodes were carrying.

:::static
val reducer = Reducer(Lambda.rules())
val net = net {
    val root = node(Lambda.ROOT, id = "root", at = vec(-180.0, -80.0), state = NodeState(energy = 0.7))
    val app = node(Lambda.APP, id = "app", at = vec(-40.0, 0.0), state = NodeState(energy = 0.8))
    val lam = node(Lambda.LAM, id = "lam", at = vec(40.0, 0.0), state = NodeState(energy = 1.4))
    val arg = node(Lambda.CONST, id = "arg", at = vec(170.0, 80.0), state = NodeState(energy = 1.1))
    val binder = node(Lambda.VAR, id = "binder", at = vec(180.0, -70.0), state = NodeState(energy = 0.9))
    val body = node(Lambda.VAR, id = "body", at = vec(170.0, 10.0), state = NodeState(energy = 1.0))

    lam.principal to app.principal
    app.aux(0) to root.principal
    app.aux(1) to arg.principal
    lam.aux(0) to binder.principal
    lam.aux(1) to body.principal
}

net.relax(20)
// Capture before rewriting; later relaxation must not move this stage.
val before = stage("Before beta", net.toFLines(), net.summaryHtml("Before beta", maxNodes = 5))
val detail = reducer.stepDetailed(net)!!
net.relax(28)
val after = stage("After beta", net.toFLines(), net.summaryHtml("After beta", maxNodes = 5))
showInteractionStages(
    before,
    after,
    cards = [detail.summaryHtml("Rewrite")],
    channel = "overview",
    graphicTitle = "Before / rewrite / after geometry",
)

println("interaction beta bridge ready")

Energy-biased scheduling

This net offers the reducer two structurally identical DUP ⟂ CONST pairs, one at energies 0.6 and 0.5 and one at 1.2 and 1.8, and asks for a single step. Under ActivationOrder.HIGHEST_PAIR_ENERGY the hotter pair fires and the colder one is left standing, so which rewrite happens next is a property of the state the nodes are carrying rather than of the order they were built in.

:::static
val reducer = Reducer(Lambda.rules(), order = ActivationOrder.HIGHEST_PAIR_ENERGY)
val net = net {
    val lowL = node(Lambda.ROOT, id = "lowL", at = vec(-320.0, -40.0), state = NodeState(energy = 0.2))
    val lowR = node(Lambda.ROOT, id = "lowR", at = vec(-320.0, 50.0), state = NodeState(energy = 0.2))
    val dupLow = node(Lambda.DUP, id = "dupLow", at = vec(-160.0, 0.0), state = NodeState(energy = 0.6))
    val constLow = node(Lambda.CONST, id = "constLow", at = vec(-40.0, 0.0), state = NodeState(energy = 0.5))

    val highL = node(Lambda.ROOT, id = "highL", at = vec(80.0, -40.0), state = NodeState(energy = 0.2))
    val highR = node(Lambda.ROOT, id = "highR", at = vec(80.0, 50.0), state = NodeState(energy = 0.2))
    val dupHigh = node(Lambda.DUP, id = "dupHigh", at = vec(220.0, 0.0), state = NodeState(energy = 1.2))
    val constHigh =
        node(Lambda.CONST, id = "constHigh", at = vec(340.0, 0.0), state = NodeState(energy = 1.8, hue = 0.14))

    dupLow.principal to constLow.principal
    dupLow.aux(0) to lowL.principal
    dupLow.aux(1) to lowR.principal

    dupHigh.principal to constHigh.principal
    dupHigh.aux(0) to highL.principal
    dupHigh.aux(1) to highR.principal
}

net.relax(20)
// Capture before rewriting; later relaxation must not move this stage.
val before = stage("Before scheduler step", net.toFLines(), net.summaryHtml("Before scheduler step", maxNodes = 5))
val detail = reducer.stepDetailed(net)!!
net.relax(28)
val after = stage("After one step", net.toFLines(), net.summaryHtml("After one step", maxNodes = 5))
showInteractionStages(
    before,
    after,
    cards = [detail.summaryHtml("Selected pair")],
    channel = "overview",
    graphicTitle = "Before / rewrite / after geometry",
)

println("interaction scheduler ready")

DUP splits state into two descendants

dup-const replaces the constant with one copy per DUP auxiliary, and the copies are not identical to it or to each other. Each inherits half the original's energy attenuated by 0.9 (0.81 from the constant's 1.8), and the two are pushed 0.05 apart in hue. Same shape, different colours: a second duplication further down then reads as a gradient rather than as a repeat.

:::static
val reducer = Reducer(Lambda.rules(), order = ActivationOrder.HIGHEST_PAIR_ENERGY)
val net = Lambda.duplicatedConstantDemo()

net.relax(20)
// Capture before rewriting; later relaxation must not move this stage.
val before = stage("Before duplication", net.toFLines(), net.summaryHtml("Before duplication", maxNodes = 5))
val detail = reducer.stepDetailed(net)!!
net.relax(28)
val after = stage("After duplication", net.toFLines(), net.summaryHtml("After duplication", maxNodes = 5))
showInteractionStages(
    before,
    after,
    cards = [detail.summaryHtml("Duplicate event")],
    channel = "overview",
    graphicTitle = "Before / rewrite / after geometry",
)

println("interaction duplication ready")

ERASE starts a visible decay cascade

erase-app does not delete a subtree. It removes the ERASE ⟂ APP pair and puts a fresh ERASE agent on each of the application's two auxiliaries, each carrying half the application's energy attenuated to 0.55 with a small bias added back, or 0.39 from the application's 1.25. So one active pair becomes two, and the cascade in the "after" card is queued rather than finished: total energy is down from 4.00 to 2.64, and the next two steps are what actually consume the constant and the variable.

:::static
val reducer = Reducer(Lambda.rules())
val net = Lambda.eraseApplicationDemo()

net.relax(20)
// Capture before rewriting; later relaxation must not move this stage.
val before = stage("Before erase", net.toFLines(), net.summaryHtml("Before erase", maxNodes = 5))
val detail = reducer.stepDetailed(net)!!
net.relax(28)
val after = stage("After erase step", net.toFLines(), net.summaryHtml("After erase step", maxNodes = 5))
showInteractionStages(
    before,
    after,
    cards = [detail.summaryHtml("Prune step")],
    channel = "overview",
    graphicTitle = "Before / rewrite / after geometry",
)

println("interaction erase ready")

Two fans that commute, run to a fixed point

The examples above each take one step. Fans and erasers usually meet near the end of a reduction, so to see fan-fan this example keeps stepping until nothing more can fire. Two DUP fans face each other at different levels, 1 and 2, so fan-fan takes its commuting branch rather than its annihilating one: each duplication has to be applied to the other, and one fan pair becomes four fans wired in a 2×2 crossing. The count goes up before it goes down. Those four fans are then facing the four constants, so four dup-const reactions follow and the four constants come out as eight copies — five reactions in total, 6 agents to 8, and not one fan left standing. Give the two fans the same label and the first step is an annihilation instead: two reactions, and the constants are spliced straight through in pairs.

The last card says 4 active pairs and is nevertheless finished. The eight constants are wired principal to principal in four pairs, and no rule in the book covers CONST ⟂ CONST, so stepDetailed returns null. An active pair only reduces when a rule matches it.

:::static
val reducer = Reducer(Lambda.rules())
val subject = net {
    val fanA = node(Lambda.DUP, id = "fanA", at = vec(-80.0, 0.0), state = Lambda.fan(1))
    val fanB = node(Lambda.DUP, id = "fanB", at = vec(80.0, 0.0), state = Lambda.fan(2))
    val c1 = node(Lambda.CONST, id = "c1", at = vec(-200.0, -80.0), state = NodeState(energy = 1.0, hue = 0.04))
    val c2 = node(Lambda.CONST, id = "c2", at = vec(-200.0, 80.0), state = NodeState(energy = 1.0, hue = 0.12))
    val c3 = node(Lambda.CONST, id = "c3", at = vec(200.0, -80.0), state = NodeState(energy = 1.0, hue = 0.20))
    val c4 = node(Lambda.CONST, id = "c4", at = vec(200.0, 80.0), state = NodeState(energy = 1.0, hue = 0.28))

    fanA.principal to fanB.principal
    fanA.aux(0) to c1.principal
    fanA.aux(1) to c2.principal
    fanB.aux(0) to c3.principal
    fanB.aux(1) to c4.principal
}

subject.relax(20)
// Capture before rewriting; later relaxation must not move this stage.
val before =
    stage("Before: labels 1 and 2", subject.toFLines(), subject.summaryHtml("Before: labels 1 and 2", maxNodes = 6))

// One step, so the commuting branch can be shown on its own.
val branch = reducer.stepDetailed(subject)!!
subject.relax(24)
val middle = stage("After fan-fan", subject.toFLines(), subject.summaryHtml("After fan-fan", maxNodes = 8))

// The rest of the way. This is the part a single stepDetailed cannot reach.
val rest = reducer.reduceDetailed(subject, maxSteps = 32)
subject.relax(28)
val after =
    stage("Fixed point", subject.toFLines(), subject.summaryHtml("Fixed point after $rest more steps", maxNodes = 8))

showInteractionStages(
    before,
    middle,
    after,
    cards = [branch.summaryHtml("fan-fan, commuting branch")],
    channel = "overview",
    graphicTitle = "Two fans, one commute, four duplications",
    stageWidth = 296.0,
    gap = 48.0,
    padding = 22.0,
)

println("interaction multi-step ready: 1 + $rest reactions, ${subject.nodes.size} agents left")

Reference

Building and wiring, inside net { }:

Reducing:

Looking at it:

λ-terms:

Lambda.duplicatedConstantDemo() and Lambda.eraseApplicationDemo() build the nets used in the duplication and erasure examples above.

See also: A λ-term you can hear, Petri nets.

The public declarations used on this page are listed, with their KDoc, in the codebase reference: interactionnets.kt. To normalise terms, draw a reduction and check the reducer against an ordinary evaluator in Field, open the interaction_nets_lambda starting point.