On 18/11/05, Paul Hudak
Cale Gibbard wrote:
Y = (\f. (\x. f (x x)) (\x. f (x x)))
In a sense, the real definition of Y is Y f = f (Y f), this lambda term just happens to have that property, but such functions aren't rare.
Actually no, the "real" definition is the top one, because the other one isn't even a valid lambda term, since it's recursive! There is no such thing as recursion in the pure lambda calculus.
I meant in the sense that Y f = f (Y f) is an axiomatic definition of Y. We're satisfied with any concrete definition of Y which meets that criterion. Of course it's not actually a lambda term, but it is an equation which a lambda term Y can satisfy. Similarly in, say, set theory, we don't say what sets *are* so much as we say what it is that they satisfy, and there are many models of set theory which meet those axioms. Y f = f (Y f) is really the only important property of Y, and any model of it will do as a concrete definition. - Cale
Of course, there are many valid definitions of Y, as you point out, both recursive and non-recursive. But I do believe that the first one above is the most concise non-recursive definition.
-Paul