Inhabiting Choice

The two preceding chapters read a century of models of computation for what they stipulated about the agents who would run them, and found that the present culture has built a metalevel constituted entirely as an instrument of its operator, with no path to recursive self-improvement in it that does not pass through a person closing every turn of the loop. That was a finding about a community. This chapter makes the finding about a mathematical object, states it once, and then says it three times — once abstractly, once for the verification of software, once for intelligence — because the book’s rule is that readers need to be told things more than once and because the three tellings are what make it a finding rather than a complaint. Then it does what the two chapters before it could not: it points at the construct, already built in the Turn, that discharges the obligation the finding leaves.

Here is the observation.

The consequence that matters is for identity. Whatever notion of “same proof” such a system adopts, it is computed from a confluent dynamics, and on a confluent dynamics the distinction between branching-time and linear-time equivalences does not exist. The identity is linear-time whether or not anyone chose it to be, and the logic adequate for it cannot distinguish two witnesses by when a choice was made, because no witness ever makes one. i follow the working note in which this was first set out [291], and i have kept its caution where it was cautious.

76.1 Abstractly

Let \(W\) be an interactive GSLT in the sense of Part Part I: a signature, an equational theory, and rewrite rules whose left-hand sides are cuts, with the context-labeled transition system of Chapter 18 over it. Write \(\approx_W\) for weak context-labeled bisimilarity on \(W\) and \(\simeq_W\) for weak trace equivalence.

Confluence alone does not give inertness, but for the \(\lambda\)-calculus the two come together: Church–Rosser supplies confluence, and standardization supplies inertness, since an application to a fresh argument commutes with internal \(\beta\)-steps up to further internal steps. That standardization delivers inertness in the labeled setting is, the source says plainly, the one step in this chapter it has not written out.

So the proof identity of a system whose witnesses are \(\lambda\)-terms is forced to be \(\beta\eta\) on the proof-assistant fragment and forced to be linear-time everywhere. It was never a choice. (An earlier note in this series said bisimulation on the \(\lambda\)-fragment was coarser than \(\beta\eta\); the corollary corrects it, and i record the correction rather than hide it.)

The pair is the textbook pair. Its interest here is what it says about witnesses. Read \(P\) and \(Q\) as proof-processes of a proposition whose discharge involves choosing between lemma \(b\) and lemma \(c\): \(P\) keeps both options open past the first obligation, \(Q\) commits before it. They are the same proof under any linear-time identity and different proofs under bisimulation, and the difference is exactly when the choice was made. No \(\lambda\)-term can be either of them.

The generated logic makes the blindness visible: on a determinate \(W\) the modalities carry no information beyond the trace they name, and the connective that distinguishes \(P\) from \(Q\) has nothing to distinguish. The adequate formulae for \(\lambda\)-witnesses are a degenerate fragment of the adequate formulae for rho-witnesses.

One level up.

Ordinary context-labeled bisimulation satisfies the expansion law — \(a \mid b\) is bisimilar to the race between \(a.b\) and \(b.a\) — so a rho-witnessed system with that identity inhabits branching but not causal independence, which is Observation 76.1 transposed one level. The remedy is a matter of presentation: adding the synchronous rule that fires two independent reductions as one step makes the identity a step bisimulation and the expansion law false. Step bisimulation records simultaneity and not dependence; for dependence rho has the unusual resource that a reduction creates at most one name, in a substitution-transparent position, so the quote structure of a name is a provenance record. Chapter 13 is where that resource lives.

The price.

\(\beta\eta\) on strongly normalizing typed terms is decidable; bisimilarity on a Turing-complete reflective calculus is not. The collapse of Proposition 76.1 is what buys a proof assistant its decidable proof identity and its cheap checking, and for propositions that are static — inhabitation, arithmetic — it loses nothing, because there is nothing behavioral to lose. The observation bites exactly where the propositions are about behavior: there a confluent witness cannot carry the branching structure that is the content of the proof, and the identity it imposes equates proofs that differ in the one respect the proposition is about. This is a price, and so it belongs in the list Chapter 77 gathers: decidability was bought with the spectrum.

76.2 For the verification of software

It is important not to overstate the case, and the source does not. Lean, Coq and Isabelle verify non-confluent systems routinely. Iris proves linearizability and race-freedom of fine-grained concurrent data structures [292]; CertiKOS certifies a concurrent operating-system kernel, scheduler included, down to assembly, through a stack of certified abstraction layers and a concurrency-aware compiler whose correctness proof is itself a Coq term [293]. A ticket-reservation system’s “no double booking under any interleaving” is a universally quantified statement over a transition relation, and its proof is a \(\lambda\)-term doing induction on reachable states with an invariant. Nothing in Section 76.1 prevents this: the non-confluence is stated, as an inductive relation, and the proof is about the relation.

