Documentation

TauCeti.Computability.SingleOracle.Agreement

Length of agreement and its restraint #

Run a program c with fuel k against oracle answers σ, and compare it with a target function g : ℕ → ℕ. The run agrees with g at x when it succeeds there with output g x. The length of agreement is the first argument at which the run does not agree with g: either it fails there, or it succeeds with another output. A run at fuel k fails on every input at or above k, so the length of agreement is at most k.

The agreement restraint is the largest stage use (TauCeti.Oracle.Single.Code.stageUse) of the runs at the arguments up to and including the length of agreement, a failed run counting as use 0. Including the first disagreement protects a run that succeeds there with a wrong output, as well as the agreeing runs below it.

In Sacks's constructions the answers are those of the stage A s of a set being built, the fuel is the stage s, and the target is the characteristic function of the stage C s of a c.e. set. Then the length of agreement and the agreement restraint are Soare's ℓ(e, s) and r(e, s) for the requirement C ≠ Φ_e^A, and the restraint protects the numbers up to r(e, s), inclusive.

Preservation #

If the answers do not change at or below the agreement restraint, every successful run at an argument up to and including the length of agreement succeeds again with the same output and use at any larger fuel. This needs no hypothesis on the target. If in addition the target does not change below the length of agreement, the agreement there persists, so neither the length of agreement nor the restraint decreases. On an interval of stages where both conditions hold at every step, the computations, the length of agreement and the restraint therefore all persist.

Absence of injury alone is not enough to iterate: a change of the target at a small argument can shorten the length of agreement, so that the next restraint no longer covers the use of a computation at a larger argument. What does iterate is a fixed prefix: if the target does not change below n and n is at most the length of agreement, then it stays so, and the computations up to and including n persist.

Effectivity #

The length of agreement and the agreement restraint are primitive recursive in the fuel and the program, uniformly in a parameter on which the answers and the target depend primitive recursively. In particular they are primitive recursive in the binary codes of a finite stage A s and a finite target stage C s, which makes them usable in computable stage constructions.

Limits of stages #

When the answers and the target are the stages A s and C s of monotone enumerations, run with fuel s, and the program computes the limit of C relative to the limit of A below n, the use principle makes the length of agreement eventually at least n.

Main definitions #

Main results #

References #

Agreement and its length #

source
def TauCeti.Oracle.Single.Code.AgreesAt (σ : ℕ → Option ℕ) (k : ℕ) (c : Code) (g : ℕ → ℕ) (x : ℕ) :
Prop

The run of c on x with fuel k against the answers σ agrees with the target g at x when it succeeds with output g x.

