Oracle computations along approximations of the oracle

A construction in stages computes against a moving oracle: at stage s it runs a program against the answers σs s of the current approximation, rather than against the limit oracle σ. This file relates these stage computations to computations against the limit, in both directions.

From the limit to the stages. When the answers converge pointwise, σs s z = σ z for all large s at each address z, a successful run against the limit is eventually a successful run, with the same output and use, against every approximation. The run reads only the finitely many addresses below its use, and these are simultaneously correct from some stage on. Combined with completeness of bounded evaluation, every value of a program relative to the limit oracle is eventually found by the stage computations with growing fuel. For a set enumerated in monotone finite stages, the set-oracle answers of the stages converge to those of the limit set, so this applies to the stage computations Φ_{e,s}^{A_s}(x) (TauCeti.Oracle.Single.Code.converges_setAnswers_stageLimit).

From the stages to the limit. The converse fails without further information: a stage computation may read an address whose answer later changes. It holds when nothing enters the enumeration below the use after the stage of the computation. Then the computation persists, with the same output and use, at every later stage and against the limit set. The priority-method consequences, for requirements that are not injured, are in TauCeti.Computability.Priority.Preservation.

Main results

• TauCeti.Oracle.Single.Code.eventually_evaln_eq_some_of_converges: a successful run against the limit of converging answers is eventually a successful run against the approximations, with the same output and use.
• TauCeti.Oracle.Single.Code.exists_eventually_evaln_eq_some_of_mem_eval: every value of a program relative to the limit oracle is eventually found by the stage computations, with fuel growing along any clock tending to infinity.
• TauCeti.Oracle.Single.Code.converges_setAnswers_stageLimit: under monotone stages, the set-oracle answers of the stages converge to those of the limit set.
• TauCeti.Oracle.Single.Code.exists_eventually_evaln_setAnswers_eq_some_of_mem_eval: a convergent computation relative to the limit of a monotone enumeration is eventually found by the stage computations against the finite stages.
• TauCeti.Oracle.Single.Code.mem_eval_of_eventually_evaln_eq_some: a run with fixed output and use that persists along converging answers is sound for the limit oracle.
• TauCeti.Oracle.Single.Code.evaln_setAnswers_eq_some_of_forall_notMem_fresh, TauCeti.Oracle.Single.Code.evaln_setAnswers_stageLimit_eq_some_of_forall_notMem_fresh: preservation, a stage computation below whose use nothing enters persists at a later stage when nothing enters up to that stage, and against the limit set when nothing ever enters.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapters III.1 and VII.1.

From the limit oracle to the approximations

theorem TauCeti.Oracle.Single.Code.eventually_evaln_eq_some_of_converges {σs : ℕ → ℕ → Option ℕ} {σ : ℕ → Option ℕ} {k n : ℕ} {c : Code} {d : Halt} (hσ : Approximation.Converges σs σ) (h : evaln σ k c n = some d) : ∀ᶠ (s : ℕ) in Filter.atTop, evaln (σs s) k c n = some d

Eventual visibility. If the answers σs s converge pointwise to σ, a successful run against σ is, from some stage on, a successful run with the same fuel, output and use against σs s.

theorem TauCeti.Oracle.Single.Code.eventually_evaln_eq_some_of_converges_of_tendsto {σs : ℕ → ℕ → Option ℕ} {σ : ℕ → Option ℕ} {k n : ℕ} {c : Code} {d : Halt} (hσ : Approximation.Converges σs σ) {t : ℕ → ℕ} (ht : Filter.Tendsto t Filter.atTop Filter.atTop) (h : evaln σ k c n = some d) : ∀ᶠ (s : ℕ) in Filter.atTop, evaln (σs s) (t s) c n = some d

Eventual visibility with growing fuel. If the answers σs s converge pointwise to σ, a successful run against σ is, from some stage on, a successful run with the same output and use against σs s with fuel t s, for any clock t tending to infinity.