So the claim is not that such systems cannot be verified with \(\lambda\)-term witnesses. It is a claim about what the certificate is a certificate of, and about which part of the trusted base can be examined.

Every such development begins by stipulating a model of the non-determinism: the interleaving semantics, the scheduler, the memory model, entered as a definition of which executions exist. The proof quantifies over that definition. The faithfulness of the definition to the machine is not a theorem anywhere; it is the trusted base, as the instruction-set model is the trusted base of a sequential verification. The asymmetry between the two cases is the point.

The trust is therefore not merely unproven; it is unexaminable by any means the prover possesses. That last qualification matters and i keep it: practitioners do audit concurrency models from outside, by litmus tests against hardware, and the observation says only that the instrument that does so is not in the prover.

Two consequences follow, both visible in the heroic projects. First, cost: the certificate is a term checked once and discarded, the running system is a different object produced by extraction, and at every refinement layer the branching structure the witness cannot carry is re-encoded by hand as a relation and the refinement re-proved as a term about two relations. CertiKOS reaches the bottom of its stack at a cost proportional to exactly the structure its proof objects cannot inhabit, and the next concurrent system starts over. Second, deployment: a \(\lambda\)-proof cannot be run against the system it certifies. A rho-witnessed proof with pending obligations is a process — under the reading of an obligation as a pending communication, it is a runtime monitor — and on a runtime that is the calculus, context-labeled bisimulation quantifies over the environments the system will actually meet, because the contexts are rho processes. The model/implementation gap does not vanish; it moves, from “this model is faithful to the machine” (per system, unauditable) to “this implementation is faithful to the calculus” (once, for the platform). That is what verified compilation did for sequential code. Process witnesses would do it for concurrent code by construction.

True concurrency widens the gap.

Interleaving is a defensible projection on one core. On multicore hardware it is false, and the field models weak memory axiomatically as partial orders on events [294], because interleaving cannot express the reorderings the hardware permits. The trusted base is then a partial-order model, and the unauditability sharpens: its faithfulness is a property of an independence relation, two levels above anything a confluent witness can inhabit. And the runtime of Part Part II is itself a partial-order system — a block DAG merging independent deploys by conflict detection (Chapter 23) — so a verification on that runtime whose identity is interleaving bisimulation under-specifies the system it runs on. For the ticket system the difference is concrete: two reservations on disjoint seats should commute, an interleaving proof reaches that fact only through a linearizability argument that re-derives commutation from outside, and a step-concurrent witness has the commutation as a single step.

76.3 For intelligence

The value proposition of the present culture is that the salient aspects of intelligence are software, and in its dominant form, that they are what one obtains by predicting traces at scale. Proposition 76.2 has a direct consequence for that form.

The proposition is almost trivial and its consequence is not. A next-token predictor trained on a corpus of completed runs, however large, represents the trace distribution and nothing more. The question “was the die cast before or after \(a\)?” has no answer in the data. The limitation is not architectural; it is information-theoretic. Branching-time structure is invisible to any observer that does not act.

To learn branching structure one has to intervene: place the system in a state, supply a context, and observe what it can still do. That is the context-labeled bisimulation game read as an epistemology, and the mortal scientist of Chapter 26 is its agent. Bisimulation is the equivalence an experimenter can learn; trace equivalence is what a spectator gets. Chapter 15 introduced Pearl’s ladder and observed that it is a statement about time — association is what a trace shows, intervention is what an experimenter can learn, counterfactual is replay — and was careful to call the alignment an observation. It is now a theorem on the first two rungs: rung one is Proposition 76.3, rung two is Proposition 76.2 with the experimenter supplying the context, and the \(\dok\) of Chapter 15 is the experimenter’s instrument.

Where the present stack sits.

The indictment is specific and should be aimed carefully. Next-token prediction on observational text is rung one by construction. Reinforcement learning is not: a Markov decision process is a branching-time object, bisimulation for such processes is an established tool [296], and an agent trained by reward learns by intervening. Post-training a language model with outcome rewards is the community purchasing rung-two data for a rung-one model, which is evidence that the limitation is felt. But reinforcement learning stops one rung short of nature. A decision process has a global clock: the world steps in lockstep. The world does not. The races of the natural world — which sperm fertilizes the egg, which antelope the pride culls, which flower the bee reaches — are truly concurrent, and an agent that models them as interleaved under a global tick attributes dependence where there is only coincidence.

