Programs with one oracle

This file defines TauCeti.Oracle.Single.Code, the programs of partial recursive functions with access to a single oracle. They are Mathlib's codes Nat.Partrec.Code with one more basic instruction, oracle, which queries the oracle at its input. Programs are numbered by an explicit bijection with ℕ, and TauCeti.Oracle.Single.Code.eval O c interprets the program c as a partial function relative to an oracle O : ℕ →. ℕ. A total oracle O : ℕ → ℕ is the case fun n => Part.some (O n), and a set oracle is the case of its characteristic function.

The main result is adequacy: for every oracle O, the partial functions computed by programs relative to O are exactly Mathlib's Nat.RecursiveIn {O} functions. The direction from programs to Nat.RecursiveIn transfers algorithms written as programs to Mathlib's notion; the direction from Nat.RecursiveIn to programs transfers statements quantifying over all programs, such as non-reducibility, back to Mathlib's notion. In particular f is Turing reducible to g exactly when some program computes f relative to g.

This adequacy is extensional: it is a statement about one fixed oracle, and does not choose a program uniformly in the oracle.

Main definitions

• TauCeti.Oracle.Single.Code: programs with one oracle.
• TauCeti.Oracle.Single.Code.encodeCode, TauCeti.Oracle.Single.Code.ofNatCode: the numbering of programs and its inverse, packaged as a Denumerable instance.
• TauCeti.Oracle.Single.Code.eval: the partial function computed by a program relative to an oracle.
• Nat.Partrec.Code.toSingleOracleCode: the query-free program of an ordinary Mathlib code.

Main results

• TauCeti.Oracle.Single.Code.primrec₂_pair and its neighbours: the program constructors are primitive recursive on numbers of programs.
• TauCeti.Oracle.Single.Code.encode_lt_pair and its neighbours: the components of a compound program have smaller numbers.
• TauCeti.Oracle.Single.Code.primrec_casesOn: case analysis on programs is primitive recursive.
• TauCeti.Oracle.Single.Code.mem_eval_pair, TauCeti.Oracle.Single.Code.mem_eval_rfind': the values of a pairing, and one step of a search.
• TauCeti.Oracle.Single.Code.eval_toSingleOracleCode: a query-free program computes the same function as the ordinary code it comes from, relative to every oracle.
• TauCeti.Oracle.Single.Code.exists_forall_eval_eq_of_partrec: every partial recursive function is computed by one program relative to every oracle.
• TauCeti.Oracle.Single.Code.exists_code: adequacy, Nat.RecursiveIn {O} f ↔ ∃ c, eval O c = f.
• TauCeti.Oracle.Single.Code.turingReducible_iff_exists_code: the same for Turing reducibility.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapter III.1.
• M. Carneiro, Formalizing computability theory via partial recursive functions, ITP 2019. The numbering, the evaluation and the adequacy proof follow Mathlib's Nat.Partrec.Code, Nat.Partrec.Code.eval and Nat.Partrec.Code.exists_code, extended by the oracle instruction.
• The namespace and constructors follow the shape of the single-oracle code proposed by Edwin Park in Mathlib pull request 38973.

inductive TauCeti.Oracle.Single.Code : Type

Programs of partial recursive functions with access to one oracle. They are Mathlib's codes Nat.Partrec.Code together with the instruction oracle, which queries the oracle at its input. See TauCeti.Oracle.Single.Code.eval for the interpretation of the constructors.

• zero : Code
• succ : Code
• left : Code
• right : Code
• oracle : Code
• pair : Code → Code → Code
• comp : Code → Code → Code
• prec : Code → Code → Code
• rfind' : Code → Code

@[instance_reducible]

instance TauCeti.Oracle.Single.instDecidableEqCode : DecidableEq Code

def TauCeti.Oracle.Single.instDecidableEqCode.decEq (x✝ x✝¹ : Code) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TauCeti.Oracle.Single.Code.instInhabited : Inhabited Code

Numbering programs

def TauCeti.Oracle.Single.Code.encodeCode : Code → ℕ

The number of a program: the five basic instructions are 0, …, 4, and a compound program is 4 * k + i + 5, where k codes its components and i < 4 its constructor.

@[irreducible]

def TauCeti.Oracle.Single.Code.ofNatCode : ℕ → Code

The program with a given number, the inverse of TauCeti.Oracle.Single.Code.encodeCode.

@[simp]

theorem TauCeti.Oracle.Single.Code.encodeCode_ofNatCode (n : ℕ) : (ofNatCode n).encodeCode = n

Decoding a number and encoding the result gives the number back.

@[simp]

theorem TauCeti.Oracle.Single.Code.ofNatCode_encodeCode (c : Code) : ofNatCode c.encodeCode = c

Encoding a program and decoding the result gives the program back.

@[instance_reducible]

instance TauCeti.Oracle.Single.Code.instDenumerable : Denumerable Code

