Preservation of protected stage computations

In a priority construction, a stage computation Φ_{e,s}^{A_s}(x) persists in the limit when nothing enters the enumeration below its use after stage s (TauCeti.Oracle.Single.Code.evaln_setAnswers_stageLimit_eq_some_of_forall_notMem_fresh). This is the case when the requirement protecting the computation is not injured after that stage, provided its restraint covers the use at every later stage. The covering premise is needed because restraints can drop: once the protected interval no longer contains the use, an entry below the use is not an injury but still changes the computation. An address below the use is covered by an inclusive restraint some b when it is at most b; for use-prefix breaches, which only count entries strictly below the restraint, it must be less than b. A restraint equal to the use covers it in both senses.

Main results

In the namespace TauCeti.Oracle.Single.Code:

• evaln_setAnswers_stageLimit_eq_some_of_injuriesAt_eq_empty, evaln_setAnswers_stageLimit_eq_some_of_injuriesAt_usePrefixRestraint_eq_empty: preservation of a stage computation whose use stays covered by a restraint that is not injured, respectively whose use prefix is not breached.

References

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

theorem TauCeti.Oracle.Single.Code.evaln_setAnswers_stageLimit_eq_some_of_injuriesAt_eq_empty {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {k n s e : ℕ} {c : Code} {d : Halt} (hA : Monotone A) (h : evaln (setAnswers ↑(A s)) k c n = some d) (hr : ∀ (t : ℕ), s ≤ t → ∀ z < d.use, ∃ (b : ℕ), r e t = some b ∧ z ≤ b) (hI : ∀ (t : ℕ), s ≤ t → Priority.injuriesAt A r e t = ∅) : evaln (setAnswers (Enumeration.stageLimit A)) k c n = some d

Preservation under a covering restraint without injury. Under monotone stages, let a run against the set oracle of A s succeed. Suppose that at every later stage requirement e is not injured, and every address below the use of the run lies in its protected interval: the restraint is active, some b, with the address at most b. Then the run succeeds with the same output and use against the set oracle of the limit.

theorem TauCeti.Oracle.Single.Code.evaln_setAnswers_stageLimit_eq_some_of_injuriesAt_usePrefixRestraint_eq_empty {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {k n s e : ℕ} {c : Code} {d : Halt} (hA : Monotone A) (h : evaln (setAnswers ↑(A s)) k c n = some d) (hr : ∀ (t : ℕ), s ≤ t → ∀ z < d.use, ∃ (b : ℕ), r e t = some b ∧ z < b) (hI : ∀ (t : ℕ), s ≤ t → Priority.injuriesAt A (Priority.usePrefixRestraint r) e t = ∅) : evaln (setAnswers (Enumeration.stageLimit A)) k c n = some d

Preservation under a covering restraint without use-prefix breach. Under monotone stages, let a run against the set oracle of A s succeed. Suppose that at every later stage the use prefix of requirement e is not breached, and every address below the use of the run lies strictly below its restraint: the restraint is active, some b, with the address less than b. Then the run succeeds with the same output and use against the set oracle of the limit.