Re: [Haskell-cafe] Detecting Cycles in Datastructures

18 Nov 2005

      Greg Woodhouse wrote:
...
--- Paul Hudak  wrote:
...
Y (\ones. cons 1 ones)
where Y (aka the "paradoxical combinator" or "fixed point
combinator") is defined as:
\f. (\x. f (x x)) (\x. f (x x))
Now, this is I have seen, but it frankly strikes me as a "formal
trick". I've never felt that this definition of Y gave me much insight
into the computation you describe below.
...
To see this, try unfolding the above term a few iterations using
normal-order reduction.  Note that the term has no recursion in it 
whatsoever.
Now, my earlier point above is that:
Y (\ones. cons 1 ones)
unwinds to the same term as:
Y (\ones. cons 1 (cons 1 ones))
yet the two terms (\ones. cons 1 ones) and
(\ones. cons 1 (cons 1 ones)) are not the same (in fact they're not 
lambda convertible, either).
-Paul
And this is what leaves me scatching my head. If you leave off the
"ones", then you get a sequence of finite lists [1], [1, 1], ... that
seems to approximate the infinite list, but I find it difficult to
imagine how you might pluck a formula like \i. 1 (the ith term)  out of
the air.
The important property of Y is this:

Y f = f (Y f)

In this way you can see it as "unwinding" the function, one step at a 
time.  If we define f as (\ones. cons 1 ones), then here is one step of 
unwinding:

Y f ==> f (Y f) ==> cons 1 (Y f)

If you do this again you get:

cons 1 (cons 1 (Y f))

and so on.  As you can see, continuing this process yields the infinite 
list of ones.

Now note that if we define g as (\ones. cons 1 (cons 1 ones)), we get:

Y g ==> g (Y g) ==> cons 1 (cons 1 (Y g))

which obviously also yields the infinite list of ones.  Yet f is not 
equal to g.

Does this help?

   -Paul