[Haskell-cafe] Infinite lists and lambda calculus

[Cale Gibbard]

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.

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