On 18/11/05, Paul Hudak <[EMAIL PROTECTED]> wrote: > 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 > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe