Bounded evaluation of oracle programs, with use

This file defines TauCeti.Oracle.Single.Code.evaln σ k c n, the run of the program c on the input n with fuel k against the oracle answers σ : ℕ → Option ℕ. A successful run records its output together with its use: one more than the largest oracle address it queried, or 0 when it made no query. An answer σ z = none means that no answer is supplied at z, not a negative answer; a run that queries there fails. A finite oracle string l is the case fun z => l[z]?, and a total oracle O : ℕ → ℕ the case fun z => some (O z).

Bounded evaluation follows Mathlib's Nat.Partrec.Code.evaln: at fuel k + 1 a run fails on inputs above k, and the recursions of prec and rfind' consume fuel. Hence a run at fuel k has input below k and queries only addresses below k, so its use is at most k.

Use is what makes oracle computations finitary: a successful run reads only the answers below its use, so it succeeds unchanged against any answers agreeing there, and its output is then a value of the program relative to every oracle extending those answers.

Main definitions

• TauCeti.Oracle.Single.Code.Halt: the output and use of a successful run.
• TauCeti.Oracle.Single.Code.evaln: bounded evaluation against oracle answers.
• TauCeti.Oracle.Single.Code.stageUse: the use of a run, or 0 when it fails.
• TauCeti.Oracle.Single.Code.setAnswers: the answers of the characteristic function of a set.

Main results

• TauCeti.Oracle.Single.Code.evaln_succ_pair_eq_some and its neighbours: the clauses of bounded evaluation, one for each program constructor.
• TauCeti.Oracle.Single.Code.evaln_mono: a successful run persists, with the same output and use, at larger fuel; TauCeti.Oracle.Single.Code.evaln_unique: its output and use do not depend on the fuel.
• TauCeti.Oracle.Single.Code.evaln_bound, TauCeti.Oracle.Single.Code.evaln_use_le: the input and the use of a run at fuel k are below k, respectively at most k.
• TauCeti.Oracle.Single.Code.evaln_eq_some_of_eqOn: the use principle, a run succeeds with the same output and use against answers agreeing below its use.
• TauCeti.Oracle.Single.Code.evaln_sound: the output of a successful run is a value of the program relative to every oracle whose values include the answers below the use.
• TauCeti.Oracle.Single.Code.mem_eval_iff_exists_evaln: when the answers are exactly the values of an oracle, the values of a program relative to that oracle are exactly the outputs of its successful runs.
• TauCeti.Oracle.Single.Code.mem_eval_iff_exists_evaln_range_map: the values of a program relative to a total oracle are exactly the outputs of its successful runs against the finite initial segments of the oracle.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapter III.1, in particular the use principle III.1.9.
• The definition and the proofs of persistence, soundness and completeness follow Mathlib's Nat.Partrec.Code.evaln, Nat.Partrec.Code.evaln_mono, Nat.Partrec.Code.evaln_sound and Nat.Partrec.Code.evaln_complete, extended by the oracle instruction and the use.

structure TauCeti.Oracle.Single.Code.Halt : Type

A successful finite run of a program: its output, and its use, one more than the largest oracle address it queried, or 0 when it made no query.

• output : ℕ

  The output of the run.

• use : ℕ

  One more than the largest address queried, or 0 when the run made no query.

theorem TauCeti.Oracle.Single.Code.Halt.ext_iff {x y : Halt} : x = y ↔ x.output = y.output ∧ x.use = y.use

theorem TauCeti.Oracle.Single.Code.Halt.ext {x y : Halt} (output : x.output = y.output) (use : x.use = y.use) : x = y

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

@[instance_reducible]

instance TauCeti.Oracle.Single.Code.instDecidableEqHalt : DecidableEq Halt

@[irreducible]

def TauCeti.Oracle.Single.Code.evaln (σ : ℕ → Option ℕ) : ℕ → Code → ℕ → Option Halt

Bounded evaluation of a program with fuel k against the oracle answers σ, where σ z = none means that no answer is supplied at z. A successful run returns its output and its use; see TauCeti.Oracle.Single.Code.Halt.

