Not Every Cut Is an Aperture

The previous chapter built a tower and indexed it by ordinals, which is how anyone first gets the intuition and is not how the thing actually works. Turing’s construction relativises a machine to an oracle, takes the halting problem of the relativised machine as the next oracle, and iterates; the index is an ordinal because the construction is a sequence. But an ordinal is a chain, and there is no reason the capacities that separate one computational system from another should be linearly ordered. This chapter and the next replace the chain with what is underneath it, and the replacement begins by asking a question the tower never had to face: where in a computation does the extra power actually get spent?

The answer proposed here is that it is spent resolving races, and that this is not a metaphor. When two sends contend for one receive, something must pick. That picking is a choice function for a definite family, the assertion that a complete schedule exists is an instance of the axiom of choice, and the strength of the choice principle required is graded — free when the contention is finite, countable or dependent choice at one \(\omega\), full choice only for class-sized families. So the oracle was never something to bolt on. In any calculus where interaction is primitive and confluence fails, the oracle is already present at every cut, wearing the name “scheduler.”

What follows is the instrument. It is deliberately mechanical: what a cut is, why the nondeterminism belongs to the cut rather than to either of the processes flanking it, what an interior has to satisfy to carry no observable choice at all, and where the boundary of such an interior falls. The next chapter turns the instrument on the question of where an agent’s boundary goes. Read in that order the machinery arrives before the thesis it supports, which is the right way round even though the thesis is the more interesting half.

59.1 Interaction, and why non-confluence is the point

Among the objects of \(\mathbf{GSLT}\), one class is built for our question. The mobile process calculi (MPCs) — Milner’s \(\pi\)-calculus and, in the form we use, the reflective higher-order (rho) calculus [40] — take a definite philosophical stance: all computation arises from interaction among agents [84]. There is no lone machine grinding a tape; there are processes that meet, exchange, and continue, and computation is what happens at their meetings. We write the meeting as a parallel composition, the cut: \[P \Par Q,\] and the single base reaction is communication across it, \[\inn{y}{x}{P} \Par \out{z}{Q} \reduces P\{@Q/y\} \qquad (x \equiv_N z),\] an input on a channel meeting a matching output. Agents flank every cut; the cut is where they act on one another.

The feature that makes the MPCs the right tool — and that distinguishes them sharply from the \(\lambda\)-calculus — is that they are fundamentally non-confluent. When several outputs and several inputs collect on the same channel, which output meets which input is not determined by the terms; it is a real choice, and different resolutions lead to genuinely different, non-reconvergent futures. This is usually presented as a complication. We present it as the entire point, because non-confluence is the computational signature of a race, and races are how agency shows up in the world. Consider, across four scales:

• two sodium atoms competing to donate their electron to one chlorine;

• two sperm racing to fertilise one egg;

• two predators converging on a single prey;

• two buyers reaching for the last concert ticket.

Each is, structurally, one consume-slot (the chlorine, the egg, the prey, the ticket) contended by several produce-candidates, resolved by a pairing that the situation does not fix, with the unmatched candidates left over. Each outcome matters: this sodium and not that one is now bound; this sperm and not that one founds the lineage. A confluent model cannot speak of these, not because it lacks the vocabulary but because confluence is precisely the claim that the choice does not matter — that all resolutions reconverge. The \(\lambda\)-calculus, the great confluent model, is the stakes-free corner of the landscape: its many reduction orders are real choices whose outcomes are identified by Church–Rosser, so the choice is free and invisible. Reality is mostly not like that. To talk about agency one needs a model in which the choice can matter, and the MPCs are the objects of \(\mathbf{GSLT}\) in which it does. This is the first crossing of our two axes: biology (the race for the egg) tells us which computational models are adequate to agency, and the answer is the non-confluent ones.

The rho calculus, specifically.

We use the rho calculus because its names are quoted processes — \(@P\) turns a process into a name, \(\deref x\) turns a name back into a process, and \(\deref @P \equiv P\) — so there are no primitive names and no name-restriction operator; reflection furnishes recursion with no primitive replication [40]. Nothing below turns on the set-theoretic models of [75, 78]; we draw only on the shape of the calculus. The reader may keep the modern surface syntax in view: \(@P\) for quote, \(\deref x\) for dereference, \(\inn{y}{x}{P}\) for input, \(\out{x}{Q}\) for output, \(\Par\) for the cut, \(\rcong\) for structural congruence, \(\bisim\) for context bisimilarity (the behavioral, congruence-by-construction equivalence) and \(\rbisim\) for resource bisimilarity (the finer equivalence that counts parallel copies).

