The primitive recursive functions #
The primitive recursive functions are the least collection of functions
ℕ → ℕ
which are closed under projections (using the pair
pairing function), composition, zero, successor, and primitive recursion
(i.e. Nat.rec
where the motive is C n := ℕ
).
We can extend this definition to a large class of basic types by
using canonical encodings of types as natural numbers (Gödel numbering),
which we implement through the type class Encodable
. (More precisely,
we need that the composition of encode with decode yields a
primitive recursive function, so we have the Primcodable
type class
for this.)
References #
- [Mario Carneiro, Formalizing computability theory via partial recursive functions][carneiro2019]
Calls the given function on a pair of entries n
, encoded via the pairing function.
Equations
- Nat.unpaired f n = f (Nat.unpair n).1 (Nat.unpair n).2
Instances For
The primitive recursive functions ℕ → ℕ
.
- zero: Nat.Primrec fun (x : ℕ) => 0
- succ: Nat.Primrec Nat.succ
- left: Nat.Primrec fun (n : ℕ) => (Nat.unpair n).1
- right: Nat.Primrec fun (n : ℕ) => (Nat.unpair n).2
- pair: ∀ {f g : ℕ → ℕ}, Nat.Primrec f → Nat.Primrec g → Nat.Primrec fun (n : ℕ) => Nat.pair (f n) (g n)
- comp: ∀ {f g : ℕ → ℕ}, Nat.Primrec f → Nat.Primrec g → Nat.Primrec fun (n : ℕ) => f (g n)
- prec: ∀ {f g : ℕ → ℕ}, Nat.Primrec f → Nat.Primrec g → Nat.Primrec (Nat.unpaired fun (z n : ℕ) => Nat.rec (f z) (fun (y IH : ℕ) => g (Nat.pair z (Nat.pair y IH))) n)
Instances For
A Primcodable
type is an Encodable
type for which
the encode/decode functions are primitive recursive.
- encode : α → ℕ
- encodek : ∀ (a : α), Encodable.decode (Encodable.encode a) = some a
- prim : Nat.Primrec fun (n : ℕ) => Encodable.encode (Encodable.decode n)
Instances
Equations
Equations
Equations
- Primcodable.option = Primcodable.mk ⋯
Primrec f
means f
is primitive recursive (after
encoding its input and output as natural numbers).
Equations
- Primrec f = Nat.Primrec fun (n : ℕ) => Encodable.encode (Option.map f (Encodable.decode n))
Instances For
Equations
- Primcodable.prod = Primcodable.mk ⋯
Primrec₂ f
means f
is a binary primitive recursive function.
This is technically unnecessary since we can always curry all
the arguments together, but there are enough natural two-arg
functions that it is convenient to express this directly.
Instances For
PrimrecPred p
means p : α → Prop
is a (decidable)
primitive recursive predicate, which is to say that
decide ∘ p : α → Bool
is primitive recursive.
Equations
- PrimrecPred p = Primrec fun (a : α) => decide (p a)
Instances For
PrimrecRel p
means p : α → β → Prop
is a (decidable)
primitive recursive relation, which is to say that
decide ∘ p : α → β → Bool
is primitive recursive.
Equations
- PrimrecRel s = Primrec₂ fun (a : α) (b : β) => decide (s a b)
Instances For
A function is PrimrecBounded
if its size is bounded by a primitive recursive function
Equations
- Primrec.PrimrecBounded f = ∃ (g : α → ℕ), Primrec g ∧ ∀ (x : α), Encodable.encode (f x) ≤ g x
Instances For
To show a function f : α → ℕ
is primitive recursive, it is enough to show that the function
is bounded by a primitive recursive function and that its graph is primitive recursive
Equations
- Primcodable.sum = Primcodable.mk ⋯
Equations
- Primcodable.list = Primcodable.mk ⋯
A subtype of a primitive recursive predicate is Primcodable
.
Equations
Instances For
Equations
- Primcodable.fin = Primcodable.ofEquiv { a : ℕ // id a < n } Fin.equivSubtype
Equations
- Primcodable.vector = Primcodable.subtype ⋯
Equations
- Primcodable.finArrow = Primcodable.ofEquiv (Mathlib.Vector α n) (Equiv.vectorEquivFin α n).symm
Equations
- Primcodable.ulower = Primcodable.subtype ⋯
An alternative inductive definition of Primrec
which
does not use the pairing function on ℕ, and so has to
work with n-ary functions on ℕ instead of unary functions.
We prove that this is equivalent to the regular notion
in to_prim
and of_prim
.
- zero: Nat.Primrec' fun (x : Mathlib.Vector ℕ 0) => 0
- succ: Nat.Primrec' fun (v : Mathlib.Vector ℕ 1) => v.head.succ
- get: ∀ {n : ℕ} (i : Fin n), Nat.Primrec' fun (v : Mathlib.Vector ℕ n) => v.get i
- comp: ∀ {m n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} (g : Fin n → Mathlib.Vector ℕ m → ℕ), Nat.Primrec' f → (∀ (i : Fin n), Nat.Primrec' (g i)) → Nat.Primrec' fun (a : Mathlib.Vector ℕ m) => f (Mathlib.Vector.ofFn fun (i : Fin n) => g i a)
- prec: ∀ {n : ℕ} {f : Mathlib.Vector ℕ n → ℕ} {g : Mathlib.Vector ℕ (n + 2) → ℕ}, Nat.Primrec' f → Nat.Primrec' g → Nat.Primrec' fun (v : Mathlib.Vector ℕ (n + 1)) => Nat.rec (f v.tail) (fun (y IH : ℕ) => g (y ::ᵥ IH ::ᵥ v.tail)) v.head
Instances For
A function from vectors to vectors is primitive recursive when all of its projections are.
Equations
- Nat.Primrec'.Vec f = ∀ (i : Fin m), Nat.Primrec' fun (v : Mathlib.Vector ℕ n) => (f v).get i