As in Nat.Partrec.Code.evaln, at fuel k + 1 each instruction fails on inputs above k, and the recursive calls of prec and rfind' at the next argument use fuel k. The oracle instruction queries σ at its input n and has use n + 1; the other basic instructions have use 0, and a compound program has the largest use of the runs it makes.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_zero {σ : ℕ → Option ℕ} (c : Code) (n : ℕ) : evaln σ 0 c n = none

Nothing succeeds without fuel.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_succ_zero_eq_some {σ : ℕ → Option ℕ} {k n : ℕ} {d : Halt} : evaln σ (k + 1) zero n = some d ↔ n ≤ k ∧ d = { output := 0, use := 0 }

The zero instruction returns 0 without queries.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_succ_succ_eq_some {σ : ℕ → Option ℕ} {k n : ℕ} {d : Halt} : evaln σ (k + 1) succ n = some d ↔ n ≤ k ∧ d = { output := n + 1, use := 0 }

The succ instruction returns the successor of its input without queries.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_succ_left_eq_some {σ : ℕ → Option ℕ} {k n : ℕ} {d : Halt} : evaln σ (k + 1) left n = some d ↔ n ≤ k ∧ d = { output := (Nat.unpair n).1, use := 0 }

The left instruction returns the first component of its input without queries.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_succ_right_eq_some {σ : ℕ → Option ℕ} {k n : ℕ} {d : Halt} : evaln σ (k + 1) right n = some d ↔ n ≤ k ∧ d = { output := (Nat.unpair n).2, use := 0 }

The right instruction returns the second component of its input without queries.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_succ_oracle_eq_some {σ : ℕ → Option ℕ} {k n : ℕ} {d : Halt} : evaln σ (k + 1) oracle n = some d ↔ n ≤ k ∧ ∃ (y : ℕ), σ n = some y ∧ d = { output := y, use := n + 1 }

The oracle instruction returns the answer at its input n, when one is supplied, with use n + 1.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_succ_pair_eq_some {σ : ℕ → Option ℕ} {k n : ℕ} {d : Halt} {cf cg : Code} : evaln σ (k + 1) (cf.pair cg) n = some d ↔ n ≤ k ∧ ∃ (df : Halt) (dg : Halt), evaln σ (k + 1) cf n = some df ∧ evaln σ (k + 1) cg n = some dg ∧ d = { output := Nat.pair df.output dg.output, use := max df.use dg.use }

pair cf cg pairs the outputs of runs of cf and cg, with the larger of their uses.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_succ_comp_eq_some {σ : ℕ → Option ℕ} {k n : ℕ} {d : Halt} {cf cg : Code} : evaln σ (k + 1) (cf.comp cg) n = some d ↔ n ≤ k ∧ ∃ (dg : Halt) (df : Halt), evaln σ (k + 1) cg n = some dg ∧ evaln σ (k + 1) cf dg.output = some df ∧ d = { output := df.output, use := max dg.use df.use }

comp cf cg runs cg, then cf on its output, with the larger of their uses.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_succ_prec_zero_eq_some {σ : ℕ → Option ℕ} {k : ℕ} {d : Halt} {cf cg : Code} {a : ℕ} : evaln σ (k + 1) (cf.prec cg) (Nat.pair a 0) = some d ↔ Nat.pair a 0 ≤ k ∧ evaln σ (k + 1) cf a = some d

