Chapter 58
The Tower of Oracle Extensions
58.1 Background: Turing’s Oracle Hierarchy
Turing [12] described a transfinite tower of computational systems above the Turing-computable. At the base is the class of Turing-computable functions. At the first stage above is the class of functions computable relative to the halting oracle \(\emptyset'\): the oracle that decides, for any Turing machine \(M\) and input \(x\), whether \(M\) halts on \(x\). At the next stage is the class computable relative to \(\emptyset''\), the halting oracle for machines with access to \(\emptyset'\). The tower continues through all countable ordinals and beyond.
Each stage is strictly more powerful than the stage below: there are functions computable at stage \(\alpha+1\) that are not computable at stage \(\alpha\), and this gap cannot be closed by any finite amount of additional computation at stage \(\alpha\).
58.2 The Subcategory of Turing-Complete GSLTs
A GSLT \(\GSLT\) is Turing-complete if the class of functions computable by terms of \(\GSLT\) (via some standard encoding of natural numbers) coincides with the class of Turing-computable functions. The full subcategory of Turing-complete GSLTs is written \(\mathbf{GSLT}_{\mathrm{TC}} \subseteq \mathbf{GSLT}\).
The \(\lambda\)-calculus, the \(\pi\)-calculus, and the Rho calculus are all Turing-complete. The category \(\mathbf{GSLT}_{\mathrm{TC}}\) is therefore large and contains the primary examples of interest.
58.3 Oracle Extension of a GSLT
Let \(\GSLT \in \mathbf{GSLT}_{\mathrm{TC}}\). An oracle term for \(\GSLT\) is a distinguished term \(\oracle \in \terms(\GSLT^{(1)})\) in an extension of \(\GSLT\), equipped with rewrite rules of the form: \[\oracle \inter \lceil (M, x) \rceil \;\rewrite\; \begin{cases} \lceil \mathtt{halt} \rceil & \text{if } M \text{ halts on } x \\ \lceil \mathtt{loop} \rceil & \text{otherwise} \end{cases}\] where \(\lceil \cdot \rceil\) denotes the encoding of Turing machine descriptions and inputs as terms of \(\GSLT\), and \(\inter\) is the interaction operator of \(\GSLT\). The oracle answers halting queries in one interaction step.
In the Rho calculus, the oracle is naturally expressed as a persistent receive on a distinguished channel \(x_{\oracle}\): \[\oracle \;=\; \mathtt{for}(q \leftarrow x_\oracle)\, \bigl( \text{compute halting of } {*}q \text{ and reply} \bigr)\] This makes the oracle a communicating process rather than a magic tape: it participates in the same interaction mechanism as every other term. This is essential if each stage of the tower is to be a GSLT rather than something that escapes the GSLT framework at each oracle step.
Let \(\GSLT \in \mathbf{GSLT}_{\mathrm{TC}}\). The first oracle extension \(\fiber{1}\) is the GSLT obtained from \(\GSLT\) by:
extending the grammar with the oracle term \(\oracle\);
adding the oracle rewrite rules to \(\rules\);
extending the equations \(\eqs\) to account for oracle interactions.
The \(\alpha\)-th oracle extension \(\fiber{\alpha}\) is defined by transfinite induction:
\(\fiber{0} = \GSLT\);
\(\fiber{\alpha+1}\) is the oracle extension of \(\fiber{\alpha}\), with oracle deciding halting in \(\fiber{\alpha}\);
\(\fiber{\lambda} = \varinjlim_{\alpha < \lambda} \fiber{\alpha}\) for limit ordinals \(\lambda\) (colimit in \(\mathbf{GSLT}\)).
58.4 The Tower
The oracle tower over \(\mathbf{GSLT}_{\mathrm{TC}}\) is the assignment \[\Phi : \mathbf{GSLT}_{\mathrm{TC}} \times \Ord \;\to\; \mathbf{GSLT}\] sending \((\GSLT, \alpha)\) to \(\fiber{\alpha}\), together with:
projection morphisms \(\proj{\alpha} : \fiber{\alpha+1} \to \fiber{\alpha}\) in \(\mathbf{GSLT}\) for each ordinal \(\alpha\);
inclusion morphisms \(\iota_\alpha : \fiber{\alpha} \to \fiber{\alpha+1}\) embedding each stage into the next.
The tower over \(\GSLT\) is \(\fiber{0} \hookrightarrow \fiber{1} \hookrightarrow \fiber{2} \hookrightarrow \cdots\)
Earlier drafts called \(\Phi\) the hypercomputational fibration, and it is not one. A Grothendieck fibration is a functor \(p : \mathcal{E} \to \mathcal{B}\) equipped with cartesian lifts. What Definition 58.4 writes down is a functor out of a product — an indexed family, from which the Grothendieck construction would build a fibration, and which is therefore the raw material for one rather than an instance of one.
Worse, the variance is overdetermined. \(\Ord\) is a poset, so a functor out of it can go one way, and both \(\proj{\alpha}\) and \(\iota_\alpha\) are given. What is being described is a section–retraction pair, and the intended reading — inclusion adds structure, projection forgets it — is that \(\iota_\alpha \dashv \proj{\alpha}\). If that adjunction holds, and the triangle identities have not been checked here, the whole tower is a tower of adjunctions, which is a better object than the one on the page and costs nothing that is not already available.
The object this act is really about is the fibration \(p : \Hyp \to \catGSLT\) of open problem (ii) in Section 60.7, where the base is all of \(\catGSLT\) rather than its Turing-complete part, and where the question of whether angelic and demonic resolution are the Lawvere adjoints \(\exists \dashv (-)^{\ast} \dashv \forall\) to reindexing can even be asked. That object has not been exhibited. This one has, and it is a ladder, so it is called one.
Each projection \(\proj{\alpha} : \fiber{\alpha+1} \to \fiber{\alpha}\) is a morphism in \(\mathbf{GSLT}\): it preserves bisimulation. If \(P \bisim_{\alpha+1} Q\) in \(\fiber{\alpha+1}\), then \(\proj{\alpha}(P) \bisim_\alpha \proj{\alpha}(Q)\) in \(\fiber{\alpha}\).
Any bisimulation in \(\fiber{\alpha+1}\) that uses only oracle-free transitions is already a bisimulation in \(\fiber{\alpha}\). The projection discards oracle interactions; the remaining bisimulation relation is preserved. The details require checking that the oracle rewrite rules are projected consistently with the extension of \(\eqs\).
The projection \(\proj{\alpha}\) is in general not a bisimulation equivalence: there exist \(P, Q\) with \(P \bisim_{\alpha+1} Q\) but \(P \not\bisim_\alpha Q\). Going down the tower collapses distinctions. Going up reveals them.
58.5 Two things this construction gets wrong
It is better to say this here than to let a reader discover it three chapters on, so: the construction just given is a scaffold, and it has two defects that the chapters after it exist to repair.
The index should not be an ordinal.
Ordinals are linearly ordered, and the thing being indexed is not. Two agents can each be able to resolve what the other cannot — one affords a choice principle the other lacks, and the other affords a different one — and an ordinal index has no room for that. The correct index is a position in the Weihrauch lattice [79], which has joins and meets and incomparable elements, and the tower is the image of that lattice under a map that flattens it into a chain. A chain-shaped shadow is a legitimate way to introduce an intuition and an illegitimate way to keep one. Chapter 59 replaces it.
The oracle should not be bolted on.
Definition 58.3 adjoins an oracle term to a theory that did not have one, with rewrite rules supplied by hand. That is a construction and it is unobjectionable as a construction, but it gets the situation backwards. In any calculus where interaction is primitive and confluence fails, something already decides which of several admissible pairings occurs, and that something is not derivable from the terms. It is the scheduler, and it is present at every cut. The excess capacity we are looking for does not have to be added to the theory; it has to be found in it, and then priced. Chapters 59 and 60 do the finding, and Chapter 61 supplies the typing discipline that says what a scheduler is allowed to be.
What survives.
Both repairs leave the tower’s actual content intact. Projections are lossy, going up reveals distinctions, and each stage carries a strictly richer physics than the one below — those are claims about oracle extensions and they do not depend on the index being well-ordered or on the oracle being adjoined rather than discovered. What does not survive is the picture of consciousness as a ladder with rungs and a reader wondering which one they are standing on.