You're replying to a comment by dasuxullebt.

February 21, 2010, 14:13

The problem with the Y-Combinator is, that it cannot be typed. We have Y = \s.(\x.s(x x))(\x.s(x x)), such that Ys reduces to (\x.s(x x))(\x.s (x x)) which reduces to s((\x.s(x x))(\x.s(x x))) = s Ys, thus, having Ys reducing to all sssss...sYs, which means, Ys is not strongly normalizing - and since all typed lambda terms are strongly normalizing, it cannot be typed (actually, in the same way, no fixpoint combinator can be typed).

Anyway, even strongly typed programming languages like Haskell have recursion, even though mostly through calling the function by its name. In the theory of typed lambda terms, you therefore mostly axiomatically define recursion operators, like R:(a->a)->(a->bool)->a, which applies the first argument to a until (a->bool) gets true (there are a lot of other possibilities, though). Anyway, these cannot be expressed as terms, they must be defined axiomatically.

Reply To This Comment

(why do I need your e-mail?)

(Your twitter name, if you have one. (I'm @pkrumins, btw.))

Type the first letter of your name: (just to make sure you're a human)

Please preview the comment before submitting to make sure it's OK.