Primitive recursion at zero runs the base program.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_succ_prec_succ_eq_some {σ : ℕ → Option ℕ} {k : ℕ} {d : Halt} {cf cg : Code} {a y : ℕ} : evaln σ (k + 1) (cf.prec cg) (Nat.pair a (y + 1)) = some d ↔ Nat.pair a (y + 1) ≤ k ∧ ∃ (di : Halt) (d' : Halt), evaln σ k (cf.prec cg) (Nat.pair a y) = some di ∧ evaln σ (k + 1) cg (Nat.pair a (Nat.pair y di.output)) = some d' ∧ d = { output := d'.output, use := max di.use d'.use }

Primitive recursion at a successor runs the recursion at the previous argument with one less fuel, then the step program, with the larger of their uses.

@[simp]

theorem TauCeti.Oracle.Single.Code.evaln_succ_rfind'_eq_some {σ : ℕ → Option ℕ} {k : ℕ} {d : Halt} {cf : Code} {a m : ℕ} : evaln σ (k + 1) cf.rfind' (Nat.pair a m) = some d ↔ Nat.pair a m ≤ k ∧ ∃ (dx : Halt), evaln σ (k + 1) cf (Nat.pair a m) = some dx ∧ (dx.output = 0 ∧ d = { output := m, use := dx.use } ∨ dx.output ≠ 0 ∧ ∃ (d' : Halt), evaln σ k cf.rfind' (Nat.pair a (m + 1)) = some d' ∧ d = { output := d'.output, use := max dx.use d'.use })

rfind' cf at m runs cf at m. On output 0 it returns m; otherwise it continues the search at m + 1 with one less fuel. Its use is the largest use of the runs of cf it makes.

theorem TauCeti.Oracle.Single.Code.evaln_bound {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {n : ℕ} {d : Halt} : evaln σ k c n = some d → n < k

A successful run at fuel k has input below k.

theorem TauCeti.Oracle.Single.Code.evaln_eq_none_of_le {σ : ℕ → Option ℕ} {k n : ℕ} {c : Code} (h : k ≤ n) : evaln σ k c n = none

A run at fuel k fails on every input at or above k.

theorem TauCeti.Oracle.Single.Code.evaln_mono {σ : ℕ → Option ℕ} {k₁ k₂ : ℕ} {c : Code} {n : ℕ} {d : Halt} : k₁ ≤ k₂ → evaln σ k₁ c n = some d → evaln σ k₂ c n = some d

Persistence. A successful run persists, with the same output and use, at larger fuel.

theorem TauCeti.Oracle.Single.Code.evaln_unique {σ : ℕ → Option ℕ} {n k₁ k₂ : ℕ} {c : Code} {d₁ d₂ : Halt} (h₁ : evaln σ k₁ c n = some d₁) (h₂ : evaln σ k₂ c n = some d₂) : d₁ = d₂

Uniqueness. Two successful runs of a program on the same input, at any two fuels, have the same output and the same use.

theorem TauCeti.Oracle.Single.Code.evaln_use_le {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {n : ℕ} {d : Halt} : evaln σ k c n = some d → d.use ≤ k

A successful run at fuel k has use at most k: it queries only addresses below k.

def TauCeti.Oracle.Single.Code.stageUse (σ : ℕ → Option ℕ) (k : ℕ) (c : Code) (n : ℕ) : ℕ

The stage use of the run of c on n with fuel k against the answers σ: the use of the run when it succeeds, and 0 when it fails. A successful run can also have use 0, so the stage use does not record whether the run succeeded.

theorem TauCeti.Oracle.Single.Code.stageUse_congr {σ : ℕ → Option ℕ} {k n : ℕ} {τ : ℕ → Option ℕ} {k' : ℕ} {c : Code} (h : evaln σ k c n = evaln τ k' c n) : stageUse σ k c n = stageUse τ k' c n

Equal stage runs have equal stage uses, including when both runs fail.

theorem TauCeti.Oracle.Single.Code.stageUse_eq_of_evaln_eq_some {σ : ℕ → Option ℕ} {k n : ℕ} {d : Halt} {c : Code} (h : evaln σ k c n = some d) : stageUse σ k c n = d.use

The stage use of a successful run is its use.

theorem TauCeti.Oracle.Single.Code.stageUse_eq_zero_of_evaln_eq_none {σ : ℕ → Option ℕ} {k n : ℕ} {c : Code} (h : evaln σ k c n = none) : stageUse σ k c n = 0

The stage use of a failed run is 0.

theorem TauCeti.Oracle.Single.Code.stageUse_le {σ : ℕ → Option ℕ} {k n : ℕ} {c : Code} : stageUse σ k c n ≤ k

The stage use at fuel k is at most k.

noncomputable def TauCeti.Oracle.Single.Code.setAnswers (A : Set ℕ) : ℕ → Option ℕ

The oracle answers of a set A: the values of its characteristic function, supplied at every address.

@[simp]

theorem TauCeti.Oracle.Single.Code.setAnswers_apply (A : Set ℕ) (z : ℕ) : setAnswers A z = some (A.indicator 1 z)

theorem TauCeti.Oracle.Single.Code.eqOn_setAnswers_iff {A B S : Set ℕ} : Set.EqOn (setAnswers A) (setAnswers B) S ↔ ∀ z ∈ S, z ∈ A ↔ z ∈ B

The answers of two sets agree on S exactly when the sets have the same members in S.

theorem TauCeti.Oracle.Single.Code.evaln_eq_some_of_eqOn {σ τ : ℕ → Option ℕ} {k : ℕ} {c : Code} {n : ℕ} {d : Halt} : evaln σ k c n = some d → Set.EqOn σ τ (Set.Iio d.use) → evaln τ k c n = some d

The use principle. A successful run against the answers σ succeeds with the same output and use against any answers τ agreeing with σ below its use.

theorem TauCeti.Oracle.Single.Code.evaln_eq_some_of_use_eq_zero {σ : ℕ → Option ℕ} {k n : ℕ} {d : Halt} (τ : ℕ → Option ℕ) {c : Code} (h : evaln σ k c n = some d) (hd : d.use = 0) : evaln τ k c n = some d

The zero-query case. A successful run with use 0 succeeds with the same output against every oracle answers.

theorem TauCeti.Oracle.Single.Code.evaln_sound {σ : ℕ → Option ℕ} {n : ℕ} {d : Halt} {O : ℕ →. ℕ} {k : ℕ} {c : Code} (h : evaln σ k c n = some d) (hσ : ∀ z < d.use, ∀ (y : ℕ), σ z = some y → y ∈ O z) : d.output ∈ eval O c n

Soundness. If a run against the answers σ succeeds, and every answer σ gives below its use is a value of the oracle O, then the output of the run is a value of the program relative to O. Answers at or above the use are not read, so they need not be correct.

theorem TauCeti.Oracle.Single.Code.exists_evaln_eq_some_of_mem_eval {σ : ℕ → Option ℕ} {n : ℕ} {O : ℕ →. ℕ} (hσ : ∀ (z y : ℕ), y ∈ O z → σ z = some y) {c : Code} {y : ℕ} (h : y ∈ eval O c n) : ∃ (k : ℕ) (d : Halt), evaln σ k c n = some d ∧ d.output = y

Completeness. If the answers σ give every value of the oracle O, every value of a program relative to O is the output of a successful run against σ at some fuel. The answers may go beyond O at addresses where O is undefined.

theorem TauCeti.Oracle.Single.Code.mem_eval_iff_exists_evaln {σ : ℕ → Option ℕ} {n : ℕ} {O : ℕ →. ℕ} (hσ : ∀ (z y : ℕ), σ z = some y ↔ y ∈ O z) {c : Code} {y : ℕ} : y ∈ eval O c n ↔ ∃ (k : ℕ) (d : Halt), evaln σ k c n = some d ∧ d.output = y

Correspondence with evaluation. If the answers σ are exactly the values of the oracle O, the values of a program relative to O are exactly the outputs of its successful runs against σ.

theorem TauCeti.Oracle.Single.Code.evaln_range_map (O : ℕ → ℕ) (k : ℕ) (c : Code) (n : ℕ) : evaln (fun (z : ℕ) => (List.map O (List.range k))[z]?) k c n = evaln (fun (z : ℕ) => some (O z)) k c n

A run with fuel k depends only on the first k answers of a total oracle. Truncating that oracle to a string of length k preserves failure as well as output and use.

theorem TauCeti.Oracle.Single.Code.mem_eval_iff_exists_evaln_range_map {O : ℕ → ℕ} {c : Code} {n y : ℕ} : y ∈ eval (↑O) c n ↔ ∃ (k : ℕ) (d : Halt), evaln (fun (z : ℕ) => (List.map O (List.range k))[z]?) k c n = some d ∧ d.output = y

Evaluation through finite initial segments. For a total oracle O, the values of a program relative to O are exactly the outputs of its successful runs, at some fuel k, against the finite oracle string O 0, …, O (k - 1).