Instances For
    source
    @[instance_reducible]
    instance TauCeti.Oracle.Single.Code.instDecidablePredNatAgreesAt (σ : ℕ → Option ℕ) (k : ℕ) (c : Code) (g : ℕ → ℕ) :
    DecidablePred (AgreesAt σ k c g)
    source
    theorem TauCeti.Oracle.Single.Code.agreesAt_iff {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} {x : ℕ} :
    AgreesAt σ k c g x ↔ ∃ (d : Halt), evaln σ k c x = some d ∧ d.output = g x

    A run agrees with the target when it succeeds with the target value.

    source
    theorem TauCeti.Oracle.Single.Code.agreesAt_iff_of_evaln_eq_some {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} {x : ℕ} {d : Halt} (h : evaln σ k c x = some d) :
    AgreesAt σ k c g x ↔ d.output = g x

    A successful run agrees with the target exactly when its output is the target value.

    source
    theorem TauCeti.Oracle.Single.Code.not_agreesAt_of_evaln_eq_none {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} {x : ℕ} (h : evaln σ k c x = none) :
    ¬AgreesAt σ k c g x

    A failed run does not agree with the target.

    source
    theorem TauCeti.Oracle.Single.Code.not_agreesAt_of_le {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} {x : ℕ} (h : k ≤ x) :
    ¬AgreesAt σ k c g x

    No run agrees with the target at an argument at or above its fuel.

    source
    def TauCeti.Oracle.Single.Code.agreementLength (σ : ℕ → Option ℕ) (k : ℕ) (c : Code) (g : ℕ → ℕ) :
    ℕ

    The length of agreement: the first argument at which the run of c with fuel k against the answers σ does not agree with the target g. It is at most k.

    Instances For
      source
      theorem TauCeti.Oracle.Single.Code.agreementLength_eq_iff {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} {n : ℕ} :
      agreementLength σ k c g = n ↔ ¬AgreesAt σ k c g n ∧ ∀ x < n, AgreesAt σ k c g x

      The length of agreement is the first argument without agreement.

      source
      theorem TauCeti.Oracle.Single.Code.le_agreementLength_iff {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} {n : ℕ} :
      n ≤ agreementLength σ k c g ↔ ∀ x < n, AgreesAt σ k c g x

      The run agrees with the target below n exactly when n is at most the length of agreement.

      source
      theorem TauCeti.Oracle.Single.Code.agreesAt_of_lt_agreementLength {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} {x : ℕ} (hx : x < agreementLength σ k c g) :
      AgreesAt σ k c g x

      The run agrees with the target below the length of agreement.

      source
      theorem TauCeti.Oracle.Single.Code.not_agreesAt_agreementLength {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} :
      ¬AgreesAt σ k c g (agreementLength σ k c g)

      The run does not agree with the target at the length of agreement.

      source
      theorem TauCeti.Oracle.Single.Code.agreementLength_le {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} :
      agreementLength σ k c g ≤ k

      The length of agreement is at most the fuel.

      The agreement restraint #

      source
      def TauCeti.Oracle.Single.Code.agreementRestraint (σ : ℕ → Option ℕ) (k : ℕ) (c : Code) (g : ℕ → ℕ) :
      ℕ

      The agreement restraint: the largest stage use of the runs of c with fuel k against the answers σ at the arguments up to and including the length of agreement with g. A failed run counts as use 0.

      Instances For
        source
        theorem TauCeti.Oracle.Single.Code.agreementRestraint_def (σ : ℕ → Option ℕ) (k : ℕ) (c : Code) (g : ℕ → ℕ) :
        agreementRestraint σ k c g = (Finset.range (agreementLength σ k c g + 1)).sup (stageUse σ k c)

        The agreement restraint is the finite maximum of the uses, including the run at the first disagreement.

        source
        theorem TauCeti.Oracle.Single.Code.agreementRestraint_eq_of_evaln_eq {σ τ : ℕ → Option ℕ} {k k' : ℕ} {c : Code} {g g' : ℕ → ℕ} (hlength : agreementLength σ k c g = agreementLength τ k' c g') (hruns : ∀ x ≤ agreementLength σ k c g, evaln σ k c x = evaln τ k' c x) :
        agreementRestraint σ k c g = agreementRestraint τ k' c g'

        Equal agreement lengths and equal runs up to and including that length give equal agreement restraints. The targets may differ.

        source
        theorem TauCeti.Oracle.Single.Code.agreementRestraint_le_iff {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} {b : ℕ} :
        agreementRestraint σ k c g ≤ b ↔ ∀ x ≤ agreementLength σ k c g, stageUse σ k c x ≤ b

        The agreement restraint is at most b exactly when every stage use up to and including the length of agreement is.

        source
        theorem TauCeti.Oracle.Single.Code.stageUse_le_agreementRestraint {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} {x : ℕ} (hx : x ≤ agreementLength σ k c g) :
        stageUse σ k c x ≤ agreementRestraint σ k c g

        Every stage use up to and including the length of agreement is at most the agreement restraint.

        source
        theorem TauCeti.Oracle.Single.Code.use_le_agreementRestraint {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} {x : ℕ} {d : Halt} (hx : x ≤ agreementLength σ k c g) (hd : evaln σ k c x = some d) :
        d.use ≤ agreementRestraint σ k c g

        The use of a successful run up to and including the length of agreement is at most the agreement restraint.

        source
        theorem TauCeti.Oracle.Single.Code.agreementRestraint_le {σ : ℕ → Option ℕ} {k : ℕ} {c : Code} {g : ℕ → ℕ} :
        agreementRestraint σ k c g ≤ k

        The agreement restraint is at most the fuel.

        Preservation #

        source
        theorem TauCeti.Oracle.Single.Code.evaln_eq_some_of_eqOn_agreementRestraint {σ τ : ℕ → Option ℕ} {k k' : ℕ} {c : Code} {g : ℕ → ℕ} {x : ℕ} {d : Halt} (hk : k ≤ k') (hστ : Set.EqOn σ τ (Set.Iic (agreementRestraint σ k c g))) (hx : x ≤ agreementLength σ k c g) (hd : evaln σ k c x = some d) :
        evaln τ k' c x = some d

        Preservation of computations. A successful run at an argument up to and including the length of agreement succeeds with the same output and use at any larger fuel, against any answers that agree with σ at and below the agreement restraint. Nothing is assumed about the target.

        source
        theorem TauCeti.Oracle.Single.Code.agreesAt_of_eqOn_agreementRestraint {σ τ : ℕ → Option ℕ} {k k' : ℕ} {c : Code} {g g' : ℕ → ℕ} {x : ℕ} (hk : k ≤ k') (hστ : Set.EqOn σ τ (Set.Iic (agreementRestraint σ k c g))) (hx : x < agreementLength σ k c g) (hg : g' x = g x) :
        AgreesAt τ k' c g' x

        Preservation of agreement. Under the hypotheses of evaln_eq_some_of_eqOn_agreementRestraint, agreement below the length of agreement persists when the target value there does not change.

        source
        theorem TauCeti.Oracle.Single.Code.agreementLength_le_of_eqOn_agreementRestraint {σ τ : ℕ → Option ℕ} {k k' : ℕ} {c : Code} {g g' : ℕ → ℕ} (hk : k ≤ k') (hστ : Set.EqOn σ τ (Set.Iic (agreementRestraint σ k c g))) (hg : ∀ x < agreementLength σ k c g, g' x = g x) :
        agreementLength σ k c g ≤ agreementLength τ k' c g'

        The length of agreement does not decrease when the fuel does not decrease, the answers do not change at or below the agreement restraint, and the target does not change below the length of agreement.

        source
        theorem TauCeti.Oracle.Single.Code.agreementRestraint_le_of_eqOn_agreementRestraint {σ τ : ℕ → Option ℕ} {k k' : ℕ} {c : Code} {g g' : ℕ → ℕ} (hk : k ≤ k') (hστ : Set.EqOn σ τ (Set.Iic (agreementRestraint σ k c g))) (hg : ∀ x < agreementLength σ k c g, g' x = g x) :
        agreementRestraint σ k c g ≤ agreementRestraint τ k' c g'

        Under the hypotheses of agreementLength_le_of_eqOn_agreementRestraint, the agreement restraint does not decrease either: every run it accounts for is preserved, at an argument still up to and including the new length of agreement.

        Preservation along an interval of stages #

        source
        theorem TauCeti.Oracle.Single.Code.agreementLength_le_of_forall_Ico {c : Code} {σ : ℕ → ℕ → Option ℕ} {g : ℕ → ℕ → ℕ} {s t : ℕ} (hst : s ≤ t) (h : ∀ u ∈ Set.Ico s t, Set.EqOn (σ u) (σ (u + 1)) (Set.Iic (agreementRestraint (σ u) u c (g u))) ∧ ∀ x < agreementLength (σ u) u c (g u), g (u + 1) x = g u x) :
        agreementLength (σ s) s c (g s) ≤ agreementLength (σ t) t c (g t)

        Along stages σ u, g u run with fuel u, the length of agreement does not decrease on an interval of stages where, at every step, the answers do not change at or below the agreement restraint and the target does not change below the length of agreement.

        source
        theorem TauCeti.Oracle.Single.Code.agreementRestraint_le_of_forall_Ico {c : Code} {σ : ℕ → ℕ → Option ℕ} {g : ℕ → ℕ → ℕ} {s t : ℕ} (hst : s ≤ t) (h : ∀ u ∈ Set.Ico s t, Set.EqOn (σ u) (σ (u + 1)) (Set.Iic (agreementRestraint (σ u) u c (g u))) ∧ ∀ x < agreementLength (σ u) u c (g u), g (u + 1) x = g u x) :
        agreementRestraint (σ s) s c (g s) ≤ agreementRestraint (σ t) t c (g t)

        Under the hypotheses of agreementLength_le_of_forall_Ico, the agreement restraint does not decrease on the interval.

        source
        theorem TauCeti.Oracle.Single.Code.le_agreementLength_of_forall_Ico {c : Code} {σ : ℕ → ℕ → Option ℕ} {g : ℕ → ℕ → ℕ} {s t n : ℕ} (hst : s ≤ t) (h : ∀ u ∈ Set.Ico s t, Set.EqOn (σ u) (σ (u + 1)) (Set.Iic (agreementRestraint (σ u) u c (g u))) ∧ ∀ x < n, g (u + 1) x = g u x) (hn : n ≤ agreementLength (σ s) s c (g s)) :
        n ≤ agreementLength (σ t) t c (g t)

        Persistence of a prefix of agreement. Along stages σ u, g u run with fuel u, if the run agrees with the target below n at stage s, it still does at stage t, provided that at every step in between the answers do not change at or below the agreement restraint and the target does not change below n. The target may change at and above n.

        source
        theorem TauCeti.Oracle.Single.Code.evaln_eq_some_of_forall_Ico_of_le {c : Code} {x : ℕ} {d : Halt} {σ : ℕ → ℕ → Option ℕ} {g : ℕ → ℕ → ℕ} {s t n : ℕ} (hst : s ≤ t) (h : ∀ u ∈ Set.Ico s t, Set.EqOn (σ u) (σ (u + 1)) (Set.Iic (agreementRestraint (σ u) u c (g u))) ∧ ∀ x < n, g (u + 1) x = g u x) (hn : n ≤ agreementLength (σ s) s c (g s)) (hx : x ≤ n) (hd : evaln (σ s) s c x = some d) :
        evaln (σ t) t c x = some d

        Preservation on an interval of stages, below a fixed prefix. Under the hypotheses of le_agreementLength_of_forall_Ico, a successful run at stage s at an argument up to and including n is a successful run at stage t, with the same output and use.

        source
        theorem TauCeti.Oracle.Single.Code.evaln_eq_some_of_forall_Ico {c : Code} {x : ℕ} {d : Halt} {σ : ℕ → ℕ → Option ℕ} {g : ℕ → ℕ → ℕ} {s t : ℕ} (hst : s ≤ t) (h : ∀ u ∈ Set.Ico s t, Set.EqOn (σ u) (σ (u + 1)) (Set.Iic (agreementRestraint (σ u) u c (g u))) ∧ ∀ x < agreementLength (σ u) u c (g u), g (u + 1) x = g u x) (hx : x ≤ agreementLength (σ s) s c (g s)) (hd : evaln (σ s) s c x = some d) :
        evaln (σ t) t c x = some d

        Preservation on an interval of stages. Under the hypotheses of agreementLength_le_of_forall_Ico, a successful run at stage s at an argument up to and including the length of agreement is a successful run at stage t, with the same output and use.

        Primitive recursiveness #

        source
        theorem TauCeti.Oracle.Single.Code.primrecPred_agreesAt {α : Type u_1} [Primcodable α] {σ : α → ℕ → Option ℕ} {g : α → ℕ → ℕ} (hσ : Primrec₂ σ) (hg : Primrec₂ g) :
        PrimrecPred fun (p : (α × ℕ × Code) × ℕ) => AgreesAt (σ p.1.1) p.1.2.1 p.1.2.2 (g p.1.1) p.2

        Agreement is primitive recursive, uniformly in a parameter a on which the answers σ a and the target g a depend primitive recursively, and in the fuel, the program and the argument.

        source
        theorem TauCeti.Oracle.Single.Code.primrec_agreementLength {α : Type u_1} [Primcodable α] {σ : α → ℕ → Option ℕ} {g : α → ℕ → ℕ} (hσ : Primrec₂ σ) (hg : Primrec₂ g) :
        Primrec fun (p : α × ℕ × Code) => agreementLength (σ p.1) p.2.1 p.2.2 (g p.1)

        The length of agreement is primitive recursive, uniformly in a parameter a on which the answers σ a and the target g a depend primitive recursively, and in the fuel and the program.

        source
        theorem TauCeti.Oracle.Single.Code.primrec_agreementRestraint {α : Type u_1} [Primcodable α] {σ : α → ℕ → Option ℕ} {g : α → ℕ → ℕ} (hσ : Primrec₂ σ) (hg : Primrec₂ g) :
        Primrec fun (p : α × ℕ × Code) => agreementRestraint (σ p.1) p.2.1 p.2.2 (g p.1)

        The agreement restraint is primitive recursive, uniformly in a parameter a on which the answers σ a and the target g a depend primitive recursively, and in the fuel and the program.

        source
        theorem TauCeti.Oracle.Single.Code.primrec_agreementLength_equivBitIndices :
        Primrec fun (p : (ℕ × ℕ) × ℕ × Code) => agreementLength (setAnswers ↑(Finset.equivBitIndices p.1.1)) p.2.1 p.2.2 ((↑(Finset.equivBitIndices p.1.2)).indicator 1)

        The length of agreement of a run against a finite set, with a finite set as target, is primitive recursive in their binary codes, the fuel and the program.

        source
        theorem TauCeti.Oracle.Single.Code.primrec_agreementRestraint_equivBitIndices :
        Primrec fun (p : (ℕ × ℕ) × ℕ × Code) => agreementRestraint (setAnswers ↑(Finset.equivBitIndices p.1.1)) p.2.1 p.2.2 ((↑(Finset.equivBitIndices p.1.2)).indicator 1)

        The agreement restraint of a run against a finite set, with a finite set as target, is primitive recursive in their binary codes, the fuel and the program.

        Limits of stages #

        source
        theorem TauCeti.Oracle.Single.Code.eventually_le_agreementLength_of_eval_eq {c : Code} {A C : ℕ → Finset ℕ} (hA : Monotone A) (hC : Monotone C) {n : ℕ} (heval : ∀ x < n, eval (Enumeration.stageLimit A).oracle c x = (Enumeration.stageLimit C).oracle x) :
        ∀ᶠ (s : ℕ) in Filter.atTop, n ≤ agreementLength (setAnswers ↑(A s)) s c ((↑(C s)).indicator 1)

        Agreement eventually covers every prefix. If the program c, relative to the limit of monotone stages A, computes the characteristic function of the limit of monotone stages C below n, then the length of agreement of c against A s with target C s and fuel s is eventually at least n.