Nature exploits races as races.

The examples must be of the right kind. Sensitivity to who won a race is observation of an outcome, rung one. The claim requires organisms sensitive to the race as a race — that it could go otherwise, and that one can act on the branching — and the ethological literature supplies them. Prey move unpredictably in order to defeat a predator’s predictive model [297]; the strategy makes sense only against an opponent reasoning in branching time, and works only if the prey can generate genuine branching. Every mixed evolutionarily stable strategy [298] is a population exploiting the fact that the opponent must model a choice, not a trace. Bet-hedging produces offspring carrying non-confluent strategies so that whichever environment arrives some win [299]: pursue both branches, keep what succeeds. The lion that drives the herd to create a race it can win is doing rung-two work; the lion that eats the slowest is doing rung one. The first is intelligence; the second is a filter.

Witnesses, again.

An agent’s knowledge is its hypotheses and plans — in the setting of Chapter 26, its clauses. Bet-hedging is a plan that is itself a race: pursue two branches in parallel and commit to whichever lands. That plan is a non-confluent witness. A confluent plan cannot be it; it can describe it from outside and hand it to a scheduler, which is the orchestration-outside-the-dynamics of the proof-search setting reappearing as a limit on cognition. So the requirement on a software rendering of intelligence is not only that it discriminate branching phenomena but that its internal representations inhabit them: an intelligence whose hypotheses are confluent can observe hedging but cannot hedge in its hypotheses. This is what Chapter 26 meant, three hundred pages ago, by taking the hypothesis to be a clause on a receipt rather than a formula in a database. A clause is a term; a term can be a race; a hypothesis that is a race is a hedge.

76.3.1 The smallest behavior, and the program that settles it

It is worth saying how small the stymieing instance is, because the smallness is the argument’s strength. Milner’s vending machines [84], \[P \;=\; \mathit{coin}.(\mathit{tea} + \mathit{coffee}) \qquad\qquad Q \;=\; \mathit{coin}.\mathit{tea} + \mathit{coin}.\mathit{coffee},\] are the pair of Proposition 76.2 with three actions. Every completed session of either is \(\mathit{coin}\;\mathit{tea}\) or \(\mathit{coin}\;\mathit{coffee}\), at identical frequencies if \(Q\) flips the coin its customer would. The observable a trace-trained learner cannot recover is a refusal: coin in, tea requested, nothing out. \(Q\) can refuse tea after a coin; \(P\) cannot; and a refusal never appears in a log of completed runs, because a log records what happened and not what could not have happened. Text records what was said, never what could not have been said.

The test is correspondingly small. Generate sessions from one of the two machines chosen by a hidden coin; record completed actions only; train, or prompt in context; ask whether, after a coin, the machine can refuse tea. Chance performance is forced rather than likely, since the two training distributions are one distribution. The remedy is equally small: let the learner try. One attempted tea after one coin, met with a refusal, settles the question, and no quantity of further logs can substitute for it. Two fairness remarks the source makes and i keep: a learner handed the term \(Q\) in its prompt answers correctly, since the stymie is for learning from observation and not for reasoning about a description; and logs that record failed attempts make the refusal a trace symbol and the distinction learnable, but such logs are intervention data in disguise, which is the point rather than a loophole.

And now the discharge. Chapter 15 built the instrument, and the test is one line in it. Render the machines with races in the usual way, with \(y\) the variable bound at the drink-selecting receipt. Then \[\dok(y = \mathit{tea})\ \ink\ (\mathit{coin}!() \mid P) \quad\text{and}\quad \dok(y = \mathit{tea})\ \ink\ (\mathit{coin}!() \mid Q)\] differ in exactly one way: the first always delivers tea, and the second, on the branch where \(Q\) has committed to coffee before the coin, has a restricted receipt with no satisfying candidate and starves. The refusal that never appears in a log is a deadlock in the intervened term, and it is the starvation Remark 15.2 already named. The benchmark — logs from one machine chosen by a hidden coin, completed actions only, then the refusal question — is answered by one \(\dok\) and one observation of whether anything was delivered. It is a term one can run, on the store of Chapter 23, today.

76.4 For the interlocutor

This book, like the note it follows here, was drafted in conversation with a transformer-derived language model, which read the preprints, proposed several of the propositions above, conceded the CertiKOS counterexample, and compiled the document. A reader is entitled to ask how a trace-trained system can have had that conversation if Section 76.3 is right. The answer is the observation applied to the book’s own assistant, and it comes in three refinements.

