Names Without Names: Combinators and the Matrix Machine

24.1 Status, first

The previous chapter reported on a store that has run in production for years. This one reports on a compiler whose first build passed its test suite in the autumn of 2026, on a software graphics driver, and whose performance has not been measured on a single program anyone wanted to run. The reader is asked to hold that asymmetry in mind throughout, and the chapter will keep saying so, because the argument it makes is of a kind that invites overstatement: it is an argument that a theoretical property of the calculus — reflection, the thing that makes rho rho — is exactly what makes the calculus cheap on hardware the store was not designed for. The argument is sound as far as it goes. How far it goes is a number nobody has yet produced.

Here is the shape of what follows. A name-free combinator calculus for rho exists, and the version of it that was published is broken in an instructive way; repairing it requires adding something the published version lacked, and the repaired calculus compiles rho in linear size where the classical method is exponential. A combinator state is a multiset of fixed-width tuples, so it is a vector; the rewrite rules are a matrix; and the one rule that gives the calculus its computational power is also the one rule that cannot be written down in advance and the one that breaks the matrix’s triangular structure. The feature that makes the theory hard makes the machine cheap: reflection is a lookup table. And the speedup available from running this on an accelerator is the width of the computation and nothing else — a falsifiable thesis that should be tested before anyone builds more hardware than has already been built.

24.2 A calculus with no bound names

Rho has no name-restriction operator: names are quoted processes, and freshness comes from quotation rather than from a binder. It nonetheless has one binder, the input prefix. Yoshida showed how to eliminate the input binder of the asynchronous \(\pi\)-calculus in favor of combinators, at the cost of keeping \(\mathsf{new}\). The combination is suggestive: a calculus with no \(\mathsf{new}\), compiled by a discipline that removes the remaining binder, would be a concurrency calculus with no bound names whatsoever. That is what the rho combinators proposed [288], and the current draft of the work [289] asks whether the proposal works.

The atoms are nine. Six are routers, which move a message without reading it: \(\mathsf{d}(a,b,c)\) duplicates a message at \(a\) to \(b\) and \(c\); \(\mathsf{k}(a)\) kills one; \(\mathsf{fw}(a,b)\) forwards \(a\) to \(b\); \(\mathsf{bl}(a,b)\) and \(\mathsf{br}(a,b)\) bind the received payload as the left or right argument of a new forwarder; and \(\mathsf{sy}(a,b,c)\) synchronizes, emitting a forwarder from \(b\) to \(c\) when a message arrives at \(a\). One is the destructor \(\mathsf{ev}(a)\), which consumes a message at \(a\) and runs its payload. Two carry values: the message \(\mathsf{m}(a,v)\) and the store \(\mathsf{q}(a,p)\), a message that only a forwarder can read. The rules are two-atom rewrites, each a message meeting one router or the destructor at a shared name.

One equation breaks the published calculus.

The published combinators inherit \(*@P \equiv P\) from a presentation in which quote and drop are mutually inverse, and they write the destructor and the drop with the same symbol. In the combinator setting the destructor is not a process former but a guard; and since every name is \(@Q\) for some \(Q\), identifying the guard with the drop makes an arbitrary running process match the guard.

An arbitrary running process can be annihilated and replaced by an arbitrary payload by anyone who knows its quotation. No faithfulness theorem survives this. The repair is to separate the drop from the guard — Figure 24.1 does — which leaves the equation optional; the source gives both presentations.

Reflection was half-implemented, and constructors complete it.

The rule \(\mathsf{ev}(a) \mid \mathsf{m}(a,@P) \rewrite P\) opens a name that arrives at run time. In the published calculus nothing builds one: combinator reduction never produces a name not already present in the redex, hereditarily. Rho reduction does, at every step, because substituting under a quotation turns \(@(*y \mid R)\) into \(@(Q \mid R)\) — a name in neither participant. So the published calculus cannot encode rho at all. The missing operation is the construction of a name from names, and it is supplied by constructors: one for parallel composition, \(\mathsf{cons}_{\mid}\), and one per atom shape, each taking its arguments as messages and emitting the quotation of the term built from them. With constructors there is no name-opaque fragment to restrict to. They are the combinator-level image of the one thing the Pledge said reflection had to do cheaply: let a network of agents be the sort of thing that can be named.

