Primitive Recursive Function

A primitive recursive function is a function $\mathbb{N}^{k}\to\mathbb{N}$ on Natural Numbers that is either:

• A constant function $\lambda\overline{x}.\;n:\mathbb{N}^{k}\to\mathbb{N}$
• A projection function $\lambda\overline{x}.\;\overline{x}_{i}:\mathbb{N}^{k}\to\mathbb{N}$
• The successor function $\lambda x.\;s(x):\mathbb{N}\to\mathbb{N}$
• An k-ary composite $\lambda\overline{x}.\;f(g_{1}(\overline{x}),g_{2}(\overline{x}),\cdots,g_{k}( \overline{x}))$ where $f$ and all the $g_{i}$ are primitive recursive.
• Primitive recursion $\lambda\overline{x}.\rho(f,g,x_{0},\overline{x})$