Statement, not inhabitation. The thesis never said a transformer cannot talk about branching time; bisimulation, refusals, the vending machines are in the corpus as described objects, and reasoning about descriptions is what a trace-trained system does. Apply the chapter’s own criterion: can the model refuse? A pure autoregressive sampler always emits a next token, and its choices form a fixed tree of conditionals determined by the trace distribution — the fairness remark above applies, since an end-of-sequence token or a refusal token is a trace symbol and not a refusal in the branching-time sense. In the precise sense of Section 76.3.1 the model is nearer to \(Q\) as described by \(P\)’s logs than to either machine. The conversation is an instance of the thesis, not a counterexample.

The loop. The session was not pure sampling. Asked to read a repository, the model cloned it; asked for a PDF, it ran the typesetter and read the log, and a compilation failed on an undefined control sequence — a refusal from the environment that no quantity of training text would have supplied, corrected on the next attempt. The harness around the model is an agent loop, and an agent loop is rung two. So what i was in conversation with is a rung-one model inside a rung-two loop: the same architecture as a \(\lambda\)-prover inside a tactic engine, with the orchestration outside the dynamics once more. Chapter 75 found the same shape from the other side — a metalevel that is an instrument of its operator — and called it a fact about a community. Here it is a fact about where the branching lives: in the harness, not in the witnesses.

The dialogue. The third refinement concerns the reader rather than the model. The conversation that produced these pages was a bisimulation game with me as experimenter. i offered contexts — “does your example not confirm my argument?”, “does this hold for true concurrency?” — and learned where the model concedes, where it pushes back, and where it corrects itself. That is rung-two knowledge about the model, obtained by intervention, that no transcript of its previous conversations would have given. Chapter 22 said that structural facts become behavioral once the observer holds instruments for taking a term apart; a pointed question is such an instrument, and i held several.

76.5 The saddle point

Section 76.4 located the present culture’s working arrangement: a confluent predictor whose hedges — best-of-\(n\), tree-of-thought, sample-and-verify — live in a harness. The arrangement works, and that is the difficulty. A harness supplies the second rung, which is enough to be useful, so the question is Socratic rather than technical: what moves a culture to bear witness to its own inhabitation of a saddle point? The answer offered here is that nothing moves it while it is buying answers, and that one thing moves it the moment it wants inheritance. Nature supplies both the diagnosis and the smallest instance.

A hedge that is inherited.

Cohen’s desert annuals [300]: in a year of uncertain rain, a fraction of a plant’s seeds germinate and the rest lie dormant. The fraction is heritable, and selection tunes it to the variance of the environment. The organism is not predicting which year it is in. It is running a race between two branches — germinate now, wait — and passing the race on to the next generation as a race, encoded in the genome, uncollapsed. That is the whole mechanism in one organism: the witness carries the branching, the branching is inherited, and selection acts on the branching structure itself. A hedge is evolvable only if the hedge is in the heritable object.

Why the saddle point is a saddle point.

Now ask where the loop architecture keeps its race. Best-of-\(n\) is a hedge, and it works; but the hedge lives in the harness. The harness runs \(n\) samples, picks a winner, and emits a string. The race is collapsed at the boundary, paid for again on every query, and handed to no one as a race. It is not heritable; nothing downstream can select on it, compose it, or run it in a different environment, because downstream receives an outcome and not a structure. The loop architecture is the desert annual that germinates every seed every year and reseeds from whichever survived. It survives, and it cannot accumulate. It answers; it does not do science in the sense of Chapter 26: hypotheses as objects that carry their own branching, are tested by environments the hypothesizer did not choose, and are inherited by the next hypothesizer with the branching intact. The saddle point is stable exactly as long as per-query answers are what is being paid for. The moment the thing paid for is an accumulating body of reusable, selectable, composable search structure — a scientific community rather than an oracle — the per-query collapse is the dominant cost, and the race has to move from the harness into the witness.

Organisms that are the mechanism.

Some natural systems do not merely exploit a race; they are the search mechanism, and they show the design built and tested at scale. Clonal selection [301]: antibodies are hypotheses, antigen binding is the obligation, lymphocytes race to bind, winners replicate, losers starve — massively parallel, non-confluent, coordinator-free search with mortality as pruning and a memory cell as a proven lemma. The slime mold in a maze [302]: explore every branch in parallel, starve the unproductive tubes, keep the shortest. Exuberance and pruning in neural development, quorum sensing in the swarm, kinetic proofreading at the molecular scale — each a race run as the computation, not simulated by a scheduler beside it. None keeps its race in a harness, and none could have evolved if it had.

Recursive self-improvement needs heritable races.