The storage combinator is about opacity, not power.

\(\mathsf{q}(a,p)\), released by a forwarder rather than by a message, adds nothing to expressiveness. What it adds is silence: it is a message that only a redirection can read, which is what stored code and intermediate results of name construction need if the encoding is to be opaque to observers.

Prefix elimination is linear.

Reflection allows a continuation to be quoted once and released by a three-atom gate. Yoshida must instead push the prefix through the body, splitting at every parallel composition and delaying every atom, which costs a constant factor per level of nesting.

That is the first payoff, and it is a theorem [289, Prop. 8.1]: storing a continuation as a name makes compiling away the input binder linear in program size, where the classical method blows up exponentially in nesting depth.

Correctness is full abstraction relative to encoded contexts.

Observation is by context-labeled bisimilarity, with the observer class taken to be the image of the translation on source contexts, and the theorem is that two rho terms are bisimilar iff their images are bisimilar against encoded observers [289, §7]. The restriction to encoded observers is forced rather than convenient — an unrestricted combinator context can see the apparatus — by the same argument that forces it for the encoding of the \(\pi\)-calculus into rho (Chapter 22). The proofs are at the level of sketches; the source says so.

An expressiveness lattice.

Including or excluding combinators gives a lattice of fragments, and three invariants draw it. Without the destructor the calculus is strongly normalizing and so not Turing complete; without constructors it cannot build a name; and the duplicator \(\mathsf{d}\) is conjectured necessary for divergence. The constructor axis is Boolean. Whether the three binders \(\mathsf{bl},\mathsf{br},\mathsf{sy}\) are separable from one another is open. The lattice has two orderings, expressive and observational, and they do not coincide, because the calculus has no hiding. We mention it because the next section will show that the same three invariants are the three finiteness conditions of a matrix.

24.3 States are vectors, rules are a matrix

Everything in this section is over the Booleans or the natural numbers; the weighted and complex readings of Chapter 14 attach to the same operator later and nothing here depends on them. The source is a design analysis [290], and it marks each of its claims as settled, as a route believed to work, as open, or as a gate on the work downstream; we carry the markings.

What a graphics processor rewards.

An accelerator is a bulk-synchronous machine with a very wide, very shallow execution model. It rewards flat, indexable state — arrays of fixed-width records at predictable addresses, pointer chasing being the single most expensive thing one can ask of it; uniform work across lanes — threads that take the same branch; bulk-synchronous phases — one kernel does one thing to everything, then a barrier; and standard sparse primitives — sparse matrix products, segmented scans, sorts and hash tables, which inherit decades of tuning. An RSpace-style interpreter does approximately the opposite of all four. Its state is a store of variably shaped terms reached by pointer; matching is a recursive walk over nested syntax; conflicts are resolved by locks; and the inner loop is a hash lookup followed by unification. None of that is a criticism of RSpace, which is a good design for a general machine. It is an itemized statement of the gap a compiler standing between the two has to close.

Four facts about the repaired combinators do the closing. Atoms are flat: every atom is a head symbol applied to at most \(w\) arguments, \(w\) known at compile time, and every argument is a name — there is no nesting, no binder, no pattern variable. The multiset is complete: the multiset of top-level atoms of a drop-free normal form is a complete invariant for structural congruence. Rules are small and subject-joined: two to \(w\) premises, each a single atom, sharing names. Name equality is decidable and internable: on closed normal forms it is decided by normalization and multiset comparison, and quotation is injective there, so names can be hash-consed to integers once and compared by integer equality thereafter.

