Documentation

TauCeti.Computability.Enumeration.Code

The canonical stage enumeration of a c.e. set #

For a code c of a partial computable function, c.domStage s is the finite stage W_{c,s}: the inputs on which c halts within s steps of Mathlib's step-bounded evaluation Nat.Partrec.Code.evaln. Step-bounded evaluation only succeeds on inputs below the step bound, so W_{c,s} ⊆ [0, s); unlike Soare's convention, neither the code nor the output is bounded.

These stages start empty, increase with s, and their limit is the domain W_c of c. Their binary finite-set codes ∑ x ∈ W_{c,s}, 2 ^ x are primitive recursive uniformly in the code and the stage, so they form a uniformly indexed family of effective enumerations of all c.e. sets.

Conversely, the limit of finite stages with computable membership is c.e. Together these give the stage characterization of c.e. predicates on ℕ: a predicate is c.e. exactly when it is the union of an increasing sequence of finite sets, starting empty, whose binary codes are computable.

These are raw simulation stages, not a serialized enumeration: several numbers may enter at the same stage.

Main definitions #

Main results #

References #

source
def Nat.Partrec.Code.domStage (c : Code) (s : ℕ) :
Finset ℕ

The stage W_{c,s} of the domain of the code c: the inputs on which c halts within s steps of step-bounded evaluation.

Instances For
    source
    @[simp]
    theorem Nat.Partrec.Code.mem_domStage {c : Code} {s x : ℕ} :
    x ∈ c.domStage s ↔ (evaln s c x).isSome = true

    A number is in W_{c,s} exactly when c halts on it within s steps.

    source
    theorem Nat.Partrec.Code.domStage_subset_range (c : Code) (s : ℕ) :
    c.domStage s ⊆ Finset.range s

    Every input enumerated by stage s is smaller than s.

    source
    @[simp]
    theorem Nat.Partrec.Code.domStage_zero (c : Code) :
    c.domStage 0 = ∅

    No computation halts within zero steps, so the stages start empty.

    source
    theorem Nat.Partrec.Code.monotone_domStage (c : Code) :
    Monotone c.domStage

    The stages of the domain of a code increase.

    source
    @[simp]
    theorem Nat.Partrec.Code.stageLimit_domStage (c : Code) :
    TauCeti.Enumeration.stageLimit c.domStage = {x : ℕ | (c.eval x).Dom}

    The limit of the stages of the domain of a code is its domain W_c.

    source
    theorem Nat.Partrec.Code.exists_mem_domStage_iff {c : Code} {x : ℕ} :
    (∃ (s : ℕ), x ∈ c.domStage s) ↔ (c.eval x).Dom

    A number is in the domain W_c of a code exactly when it is in some stage of the domain.

    source
    theorem Nat.Partrec.Code.primrec₂_evaln_isSome :
    Primrec₂ fun (p : Code × ℕ) (x : ℕ) => (evaln p.2 p.1 x).isSome

    Halting of step-bounded evaluation is primitive recursive in the code, the step bound and the input.

    source
    theorem Nat.Partrec.Code.primrecRel_mem_domStage :
    PrimrecRel fun (p : Code × ℕ) (x : ℕ) => x ∈ p.1.domStage p.2

    Membership in the stages of the domain of a code is primitive recursive, uniformly in the code, the stage and the number.

    source
    theorem Nat.Partrec.Code.primrecRel_mem_domStage_ofNat :
    PrimrecRel fun (p : ℕ × ℕ) (x : ℕ) => x ∈ (Denumerable.ofNat Code p.1).domStage p.2

    Membership in the stages of the domain of the code numbered i is primitive recursive, uniformly in the number i, the stage and the number.

    source
    theorem Nat.Partrec.Code.primrec_domStage :
    Primrec fun (p : Code × ℕ) => Finset.equivBitIndices.symm (p.1.domStage p.2)

    The binary finite-set codes ∑ x ∈ W_{c,s}, 2 ^ x of the stages of the domain of a code are primitive recursive, uniformly in the code and the stage.

    source
    theorem TauCeti.Enumeration.computablePred_mem_of_computable_equivBitIndices {A : ℕ → Finset ℕ} (hA : Computable fun (s : ℕ) => Finset.equivBitIndices.symm (A s)) :
    ComputablePred fun (p : ℕ × ℕ) => p.2 ∈ A p.1

    Membership in finite stages is computable, uniformly in the stage and the number, when their binary finite-set codes are computable.

    source
    theorem TauCeti.Enumeration.rePred_mem_stageLimit {A : ℕ → Finset ℕ} (hA : ComputablePred fun (p : ℕ × ℕ) => p.2 ∈ A p.1) :
    REPred fun (x : ℕ) => x ∈ stageLimit A

    The limit of finite stages is c.e. when membership in the stages is computable, uniformly in the stage and the number.

    source
    theorem TauCeti.Enumeration.rePred_iff_exists_stages {p : ℕ → Prop} :
    REPred p ↔ ∃ (A : ℕ → Finset ℕ), Monotone A ∧ A 0 = ∅ ∧ (Computable fun (s : ℕ) => Finset.equivBitIndices.symm (A s)) ∧ stageLimit A = {x : ℕ | p x}

    A predicate on ℕ is c.e. if and only if it is the limit of increasing finite stages, starting empty, whose binary finite-set codes are computable.