A universal oracle program

This file constructs a universal program TauCeti.Oracle.Single.Code.universal: a single program which, relative to every total oracle O : ℕ → ℕ, computes on the input Nat.pair e x the value of the program numbered e on x. The program is the same for every oracle. This is the uniform form of evaluation: adequacy (TauCeti.Oracle.Single.Code.exists_code) gives, for one fixed oracle, a program for each partial function recursive in it, whereas the universal program works for all oracles at once.

On the input Nat.pair e x, the universal program searches for the least fuel k at which the run of the program numbered e on x against the finite oracle string O 0, …, O (k - 1) succeeds, and returns the output of that run. It gathers the string by querying the oracle, and bounded evaluation against a finite string is primitive recursive. A successful run is correct by the use principle, and every computation relative to O is found at some fuel (TauCeti.Oracle.Single.Code.mem_eval_iff_exists_evaln_range_map).

The construction needs a total oracle: the universal program queries the oracle at every address below the fuel before running anything, so relative to a partial oracle it would diverge at an undefined address that the simulated program never queries.

Main definitions

• TauCeti.Oracle.Single.Code.universal: a universal program.

Main results

• TauCeti.Oracle.Single.Code.eval_universal: the universal program computes the value of the program numbered e on x from Nat.pair e x, relative to every total oracle.
• TauCeti.Oracle.Single.Code.recursiveIn₂_eval: evaluation of programs is recursive in a total oracle, uniformly in the program. This is the oracle-relative form of Mathlib's Nat.Partrec.Code.eval_part.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapter I.3 (the enumeration theorem) and Chapter III.1 (its relativization).

The universal program

noncomputable def TauCeti.Oracle.Single.Code.universal : Code

A universal program: relative to every total oracle O, on the input Nat.pair e x it computes the value of the program numbered e on x.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_universal (O : ℕ → ℕ) (e x : ℕ) : eval (↑O) universal (Nat.pair e x) = eval (↑O) (Denumerable.ofNat Code e) x

Relative to every total oracle, the universal program computes the value of the program numbered e on x from Nat.pair e x.

theorem TauCeti.Oracle.Single.Code.recursiveIn₂_eval (O : ℕ → ℕ) : RecursiveIn₂ {↑O} (eval ↑O)

Evaluation is recursive in a total oracle, uniformly in the program: the function (c, x) ↦ eval O c x is recursive in O.