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

• Nat.Partrec.Code: Inductive datatype for partial recursive codes.
• Nat.Partrec.Code.encodeCode: A (computable) encoding of codes as natural numbers.
• Nat.Partrec.Code.ofNatCode: The inverse of this encoding.
• Nat.Partrec.Code.eval: The interpretation of a Nat.Partrec.Code as a partial function.

Main Results

• Nat.Partrec.Code.rec_prim: Recursion on Nat.Partrec.Code is primitive recursive.
• Nat.Partrec.Code.rec_computable: Recursion on Nat.Partrec.Code is computable.
• Nat.Partrec.Code.smn: The $S_n^m$ theorem.
• Nat.Partrec.Code.exists_code: Partial recursiveness is equivalent to being the eval of a code.
• Nat.Partrec.Code.evaln_prim: evaln is primitive recursive.
• Nat.Partrec.Code.fixed_point: Roger's fixed point theorem.

References

• [Mario Carneiro, Formalizing computability theory via partial recursive functions][carneiro2019]

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 (Nat.pair a (n + m))))

inductive Nat.Partrec.Code : Type

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

• zero: Nat.Partrec.Code
• succ: Nat.Partrec.Code
• left: Nat.Partrec.Code
• right: Nat.Partrec.Code
• pair: Nat.Partrec.Code → Nat.Partrec.Code → Nat.Partrec.Code
• comp: Nat.Partrec.Code → Nat.Partrec.Code → Nat.Partrec.Code
• prec: Nat.Partrec.Code → Nat.Partrec.Code → Nat.Partrec.Code
• rfind': Nat.Partrec.Code → Nat.Partrec.Code

instance Nat.Partrec.Code.instInhabited : Inhabited Nat.Partrec.Code

Equations

• Nat.Partrec.Code.instInhabited = { default := Nat.Partrec.Code.zero }

def Nat.Partrec.Code.const : ℕ → Nat.Partrec.Code

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

Equations

• Nat.Partrec.Code.const 0 = Nat.Partrec.Code.zero
• Nat.Partrec.Code.const (Nat.succ n) = Nat.Partrec.Code.comp Nat.Partrec.Code.succ (Nat.Partrec.Code.const n)

theorem Nat.Partrec.Code.const_inj {n₁ : ℕ} {n₂ : ℕ} : Nat.Partrec.Code.const n₁ = Nat.Partrec.Code.const n₂ → n₁ = n₂

def Nat.Partrec.Code.id : Nat.Partrec.Code

A code for the identity function.

Equations

• Nat.Partrec.Code.id = Nat.Partrec.Code.pair Nat.Partrec.Code.left Nat.Partrec.Code.right

def Nat.Partrec.Code.curry (c : Nat.Partrec.Code) (n : ℕ) : Nat.Partrec.Code

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

Equations

• Nat.Partrec.Code.curry c n = Nat.Partrec.Code.comp c (Nat.Partrec.Code.pair (Nat.Partrec.Code.const n) Nat.Partrec.Code.id)

def Nat.Partrec.Code.encodeCode : Nat.Partrec.Code → ℕ

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

Equations

• Nat.Partrec.Code.encodeCode Nat.Partrec.Code.zero = 0
• Nat.Partrec.Code.encodeCode Nat.Partrec.Code.succ = 1
• Nat.Partrec.Code.encodeCode Nat.Partrec.Code.left = 2
• Nat.Partrec.Code.encodeCode Nat.Partrec.Code.right = 3
• Nat.Partrec.Code.encodeCode (Nat.Partrec.Code.pair cf cg) = 2 * (2 * Nat.pair (Nat.Partrec.Code.encodeCode cf) (Nat.Partrec.Code.encodeCode cg)) + 4
• Nat.Partrec.Code.encodeCode (Nat.Partrec.Code.comp cf cg) = 2 * (2 * Nat.pair (Nat.Partrec.Code.encodeCode cf) (Nat.Partrec.Code.encodeCode cg) + 1) + 4
• Nat.Partrec.Code.encodeCode (Nat.Partrec.Code.prec cf cg) = 2 * (2 * Nat.pair (Nat.Partrec.Code.encodeCode cf) (Nat.Partrec.Code.encodeCode cg)) + 1 + 4
• Nat.Partrec.Code.encodeCode (Nat.Partrec.Code.rfind' cf) = 2 * (2 * Nat.Partrec.Code.encodeCode cf + 1) + 1 + 4

def Nat.Partrec.Code.ofNatCode : ℕ → Nat.Partrec.Code

A decoder for Nat.Partrec.Code.encodeCode, taking any ℕ to the Nat.Partrec.Code it represents.

Equations

• One or more equations did not get rendered due to their size.
• Nat.Partrec.Code.ofNatCode 0 = Nat.Partrec.Code.zero
• Nat.Partrec.Code.ofNatCode 1 = Nat.Partrec.Code.succ
• Nat.Partrec.Code.ofNatCode 2 = Nat.Partrec.Code.left
• Nat.Partrec.Code.ofNatCode 3 = Nat.Partrec.Code.right

instance Nat.Partrec.Code.instDenumerable : Denumerable Nat.Partrec.Code

Equations

• One or more equations did not get rendered due to their size.

theorem Nat.Partrec.Code.encodeCode_eq : Encodable.encode = Nat.Partrec.Code.encodeCode

theorem Nat.Partrec.Code.ofNatCode_eq : Denumerable.ofNat Nat.Partrec.Code = Nat.Partrec.Code.ofNatCode

theorem Nat.Partrec.Code.encode_lt_pair (cf : Nat.Partrec.Code) (cg : Nat.Partrec.Code) : Encodable.encode cf < Encodable.encode (Nat.Partrec.Code.pair cf cg) ∧ Encodable.encode cg < Encodable.encode (Nat.Partrec.Code.pair cf cg)

theorem Nat.Partrec.Code.encode_lt_comp (cf : Nat.Partrec.Code) (cg : Nat.Partrec.Code) : Encodable.encode cf < Encodable.encode (Nat.Partrec.Code.comp cf cg) ∧ Encodable.encode cg < Encodable.encode (Nat.Partrec.Code.comp cf cg)

theorem Nat.Partrec.Code.encode_lt_prec (cf : Nat.Partrec.Code) (cg : Nat.Partrec.Code) : Encodable.encode cf < Encodable.encode (Nat.Partrec.Code.prec cf cg) ∧ Encodable.encode cg < Encodable.encode (Nat.Partrec.Code.prec cf cg)

theorem Nat.Partrec.Code.encode_lt_rfind' (cf : Nat.Partrec.Code) : Encodable.encode cf < Encodable.encode (Nat.Partrec.Code.rfind' cf)

theorem Nat.Partrec.Code.pair_prim : Primrec₂ Nat.Partrec.Code.pair

theorem Nat.Partrec.Code.comp_prim : Primrec₂ Nat.Partrec.Code.comp

theorem Nat.Partrec.Code.prec_prim : Primrec₂ Nat.Partrec.Code.prec

theorem Nat.Partrec.Code.rfind_prim : Primrec Nat.Partrec.Code.rfind'

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.Code → Nat.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.Code → Nat.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.Code → Nat.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.

def Nat.Partrec.Code.eval : Nat.Partrec.Code → ℕ →. ℕ

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

• Nat.Partrec.Code.zero: The constant zero function.
• Nat.Partrec.Code.succ: The successor function.
• Nat.Partrec.Code.left: Left unpairing of a pair of ℕ (encoded by Nat.pair)
• Nat.Partrec.Code.right: Right unpairing of a pair of ℕ (encoded by Nat.pair)
• Nat.Partrec.Code.pair: Pairs the outputs of argument codes using Nat.pair.
• Nat.Partrec.Code.comp: Composition of two argument codes.
• Nat.Partrec.Code.prec: Primitive recursion. Given an argument of the form Nat.pair a n:
  • If n = 0, returns eval cf a.
  • If n = succ k, returns eval cg (pair a (pair k (eval (prec cf cg) (pair a k))))
• Nat.Partrec.Code.rfind': Minimization. For f an argument of the form Nat.pair a m, rfind' f m returns the least a such that f a m = 0, if one exists and f b m terminates for b < a

Equations

• One or more equations did not get rendered due to their size.
• Nat.Partrec.Code.eval Nat.Partrec.Code.zero = pure 0
• Nat.Partrec.Code.eval Nat.Partrec.Code.succ = ↑Nat.succ
• Nat.Partrec.Code.eval Nat.Partrec.Code.left = ↑fun (n : ℕ) => (Nat.unpair n).1
• Nat.Partrec.Code.eval Nat.Partrec.Code.right = ↑fun (n : ℕ) => (Nat.unpair n).2
• Nat.Partrec.Code.eval (Nat.Partrec.Code.pair cf cg) = fun (n : ℕ) => Seq.seq (Nat.pair <$> Nat.Partrec.Code.eval cf n) fun (x : Unit) => Nat.Partrec.Code.eval cg n
• Nat.Partrec.Code.eval (Nat.Partrec.Code.comp cf cg) = fun (n : ℕ) => Nat.Partrec.Code.eval cg n >>= Nat.Partrec.Code.eval cf

@[simp]

theorem Nat.Partrec.Code.eval_prec_zero (cf : Nat.Partrec.Code) (cg : Nat.Partrec.Code) (a : ℕ) : Nat.Partrec.Code.eval (Nat.Partrec.Code.prec cf cg) (Nat.pair a 0) = Nat.Partrec.Code.eval cf 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 : ℕ) : Nat.Partrec.Code.eval (Nat.Partrec.Code.prec cf cg) (Nat.pair a (Nat.succ k)) = do let ih ← Nat.Partrec.Code.eval (Nat.Partrec.Code.prec cf cg) (Nat.pair a k) Nat.Partrec.Code.eval cg (Nat.pair a (Nat.pair k ih))

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

instance Nat.Partrec.Code.instMembershipPFunNatCode : Membership (ℕ →. ℕ) Nat.Partrec.Code

