The primitive recursive functions #
The primitive recursive functions are the least collection of functions
nat → nat
which are closed under projections (using the mkpair
pairing function), composition, zero, successor, and primitive recursion
(i.e. nat.rec where the motive is C n := nat).
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 #
Equations
- nat.unpaired f n = f (nat.unpair n).fst (nat.unpair n).snd
- zero : nat.primrec (λ (n : ℕ), 0)
- succ : nat.primrec nat.succ
- left : nat.primrec (λ (n : ℕ), (nat.unpair n).fst)
- right : nat.primrec (λ (n : ℕ), (nat.unpair n).snd)
- pair : ∀ {f g : ℕ → ℕ}, nat.primrec f → nat.primrec g → nat.primrec (λ (n : ℕ), nat.mkpair (f n) (g n))
- comp : ∀ {f g : ℕ → ℕ}, nat.primrec f → nat.primrec g → nat.primrec (λ (n : ℕ), f (g n))
- prec : ∀ {f g : ℕ → ℕ}, nat.primrec f → nat.primrec g → nat.primrec (nat.unpaired (λ (z n : ℕ), nat.elim (f z) (λ (y IH : ℕ), g (nat.mkpair z (nat.mkpair y IH))) n))
The primitive recursive functions ℕ → ℕ
.
- to_encodable : encodable α
- prim : nat.primrec (λ (n : ℕ), encodable.encode (encodable.decode α n))
A primcodable
type is an encodable
type for which
the encode/decode functions are primitive recursive.
Instances of this typeclass
Instances of other typeclasses for primcodable
- primcodable.has_sizeof_inst
Equations
- primcodable.of_denumerable α = {to_encodable := denumerable.to_encodable _inst_1, prim := _}
Equations
- primcodable.of_equiv α e = {to_encodable := {encode := encodable.encode (encodable.of_equiv α e), decode := encodable.decode β (encodable.of_equiv α e), encodek := _}, prim := _}
Equations
Equations
- primcodable.unit = {to_encodable := punit.encodable, prim := primcodable.unit._proof_1}
Equations
Equations
- primcodable.bool = {to_encodable := bool.encodable, prim := primcodable.bool._proof_1}
primrec f
means f
is primitive recursive (after
encoding its input and output as natural numbers).
Equations
- primrec f = nat.primrec (λ (n : ℕ), encodable.encode (option.map f (encodable.decode α n)))
Equations
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.
primrec_pred p
means p : α → Prop
is a (decidable)
primitive recursive predicate, which is to say that
to_bool ∘ p : α → bool
is primitive recursive.
Equations
- primrec_pred p = primrec (λ (a : α), decidable.to_bool (p a))
primrec_rel p
means p : α → β → Prop
is a (decidable)
primitive recursive relation, which is to say that
to_bool ∘ p : α → β → bool
is primitive recursive.
Equations
- primrec_rel s = primrec₂ (λ (a : α) (b : β), decidable.to_bool (s a b))
Equations
Equations
Equations
- primcodable.subtype hp = {to_encodable := subtype.encodable (λ (a : α), _inst_3 a), prim := _}
Equations
- primcodable.fin = primcodable.of_equiv {a // id a < n} (equiv.refl {a // id a < n})
Equations
- primcodable.vector = primcodable.subtype primcodable.vector._proof_1
Equations
Equations
- primcodable.array = primcodable.of_equiv (fin n → α) (equiv.array_equiv_fin n α)
Equations
- primcodable.ulower = have this : primrec_pred (λ (n : ℕ), encodable.decode₂ α n ≠ option.none), from primcodable.ulower._proof_2, primcodable.subtype _
- zero : nat.primrec' (λ (_x : vector ℕ 0), 0)
- succ : nat.primrec' (λ (v : vector ℕ 1), v.head.succ)
- nth : ∀ {n : ℕ} (i : fin n), nat.primrec' (λ (v : vector ℕ n), v.nth i)
- comp : ∀ {m n : ℕ} {f : vector ℕ n → ℕ} (g : fin n → vector ℕ m → ℕ), nat.primrec' f → (∀ (i : fin n), nat.primrec' (g i)) → nat.primrec' (λ (a : vector ℕ m), f (vector.of_fn (λ (i : fin n), g i a)))
- prec : ∀ {n : ℕ} {f : vector ℕ n → ℕ} {g : vector ℕ (n + 2) → ℕ}, nat.primrec' f → nat.primrec' g → nat.primrec' (λ (v : vector ℕ (n + 1)), nat.elim (f v.tail) (λ (y IH : ℕ), g (y ::ᵥ IH ::ᵥ v.tail)) v.head)
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
.
Equations
- nat.primrec'.vec f = ∀ (i : fin m), nat.primrec' (λ (v : vector ℕ n), (f v).nth i)