The seed is the challenge of recursive self-improvement in a nutshell. Self-improvement needs an improvement operator that acts on the thing that generates behavior, and the seed shows what the operator has to preserve. The germination fraction is improvable only because the plant does not know which year it is in: the information that would say whether the hedge was right arrives after it has committed, often after it is dead. So the hedge must be kept uncollapsed through the evaluation, and the signal must land on the next generation’s copy of the hedge, not on this generation’s outcome. Improvement acts on the race. It cannot act on the result of the race, because by the time there is a result there is nothing left to improve.

That is where the loop architecture fails as a self-improver, and the failure has been measured. Its improvement operator is a gradient on outcomes: sample \(n\), reward the winner, move the policy toward it. Each step collapses the race it was run on; the structure the next step would need — the hedge, the diversity, the dormant seeds — is what the current step consumes. Loss of output diversity under outcome-based fine-tuning [303] is the symptom; the cause is that the operator acts on results, and results are confluent. Nature’s operator lacks the defect because it acts on the witness and pays for the losers: dormant seeds are branches that did not win this year, funded anyway, and the fraction funded is itself the heritable, improvable parameter. In the vocabulary of this book it is the token economy with a non-zero budget for losing branches, the budget part of the genome.

The observation is informal and its last sentence is a strong universal claim; the source lists making it a theorem among its obligations, and Chapter 15 has supplied the materials. A \(\dok\) is an operator on witnesses that changes their branching — by the carrier result of that chapter it is the only kind there is — and the set-valued form \(\dok(y \in S)\) with \(S\) the losing candidates is the operator that funds them: it restricts the race away from its current winner. That an improvement operator definable on a determinate language cannot increase branching is Proposition 15.1 read for the whole language; that one definable on rho with the cost monad can is Chapter 15. Requirement (iii) is the reproduction section of Chapter 26 with one addition: a hypothesis is a clause; a clause under a \(\dok\) is a hypothesis together with the experiment that would test it; and a germ carrying both is a hedge that is inherited, since a \(\dok\) is a term and crossover on quoted code applies to it unchanged. The plant does this with one parameter. Whether it can be done with the whole genome of rewrite rules is the question Chapter 75’s four questions were circling.

The honest version.

A determined harness engineer can make the loop emit a portfolio rather than a winner: output \(k\) candidates and let the consumer choose. But then the consumer must be able to run the portfolio under its own environment, which makes the consumer a process runtime and the artifact passed between them a process. At that point the rho mechanism has been rebuilt at the boundary, and the question is only whether to build it once as the substrate or repeatedly at every interface. So there is no phenomenon that forces a culture off the saddle point while it is buying answers. There is one that forces it the moment it wants inheritance: a hedge that has to survive its author. Nature found that phenomenon first, and the fraction of seeds that stay in the ground is its smallest instance.

76.6 One point, three registers

The rows of Table 76.1 are not analogies. The same proposition — collapse of the spectrum under confluence — underlies all three columns, and the same remedy answers all three: witnesses that can be races, and an identity on them at least as fine as step bisimulation, with the generated logic following the presentation. The verification column and the intelligence column are the abstract column applied to a certificate and to a hypothesis respectively; a certificate is a hypothesis one has stopped testing. The saddle-point row is the same arrangement three times — confluent object, branching supplied from outside — and the row beneath it is the same departure three times: put the race in the object that is kept. The last row is this book’s addition to the note’s table, and it is why the chapter is in the Prestige rather than the Turn: the instruments were built in the Turn, and the reveal is that they were built for this.

76.7 What is claimed

Claimed: Propositions 76.1 (as a sketch resting on standardization), 76.2 and 76.3; that a confluent system states and does not inhabit; that the certificate of a \(\lambda\)-term prover for a concurrent system is relative to a model of non-determinism the prover cannot audit; that a trace-trained learner stands on rung one by an information-theoretic argument and not an architectural one; that the vending-machine benchmark is answered by one \(\dok\); and that the present culture’s hedges live in its harnesses.

Not claimed: that Lean-style verification covers only sequential or linear-time software — it does not, and Section 76.2 opens by saying so; that the alignment of the ladder with the linear/branching/causal spectrum is a theorem beyond its first two rungs; that Observation 76.3 is a theorem, though the materials for one are now in the book; or that any transformer cannot be made to inhabit a race — only that inhabiting is a property of the witness language and not of the model’s size. The thing this book can do about the saddle point is what the Turn did: build the witness language in which a hypothesis can be a race, a certificate can run, and a hedge can be inherited, and show that it runs on a machine. Whether anyone leaves the saddle point is not a question a book answers.