From tree calculus to TC-Net

disp's evaluator has a spec — five rewrite rules — and several machines that realize it. Two are worth contrasting head-to-head. The eager reducer (the checker's backend) interns every node and memoizes every application: it shares aggressively and equality is a pointer compare. The TC-Net reducer (the optimizer's substrate) does the opposite — it turns the whole computation into a graph of little machine-nodes and rewrites them locally, sharing nothing by default.

The surprise, which this page builds toward with real numbers: the net is not a speedup. On raw reduction it loses to the eager reducer by 20–550×. You materialize it anyway, on purpose, to buy two things hash-consing structurally cannot give you. Getting to why is the whole journey.

Act 0 · the specificationTree calculus and its five rules

Tree calculus has one symbol, △, and binary application. Every value is a tree built from three shapes, distinguished only by how many arguments △ has so far received:

A leaf is bare △; a stem is △a (one child); a fork is △a b (two children). Leaves, stems, and forks are values — they sit still. Computation happens only when a fork receives a third argument.

At that moment one of five rules fires. The first two (K and S) are Turing-completeness; the last three (triage) are what lets a program branch on the shape of any value — including another program. That is self-reflection, and it falls out for free with no quotation or Gödel numbering.

△ △ y z          ⟶  y              — K   (return the first branch)
△ (△x) y z       ⟶  x z (y z)      — S   (the only rule that DUPLICATES)
△ (△w x) y △     ⟶  w              — triage: arg is a leaf
△ (△w x) y (△u)  ⟶  x u            — triage: arg is a stem
△ (△w x) y (△u v)⟶  y u v          — triage: arg is a fork

That is the entire semantics. Everything below is a machine that applies these rules — the rules never change. Here is "regular" tree-calculus evaluation: an application tree, with the next redex highlighted. Step it.

Act 1 · machine oneThe eager reducer: sharing and memo

The reducer that the type-checker actually runs (src/core/tree.ts, and its Rust twin rust-eager) makes two moves that the plain rewriter above does not. Both are about not doing the same work twice.

Move 1 — hash-consing: identical trees are one node

Every node is interned in a table keyed by (tag, child-ids). Build stem(leaf) twice and you get back the same object the second time. A term is therefore not a tree but a DAG: repeated subterms are pointers to one shared node. Two consequences fall out immediately — memory is collapsed, and equality becomes O(1): two terms are equal iff they are the same pointer. That O(1) conversion check (tree_eq) is the single most load-bearing fact in the type checker.

Move 2 — memoization: applications are cached

Reduction is a function apply(f, x). Its result is cached in a table keyed by the pointer identities (f.id, x.id) — which only works because of hash-consing. Apply the same function to the same (interned) argument again and you pay nothing. This is cross-occurrence sharing of work, not just structure.

Act 2 · machine twoMaterialize it: the interaction net

An interaction net is a graph of agents. Each agent has one principal port and some auxiliary ports. When two agents meet principal-to-principal, that is an active pair (a redex), and a local rule rewrites just those two agents and their immediate wires. Nothing else in the graph is touched. TC-Net realizes tree calculus with ten agent kinds:

The four producers (L, S, F, P) are the data — trees and not-yet-evaluated applications. The six consumers are the verbs: they ask things of a producer's root. Evaluation is just consumers eating producers. A P node is the crucial one — it is a suspended f a with its own principal root, so it can be demanded, duplicated, or erased like any value. That "rooting" is the one repair that makes the whole thing work.

Watch not true reduce as a net. Each step pops one active pair and applies its rule. The focused view shows the rule firing in close-up (locality); the overview shows the whole graph growing and shrinking.

Two things to notice in the counters. First, erasure is real work: when the K and triage rules throw away a branch, an ε agent has to walk in and delete it, interaction by interaction. The eager reducer just stops pointing at it. Second, the totals are much larger than the eager reducer's handful of steps for the same answer — the net is paying, in allocations and interactions, for the privilege of having made every operation an explicit object. Hold that thought for Act 6.

Act 3 · sharing, on purposeTwo duplicators: δˢ vs δⁿ

The eager reducer shares for free (that is hash-consing). A materialized net has to share by doing something — and there are two ways, which differ only in what happens when a duplicator meets a suspended computation P.

Here is the spec's own worked case: a suspended not true that the S-rule duplicates into two strict positions. Flip the duplicator species and watch the cost move.

Act 4 · the payoffWhy materialize at all: parallelism & provenance

If the net is slower (Act 2) and you had to add work to recover the sharing the eager reducer got for free (Act 3), why build it? Two reasons, and both are things hash-consing structurally cannot do.

Reason 1 — parallelism

Recall strong confluence: distinct active pairs share no agents (each agent has exactly one principal port, so it is in at most one redex). Therefore every active pair in the bag can fire at the same time, and the order never changes the answer. The eager reducer's call stack is inherently sequential; the net's work-bag is a pool of independent jobs.

Below, N independent not true computations share one net. A round fires all currently-active pairs at once; rounds ≈ span (critical-path length) and interactions ≈ work (total). Slide the worker count and watch work spread across rounds.

Reason 2 — provenance (the real reason)

This is the one that actually justifies the machine. The verified optimizer (disp's north star) searches for a better program and must attribute blame — "which candidate subterm caused this?" Hash-consing is fatal to that: it merges two distinct-but-equal subterms into one node. Wonderful for a checker; catastrophic for blame attribution, because once merged you can no longer tell the candidates apart. The materialized net keeps distinct-but-equal subnets distinct. Abandoning sharing is not a regression here — it is a prerequisite.

candidate A ─┐
             ├─▶ one node   blame: ???
candidate B ─┘

candidate A ─▶ subnet A   blame: A
candidate B ─▶ subnet B   blame: B

A third use builds on the same property: superposition — packing n^k candidate programs into one shared net and reducing them all at once. That is the optimizer's search engine, and it needs exactly this non-merging substrate. (Its soundness is still open research — δ must distribute over superposition — but the substrate it requires is precisely this one.)

Act 5 · under the floorboardsThe memory backend

So far "agent," "wire," and "the bag" have been abstract. Here is how the real Rust crate stores them — and why each choice is forced by the goals above. This section is a diagram, not a live sim: the operations below are 64-bit atomics on a flat arena, and faking that in JavaScript would only mislead.

The arena, not a heap of objects

• A port is one tagged machine word — [tag : 4 bits | address : 28]. The tag is the agent kind, and it is carried in the referencing port ("kind-in-pointer"). So an active pair is two words that name both interacting kinds with zero memory loads: the rule dispatcher reads two 4-bit tags out of one 64-bit redex and jumps.
• A node is a uniform fixed-width cell of auxiliary ports; the principal port is implicit — it is whichever slot references the node. No per-node header, no discriminant to load. Producers (≤2 aux) are one 2-slot cell; the wide dispatch agents T₁/T₂ are a contiguous block, read per-slot.
• There is no global intern table. That table was hash-consing. Dropping it is what makes Act 4 possible — sharing is now expressed by wires and duplication by an explicit δ wave — and it is also the single biggest parallel-allocation win, because alloc no longer touches global shared state.

The linker: one atomic exchange, never a lock

The crown jewel, and it is agent-agnostic. To connect a wire you do one unconditional atomic_exchange (a swap) into a variable slot — never a compare-and-swap, never a lock:

fn link(neg, pos):
    if pos is not a Var:            // two principals → active pair
        bag.push(neg, pos)          // redex DETECTED at link time, never scanned
    else:
        prev = swap(slot[pos], neg)    // the ONE atomic op
        if prev == EMPTY: return    // we deposited our half; partner will find it
        else: relink(prev)          // raced: take partner's half, retry

It is race-free with no lock because every variable occurs exactly twice: the second linker to reach a slot atomically swaps out the first's deposited half and wins ownership. And we only ever need memory safety here — never result determinism — because strong confluence already guarantees the answer. The two nodes of a popped redex are exclusively owned by the firing worker (each had its single principal there), so it overwrites and reuses them in place; only links into far variable slots touch the atomic.

Garbage collection: the net is linear

A subtlety lazy interaction nets are infamous for: a parked δⁿ whose two copies are both discarded becomes unreachable (ε acts at principal ports; the parked duplicator hides on an auxiliary wire). The design's answer leans on structure:

• The net is a DAG — recursion is a tree that unfolds, never a graph cycle — so reference counting is complete; no cycle collector is ever needed.
• In the eager schedule it is even simpler: an interaction net is linear (each agent is consumed exactly once), so reclamation is just "free both agents of every active pair as it fires." Peak memory then tracks the live working set — in the real crate this took a fib(8) run from 7.6M nodes down to 64K (~119×). That is not an optimization; without it the net OOMs on anything real.

Act 6 · the verdictThe honest scorecard

Now the payoff of all the honesty. You have seen the net pay in interactions (Act 2), seen it claw back sharing only by adding machinery (Act 3), and seen what it buys (Act 4). Here is what the real crate measures when you race it against rust-eager on actual programs.

The scheduler journey (a cautionary tale)

Making the parallel net actually go faster than its own single thread was not free either. The first parallel version was a 7× regression: per-interaction global atomics (a budget decrement, an interaction counter, an in-flight RMW — on every interaction) plus one shared work-queue meant cache-line ping-pong between cores serialized faster than parallelism recovered. The fix was to get coordination off the hot path entirely:

Measured on a 6-core Ryzen, 8 threads vs 1. Budget leasing → per-worker work-stealing deques (kill the shared queue) → per-worker bump-allocation regions. Net result: from a ~7× regression to a ~2.4× speedup — but it plateaus at ~6 cores because the materialized net is memory-bandwidth bound, and even at full tilt still trails rust-eager-native ~1.5–1.7×.

So when do you reach for which?

The arc in one line: hash-consing collapses the interaction net into a fast sequential reducer by sharing structure and work; materializing the net un-collapses it, paying in speed to regain the two things that collapse destroyed — parallelism and provenance. Neither machine is "better." They sit at opposite ends of one design axis, and disp keeps both because the checker and the optimizer want opposite things.

Sources, all in this repo: the calculus and its rule tables — research/interaction-combinator/tc-net.typ · the materialized machine, linker, GC, and all measured numbers — research/interaction-combinator/RUST_IC_NET_DESIGN.md · the backend map and the differential-oracle discipline — EVALUATOR.md · the eager reducer this page reimplements — src/core/tree.ts · why the optimizer needs provenance — research/OPTIMIZER.md. The two reduction engines on this page were validated against each other before shipping, using the project's own differential method.