59.2 RSpace: the bridge, and where the choice is

The MPCs are admirable for reasoning and awkward to run. RSpace is the abstraction that closes the gap: it presents the parallel fragment of the rho calculus as a store — a hashtable from channels to polarity-homogeneous bags, either of data (produces) or of continuations (consumes) — and interprets the cut as keyed multiset union, so the denotation \(\sem{-}\) is a monoid homomorphism and the structural laws of \(\Par\) become literal equalities of tables [75]. This is not a toy: it is how the calculus is compiled into a high-performance, persistent, content-addressed store in production. We invoke it here for one reason: it makes the choice of §59.1 visible and operational.

When a channel carries both a bag of consumes and a bag of produces, communication chooses an underlying list of each and zips them — matching pairs react, unmatched payloads remain as surplus at the channel. The denotation stays a function; the zip is the separate dynamics; and the choice of which list orderings to zip is the calculus’s nondeterminism, now pinned to a key. The four races of §59.1 are this forgiving zip with surplus, drawn from life: several candidates, one slot, a pairing the data does not fix, leftovers remaining. RSpace’s contribution to the present inquiry is to show that the nondeterminism is not a haze over the system but a specific, locatable act of selection — and an act of selection is a choice, in the sense the next section makes exact.

59.3 Choice as a computational resource

Begin with the one feature of the RSpace example we will actually use. When a channel carries both a bag of consumes \(\{\!|(y_1)P_1,\dots,(y_n)P_n|\!\}\) and a bag of produces \(\{\!|Q_1,\dots,Q_m|\!\}\), communication chooses an underlying list of each and zips them, keeping unmatched payloads as surplus. The choice of list orderings is the nondeterminism of the calculus — which send meets which receive — now localized at the key. The denotation itself remains a function; reaction is the separate dynamics; and the indeterminacy is exactly the choice of pairing.

That is not a metaphor for choice. It is a choice function, for a specific family. Index by the cuts that carry mixed polarity (or, for a run, by the reaction events); at each such index the fiber is the set of admissible pairings, inhabited precisely when a redex is present. A completed schedule is a section of this family — an element of the product of the fibers — and the assertion that such a section exists is an instance of the axiom of choice. The scheduler is the choice function for the pairing family, not by analogy but by construction. This gives the practical reframing we want: choice is a computational resource, the resource of nondeterminism, and different ways of supplying it import different amounts of computational power.

The resource is graded by the same \(\omega\) the risk ledger charges.

The strength of the choice principle one must invoke is not uniform; it tracks the infinitude of the family.

• Finite bags, finite run. The index set is finite, the product is inhabited with no choice axiom at all (constructively, in \(\mathrm{IZF}\)). More than that: a bag is a parallel composition of finitely many prefixes, so it arrives presented as a list-up-to-permutation. The term hands you the enumeration; picking a linearization is constructively free. The term is its own choice structure.

• One \(\omega\). Replication and reflection install an \(\omega\)-fold bag, or a non-terminating run yields an \(\omega\)-sequence of events. Now one needs countable choice for the static store, or — for a run whose pairings depend on the residuals of the previous step — Dependent Choice. The cascade of a deep cut unpacking into a deeper cut [76] is exactly a dependent-choice sequence. This is the single \(\omega\) — the “black infinity” — the risk ledger of [75] already spends; choice-as-resource and the \(\omega\)-meter are the same gauge.

• Class-sized. Full \(\mathrm{AC}\), and only here.

So the slogan “choice is not non-constructive” is exactly true in the finite fragment and relocated, not dissolved, above it. The constructive escape at \(\omega\) is to never form the completed schedule: take each pairing locally, on demand, as a decidable step, replacing the choice function (whose bare existence needs \(\mathrm{DC}\) or \(\mathrm{AC}\)) with a choice process. That is what lazy, on-demand reaction does operationally; it keeps choice potential rather than actual. The honest reading is of a piece with the rest of the program: recursion relocated from anti-foundation into reflection, congruence from an afterthought into the context labels, and now choice from a metatheoretic existence axiom into an operationally consumed resource.

