= Lambda definition of primitive recursion by pair iteration
If total <functions> $g$ and $h$ are represented by <lambda terms> $G,H$, define
$$
\mathsf{Step}_{\mathbf x}=\lambda p.\mathsf{Pair}(\mathsf{Succ}(\mathsf{Fst}\,p))(H\mathbf x(\mathsf{Fst}\,p)(\mathsf{Snd}\,p)),
$$
and
$$
R=\lambda\mathbf x n.\mathsf{Snd}\bigl(n\mathsf{Step}_{\mathbf x}(\mathsf{Pair}\,c_0\,(G\mathbf x))\bigr).
$$
After $j$ iterations the <Church pair> holds $(c_j,c_{f(\mathbf x,j)})$, proved by <mathematical induction> using the defining recursion equations. Consequently $R$ represents the total <primitive recursive function> $f$. This statement concerns total inputs and total recursion constituents; it is not an unguarded composition theorem for arbitrary partial <functions>.
Back to article page