theorem TauCeti.Oracle.Single.Code.encodeCode_eq : Encodable.encode = encodeCode

The Denumerable encoding of programs is TauCeti.Oracle.Single.Code.encodeCode.

theorem TauCeti.Oracle.Single.Code.ofNatCode_eq : Denumerable.ofNat Code = ofNatCode

The Denumerable decoding of programs is TauCeti.Oracle.Single.Code.ofNatCode.

theorem TauCeti.Oracle.Single.Code.encode_lt_pair (cf cg : Code) : Encodable.encode cf < Encodable.encode (cf.pair cg) ∧ Encodable.encode cg < Encodable.encode (cf.pair cg)

The components of a pairing have smaller numbers.

theorem TauCeti.Oracle.Single.Code.encode_lt_comp (cf cg : Code) : Encodable.encode cf < Encodable.encode (cf.comp cg) ∧ Encodable.encode cg < Encodable.encode (cf.comp cg)

The components of a composition have smaller numbers.

theorem TauCeti.Oracle.Single.Code.encode_lt_prec (cf cg : Code) : Encodable.encode cf < Encodable.encode (cf.prec cg) ∧ Encodable.encode cg < Encodable.encode (cf.prec cg)

The components of a primitive recursion have smaller numbers.

theorem TauCeti.Oracle.Single.Code.encode_lt_rfind' (cf : Code) : Encodable.encode cf < Encodable.encode cf.rfind'

The component of a search has a smaller number.

Primitive recursive constructors

theorem TauCeti.Oracle.Single.Code.primrec₂_pair : Primrec₂ pair

Pairing programs is primitive recursive.

theorem TauCeti.Oracle.Single.Code.primrec₂_comp : Primrec₂ comp

Composing programs is primitive recursive.

theorem TauCeti.Oracle.Single.Code.primrec₂_prec : Primrec₂ prec

Forming the primitive recursion of two programs is primitive recursive.

theorem TauCeti.Oracle.Single.Code.primrec_rfind' : Primrec rfind'

Forming the search program of a program is primitive recursive.

theorem TauCeti.Oracle.Single.Code.primrec_casesOn {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] {c : α → Code} (hc : Primrec c) {z s l r o : α → σ} (hz : Primrec z) (hs : Primrec s) (hl : Primrec l) (hr : Primrec r) (ho : Primrec o) {pr co pc : α → Code × Code → σ} (hpr : Primrec₂ pr) (hco : Primrec₂ co) (hpc : Primrec₂ pc) {rf : α → Code → σ} (hrf : Primrec₂ rf) : Primrec fun (a : α) => casesOn (c a) (z a) (s a) (l a) (r a) (o a) (fun (cf cg : Code) => pr a (cf, cg)) (fun (cf cg : Code) => co a (cf, cg)) (fun (cf cg : Code) => pc a (cf, cg)) (rf a)

Case analysis on programs is primitive recursive, uniformly in a parameter: the branch taken is read off the number of the program, and the branches receive its components.

Evaluation

def TauCeti.Oracle.Single.Code.eval (O : ℕ →. ℕ) : Code → ℕ →. ℕ

The partial function computed by a program relative to the oracle O.

• zero, succ, left, right: zero, successor, and the two components of Nat.unpair.
• oracle: the oracle O itself, queried at the input.
• pair cf cg: pairs the outputs of cf and cg with Nat.pair.
• comp cf cg: runs cg, then cf on its output.
• prec cf cg: primitive recursion. On input Nat.pair a 0 it returns the output of cf on a, and on Nat.pair a (k + 1) the output of cg on Nat.pair a (Nat.pair k i), where i is the output of prec cf cg on Nat.pair a k.
• rfind' cf: search from a start. On input Nat.pair a m it returns the least n ≥ m with output 0 from cf on Nat.pair a n, provided cf halts on Nat.pair a k for every k from m to n.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_zero {O : ℕ →. ℕ} (n : ℕ) : eval O zero n = Part.some 0

The zero instruction returns 0.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_succ {O : ℕ →. ℕ} (n : ℕ) : eval O succ n = Part.some (n + 1)

The succ instruction returns the successor of its input.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_left {O : ℕ →. ℕ} (n : ℕ) : eval O left n = Part.some (Nat.unpair n).1

The left instruction returns the first component of its unpaired input.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_right {O : ℕ →. ℕ} (n : ℕ) : eval O right n = Part.some (Nat.unpair n).2

The right instruction returns the second component of its unpaired input.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_oracle {O : ℕ →. ℕ} : eval O oracle = O

The oracle instruction computes the oracle.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_pair {O : ℕ →. ℕ} (cf cg : Code) (n : ℕ) : eval O (cf.pair cg) n = Nat.pair <$> eval O cf n <*> eval O cg n

pair cf cg pairs the outputs of cf and cg.

