Documentation

TauCeti.Computability.SingleOracle.Primrec

Bounded evaluation of oracle programs is primitive recursive #

Bounded evaluation TauCeti.Oracle.Single.Code.evaln σ k c n runs the program c on the input n with fuel k against the oracle answers σ. This file proves that the run, its output and its use, is primitive recursive in the program, the fuel and the input, uniformly in a parameter on which the oracle answers depend primitive recursively. The finite oracle data of a stage construction are the main instances: a finite oracle string l, answering l[z]?, and a finite set D, given by its binary code and answering 1 on D and 0 outside it.

This is what makes stage computations effective: for instance, whether Φ_{e,s}^{A_s}(x) converges, with which output and with which use, is primitive recursive in e, s, x and the binary code of the finite stage A_s.

Main definitions #

Main results #

References #

Encoding successful runs #

source
def TauCeti.Oracle.Single.Code.Halt.equivProd :
Halt ≃ ℕ × ℕ

A successful run is its output and its use.

Instances For
    source
    @[instance_reducible]
    instance TauCeti.Oracle.Single.Code.instPrimcodableHalt :
    Primcodable Halt

    Successful runs are encoded as pairs of their output and their use.

    source
    @[simp]
    theorem TauCeti.Oracle.Single.Code.Halt.equivProd_apply (d : Halt) :
    equivProd d = (d.output, d.use)

    A successful run corresponds to the pair of its output and its use.

    source
    @[simp]
    theorem TauCeti.Oracle.Single.Code.Halt.equivProd_symm_apply (p : ℕ × ℕ) :
    equivProd.symm p = { output := p.1, use := p.2 }

    A pair corresponds to the successful run with that output and use.

    source
    theorem TauCeti.Oracle.Single.Code.Halt.primrec_output :
    Primrec output

    The output of a successful run is primitive recursive.

    source
    theorem TauCeti.Oracle.Single.Code.Halt.primrec_use :
    Primrec use

    The use of a successful run is primitive recursive.

    source
    theorem TauCeti.Oracle.Single.Code.Halt.primrec₂_mk :
    Primrec₂ mk

    Forming a successful run from its output and its use is primitive recursive.

    One step of bounded evaluation #

    The course-of-values table #

    Primitive recursiveness #

    source
    theorem TauCeti.Oracle.Single.Code.primrec_evaln {α : Type u_1} [Primcodable α] {σ : α → ℕ → Option ℕ} (hσ : Primrec₂ σ) :
    Primrec fun (p : α × ℕ × Code × ℕ) => evaln (σ p.1) p.2.1 p.2.2.1 p.2.2.2

    Bounded evaluation is primitive recursive, uniformly in a parameter a on which the oracle answers σ a depend primitive recursively: the output and the use of the run of the program c on the input n with fuel k against σ a, or its failure, are primitive recursive in a, k, c and n.

    source
    theorem TauCeti.Oracle.Single.Code.primrec_stageUse {α : Type u_1} [Primcodable α] {σ : α → ℕ → Option ℕ} (hσ : Primrec₂ σ) :
    Primrec fun (p : α × ℕ × Code × ℕ) => stageUse (σ p.1) p.2.1 p.2.2.1 p.2.2.2

    The stage use is primitive recursive, uniformly in a parameter a on which the answers σ a depend primitive recursively, and in the fuel, the program and the argument.

    source
    theorem TauCeti.Oracle.Single.Code.primrec_evaln_list :
    Primrec fun (p : List ℕ × ℕ × Code × ℕ) => evaln (fun (z : ℕ) => p.1[z]?) p.2.1 p.2.2.1 p.2.2.2

    Bounded evaluation against a finite oracle string l, which answers l[z]? at z, is primitive recursive in the string, the fuel, the program and the input.

    source
    theorem TauCeti.Oracle.Single.Code.primrec_evaln_equivBitIndices :
    Primrec fun (p : ℕ × ℕ × Code × ℕ) => evaln (fun (z : ℕ) => some (if z ∈ Finset.equivBitIndices p.1 then 1 else 0)) p.2.1 p.2.2.1 p.2.2.2

    Bounded evaluation against a finite set, given by its binary code m and answering 1 on the set Finset.equivBitIndices m and 0 outside it, is primitive recursive in the code, the fuel, the program and the input.

    source
    theorem TauCeti.Oracle.Single.Code.primrec₂_setAnswers_equivBitIndices :
    Primrec₂ fun (m z : ℕ) => setAnswers (↑(Finset.equivBitIndices m)) z

    The answers of a finite set given by its binary code m, 1 on Finset.equivBitIndices m and 0 outside it, are primitive recursive in the code and the address.

    source
    theorem TauCeti.Oracle.Single.Code.computable₂_evaln_setAnswers {A : ℕ → Finset ℕ} (hA : Computable fun (s : ℕ) => Finset.equivBitIndices.symm (A s)) (c : Code) :
    Computable₂ fun (s x : ℕ) => evaln (setAnswers ↑(A s)) s c x

    Bounded evaluation against computable finite stages is computable uniformly in the stage and the input. The stages are supplied by their binary finite-set codes.