A lattice, not a tower.

The natural home for “choice as a resource” already exists: the Weihrauch lattice of Brattka, Gherardi and Pauly [79], whose objects are choice principles ordered by uniform reducibility, with demonic binary choice appearing as the lesser-limited-principle-of-omniscience and composition \(\star\) modeling “use one resource, then another.” The decisive structural fact, for our purposes, is that the Weihrauch degrees form a lattice with rich algebra, not a linear hierarchy. We will return to this: the intuition that a universe of computational agents is “of all stripes, not neatly sorted by a tower of oracles” is, formally, the statement that the relevant degree structure is a lattice and not an ordinal chain.

59.4 Apertures, and why the cut owns them

Two notions first, since everything after this turns on them.

It is tempting to summarize §59.3 by saying that an agent’s nondeterminism budget is its interface to the rest of the universe: a fully deterministic process is sealed, with every slot filled by its own transition function and nowhere for anything external to write; a nondeterministic agent is open precisely at its choice points. There is a true idea here — under-determination is the aperture — but the locus is wrong, and the parallel-composition algebra is what makes it wrong.

Nondeterminism is not preserved by \(\Par\) in either direction. A whole that is deterministic can decompose into parts each wildly underdetermined at its internal cuts; and parts each internally rigid can compose into a whole whose only indeterminacy is at the boundary between them. The aperture is therefore a property of the cut, not of either agent at it, and — this is the consequence that matters — which cut one privileges as “the agent boundary” is a modeling choice. Different observers draw it at different depths of the same term, and the interior lights up or goes dark accordingly.

In the path reading of [76], where keys are routes through a trie and the prefix order gives one channel a subspace of another, the modeling freedom becomes literal: a choice of agent boundary is a choice of prefix, and the trie is the lattice of possible boundaries. A coarse boundary is a short prefix, near the root, folding everything below into one sub-store and exposing only a shallow aperture; a fine boundary is a long prefix, exposing apertures at every internal branch. These are not rival claims about where the boundary “really” is. They are different truncation depths on one structure, ordered by the prefix order, which is precisely the order “coarser agent / finer agent.” The In-deep rule of [76] — a reaction at a shallow cut unpacking a cut that lives deeper than the boundary-drawer was tracking — is what it looks like when the same dynamics is read at two depths at once.

59.5 The macro-component: confluence, not linearity

We want a name for the object Smith’s interior instantiates: a sub-term all of whose internal cuts are sealed, with apertures only at its boundary. The first guess is that the interior is sealed by rigidity — that at every internal key the consume-bag and produce-bag admit a unique compatible pairing, so that the forgiving zip is a function and there is no race to resolve. Determinism not by scheduling but by there being nothing to schedule. Syntactically this is a linearity condition: every internal channel is used at multiplicity one per polarity, each consume a linear hypothesis discharged by exactly one produce, the boundary the residue of the non-linear, contended channels. On this reading EnergyEaters are exactly the non-linear channels — the ones contended by many consumers, the sun feeding everyone — and the factorization is linear interior, non-linear boundary.

Linearity is, however, too strong. It is a syntactic sufficient condition for what we actually care about, which is that the interior have no observable choice. The semantic statement of exactly that, and nothing more, is confluence.

Confluence permits the branching that linearity forbids. The bee may have several internally admissible pairings; if they all flow to \(\rbisim\)-equal normal forms, the bee is still not a site of observable choice, which is all the factorization needs. Metabolism is full of internal branching — parallel pathways, redundant enzymes, order-independent cascades — that converges on the same steady state: confluent, not linear. So the right slogan is the interior is \(\lambda\)-like, not linear-like.

\(\lambda\) is really deterministic.

