Stage-bounded oracle evaluation

TauCeti.Oracle.Single.Code.evalStage normalizes raw bounded evaluation to the stage convention of Soare, III.1.7: a successful computation at stage s has program index, input and output strictly below s, and use at most s. Stage zero has no successful computations.

Raw fuel and normalized stages are different: an oracle can return an arbitrarily large number even at small fuel. Normalization delays such a result until the output and program index fit inside the stage bound. It does not alter the output or use. Every successful raw run appears at an explicitly bounded later stage, and successful stage computations persist with the same use when the oracle is fixed. Agreement below the recorded use also permits changing the oracle.

The primitive-recursive certificates include both finite strings (unanswered beyond their length) and binary-coded finite sets (answering zero outside the set). This supplies effective finite stage observations for constructions using oracle computations and restraints.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, III.1.7–9.

def TauCeti.Oracle.Single.Code.evalStage (σ : ℕ → Option ℕ) (s : ℕ) (c : Code) (n : ℕ) : Option Halt

Oracle evaluation at stage s: raw evaluation with fuel s, retaining only computations whose program index and output are below s. Raw evaluation already bounds the input and the use. Failure is none, distinct from a successful computation with use zero.

@[simp]

theorem TauCeti.Oracle.Single.Code.evalStage_eq_some_iff {σ : ℕ → Option ℕ} {s n : ℕ} {c : Code} {d : Halt} : evalStage σ s c n = some d ↔ Encodable.encode c < s ∧ evaln σ s c n = some d ∧ d.output < s

Normalization keeps exactly the raw runs whose program index and output fit the stage.

@[simp]

theorem TauCeti.Oracle.Single.Code.evalStage_zero (σ : ℕ → Option ℕ) (c : Code) (n : ℕ) : evalStage σ 0 c n = none

Stage zero has no successful computations.

theorem TauCeti.Oracle.Single.Code.evalStage_eq_none_of_le_encode {σ : ℕ → Option ℕ} {s n : ℕ} {c : Code} (hs : s ≤ Encodable.encode c) : evalStage σ s c n = none

Programs whose indices are at least the stage have no successful stage computations. This bounds the program indices that a finite-priority search needs to inspect.

theorem TauCeti.Oracle.Single.Code.evalStage_index_lt {σ : ℕ → Option ℕ} {s n : ℕ} {c : Code} {d : Halt} (h : evalStage σ s c n = some d) : Encodable.encode c < s

A successful stage computation has program index below the stage.

theorem TauCeti.Oracle.Single.Code.evalStage_input_lt {σ : ℕ → Option ℕ} {s n : ℕ} {c : Code} {d : Halt} (h : evalStage σ s c n = some d) : n < s

A successful stage computation has input below the stage.

theorem TauCeti.Oracle.Single.Code.evalStage_output_lt {σ : ℕ → Option ℕ} {s n : ℕ} {c : Code} {d : Halt} (h : evalStage σ s c n = some d) : d.output < s

A successful stage computation has output below the stage.

theorem TauCeti.Oracle.Single.Code.evalStage_use_le {σ : ℕ → Option ℕ} {s n : ℕ} {c : Code} {d : Halt} (h : evalStage σ s c n = some d) : d.use ≤ s

A successful stage computation queries only addresses below the stage.

theorem TauCeti.Oracle.Single.Code.evalStage_eq_some_of_evaln {σ : ℕ → Option ℕ} {s k n : ℕ} {c : Code} {d : Halt} (h : evaln σ k c n = some d) (hks : k ≤ s) (hc : Encodable.encode c < s) (hd : d.output < s) : evalStage σ s c n = some d

A raw run is retained at any later stage large enough for its program index and output.

theorem TauCeti.Oracle.Single.Code.evalStage_max_eq_some {σ : ℕ → Option ℕ} {k n : ℕ} {c : Code} {d : Halt} (h : evaln σ k c n = some d) : evalStage σ (max k (max (Encodable.encode c) d.output + 1)) c n = some d

An explicit raw-fuel to stage comparison, preserving both output and use.

theorem TauCeti.Oracle.Single.Code.evalStage_mono {σ : ℕ → Option ℕ} {s t n : ℕ} {c : Code} {d : Halt} (hst : s ≤ t) (h : evalStage σ s c n = some d) : evalStage σ t c n = some d

Successful stage computations persist, with unchanged output and use, for a fixed oracle.

theorem TauCeti.Oracle.Single.Code.evalStage_eq_none_of_le {σ : ℕ → Option ℕ} {s t n : ℕ} {c : Code} (hts : t ≤ s) (h : evalStage σ s c n = none) : evalStage σ t c n = none

Failure at a later stage implies failure at every earlier stage for a fixed oracle.

theorem TauCeti.Oracle.Single.Code.evalStage_unique {σ : ℕ → Option ℕ} {s t n : ℕ} {c : Code} {d d' : Halt} (h : evalStage σ s c n = some d) (h' : evalStage σ t c n = some d') : d = d'

Two successful stage computations against the same oracle have the same output and use.

theorem TauCeti.Oracle.Single.Code.evalStage_eq_some_of_eqOn {σ τ : ℕ → Option ℕ} {s t n : ℕ} {c : Code} {d : Halt} (h : evalStage σ s c n = some d) (hστ : Set.EqOn σ τ (Set.Iio d.use)) (hst : s ≤ t) : evalStage τ t c n = some d

Stage-to-stage use principle: agreement below the recorded use and an increased stage bound preserve both output and use. No persistence is asserted for arbitrary moving oracles.

theorem TauCeti.Oracle.Single.Code.exists_forall_evalStage_eq_some {σ : ℕ → Option ℕ} {k n : ℕ} {c : Code} {d : Halt} (h : evaln σ k c n = some d) : ∃ (s₀ : ℕ), ∀ s ≥ s₀, evalStage σ s c n = some d

Every successful raw run is eventually retained at all normalized stages. The output and recorded use are those of the original run, not merely some run with the same output.

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

A successful normalized computation is sound for every partial oracle containing the supplied answers below its use.

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

Completeness at normalized stages: if all values of an oracle are supplied, every output appears at all sufficiently large stages, with one fixed recorded use.

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

Normalized stages present exactly the partial evaluation when the supplied answers are exactly the values of the oracle.

theorem TauCeti.Oracle.Single.Code.primrec_evalStage {α : Type u_1} [Primcodable α] {σ : α → ℕ → Option ℕ} (hσ : Primrec₂ σ) : Primrec fun (p : α × ℕ × Code × ℕ) => evalStage (σ p.1) p.2.1 p.2.2.1 p.2.2.2

Stage evaluation is primitive recursive uniformly in any primitive-recursive family of finite oracle answers. The normalization tests require no unbounded search.

theorem TauCeti.Oracle.Single.Code.primrec_evalStage_list : Primrec fun (p : List ℕ × ℕ × Code × ℕ) => evalStage (fun (z : ℕ) => p.1[z]?) p.2.1 p.2.2.1 p.2.2.2

Normalized evaluation on finite strings is primitive recursive. Missing answers are not replaced by zero.

theorem TauCeti.Oracle.Single.Code.primrec_evalStage_equivBitIndices : Primrec fun (p : ℕ × ℕ × Code × ℕ) => evalStage (fun (z : ℕ) => some (if z ∈ Finset.equivBitIndices p.1 then 1 else 0)) p.2.1 p.2.2.1 p.2.2.2

Normalized evaluation on binary-coded finite sets, answering zero outside the set, is primitive recursive in the code, the stage, the program and the input.