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?
primitive recursion on untyped lambda calculus
lambda calculus;primitive recursion
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$.