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 aNat.Partrec.Code
as a partial function.
Main Results #
Nat.Partrec.Code.rec_prim
: Recursion onNat.Partrec.Code
is primitive recursive.Nat.Partrec.Code.rec_computable
: Recursion onNat.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 #
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
Instances For
Equations
- Nat.Partrec.Code.instInhabited = { default := Nat.Partrec.Code.zero }
Returns a code for the constant function outputting a particular natural.
Equations
Instances For
A code for the identity function.
Equations
Instances For
Given a code c
taking a pair as input, returns a code using n
as the first argument to c
.
Equations
- c.curry n = c.comp ((Nat.Partrec.Code.const n).pair Nat.Partrec.Code.id)
Instances For
An encoding of a Nat.Partrec.Code
as a ℕ.
Equations
- Nat.Partrec.Code.zero.encodeCode = 0
- Nat.Partrec.Code.succ.encodeCode = 1
- Nat.Partrec.Code.left.encodeCode = 2
- Nat.Partrec.Code.right.encodeCode = 3
- (cf.pair cg).encodeCode = 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
- (cf.comp cg).encodeCode = 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode + 1) + 4
- (cf.prec cg).encodeCode = 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 1 + 4
- cf.rfind'.encodeCode = 2 * (2 * cf.encodeCode + 1) + 1 + 4
Instances For
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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Recursion on Nat.Partrec.Code
is primitive recursive.
Recursion on Nat.Partrec.Code
is computable.
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 byNat.pair
)Nat.Partrec.Code.right
: Right unpairing of a pair of ℕ (encoded byNat.pair
)Nat.Partrec.Code.pair
: Pairs the outputs of argument codes usingNat.pair
.Nat.Partrec.Code.comp
: Composition of two argument codes.Nat.Partrec.Code.prec
: Primitive recursion. Given an argument of the formNat.pair a n
:Nat.Partrec.Code.rfind'
: Minimization. Forf
an argument of the formNat.pair a m
,rfind' f m
returns the leasta
such thatf a m = 0
, if one exists andf b m
terminates forb < a
Equations
- Nat.Partrec.Code.zero.eval = pure 0
- Nat.Partrec.Code.succ.eval = ↑Nat.succ
- Nat.Partrec.Code.left.eval = ↑fun (n : ℕ) => (Nat.unpair n).1
- Nat.Partrec.Code.right.eval = ↑fun (n : ℕ) => (Nat.unpair n).2
- (cf.pair cg).eval = fun (n : ℕ) => Nat.pair <$> cf.eval n <*> cg.eval n
- (cf.comp cg).eval = fun (n : ℕ) => cg.eval n >>= cf.eval
- (cf.prec cg).eval = Nat.unpaired fun (a n : ℕ) => Nat.rec (cf.eval a) (fun (y : ℕ) (IH : Part ℕ) => do let i ← IH cg.eval (Nat.pair a (Nat.pair y i))) n
- cf.rfind'.eval = Nat.unpaired fun (a m : ℕ) => Part.map (fun (x : ℕ) => x + m) (Nat.rfind fun (n : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> cf.eval (Nat.pair a (n + m)))
Instances For
Helper lemma for the evaluation of prec
in the base case.
Helper lemma for the evaluation of prec
in the recursive case.
Equations
- Nat.Partrec.Code.instMembershipPFun = { mem := fun (c : Nat.Partrec.Code) (f : ℕ →. ℕ) => c.eval = f }
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.
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 k.succ Nat.Partrec.Code.zero = fun (n : ℕ) => do guard (n ≤ k) pure 0
- Nat.Partrec.Code.evaln k.succ Nat.Partrec.Code.succ = fun (n : ℕ) => do guard (n ≤ k) pure n.succ
- Nat.Partrec.Code.evaln k.succ Nat.Partrec.Code.left = fun (n : ℕ) => do guard (n ≤ k) pure (Nat.unpair n).1
- Nat.Partrec.Code.evaln k.succ Nat.Partrec.Code.right = fun (n : ℕ) => do guard (n ≤ k) pure (Nat.unpair n).2
- Nat.Partrec.Code.evaln k.succ (cf.pair cg) = fun (n : ℕ) => do guard (n ≤ k) Nat.pair <$> Nat.Partrec.Code.evaln (k + 1) cf n <*> Nat.Partrec.Code.evaln (k + 1) cg n
- Nat.Partrec.Code.evaln k.succ (cf.comp 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
Instances For
The Nat.Partrec.Code.evaln
function is primitive recursive.
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.
There are only countably many computable functions ℕ → ℕ
.