[Haskell-cafe] Detecting Cycles in Datastructures

[Paul Hudak]

Greg Woodhouse wrote:
> --- Paul Hudak <paul.hudak at yale.edu> 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