Does a definition of primitive recursion exist for the untyped lambda calculus? Does the definition of primitive recursion require typing for natural numbers?
The only definitions I can find are for the typed lambda calculus: http://www.math.nagoya-u.ac.jp/~garrigue/lecture/2013_tenbo/recfun_en.pdf. Perhaps if I just ignore the types it will still be valid?
Famously, the fixed-point operator $Y$ of the untyped $\lambda$-calculus, which has the property that $$ Y\ F=_{\beta}F\ (Y\ F)$$ for every term $F$, is enough to implement primitive (and indeed, non-primitive!) recursion.
Given any encoding of the natural numbers which allows decrementing, if you have an expression $$ e(n)=C[e(n-1)]$$ where $C$ is some programatic context, you can create a term, $P_e$, defined by: $$ P_e\equiv\lambda F\ n.C[F\ (n-1)] $$
Now it's easy to show that $$(Y\ P_e)\ n = P_e\ (Y\ P_e)\ n= C[(Y\ P_e)\ (n-1)]$$ and so it makes sense to define the function $e$ as $Y\ P_e$.
