[Haskell-cafe] Infinite lists and lambda calculus (was: Detecting Cycles in Datastructures)

Greg Woodhouse gregory.woodhouse at sbcglobal.net
Fri Nov 18 18:45:22 EST 2005

--- Lennart Augustsson <lennart at augustsson.net> wrote:

I guess I'm not doing a very good job of expressing myself. I see that
if you define Y as you do, then the various functions you list have the
property that Y f = f (Y f).

I don't want to draw out a boring discussion that is basically about my
own qualms here, especially since I haven't really been able to
articulate what it is that bothers me.

Perhaps the issue is that the manipulations below are purely syntactic,
and though they work, it is not at all clear how to make contact with
other notions of computability. Perhaps it is that

Y = (\f. (\x. f (x x)) (\x. f (x x))) 

is a perfect sensible definition, it's still just a recipe for a
computation. Maybe I'm thinking too hard, but it reminds me of the mu
operator. Primiive recursive functions are nice and constructive, but
minimization is basically a "search", there's no guarantee it will
work. If I write

g(x) = mu x (f(x) - x)

then I've basically said "look at every x and stop when you find a
fixed point". Likewise, given a candidate for f, it's easy to verify
that Y f = f (Y f), as you've shown, but can the f be found without
some kind of "search"? Since there are recursive functions that aren't
primitive recursive, the answer has to be "no".

Finally, you've exhibited a sequence of fixed points, and in this case
it's intuitively clear how these correspond to something we might call
an infinite list. But is there an interpetration that makes this
precise? The notation

ones = cons 1 ones
ones = cons 1 (cons 1 ones)

is suggestive, but only suggestive (at least as far as I can see). Is
there a model in which [1, 1 ...] is a real "thing" that is somehow
"approached" by the finite lists?
> You can easily verify that
> 	Y f = f (Y f)
> LHS =
> Y f =
> (\f. (\x. f (x x)) (\x. f (x x))) f =
> (\x. f (x x)) (\x. f (x x)) =
> f ((\x. f (x x) (\x. f (x x)))
> RHS =
> f (Y f) =
> f ((\f. (\x. f (x x)) (\x. f (x x))) f) =
> f ((\x. f (x x)) (\x. f (x x)))
> So (\f. (\x. f (x x)) (\x. f (x x))) is a fixpoint combinator
> (one of infinitely many).
> 	-- Lennart
> 	-- Lennart

Gregory Woodhouse  <gregory.woodhouse at sbcglobal.net>

"Interaction is the mind-body problem of computing."

--Philip Wadler

More information about the Haskell-Cafe mailing list