# [Haskell-cafe] Detecting Cycles in Datastructures

Lennart Augustsson lennart at augustsson.net
Fri Nov 18 18:10:30 EST 2005

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