theorem TauCeti.Oracle.Single.Code.exists_eventually_evaln_eq_some_of_mem_eval {σs : ℕ → ℕ → Option ℕ} {σ : ℕ → Option ℕ} {n : ℕ} {c : Code} {O : ℕ →. ℕ} (hO : ∀ (z y : ℕ), y ∈ O z → σ z = some y) (hσ : Approximation.Converges σs σ) {t : ℕ → ℕ} (ht : Filter.Tendsto t Filter.atTop Filter.atTop) {y : ℕ} (h : y ∈ eval O c n) : ∃ (d : Halt), d.output = y ∧ ∀ᶠ (s : ℕ) in Filter.atTop, evaln (σs s) (t s) c n = some d

Stage computations find every limit value. Suppose the answers σs s converge pointwise to answers σ that give every value of the oracle O. Every value y of a program relative to O is the output of a single run, with a fixed use, that from some stage on succeeds against σs s with fuel t s, for any clock t tending to infinity.

theorem TauCeti.Oracle.Single.Code.mem_eval_of_eventually_evaln_eq_some {σs : ℕ → ℕ → Option ℕ} {σ : ℕ → Option ℕ} {n : ℕ} {c : Code} {d : Halt} {O : ℕ →. ℕ} {t : ℕ → ℕ} (hO : ∀ (z y : ℕ), σ z = some y → y ∈ O z) (hσ : Approximation.Converges σs σ) (hd : ∀ᶠ (s : ℕ) in Filter.atTop, evaln (σs s) (t s) c n = some d) : d.output ∈ eval O c n

Soundness of a persistent stage run. If the answers converge and a run with a fixed output and use succeeds at all sufficiently large stages, its output belongs to the evaluation against the limit oracle. No monotonicity of the answers or of the simulation clock is needed.

theorem TauCeti.Oracle.Single.Code.converges_setAnswers_stageLimit {A : ℕ → Finset ℕ} (hA : Monotone A) : Approximation.Converges (fun (s : ℕ) => setAnswers ↑(A s)) (setAnswers (Enumeration.stageLimit A))

Under monotone stages, the set-oracle answers of the stages A s converge pointwise to the set-oracle answers of the limit.

theorem TauCeti.Oracle.Single.Code.exists_eventually_evaln_setAnswers_eq_some_of_mem_eval {n : ℕ} {c : Code} {A : ℕ → Finset ℕ} (hA : Monotone A) {t : ℕ → ℕ} (ht : Filter.Tendsto t Filter.atTop Filter.atTop) {y : ℕ} (h : y ∈ eval (Enumeration.stageLimit A).oracle c n) : ∃ (d : Halt), d.output = y ∧ ∀ᶠ (s : ℕ) in Filter.atTop, evaln (setAnswers ↑(A s)) (t s) c n = some d

Stage computations against a monotone enumeration. If a program relative to the set oracle of the limit of monotone finite stages A s has the value y, then a single run with output y and a fixed use succeeds, from some stage on, against the set oracle of A s with fuel t s, for any clock t tending to infinity.

From the approximations to the limit oracle

theorem TauCeti.Oracle.Single.Code.evaln_setAnswers_eq_some_of_forall_notMem_fresh {k n : ℕ} {c : Code} {d : Halt} {A : ℕ → Finset ℕ} {s : ℕ} (hA : Monotone A) (h : evaln (setAnswers ↑(A s)) k c n = some d) {t : ℕ} (hst : s ≤ t) (hfresh : ∀ (t' : ℕ), s ≤ t' → t' < t → ∀ z < d.use, z ∉ Enumeration.fresh A t') : evaln (setAnswers ↑(A t)) k c n = some d

Preservation at later stages. Under monotone stages, if a run against the set oracle of A s succeeds and no number below its use enters from stage s up to a later stage t, then it succeeds with the same output and use against the set oracle of A t.

theorem TauCeti.Oracle.Single.Code.evaln_setAnswers_stageLimit_eq_some_of_forall_notMem_fresh {k n : ℕ} {c : Code} {d : Halt} {A : ℕ → Finset ℕ} {s : ℕ} (hA : Monotone A) (h : evaln (setAnswers ↑(A s)) k c n = some d) (hfresh : ∀ (t : ℕ), s ≤ t → ∀ z < d.use, z ∉ Enumeration.fresh A t) : evaln (setAnswers (Enumeration.stageLimit A)) k c n = some d

Preservation in the limit. Under monotone stages, if a run against the set oracle of A s succeeds and no number below its use enters after stage s, then it succeeds with the same output and use against the set oracle of the limit.