Re: [Haskell-cafe] Detecting Cycles in Datastructures

Greg Woodhouse wrote:

--- Paul Hudak wrote:

...

The important property of Y is this:

Y f = f (Y f)

Right. This is just a formal statement of the property thaat f fixex Y f. I'm with you so far.

...

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)

I'm with you here, too, except that we are *assuming* that Y has the stated property. If it does, it's absolutely clear that the above should hold.

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