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]
- zero: Nat.Primrec fun x => 0
- succ: Nat.Primrec Nat.succ
- left: Nat.Primrec fun n => (Nat.unpair n).fst
- right: Nat.Primrec fun n => (Nat.unpair n).snd
- 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)
The primitive recursive functions ℕ → ℕ
.
Instances For
- encode : α → ℕ
- encodek : ∀ (a : α), Encodable.decode (Encodable.encode a) = some a
- prim : Nat.Primrec fun n => Encodable.encode (Encodable.decode n)
A Primcodable
type is an Encodable
type for which
the encode/decode functions are primitive recursive.
Instances
Builds a Primcodable
instance from an equivalence to a Primcodable
type.
Instances For
Primrec f
means f
is primitive recursive (after
encoding its input and output as natural numbers).
Instances For
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.
Instances For
PrimrecRel p
means p : α → β → Prop
is a (decidable)
primitive recursive relation, which is to say that
decide ∘ p : α → β → Bool
is primitive recursive.
Instances For
A function is PrimrecBounded
if its size is bounded by a primitive recursive function
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
A subtype of a primitive recursive predicate is Primcodable
.
Instances For
- zero: Nat.Primrec' fun x => 0
- succ: Nat.Primrec' fun v => Nat.succ (Vector.head v)
- get: ∀ {n : ℕ} (i : Fin n), Nat.Primrec' fun v => Vector.get v i
- comp: ∀ {m n : ℕ} {f : Vector ℕ n → ℕ} (g : Fin n → Vector ℕ m → ℕ), Nat.Primrec' f → (∀ (i : Fin n), Nat.Primrec' (g i)) → Nat.Primrec' fun a => f (Vector.ofFn fun i => g i a)
- prec: ∀ {n : ℕ} {f : Vector ℕ n → ℕ} {g : Vector ℕ (n + 2) → ℕ}, Nat.Primrec' f → Nat.Primrec' g → Nat.Primrec' fun v => Nat.rec (f (Vector.tail v)) (fun y IH => g (y ::ᵥ IH ::ᵥ Vector.tail v)) (Vector.head v)
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
.