Documentation

TauCeti.Computability.Priority.Agreement.Basic

Preservation of agreement along a stage enumeration #

In Sacks's constructions a set is enumerated in finite stages A s, and the requirement C ≠ Φ_e^A holds a restraint at least the agreement restraint of Φ_e against the answers of A s (TauCeti.Oracle.Single.Code.setAnswers) with fuel s and the target C s, Soare's r(e, s). This file specializes the preservation theorems of TauCeti.Computability.SingleOracle.Agreement to that setting: a transition that does not injure the requirement keeps the answers at and below the restraint, hence the computations up to and including the length of agreement, and the agreements where the target bit does not change.

It then proves the key step of Sacks's constructions, Soare's Lemma 1 in the proof of Theorem VII.3.1: when the requirement is injured only finitely often, Φ_e^A = C forces C to be computable. If Φ_e^A computes C, the length of agreement eventually exceeds every bound. After the last injury, the computation at x is never lost while C does not change below x, so its output is the value of Φ_e^A at x; by induction on x, the stage C s is then already correct at x. Hence membership in C is decided by searching for a stage after the last injury whose length of agreement exceeds the argument. In a construction, this turns noncomputability of C into the inequality C ≠ Φ_e^A.

Main results #

References #

source
theorem TauCeti.Oracle.Single.Code.eqOn_setAnswers_of_injuriesAt_eq_empty {A : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s b : ℕ} (hA : A s ⊆ A (s + 1)) (hr : r e s = some b) (hI : Priority.injuriesAt A r e s = ∅) :
Set.EqOn (setAnswers ↑(A s)) (setAnswers ↑(A (s + 1))) (Set.Iic b)

If nothing injures requirement e, with active restraint b, in the transition to stage s + 1, and A s ⊆ A (s + 1), then the oracle answers of A s and A (s + 1) agree at and below b.

source
theorem TauCeti.Oracle.Single.Code.evaln_succ_eq_some_of_injuriesAt_eq_empty {A C : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s b x : ℕ} {c : Code} {d : Halt} (hA : A s ⊆ A (s + 1)) (hr : r e s = some b) (hb : agreementRestraint (setAnswers ↑(A s)) s c ((↑(C s)).indicator 1) ≤ b) (hI : Priority.injuriesAt A r e s = ∅) (hx : x ≤ agreementLength (setAnswers ↑(A s)) s c ((↑(C s)).indicator 1)) (hd : evaln (setAnswers ↑(A s)) s c x = some d) :
evaln (setAnswers ↑(A (s + 1))) (s + 1) c x = some d

One-step preservation of computations. Let requirement e hold, at stage s, a restraint b at least the agreement restraint of c against the answers of A s with fuel s and the target C s. If no number injures e in the transition to stage s + 1, and A s ⊆ A (s + 1), then every successful stage-s run at an argument up to and including the length of agreement is a successful stage-s + 1 run, with the same output and use. The target C may change.

source
theorem TauCeti.Oracle.Single.Code.agreesAt_succ_of_injuriesAt_eq_empty {A C : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s b x : ℕ} {c : Code} (hA : A s ⊆ A (s + 1)) (hr : r e s = some b) (hb : agreementRestraint (setAnswers ↑(A s)) s c ((↑(C s)).indicator 1) ≤ b) (hI : Priority.injuriesAt A r e s = ∅) (hx : x < agreementLength (setAnswers ↑(A s)) s c ((↑(C s)).indicator 1)) (hC : x ∈ C (s + 1) ↔ x ∈ C s) :
AgreesAt (setAnswers ↑(A (s + 1))) (s + 1) c ((↑(C (s + 1))).indicator 1) x

One-step preservation of agreement. Under the hypotheses of evaln_succ_eq_some_of_injuriesAt_eq_empty, agreement at an argument below the length of agreement persists to stage s + 1 when membership of that argument in C does not change.

Soare's Lemma 1: a limiting reduction makes the target computable #

source
theorem TauCeti.Oracle.Single.Code.mem_stageLimit_iff_of_lt_agreementLength {A C : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e s x : ℕ} {c : Code} {s₀ : ℕ} (hA : Monotone A) (hC : Monotone C) (hr : ∀ (s : ℕ), s₀ ≤ s → ∃ (b : ℕ), r e s = some b ∧ agreementRestraint (setAnswers ↑(A s)) s c ((↑(C s)).indicator 1) ≤ b) (hI : ∀ (s : ℕ), s₀ ≤ s → Priority.injuriesAt A r e s = ∅) (heval : ∀ y ≤ x, eval (Enumeration.stageLimit A).oracle c y = (Enumeration.stageLimit C).oracle y) (hs : s₀ ≤ s) (hx : x < agreementLength (setAnswers ↑(A s)) s c ((↑(C s)).indicator 1)) :
x ∈ Enumeration.stageLimit C ↔ x ∈ C s

Soare's Lemma 1, correctness of late agreement. Let the program c, relative to the limit of monotone stages A, compute the characteristic function of the limit of monotone stages C at every argument up to and including x. Suppose that from stage s₀ on, requirement e holds a restraint at least the agreement restraint of c against A s with target C s and fuel s, and is never injured. Then at every stage s ≥ s₀ at which x is below the length of agreement, membership of x in C is already decided by C s.

source
theorem TauCeti.Oracle.Single.Code.computablePred_mem_stageLimit_of_eval_eq {A C : ℕ → Finset ℕ} {r : ℕ → ℕ → Option ℕ} {e : ℕ} {c : Code} (hA : Monotone A) (hC : Monotone C) (hAc : Computable fun (s : ℕ) => Finset.equivBitIndices.symm (A s)) (hCc : Computable fun (s : ℕ) => Finset.equivBitIndices.symm (C s)) (hr : ∀ (s : ℕ), ∃ (b : ℕ), r e s = some b ∧ agreementRestraint (setAnswers ↑(A s)) s c ((↑(C s)).indicator 1) ≤ b) (hI : (Priority.injurySet A r e).Finite) (heval : eval (Enumeration.stageLimit A).oracle c = (Enumeration.stageLimit C).oracle) :
ComputablePred fun (x : ℕ) => x ∈ Enumeration.stageLimit C

Soare's Lemma 1. Let A and C be the limits of monotone stages whose binary codes are computable, and let requirement e hold, at every stage s, a restraint at least the agreement restraint of the program c against A s with target C s and fuel s. If only finitely many numbers injure e, and c relative to the limit of A computes the characteristic function of the limit of C, then the limit of C is computable.