primitive recursion

Primitive recursion

May 11, 2020
type theory
primitive recursion

Finding a primitive recursion representation of a given function \(f\) can be reduced to finding functions \(g, h, k\) such that \(f(m,0) = g(m)\) \(f(m,S(n)) = k(h(m,n), f(m,n))\) where \(S: \mathbf{N} \rightarrow \mathbf{N}\) is a successor function turning a natural number into its successor (1 maps to 2, 2 maps to 3, and so on). The sought functions should be a composition of one of the following primitive functions: ...