2
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • 1
    $\begingroup$ 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. $\endgroup$ – jmite Jan 14 '16 at 6:49
  • $\begingroup$ So I can just ignore the type rules, and implement it on church numerals, and nothing bad will happen? $\endgroup$ – 44701 Jan 14 '16 at 6:58
  • 1
    $\begingroup$ Nothing bad will happen, except for the bad things that happen in the untyped $\lambda$-calculus :-) $\endgroup$ – Andrej Bauer Jan 14 '16 at 13:23
4
$\begingroup$

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

Improve this answer
$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$ – chi Jan 15 '16 at 18:10
  • $\begingroup$ 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. $\endgroup$ – cody Jan 15 '16 at 18:32
  • $\begingroup$ 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. $\endgroup$ – cody Jan 15 '16 at 18:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.