[Haskell-cafe] Infinite lists and lambda calculus
cgibbard at gmail.com
Fri Nov 18 22:39:13 EST 2005
On 18/11/05, Paul Hudak <paul.hudak at yale.edu> 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.
> 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.
More information about the Haskell-Cafe