This is the first place the combinators pay. In a direct rho machine, matching modulo structural congruence is a recurring cost and a recurring source of subtlety; here it is a property of the data structure. It is also, the reader will notice, Chapter 23’s Proposition 23.1 said a second way: the store made \(\Par\) into multiset union of bags at keys; the matrix machine makes the whole state into one multiset over species, and the keys have become coordinates.

The entries are mass-action counts. A combinator program is, without any choice having been made, a chemical reaction network: species, reactions, and a transfer operator whose entries are the number of ways each reaction can fire. Chapter 14’s multiplicity factor — count redexes by occurrence, or run the system at half rate — is here the definition of the matrix element. The weighted reading attaches at exactly one place, a diagonal factor in each rule’s operator term, which is why the Gillespie reading of that chapter and the matrix machine of this one are one object.

The self-indexing problem.

Species are indexed by names, and names are quoted processes, so by completeness of the multiset they are finite multisets over species. The index set of the basis therefore satisfies \[\mathrm{Nm} \;\cong\; M_{\mathrm{fin}}(\mathrm{Spec}), \qquad \mathrm{Spec} \;=\; \textstyle\coprod_{A} \mathrm{Nm}^{\mathrm{ar}(A)} .\] The basis of the state space indexes itself. This is reflection seen through the linear algebra, and it is the reason no finite matrix can be written down in advance for the full calculus. The solution of the domain equation is the initial algebra: names are finite trees, so the name set is countable, finitely branching, and graded by depth of quotation.

The three invariants the expressiveness lattice was drawn with are, without modification, the three finiteness conditions a matrix representation needs, one per axis of the lattice. That is the source’s main structural observation and it is proved. The corollary the original proposal wanted — that the reduction graph is an upper triangular matrix, so that reachability is a finite Neumann series computed by repeated squaring — holds exactly on the destructor-free fragment. With \(\mathsf{ev}\) the graph can have cycles, because reflection admits terms that step to a structurally congruent copy of themselves, and by Principle 24.1 congruent means equal.

The recommendation that follows is the one the source makes, and it reverses the original proposal. For running a program one needs a frontier, not a closure: the current state and its successors. Triangularity is a property of the whole graph and buys nothing at the frontier; a general sparse non-negative operator applied to a sparse vector is entirely adequate, and iterative methods are indifferent to cycles. The upper triangular matrix is the right object for model checking — or, working in the unfolding, for the history monad’s universal cover, which is acyclic by construction — and the wrong object for execution. Do not ask for it.

24.4 What actually gets multiplied

Not the reduction graph. The object the machine multiplies is the sparse incidence matrix between atom occurrences and names — term-sized, not graph-sized — and three operations on it are the whole of a step. Redex finding is a join: the rules are subject-joined, so the instances of a rule enabled in the current state are found by joining the atom table with itself on the shared name column, which is a sparse product. Conflict detection is a second product: two redexes conflict when they consume a common atom occurrence, and the conflict graph is \(BB^{\top}\) for \(B\) the redex-atom incidence. Independent-set selection is a standard parallel primitive. Each step fires a maximal independent set of redexes, which is one barrier per causal layer — and firing a maximal independent set per step is sound with respect to the interleaving semantics, so that machine steps count causal depth. This is the contention-component structure of Chapter 14 with the components found by linear algebra: the independent-set step is the \(k\)-ary generalization of the contention-set normalization, and the source files reconciling the two as an obligation.

This also explains Proposition 24.2 from the machine side. Yoshida’s elimination must rewrite a continuation to delay it; the reflective encoding stores it as a name and pays for a gate. A machine that stores continuations as integers in a table is doing the same thing, and the \(O(|P|)\) bound is what keeps the state array small enough to be worth the transfer to a device. The intern table is the one place the bulk-synchronous discipline is violated — it is shared mutable state — but both of its operations are commutative and idempotent in effect, so it can be updated by an unordered batch insert per step rather than by locking. Interning order is a gauge freedom: two runs may assign different integers to the same name, the states are equal up to the canonical bijection, and the machine must never let an integer comparison stand in for a semantic distinction between runs.

