[Haskell-cafe] Detecting Cycles in Datastructures

[Lennart Augustsson]

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