# primitive recursion on untyped lambda calculus

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?

• I'm not sure what you mean by "a definition." If you look at Church Numerals they're basically an untyped way to do primitive recursion. – jmite Jan 14 '16 at 6:49
• So I can just ignore the type rules, and implement it on church numerals, and nothing bad will happen? – 44701 Jan 14 '16 at 6:58
• Nothing bad will happen, except for the bad things that happen in the untyped $\lambda$-calculus :-) – Andrej Bauer Jan 14 '16 at 13:23

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$.

• Since the OP started from the typed calculus, I believe it's worth mentioning that the standard definition of $Y$ is not typeable -- the above does not immediately translate back to the typed calculus. – chi Jan 15 '16 at 18:10
• That's true, but I feel that I am answering the question "Does a definition of primitive recursion exists for the untyped $\lambda$-calculus?", and so, answers the second question in the negative. – cody Jan 15 '16 at 18:32
• Also: the combinator $Y$ is not typeable in the simply typed calculus. One can work in a more lenient type system, or just add $Y$ by fiat, as in the PCF language. – cody Jan 15 '16 at 18:34