theorem TauCeti.Oracle.Single.Code.mem_eval_pair {O : ℕ →. ℕ} {cf cg : Code} {n y : ℕ} : y ∈ eval O (cf.pair cg) n ↔ ∃ y₁ ∈ eval O cf n, ∃ y₂ ∈ eval O cg n, Nat.pair y₁ y₂ = y

The outputs of pair cf cg are the pairings of outputs of cf and cg.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_comp {O : ℕ →. ℕ} (cf cg : Code) (n : ℕ) : eval O (cf.comp cg) n = eval O cg n >>= eval O cf

comp cf cg runs cg, then cf on its output.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_prec_zero {O : ℕ →. ℕ} (cf cg : Code) (a : ℕ) : eval O (cf.prec cg) (Nat.pair a 0) = eval O cf a

Primitive recursion at zero.

theorem TauCeti.Oracle.Single.Code.eval_prec_succ {O : ℕ →. ℕ} (cf cg : Code) (a k : ℕ) : eval O (cf.prec cg) (Nat.pair a (k + 1)) = do let i ← eval O (cf.prec cg) (Nat.pair a k) eval O cg (Nat.pair a (Nat.pair k i))

Primitive recursion at a successor.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_rfind' {O : ℕ →. ℕ} (cf : Code) (a m : ℕ) : eval O cf.rfind' (Nat.pair a m) = Part.map (fun (x : ℕ) => x + m) (Nat.rfind fun (n : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> eval O cf (Nat.pair a (n + m)))

rfind' cf on Nat.pair a m searches for the least n ≥ m with output 0 from cf on Nat.pair a n.

theorem TauCeti.Oracle.Single.Code.mem_eval_rfind' {O : ℕ →. ℕ} {cf : Code} {a m y : ℕ} : y ∈ eval O cf.rfind' (Nat.pair a m) ↔ ∃ x ∈ eval O cf (Nat.pair a m), x = 0 ∧ y = m ∨ x ≠ 0 ∧ y ∈ eval O cf.rfind' (Nat.pair a (m + 1))

One step of the search of rfind' cf from m: the search returns m when cf outputs 0 at m, and otherwise, when cf halts at m with a nonzero output, continues from m + 1.

theorem TauCeti.Oracle.Single.Code.le_of_mem_eval_rfind' {O : ℕ →. ℕ} {cf : Code} {a m y : ℕ} (h : y ∈ eval O cf.rfind' (Nat.pair a m)) : m ≤ y

The search of rfind' cf from m returns a number at least m.

Adequacy

theorem TauCeti.Oracle.Single.Code.recursiveIn_eval (O : ℕ →. ℕ) (c : Code) : Nat.RecursiveIn {O} (eval O c)

Every program computes a function recursive in its oracle.

theorem TauCeti.Oracle.Single.Code.exists_code_of_recursiveIn {O f : ℕ →. ℕ} (hf : Nat.RecursiveIn {O} f) : ∃ (c : Code), eval O c = f

Every function recursive in O is computed by a program relative to O.

theorem TauCeti.Oracle.Single.Code.exists_code {O f : ℕ →. ℕ} : Nat.RecursiveIn {O} f ↔ ∃ (c : Code), eval O c = f

Adequacy. For every oracle O, a partial function is recursive in O exactly when some program computes it relative to O.

theorem TauCeti.Oracle.Single.Code.turingReducible_iff_exists_code {f g : ℕ →. ℕ} : TuringReducible f g ↔ ∃ (c : Code), eval g c = f

Adequacy for Turing reducibility. f is Turing reducible to g exactly when some program computes f relative to the oracle g.

Query-free programs

def Nat.Partrec.Code.toSingleOracleCode : Code → TauCeti.Oracle.Single.Code

The query-free program of an ordinary Mathlib code: the same code, never using oracle.

theorem Nat.Partrec.Code.toSingleOracleCode_injective : Function.Injective toSingleOracleCode

Nat.Partrec.Code.toSingleOracleCode is injective: distinct ordinary codes give distinct programs.

theorem Nat.Partrec.Code.primrec_toSingleOracleCode : Primrec toSingleOracleCode

The translation of ordinary codes into query-free programs is primitive recursive.

@[simp]

theorem TauCeti.Oracle.Single.Code.eval_toSingleOracleCode (O : ℕ →. ℕ) (c : Nat.Partrec.Code) : eval O c.toSingleOracleCode = c.eval

Query-free programs. Relative to every oracle, the program c.toSingleOracleCode computes the same function as the ordinary code c.

theorem TauCeti.Oracle.Single.Code.exists_forall_eval_eq_of_partrec {f : ℕ →. ℕ} (hf : Nat.Partrec f) : ∃ (c : Code), ∀ (O : ℕ →. ℕ), eval O c = f

Every partial recursive function is computed by one program relative to every oracle: the query-free program of an ordinary code computing it.