The \(\lambda\)-calculus is the load-bearing witness, not an aside. Operationally it is radically nondeterministic: a term with many redexes has many reduction sequences, every interleaving a distinct branch. And it is the paradigm of determinism — because Church–Rosser says the branching is fictional: one normal form, reached however you like. The choice of redex is real and it is free in the sense of §59.3, semantically free, spent but unobservable, eliminated by the quotient to the normal form. \(\beta\)-reduction is the cleanest instance in all of computing of a process saturated with races whose races do not matter, and it is deterministic for precisely the reason Definition 59.2 asks of an interior: confluence, not absence of branching. A closed \(\lambda\)-term — no free variables — is then a sealed macro-component at every scale, nothing to interfere with because there is no contended channel for anything to write to. An open term is the agent with an aperture: its free variables are its boundary channels, the spots where a context (a higher agent) can substitute and change the result. In the MPC vocabulary the free variable is the unmatched consume, the dangling polarity — the same object, the port where the universe reaches in.

59.5.1 The islands are small

The picture this forces is not one determinate interior behind one skin. If selection, predation, and competition are non-confluent and pervasive — and §60.2 will grant that they are — then confluent macro-components are small and local: a tightly coupled metabolic or developmental subsystem whose internal branching genuinely reconverges, redundant enzymatic pathways and buffered developmental cascades, bounded by an aperture wherever a real race begins. The biosphere is then a vast field of small confluent islands in a dense sea of races, rather than a single interior. This is less tidy than a clean interface and it is the true shape: apertures are everywhere, the determinate regions are the exception, and “where is the agent?” has many local answers rather than one global one. An ecosystem may be the right scale for some such island — but only the parts of its food web that reconverge up to resource bisimilarity, with its contended predation and its competition for influx counted as apertures at or within it, not as interior. The ecological races are not quarantined behind the boundary; they are the boundary, threaded through.

Here is where two senses of “agent” come apart, and the distinction is the conceptual payoff.

59.6 Three frontiers, one locus

The reward of taking confluence as the criterion is that the boundary of the macro-component coincides with two frontiers we already had names for.

The coincidence is a consistency check on the vocabulary: the place where the interior stops being able to hide its schedule is the place where external interference starts being able to leave a mark, which is the place where the formal confluence obligation bites. One frontier, three readings — confluence-failure from inside, interference-visibility from outside, proof obligation from the meta-theory. That a single locus answers to all three is the kind of agreement that suggests the apparatus is carving at a joint.

It also tells us when interference is a measurement. Where internal reaction is confluent up to \(\rbisim\), a biased pairing picks the trajectory but not the destination; the weak agent is steered to a \(\rbisim\)-equal normal form and cannot tell. Where confluence fails, the bias becomes a different observable outcome. Detectable interference is interference at a non-confluent cut — an interaction that resolves an otherwise-unobservable choice into an observable distinction, which is close to the definition of a measurement. We note, without leaning on it, that the way a weak agent could in principle detect a stronger one is information-theoretic and contextual: its “free” choices would look random relative to its own capacity yet be compressible relative to the higher degree, carrying more mutual information with the oracle than chance allows — local sections admitting no degree-uniform global section, in the sheaf-theoretic sense of contextuality [91]. The probabilistic face is cleaner: a flat jumble is one joint distribution, an agent’s view a marginal, and a strong agent biasing a weak one’s choices is conditioning that marginal on oracle information the weak agent cannot access. We flag these as directions, not results.

59.7 Choice types, and the terms that inhabit an aperture

Everything above treats choice as a quantity: how much of it a cut consumes, where in the Weihrauch lattice that lands. It can be treated as a type instead, and \(\chChs\) does exactly that — a Curry–Howard correspondence in which choice principles are the types and fair schedulers are the terms. Two of its consequences are needed here, ahead of their development.

The first is a reading of the macro-component. At an aperture the obligation is a \(\forall\exists\) statement: for the contended slot, there exists an admissible pairing. That formula is the choice type of the aperture, and a scheduler producing the pairing is a proof of it. A macro-component in the sense of Definition 59.2 is then a region whose choice type is proof-irrelevant: several pairings inhabit it, all normalize to \(\rbisim\)-equal results, so the term carries no observable information. “Capacity lives at the apertures” becomes “the term content lives where the choice type is not proof-irrelevant” — the same claim with a metatheory attached to it.

The second is why the next chapter’s closing question is a question about typing rather than about dynamics. Subject reduction — that running a schedule preserves the type — says operationally that scheduling cannot bootstrap an oracle. Whether it holds is the load-bearing open problem of these chapters, and §60.6 states it in both dresses.