24.5 What has been measured, and the thesis

A reference implementation accompanies the design note, and its measurements are step counts and widths, not timings. On four synthetic term families with analytically known widths — \(k\) independent forwarder chains of length \(d\); \(c\) messages and \(c\) consumers on one channel; a binary duplicator tree of height \(h\); a construct-then-eval family — the number of parallel steps equals the causal depth exactly and the ratio of sequential to parallel steps equals the width exactly: \(64.00\) for \(64\) chains, \(16.00\) for \(16\) contenders, \(18.14\) for a duplicator tree of height six. The join formulation of redex finding agrees with naive enumeration on \(400\) of \(400\) random states.

Three things are not claimed, and the source says so in its own voice: that any of this beats a well-tuned sequential interpreter on real workloads; that the reduction graph should ever be materialized; that maximal progress is the right resolver rather than a resolver whose cost is an open question. And one thing is marked as the gate on the whole enterprise: the width of the combinator image of a compiled rho program has not been measured. The measurements establish that the construction is correct and that step count is causal depth on families whose depth is known. They establish nothing about real programs, because that measurement requires the compiler, not the machine.

24.6 The compiler, as it stands

The compiler is called Saph1r3. It is a Rust workspace of eight crates, about eight thousand lines, whose front end is the kernel-rho parser and normalizer of the campf1r3 project taken unmodified, and whose pipeline is: parse and normalize; phase one, a homomorphism on the normal form into the combinators extended with a binder; phase two, which eliminates the binder by giving each run-time instance an address and erecting its apparatus under that address with an instantiation combinator; then deployment to a host matrix machine or to a device bundle — a program matrix, kernels generated from the rule table in the WebGPU shading language, and a manifest — targeting Vulkan, Metal or DirectX through a portable layer. The device finds redexes and selects the independent set; the host commits each step; the intern table stays on the host.

Its test suite reports forty-eight passing tests at the time of writing: a hundred-seed regression against a reference reducer on the paper’s own adversarial term and its variants; a nineteen-program corpus covering every occurrence kind, nesting, relays, races and received code with inputs; device traces byte-identical to host traces; address independence; canonicity of the encoding; golden files for the full reduction traces of two programs; an adversarial cross-instance scheduler with zero disagreements over a hundred seeds; and a nesting family on which phase-one atoms grow linearly in depth, which is Proposition 24.2 observed. The device tests were run on a software Vulkan driver. No performance target has been set, let alone met.

The build also found things wrong in the specifications it implements, and reported them. Collapsing the hole indices of nested contexts to a single marker is unsound for nested units — a parent’s instantiation would fill a child’s hole — and de Bruijn indices over context nodes repair it. The specification’s address supply for received code was unstated, and the build closes the gap with one address per release site at a shared static channel. A quoted process containing an input is a unit and must be erected like an input body. These are the ordinary findings of a first implementation, and they are recorded in the repository’s own words as findings for the papers.

24.7 Two realizations of one rule

The store and the matrix machine implement the same COMM rule and agree on what it means, and they disagree about everything else. The store keys the state by channel and finds a redex by looking up a key; the machine flattens the state to species and finds every redex at once by a join. The store resolves a race at a key, under a lock, with a seeded shuffle; the machine resolves every race in a layer at once, by independent-set selection, under maximal progress. The store is a general machine’s realization and runs anything; the machine is an accelerator’s realization and runs what is wide. The store carries reflection as a content-addressed key — a quoted process is its hash; the machine carries it as an intern table — a quoted process is its integer. And the store knows the two messages at \(a\) are two because it keeps a bag; the machine knows it because the matrix element is \(2\).

Which is to say that the resource layer of Chapter 23 — the layer the behavioral layer forgets, the layer that keeps counts and keys — is the layer both machines live in, and that they are two coordinate systems on it. A reader who has followed the book’s habit of asking what a construction prices will want to know what the change of coordinates costs and buys. That is the next chapter.