Documentation

Mathlib.Computability.PartrecCode

Gödel Numbering for Partial Recursive Functions. #

This file defines Nat.Partrec.Code, an inductive datatype describing code for partial recursive functions on ℕ. It defines an encoding for these codes, and proves that the constructors are primitive recursive with respect to the encoding.

It also defines the evaluation of these codes as partial functions using PFun, and proves that a function is partially recursive (as defined by Nat.Partrec) if and only if it is the evaluation of some code.

Main Definitions #

Main Results #

References #

theorem Nat.Partrec.rfind' {f : →. } (hf : Nat.Partrec f) :
Nat.Partrec (Nat.unpaired fun (a m : ) => Part.map (fun (x : ) => x + m) (Nat.rfind fun (n : ) => (fun (m : ) => decide (m = 0)) <$> f (a.pair (n + m))))

Code for partial recursive functions from ℕ to ℕ. See Nat.Partrec.Code.eval for the interpretation of these constructors.

Instances For

    Returns a code for the constant function outputting a particular natural.

    Equations
    Instances For
      theorem Nat.Partrec.Code.const_inj {n₁ : } {n₂ : } :

      Given a code c taking a pair as input, returns a code using n as the first argument to c.

      Equations
      Instances For

        An encoding of a Nat.Partrec.Code as a ℕ.

        Equations
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          theorem Nat.Partrec.Code.rec_prim' {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] {c : αNat.Partrec.Code} (hc : Primrec c) {z : ασ} (hz : Primrec z) {s : ασ} (hs : Primrec s) {l : ασ} (hl : Primrec l) {r : ασ} (hr : Primrec r) {pr : αNat.Partrec.Code × Nat.Partrec.Code × σ × σσ} (hpr : Primrec₂ pr) {co : αNat.Partrec.Code × Nat.Partrec.Code × σ × σσ} (hco : Primrec₂ co) {pc : αNat.Partrec.Code × Nat.Partrec.Code × σ × σσ} (hpc : Primrec₂ pc) {rf : αNat.Partrec.Code × σσ} (hrf : Primrec₂ rf) :
          let PR := fun (a : α) (cf cg : Nat.Partrec.Code) (hf hg : σ) => pr a (cf, cg, hf, hg); let CO := fun (a : α) (cf cg : Nat.Partrec.Code) (hf hg : σ) => co a (cf, cg, hf, hg); let PC := fun (a : α) (cf cg : Nat.Partrec.Code) (hf hg : σ) => pc a (cf, cg, hf, hg); let RF := fun (a : α) (cf : Nat.Partrec.Code) (hf : σ) => rf a (cf, hf); let F := fun (a : α) (c : Nat.Partrec.Code) => Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a); Primrec fun (a : α) => F a (c a)
          theorem Nat.Partrec.Code.rec_prim {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] {c : αNat.Partrec.Code} (hc : Primrec c) {z : ασ} (hz : Primrec z) {s : ασ} (hs : Primrec s) {l : ασ} (hl : Primrec l) {r : ασ} (hr : Primrec r) {pr : αNat.Partrec.CodeNat.Partrec.Codeσσσ} (hpr : Primrec fun (a : α × Nat.Partrec.Code × Nat.Partrec.Code × σ × σ) => pr a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) {co : αNat.Partrec.CodeNat.Partrec.Codeσσσ} (hco : Primrec fun (a : α × Nat.Partrec.Code × Nat.Partrec.Code × σ × σ) => co a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) {pc : αNat.Partrec.CodeNat.Partrec.Codeσσσ} (hpc : Primrec fun (a : α × Nat.Partrec.Code × Nat.Partrec.Code × σ × σ) => pc a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) {rf : αNat.Partrec.Codeσσ} (hrf : Primrec fun (a : α × Nat.Partrec.Code × σ) => rf a.1 a.2.1 a.2.2) :
          let F := fun (a : α) (c : Nat.Partrec.Code) => Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (pr a) (co a) (pc a) (rf a); Primrec fun (a : α) => F a (c a)

          Recursion on Nat.Partrec.Code is primitive recursive.

          theorem Nat.Partrec.Code.rec_computable {α : Type u_1} {σ : Type u_2} [Primcodable α] [Primcodable σ] {c : αNat.Partrec.Code} (hc : Computable c) {z : ασ} (hz : Computable z) {s : ασ} (hs : Computable s) {l : ασ} (hl : Computable l) {r : ασ} (hr : Computable r) {pr : αNat.Partrec.Code × Nat.Partrec.Code × σ × σσ} (hpr : Computable₂ pr) {co : αNat.Partrec.Code × Nat.Partrec.Code × σ × σσ} (hco : Computable₂ co) {pc : αNat.Partrec.Code × Nat.Partrec.Code × σ × σσ} (hpc : Computable₂ pc) {rf : αNat.Partrec.Code × σσ} (hrf : Computable₂ rf) :
          let PR := fun (a : α) (cf cg : Nat.Partrec.Code) (hf hg : σ) => pr a (cf, cg, hf, hg); let CO := fun (a : α) (cf cg : Nat.Partrec.Code) (hf hg : σ) => co a (cf, cg, hf, hg); let PC := fun (a : α) (cf cg : Nat.Partrec.Code) (hf hg : σ) => pc a (cf, cg, hf, hg); let RF := fun (a : α) (cf : Nat.Partrec.Code) (hf : σ) => rf a (cf, hf); let F := fun (a : α) (c : Nat.Partrec.Code) => Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a); Computable fun (a : α) => F a (c a)

          Recursion on Nat.Partrec.Code is computable.

          The interpretation of a Nat.Partrec.Code as a partial function.

          Equations
          Instances For
            @[simp]
            theorem Nat.Partrec.Code.eval_prec_zero (cf : Nat.Partrec.Code) (cg : Nat.Partrec.Code) (a : ) :
            (cf.prec cg).eval (a.pair 0) = cf.eval a

            Helper lemma for the evaluation of prec in the base case.

            theorem Nat.Partrec.Code.eval_prec_succ (cf : Nat.Partrec.Code) (cg : Nat.Partrec.Code) (a : ) (k : ) :
            (cf.prec cg).eval (a.pair k.succ) = do let ih(cf.prec cg).eval (a.pair k) cg.eval (a.pair (k.pair ih))

            Helper lemma for the evaluation of prec in the recursive case.

            @[simp]
            theorem Nat.Partrec.Code.eval_curry (c : Nat.Partrec.Code) (n : ) (x : ) :
            (c.curry n).eval x = c.eval (n.pair x)
            theorem Nat.Partrec.Code.curry_inj {c₁ : Nat.Partrec.Code} {c₂ : Nat.Partrec.Code} {n₁ : } {n₂ : } (h : c₁.curry n₁ = c₂.curry n₂) :
            c₁ = c₂ n₁ = n₂
            theorem Nat.Partrec.Code.smn :
            ∃ (f : Nat.Partrec.CodeNat.Partrec.Code), Computable₂ f ∀ (c : Nat.Partrec.Code) (n x : ), (f c n).eval x = c.eval (n.pair x)

            The $S_n^m$ theorem: There is a computable function, namely Nat.Partrec.Code.curry, that takes a program and a ℕ n, and returns a new program using n as the first argument.

            A function is partial recursive if and only if there is a code implementing it. Therefore, eval is a universal partial recursive function.

            @[irreducible]

            A modified evaluation for the code which returns an Option instead of a Part. To avoid undecidability, evaln takes a parameter k and fails if it encounters a number ≥ k in the course of its execution. Other than this, the semantics are the same as in Nat.Partrec.Code.eval.

            Equations
            Instances For
              theorem Nat.Partrec.Code.evaln_mono {k₁ : } {k₂ : } {c : Nat.Partrec.Code} {n : } {x : } :
              k₁ k₂x Nat.Partrec.Code.evaln k₁ c nx Nat.Partrec.Code.evaln k₂ c n
              theorem Nat.Partrec.Code.evaln_sound {k : } {c : Nat.Partrec.Code} {n : } {x : } :
              x Nat.Partrec.Code.evaln k c nx c.eval n
              theorem Nat.Partrec.Code.evaln_complete {c : Nat.Partrec.Code} {n : } {x : } :
              x c.eval n ∃ (k : ), x Nat.Partrec.Code.evaln k c n

              The Nat.Partrec.Code.evaln function is primitive recursive.

              theorem Nat.Partrec.Code.fixed_point {f : Nat.Partrec.CodeNat.Partrec.Code} (hf : Computable f) :
              ∃ (c : Nat.Partrec.Code), (f c).eval = c.eval

              Roger's fixed-point theorem: Any total, computable f has a fixed point: That is, under the interpretation given by Nat.Partrec.Code.eval, there is a code c such that c and f c have the same evaluation.