4 Computability
This chapter collects the computability-theoretic ingredients of the proof: classical statements with no quantum content, several of which partially exist in Mathlib. Like the results of Section 3, these are external results that the project may initially assume as axioms, and each entry carries the same formalization-effort estimate. The concrete machine model and its canonical codes come first; then the toolkit of resource-bounded computability results; the recursive compression lemma, which builds on the toolkit, isolates the self-referential part of the proof.
4.1 The machine model
The machine-level side of the project is formalized directly: a concrete multi-tape machine model with several input tapes, a canonical first-order syntax of machine codes with an exact binary serialization, and a reference evaluator.
A multi-input Turing machine with \(i\) input tapes and \(w\) work tapes has \(i\) two-way read-only input tapes (heads clamped one blank cell beyond either end of the input), \(w\) bidirectional work tapes over an alphabet extended with a blank symbol, and a write-only output stream. A transition may write and move on every work tape, move every input head, emit at most one output symbol, and either continue or halt. Time is counted in steps, and space as the number of work-tape cells visited.
At \(i = 1\) this is exactly the CSLib multi-tape model.
A machine code is first-order data: a header (number of work tapes, alphabet size, number of states, start state) and a dense transition table with one entry per observation, in a fixed canonical order. A well-formed code is interpreted as a multi-input machine, with binary input and output through two reserved alphabet symbols. Codes serialize exactly: the description \(\alpha \in \{ 0,1\} ^*\) of a code has size \(\left\vert {\alpha } \right\vert \), and total decoding interprets every string — \([\alpha ]_i\) denotes the coded machine with \(i\) input tapes described by \(\alpha \), with every malformed string denoting one fixed machine that immediately rejects.
Let \(c\) be a machine code with \(i\) input tapes, \(x = (x_1, \ldots , x_i)\) bit strings and \(y \in \{ 0,1\} ^*\). The code \(c\) produces \(y\) on \(x\) if its run on \(x\) halts with output \(y\) (in some time and space). The budgeted evaluation of \(c\) on \(x\) with budget \(T\) returns the output if \(c\) has halted within \(T\) steps, and a timeout marker otherwise; it is total and executable, and the two notions agree: \(c\) produces \(y\) if and only if some budget suffices to observe it.
Exact decoding inverts encoding, distinct codes have distinct descriptions, and every description accepted by the exact decoder is the canonical encoding of the code it parses to.
Compositional, from paired prefix and soundness lemmas for each field of the description format.
The following two statements are the machine-level counterparts of Lemma 4.7.
For each arity \(i\) there are a machine code \(U\) with \(i + 1\) input tapes and a polynomial \(P\) such that for all \(\alpha \in \{ 0,1\} ^*\), all inputs \(x\) and all \(y\): \(U\) on \((\alpha ; x)\) produces \(y\) if and only if \([\alpha ]_i\) on \(x\) produces \(y\); and whenever \([\alpha ]_i\) halts on \(x\) within \(t\) steps, \(U\) halts on \((\alpha ; x)\) within \(P(\left\vert {\alpha } \right\vert + t)\) time and space.
TODO
For each arity \(i\) there are a machine code \(U\) with \(i + 2\) input tapes and a polynomial \(P\) such that on input \((\alpha ;\, T \text{ in binary};\, x)\), the machine \(U\) always halts within \(P(\left\vert {\alpha } \right\vert + T)\) steps, outputting the canonically encoded budgeted evaluation of \([\alpha ]_i\) on \(x\) with budget \(T\).
TODO
4.2 Efficient computability toolkit
[\(\bullet \bullet \bullet \) hard] (infrastructure: requires a cost model for computation)
There is a program \(u\) and a polynomial \(p\) such that \(\phi _u(e, x) = \phi _e(x)\) for all \(e, x\), with \(\mathrm{runtime}(u, (e,x)) \leq p\bigl(\left\vert {e} \right\vert , \left\vert {x} \right\vert , \mathrm{runtime}(e, x)\bigr)\).
Both the universal program and its clocked variant are self-interpreters of the ambient list language, written in the language itself (MIPRE.Cost.Machine.univProg, MIPRE.Cost.Machine.univTProg). Evaluation is first presented as an abstract machine on configurations (a control “evaluate \(p\)” or “return \(v\)”, an environment and a stack of frames) whose steps are charged exactly the costs of the evaluation rules, so that a derivation of cost \(t\) corresponds to a machine run of at most \(3t\) steps reaching a final configuration, and conversely every run reaching a final configuration comes from a derivation. Configurations are encoded as data and the step function is implemented by a fixed program (stepProg) at cost quadratic in the size of the configuration. Along the run simulating a derivation of cost \(t\) on the input \(x\), every configuration has size polynomial in \(\left\vert {e} \right\vert + \left\vert {x} \right\vert + t\): values are results of sub-derivations, hence of size at most \(t\); environments and stacks grow by at most one entry per unit of cost. The universal program iterates stepProg until a final configuration is reached, so its runs are polynomially bounded, and any of its halting runs is a machine run reaching a final configuration, hence a derivation with the same result. The clocked variant additionally carries, in unary, the remaining cost budget (decremented by the exact cost of each step), a step budget \(3k+1\) guaranteeing termination, and a size guard \(\Theta \), a fixed polynomial in \(k + \left\vert {e} \right\vert + \left\vert {x} \right\vert \) dominating the configuration sizes of any run of cost at most \(k\); it returns the timeout value when a budget or the guard is exceeded. The guard is checked on the configuration produced by each step, whose size is bounded by the cost of producing it, so the loop only handles configurations of polynomial size even when the simulated run does not halt.
There is a polynomial-time computable \(s\) such that \(\phi _{s(e,x)}(y) = \phi _e(x, y)\) for all \(e, x, y\), with the runtimes of \(e\) and \(s(e,x)\) polynomially equivalent.
In the ambient list language, \(s(e, x)\) is the program that pairs the literal \(x\) with its input and runs \(e\) on the pair (MIPRE.Cost.hardcode). The time overhead is additive and linear in \(\left\vert {x} \right\vert \) and the input size, in both directions, and the description of \(s(e, x)\) is that of \(e\) plus \(\left\vert {x} \right\vert \) plus a constant. The map \(s\) itself is computed in linear time by a fixed program assembling the description (smnProg).
For every polynomial-time computable \(f : \{ 0,1\} ^* \to \{ 0,1\} ^*\) there is a program \(e\) with \(\phi _e = \phi _{f(e)}\) and the runtime of \(e\) polynomially bounded in terms of that of \(f(e)\). (This is the direction used by Lemma 4.10; [ 8 ] states the runtimes as polynomially equivalent, and the converse direction would require a simulator that is never faster than the simulated program.)
The classical construction. Let \(G\) be the program that on input \((x, v)\) computes \(s(x, x)\) (Lemma 4.8), applies \(f\) to it, and runs the resulting program on \(v\) through the universal machine (Lemma 4.7); put \(e = s(G, G)\). Then \(e\) on \(v\) is \(G\) on \((G, v)\), which runs \(f(s(G, G)) = f(e)\) on \(v\): the two programs halt on the same inputs with the same results (the backward direction inverts the run of \(G\) step by step and uses that the universal machine halts only if the simulated program does), and a run of \(f(e)\) of time \(t\) gives a run of \(e\) within \(p(\left\vert {v} \right\vert , t)\), where \(p\) is the universal machine’s overhead polynomial shifted by the fixed size of \(f(e)\), plus a linear term for the copies of the input and a constant for the fixed computation of \(f(e)\).
Source.
Folklore; stated in this efficient form in [ 8 ] , Lemmas 2.1–2.3.
Comments.
Mathlib contains the non-resource-bounded versions (universal machine, s-m-n and the Rogers fixed-point theorem for Nat.Partrec.Code). The efficient versions require a cost model for the chosen machine model; this is real infrastructure work and a prerequisite for everything involving “polynomial-time”. The formalization’s ambient model is not a Turing machine but a small first-order list-processing language (MIPRE.Cost.Prog, over binary trees) with a unit-cost semantics in which reading a value costs its size; it is polynomially equivalent to Turing-machine time, programs are their own tree serializations (so “a program \(e\)” and “\(\left\vert {e} \right\vert \)” are literal), and the s-m-n theorem is a linear-overhead syntactic operation. Mathlib’s Turing.ToPartrec.Code was tried first and rejected: its programs cannot rebuild a list in polynomial time. A pragmatic first pass can replace “polynomial time” by “computable” wherever Section 1.3 permits, deferring the cost model. The machine-level counterpart, for the concrete model of Section 4.1, is stated as Lemmas 4.5 and 4.6; the pipeline consumes only the present ambient version.
4.3 The abstract compression lemmas
[\(\bullet \) easy] (given the toolkit of Section 4.2)
Let \(f : \{ 0,1\} ^* \to \mathbb {N}\cup \{ \infty \} \) be a function and \(A \subseteq \{ x : f(x) {\lt} \infty \} \) a nonempty language. Suppose there is a polynomial-time computable function \(\textsc{Compr}: \{ 0,1\} ^* \times \mathbb {N}\to \{ 0,1\} ^*\) such that whenever \(\hat{x}\) is a succinct description (Definition 2.23) of a string \(x\) and \(y = \textsc{Compr}(\hat{x}, n)\):
\(f(y) \geq \max \{ f(x), n \} \), and
if \(x \in A\) then \(y \in A\).
Then there is a polynomial-time computable function \(g\) reducing the halting problem to \(A\): for every Turing machine \(e\), if \(\phi _e\) halts on the empty input then \(g(e) \in A\), and otherwise \(f(g(e)) = \infty \).
The construction of [ 8 ] , with two harmless modifications: the “next level” of the recursion is \(2n + 1\) instead of \(n + 1\) (prepending a bit to a binary numeral is one step in the list language, an increment is not), and the threshold below is explicit. Let \(\beta \) be the fixed bit-query program that, on input \((((c', e), n), m)\), runs the universal machine on \(c'\) with input \((e, n)\) to obtain a string \(y\) and outputs the \(m\)-th bit of \(y\) (or \(2\) if \(m \geq \left\vert {y} \right\vert \)). Let \(a\) be the polynomial-time decider that on \((c', (e, n))\) outputs a fixed \(y_0 \in A\) if \(e\) halts on the empty input within \(\log n\) steps, and \(\textsc{Compr}\bigl((s(\beta , ((c', e), 2n+1)), n), n\bigr)\) otherwise, where \(s\) is the s-m-n map of Lemma 4.8. By Lemma 4.9 there is a program \(c\) with \(\phi _c(e, n) = \phi _a(c, (e, n)) =: h(e, n)\), running in time polynomial in \(\left\vert {e} \right\vert + \log n\). Hence for \(n\) above a threshold \(r(e) = 2^{K + 1 + \left\vert {e} \right\vert }\) (with \(K\) a constant depending only on the polynomial overheads), \((s(\beta , ((c, e), 2n+1)), n)\) is a succinct description of \(h(e, 2n+1)\): the string has length at most \(2^n\) and the bit-query program answers within the budget of Definition 2.23. The reduction is \(g(e) = h(e, r(e))\). If \(e\) does not halt, then for every \(n \geq r(e)\) the decider compresses, so \(f(h(e, n)) \geq \max \{ f(h(e, 2n+1)), n\} \), and iterating gives \(f(h(e, n)) \geq n + k\) for all \(k\), i.e. \(f(g(e)) = \infty \). If \(e\) halts in \(T\) steps, then \(h(e, n) = y_0 \in A\) once \(n \geq 2^T\), and by downward induction along the levels \(n, 2n+1, 4n + 3, \ldots \) the second property of \(\textsc{Compr}\) gives \(h(e, n) \in A\) for every \(n \geq r(e)\), in particular \(g(e) \in A\).
Source.
Marks, Nezhadi and Yuen [ 8 ] , Lemma 5.1 (the variant of their Lemma 3.1 with compression parameter \(n\)); the technique is implicit in [ 26 , 12 , 1 ] . The proof is a fixed-point construction using the efficient universal machine, s-m-n and Kleene recursion theorems (Section 4.2).
Comments.
This is the entire “self-referential” part of the proof, isolated in a statement with no quantum content. In the application (Section 6.7), \(A\) is the set of normal form verifier descriptions with \(\mathrm{val}^{s}= 1\) and finite entanglement requirement, and \(f(\mathsf{V}) = \mathrm{Ent}(\mathsf{V}, \frac12)\) (suitably formalized); the compression procedure is Theorem 6.6. The value-form pipeline of Section 6 uses Lemma 4.11 below instead; this lemma is retained as the entanglement-form route (Remark 6.8), where the factor \(\frac12\) in the entanglement bound of compression requires the variant with hypothesis \(f(y) \geq \frac12 \max \{ f(x), G(n)\} \) for a function \(G\) growing faster than the levels. Note that [ 8 ] also proves a converse (their Lemma 4.1): a halting reduction of this kind exists only if a compression procedure does, which is evidence that this decomposition of the proof is canonical. The lemma and its proof are a self-contained computability project, an ideal early milestone.
Let \(A, B \subseteq \{ 0,1\} ^*\) be languages with distinguished elements \(y_{\mathrm{yes}} \in A\) and \(y_{\mathrm{no}} \in B\), and suppose that the complement of \(B\) is recursively enumerable: there is a program \(S\) that halts on input \(x\) if and only if \(x \notin B\). Suppose there is a polynomial-time computable function \(\textsc{Compr}: \{ 0,1\} ^* \times \mathbb {N}\to \{ 0,1\} ^*\) such that whenever \(\hat{x}\) is a succinct description (Definition 2.23) of a string \(x\) and \(y = \textsc{Compr}(\hat{x}, n)\):
if \(x \in A\) then \(y \in A\), and
if \(x \in B\) then \(y \in B\).
Then there is a polynomial-time computable function \(g\) reducing the halting problem to \((A, B)\): for every Turing machine \(e\), if \(\phi _e\) halts on the empty input then \(g(e) \in A\), and otherwise \(g(e) \in B\).
The construction of Lemma 4.10, with a third branch. Let \(\beta \) be the bit-query program of that proof, and let \(\sigma \) be the program that, on \(((c', (e, (m, m))), \cdot )\), runs the universal machine on \(c'\) with input \((e, (m, m))\) to obtain a string \(x\) and then runs \(S\) on \(x\). Let \(a\) be the polynomial-time decider that on \((c', (e, (m, n)))\) outputs \(y_{\mathrm{yes}}\) if \(e\) halts on the empty input within \(\log n\) steps; otherwise \(y_{\mathrm{no}}\) if \(s(\sigma , (c', (e, (m, m))))\) halts within \(\log n\) steps; and otherwise \(\textsc{Compr}\bigl((s(\beta , ((c', e), (m, 2n+1))), n), n\bigr)\), where \(s\) is the s-m-n map of Lemma 4.8. By Lemma 4.9 there is a program \(c\) with \(\phi _c(e, (m, n)) = \phi _a(c, (e, (m, n))) =: h(e, m, n)\), running in time polynomial in \(\left\vert {e} \right\vert + \log m + \log n\). As before, for \(n\) above a threshold \(r(e) = 2^{K + 1 + \left\vert {e} \right\vert }\) and \(m = r(e)\), the pair \((s(\beta , ((c, e), (m, 2n+1))), n)\) is a succinct description of \(h(e, m, 2n+1)\); the start level \(m\) is carried as data so that the threshold can be chosen from the running time of \(a\) afterwards. The reduction is \(g(e) = h(e, r(e), r(e)) =: x_e\); the second branch tests, at every level, whether \(S\) halts on \(x_e\).
If \(e\) does not halt, suppose \(x_e \notin B\). Then \(S\) halts on \(x_e\) in some time \(T\), so at every level \(n\) with \(\log n \geq T\) the decider outputs \(y_{\mathrm{no}} \in B\), and by downward induction along the levels \(r(e), 2r(e)+1, 4r(e)+3, \ldots \) from such a level, property 2 of \(\textsc{Compr}\) gives \(h(e, r(e), n) \in B\) at every level, in particular \(x_e \in B\), a contradiction. If \(e\) halts in \(T\) steps, then \(h(e, r(e), n) = y_{\mathrm{yes}} \in A\) once \(\log n \geq T\), and by downward induction property 1 gives \(h(e, r(e), n) \in A\) at every level, provided the second branch never fires at a level where the first has not. If it fired at such a level \(n_1\), then \(S\) halts on \(x_e\), so \(x_e \notin B\); but the output \(y_{\mathrm{no}} \in B\) at level \(n_1\) and property 2, by downward induction along the levels between \(r(e)\) and \(n_1\) (at which the first branch does not fire either), give \(x_e \in B\), a contradiction. Hence \(g(e) = x_e \in A\).
Source.
Lin [ 10 ] , the compression criterion for \(\mathrm{RE}\)-complete problems (direction “weakly compressible implies \(\mathrm{RE}\)-complete”), whose self-referential sequence has exactly these three branches; the formulation through succinct descriptions is that of [ 8 ] and of Lemma 4.10. Lin’s theorem is an equivalence: given that the no-instances form a \(\mathrm{coRE}\) set, a decision problem is \(\mathrm{RE}\)-complete if and only if it is compressible.
Comments.
This is the lemma the main theorem uses (Section 6.7): \(A\) is the set of normal form verifier descriptions with a value-\(1\) PCC strategy, \(B\) the set of those with \(\mathrm{val}^{s}\leq \frac12\), and \(S\) the enumeration of Lemma 3.13. Compared with Lemma 4.10, the growth hypothesis on a measure is replaced by the semidecidability of the complement of \(B\) — both directions of the specification of \(S\) are used — and nothing about entanglement is required of the compression procedure. The Lean proof reuses the toolkit of Section 4.2: the search branch runs the semidecision procedure through the clocked universal machine, and the start level of the recursion is carried as data next to the current level.