Choice Principles are the Types; Schedulers are the Terms

The previous two chapters left a debt. They argued that the resolution of a race is a computational resource, that its strength is a coordinate, and that the whole factorization of a term into determinate islands and open seas stands or falls on one question — whether a scheduler can climb, merely by running, above the strength it started with. What they did not supply is a discipline in which that question can be posed rigorously. You cannot ask whether a thing preserves its type until you have said what its types are.

This chapter says. The proposal is a Curry–Howard correspondence for nondeterminism, and it is the third instance of a pattern the reader has now met twice: a declarative logic, an operational term language, and an extraction that turns proofs into programs by normalization. Here the declarative side is the mathematical theory of choice — a choice principle is a specification of what nondeterministic resolution a computation is permitted to assume — and the operational side is the theory of fairness and scheduling. The slogan, before the unpacking:

Two things make this more than a pleasing symmetry. The first is practical. Schedulers and fairness disciplines are written by hand today and verified, if at all, afterwards; a correspondence would make them correct-by-construction, extracted from a specification of the nondeterminism a system requires. The second is why the chapter sits here rather than in an appendix. If a scheduler can smuggle in an oracle — and the thesis of the preceding chapters is that it can — then a type discipline in which the choice principle is the type is precisely an accounting of how much it smuggles. The type is the altitude. A well-typed scheduler is one whose imported power is declared on its face.

Which turns the crux into a metatheorem. Subject reduction — the ordinary demand that reduction preserve typing — says here that running a schedule does not come to realize a stronger choice principle than the scheduler was typed for. Scheduling cannot bootstrap an oracle. That is the same sentence as “an island cannot crack while it runs,” reached from proof theory rather than from ecology, and the coincidence is the best evidence available that the correspondence is the right one.

The program is stated to be discharged, not completed. What follows lays out the two theories, records the bridge that already exists in the realizability literature, identifies the gap that makes room for it, sketches the term assignment, and ends with the extraction pipeline and a list of what a rigorous development owes.

61.1 Two theories of nondeterminism

61.1.1 Choice, declaratively

The mathematical theory of choice is a graded family of principles asserting that a section exists for a family of nonempty sets. We read each principle as a type: a specification of the nondeterministic resolution a computation is permitted to assume.

• Finite choice. For a finite family the section exists with no axiom, constructively; and when the family is presented — each fiber given as a list, as a finite bag of prefixes is — the choice function is definable outright. This is the type of a scheduler that needs no special power: the term is its own choice structure.

• Countable choice \(\CCh\) and dependent choice \(\DC\). A countable family, or a family whose later fibers depend on earlier selections. \(\DC\) is the type of a scheduler with memory and lookahead, choosing each step in the context of the residuals of the last.

• Full \(\AC\). An arbitrary family. The type of a scheduler that can survey an unindexed contention and select coherently — the strongest principle, and (Diaconescu [103]) the one that, in a topos, imports excluded middle.

These principles are not linearly ordered by logical strength alone; the finer structure is the Weihrauch lattice [79], whose objects are choice (and choice-like) principles ordered by uniform reducibility and composed by the operation “solve one, then, using its answer, the next.” We take the Weihrauch lattice to be the entailment order of the logic of choice: the order in which one scheduler-type is at least as strong as another, and the composition along which schedules are chained. That it is a lattice and not a chain is the declarative shadow of the “jumble, not tower” ontology of §60.4.

61.1.2 Fairness and scheduling, operationally

A scheduler resolves the nondeterminism a system leaves open: at each point of contention it selects which enabled interaction fires. A fairness discipline constrains the schedulers under consideration — weak fairness (a continuously enabled action eventually fires), strong fairness (an infinitely-often-enabled action eventually fires), and their refinements — and is, classically, the assumption under which liveness and progress can be guaranteed (Francez [98]). We take this to be the term language: schedulers are the terms, fairness disciplines the typing constraints they must satisfy. The polarities of the scheduling literature — demonic (adversarial: must survive every resolution) and angelic (cooperative: may seek a good resolution) — are, in this reading, the two ways a term can inhabit a choice-type, and (as §60.4 conjectures) the left and right adjoints to reindexing along the strength order.

61.2 The bridge already exists, in fragments

The correspondence is not built from nothing. The computational content of choice has been studied for decades, and in every case the realizer of a choice principle is a program whose extra power matches the principle’s strength — which is exactly the typing discipline we want, in a sequential setting.