Equations

• Nat.Partrec.Code.instMembershipPFunNatCode = { mem := fun (f : ℕ →. ℕ) (c : Nat.Partrec.Code) => Nat.Partrec.Code.eval c = f }

@[simp]

theorem Nat.Partrec.Code.eval_const (n : ℕ) (m : ℕ) : Nat.Partrec.Code.eval (Nat.Partrec.Code.const n) m = Part.some n

@[simp]

theorem Nat.Partrec.Code.eval_id (n : ℕ) : Nat.Partrec.Code.eval Nat.Partrec.Code.id n = Part.some n

@[simp]

theorem Nat.Partrec.Code.eval_curry (c : Nat.Partrec.Code) (n : ℕ) (x : ℕ) : Nat.Partrec.Code.eval (Nat.Partrec.Code.curry c n) x = Nat.Partrec.Code.eval c (Nat.pair n x)

theorem Nat.Partrec.Code.const_prim : Primrec Nat.Partrec.Code.const

theorem Nat.Partrec.Code.curry_prim : Primrec₂ Nat.Partrec.Code.curry

theorem Nat.Partrec.Code.curry_inj {c₁ : Nat.Partrec.Code} {c₂ : Nat.Partrec.Code} {n₁ : ℕ} {n₂ : ℕ} (h : Nat.Partrec.Code.curry c₁ n₁ = Nat.Partrec.Code.curry c₂ n₂) : c₁ = c₂ ∧ n₁ = n₂

theorem Nat.Partrec.Code.smn : ∃ (f : Nat.Partrec.Code → ℕ → Nat.Partrec.Code), Computable₂ f ∧ ∀ (c : Nat.Partrec.Code) (n x : ℕ), Nat.Partrec.Code.eval (f c n) x = Nat.Partrec.Code.eval c (Nat.pair n 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.

theorem Nat.Partrec.Code.exists_code {f : ℕ →. ℕ} : Nat.Partrec f ↔ ∃ (c : Nat.Partrec.Code), Nat.Partrec.Code.eval c = f

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

def Nat.Partrec.Code.evaln : ℕ → Nat.Partrec.Code → ℕ → Option ℕ

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

• One or more equations did not get rendered due to their size.
• Nat.Partrec.Code.evaln 0 x = fun (x : ℕ) => none
• Nat.Partrec.Code.evaln (Nat.succ k) Nat.Partrec.Code.zero = fun (n : ℕ) => do guard (n ≤ k) pure 0
• Nat.Partrec.Code.evaln (Nat.succ k) Nat.Partrec.Code.succ = fun (n : ℕ) => do guard (n ≤ k) pure (Nat.succ n)
• Nat.Partrec.Code.evaln (Nat.succ k) Nat.Partrec.Code.left = fun (n : ℕ) => do guard (n ≤ k) pure (Nat.unpair n).1
• Nat.Partrec.Code.evaln (Nat.succ k) Nat.Partrec.Code.right = fun (n : ℕ) => do guard (n ≤ k) pure (Nat.unpair n).2
• Nat.Partrec.Code.evaln (Nat.succ k) (Nat.Partrec.Code.comp cf cg) = fun (n : ℕ) => do guard (n ≤ k) let x ← Nat.Partrec.Code.evaln (k + 1) cg n Nat.Partrec.Code.evaln (k + 1) cf x

theorem Nat.Partrec.Code.evaln_bound {k : ℕ} {c : Nat.Partrec.Code} {n : ℕ} {x : ℕ} : x ∈ Nat.Partrec.Code.evaln k c n → n < k

theorem Nat.Partrec.Code.evaln_mono {k₁ : ℕ} {k₂ : ℕ} {c : Nat.Partrec.Code} {n : ℕ} {x : ℕ} : k₁ ≤ k₂ → x ∈ Nat.Partrec.Code.evaln k₁ c n → x ∈ 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 n → x ∈ Nat.Partrec.Code.eval c n

theorem Nat.Partrec.Code.evaln_complete {c : Nat.Partrec.Code} {n : ℕ} {x : ℕ} : x ∈ Nat.Partrec.Code.eval c n ↔ ∃ (k : ℕ), x ∈ Nat.Partrec.Code.evaln k c n

theorem Nat.Partrec.Code.evaln_prim : Primrec fun (a : (ℕ × Nat.Partrec.Code) × ℕ) => Nat.Partrec.Code.evaln a.1.1 a.1.2 a.2

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

theorem Nat.Partrec.Code.eval_eq_rfindOpt (c : Nat.Partrec.Code) (n : ℕ) : Nat.Partrec.Code.eval c n = Nat.rfindOpt fun (k : ℕ) => Nat.Partrec.Code.evaln k c n

theorem Nat.Partrec.Code.eval_part : Partrec₂ Nat.Partrec.Code.eval

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

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.

theorem Nat.Partrec.Code.fixed_point₂ {f : Nat.Partrec.Code → ℕ →. ℕ} (hf : Partrec₂ f) : ∃ (c : Nat.Partrec.Code), Nat.Partrec.Code.eval c = f c