• Constructive \(\AC\) as a theorem (Martin-L\"of [93]). The proof is the choice function; the term assignment is the identity insight. This is the base case of the correspondence: at the bottom of the stalk, the scheduler is read straight off the proof.

• Bar recursion (Spector [94]). Spector’s bar recursion realizes the double-negation shift and hence countable choice and classical analysis, as a recursion schema in an extension of G\"odel’s System T. A choice principle is realized by a specific recursion operator — a term with a definite computational shape, a scheduler with backward-inductive lookahead.

• Computational content of \(\AC\) (Berardi–Bezem–Coquand [95]). A realizer of the axiom of choice that proceeds by learning — updating a finite approximation to the choice function as it goes. Read operationally it is a scheduler that commits provisionally and revises: precisely the on-demand, never-completed choice process §59.3 calls for at \(\omega\).

• Dependent choice by control (Krivine [96]). Krivine’s classical realizability interprets \(\DC\) using a “quote” instruction and a clock — the realizer is a program with a specific non-functional primitive. The strength of the principle is the strength of the primitive: the cleanest existing statement that a choice-type’s inhabitant is a program with matching extra power.

• The selection monad (Escard\’o–Oliva [97]). Selection functions — “given a predicate, choose a witnessing point” — form a monad whose algebra is the algebra of choice-as-program, with bar recursion as its characteristic operation and backward induction as its paradigm. This is the categorical home for “scheduler as term”: the selection monad is, we propose, the monad of the scheduler calculus.

Each of these gives choice a term content. None gives it in a concurrent setting, where the contention is a race at a channel and the realizer is a scheduler over a store. Assembling them there is the program.

61.3 The gap: proofs-as-processes is confluent

The companion note’s analogy was “Coalition Logic is to rho as linear logic is to \(\pi\).” The second half of that analogy — the proofs-as-processes program of Abramsky and of Bellin–Scott [99, 100], and the propositions-as-sessions of Caires–Pfenning and Wadler [101, 102] — is exactly where the present opening lies. In that program a linear-logic proof is a session-typed process and cut elimination is communication; it is a genuine Curry–Howard correspondence for concurrency, and it is, by design, confluent and deadlock-free. Wadler’s CP is Church–Rosser: cut elimination has a unique normal form, sessions do not race, and deadlock is ruled out by the logic.

That confluence is the point and the limitation. It means the proofs-as-processes correspondence captures the communication skeleton — who talks to whom on which protocol — while discarding precisely the nondeterminism the mobile process calculi exist to express: the races of \(\chApr\), two sends contending for one receive, the choice of which meets which. A confluent system cannot type that choice, because confluence is the assertion that the choice does not matter. So linear logic types the structure of interaction and is silent on its resolution.

This is why the theory of choice, and not linear logic, is the right declarative partner for the nondeterministic content. Linear logic deliberately excluded it; choice is the logic of exactly what was excluded.

61.4 The proposed correspondence

We sketch the term assignment. As in [92] this is a program, stated to be discharged, not a completed system.

61.4.1 The dictionary

61.4.2 Formulae, proofs, and the site of the term

At an aperture — a channel carrying both polarities, a race — the obligation is a \(\forall\exists\): for the contended slot, there exists an admissible pairing. The formula is the choice-type of that aperture; a proof is a scheduler that, for the slot, produces the pairing; the term acts at exactly the forgiving zip of [75], where the underlying lists are chosen and matched. The denotation \(\sem{-}\) stays a function and the zip is the separate dynamics [75]; in the present reading the zip’s choice of list orderings is the term inhabiting the aperture’s choice-type, and normalization — running the schedule — is the firing of matched pairs with surplus remaining.

A confluent interior — a macro-component of \(\chApr\) — is, in this light, a region whose choice-type is proof-irrelevant: several pairings inhabit it but all normalize to \(\rbisim\)-equal results, so the term carries no observable information. The genuine proof content sits at the boundary apertures. “Capacity lives at the apertures” becomes “the term content lives where the choice-type is not proof-irrelevant.”

61.4.3 Subject reduction is the no-bootstrap law — and the open hinge

The two metatheorems one demands of a term assignment have, here, direct operational meaning.

Progress: a well-typed live choice can be scheduled — the system does not deadlock except where the type (the \(f\)-zone) says no resolution exists. This is the fairness guarantee, internalized as a typing property.

Subject reduction: running the schedule preserves the type — the scheduler does not, by reducing, come to realize a stronger choice principle than it was typed for. Operationally: scheduling cannot bootstrap an oracle. This is the proof-theoretic form of the no-implicit-interaction discipline of [76], and of the constant-altitude claim of \(\chAgy\): a scheduler of degree \(\mathbf d\) keeps degree \(\mathbf d\) as it runs.

This is Question 60.2 of \(\chAgy\), and the two are the same statement: whether the resolution of a boundary race can cause an interior to acquire a choice type it did not have, climbing the stalk as it reduces.

If subject reduction holds, the graded factorization of \(\chAgy\) is stable: determinate interiors stay determinate under scheduling, and a scheduler’s imported power is fixed by its type once and for all. If it fails, the failure is perturbation: a high-capacity scheduler, reducing against a low-capacity system, manufactures new choice in it — a well-typed term reducing to an ill-typed one, the type-theoretic signature of an agent changing another’s capacity. The same lemma settles the agency question and the metatheory of the correspondence.

61.5 The synthesis pipeline

Mirroring [92], the extraction has three stages.

Stage 1 — specification. The nondeterminism a system requires is specified as a choice-type: which contentions must be resolvable, under which fairness discipline, at what permitted strength. The permitted strength is a Weihrauch-degree bound — a ceiling on the oracle the scheduler may import.

Stage 2 — proof and extraction. A proof that the specification is satisfiable in the logic of choice is constructed; the term assignment extracts a scheduler. It is correct-by-construction: it resolves exactly the specified contentions, under the specified fairness, and within the specified strength — the type certifies that it smuggles in no more oracle than declared.

Stage 3 — optimization. As in [92], extraction yields a naive scheduler; bisimulation-preserving transformations reduce overhead while preserving the realized choice-type, and the phlogiston metering of the rholang runtime serves as the objective, now with the added invariant that optimization must not raise the scheduler’s altitude.

61.6 Connections and context

To \(\chApr\) and \(\chAgy\). This note is its proof-theoretic face. The aperture is the site of a non-trivial choice-type; the macro-component is a proof-irrelevant region; the hypercomputation stalk is the strength order made into types; interference is a realizer supplied from a stronger type than the lower system’s own; and the open hinge is subject reduction (Question 60.2).

To the consensus note [92]. Both instantiate one pattern — declarative logic, term language, extraction by normalization. The notes compose rather than merely resemble: Coalition Logic over the communication structure, choice-logic over the nondeterministic resolution, with the rho calculus the common term substrate and cut-elimination-as-communication the shared engine.

To proofs-as-processes [99, 100, 101, 102]. The complementary axis (Principle 61.1). Linear logic types the confluent skeleton; choice-logic types the discarded nondeterminism. A mobile process is fully accounted for only by both, and the present program is the missing half.

To realizability and selection functions [93, 94, 95, 96, 97]. The technical grounding: choice principles already have realizers whose power tracks their strength. The contribution sought here is to carry that into a concurrent, store-based setting where the realizers are schedulers and the contention is a race — with the selection monad [97] the likely categorical backbone.

61.7 Open problems

1. The logic of choice as a formal system. Present the choice principles as a deductive calculus with the Weihrauch lattice [79] as its entailment order and Weihrauch composition \(\star\) as the cut. Identify the analogue of geometric/structural rules for the gradations (finite, \(\CCh\), \(\DC\), \(\AC\)).

2. The scheduler calculus. Define the term language precisely — schedulers as terms over the RSpace store, fairness disciplines as typing constraints, the selection monad [97] as the computational structure — and the operation that runs a schedule.

3. Term assignment and metatheory. Define the assignment of Section 61.4 and prove progress (fairness as a typing property) and subject reduction (Question 60.2).

4. The grading theorem. Prove that the choice-type of an extracted scheduler equals its Weihrauch/Turing degree equals its altitude in the tower of §58: type, degree, and altitude are one.

5. The hinge. Resolve Question 60.2 — whether scheduling can climb the stalk — proving stability of the factorization if subject reduction holds, or characterizing perturbation as its definite failure mode if it does not.

6. Composition with consensus. Make precise the stacking of this pipeline with [92]: a single extraction whose output is correct-by-construction in protocol logic and fair-and-bounded-by-construction in scheduling.

7. Mechanisation. Formalize the logic of choice, the scheduler calculus, and the term assignment in a proof assistant (Lean 4), enabling machine-checked extraction of bounded-strength fair schedulers.