[Haskell-cafe] Detecting Cycles in Datastructures

[Greg Woodhouse]

--- 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.

> 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.

Right.

> 
> 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))

Now, this is where things get a little mysterious. Where did g come
from?

I understand that the "x x" om formal definition of Y is what makes
everything work (or, at least I think I do). When I try and think this
all through, I wind up with something like this:

First of all, I'm after a "list" (named ones) with the property that
ones = cons 1 ones. How can I express the existence of such a thing as
a fixed point? Well, if it does exist, it must be a fixed point of f =
\x. cons 1 x, because

f ones ==> (\x. cons 1 x) ones ==> cons 1 ones ==? ones

Now, if I write

Y = \y. (\x y (x x)) (\x. y x x)

then,

Y f ==> cons 1 (\x. cons 1 ( x x)) (\x (cons 1) x x)

and I'm left to ponder what that might mean. Formally, I can see that
this pulls an extra cons 1 out to the left, and so we're led to your g

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

To me, all this really seems to be saying is that for any n, there's a
lambda expression explicitly involving [1, 1, ..., 1] (n times) that is
a "solution" to the above problem, which I interpet (perhaps
incorrectly) to mean that *if* there were a "real" list that wedre a
solution to the above recurrence, then for any n, there would be an
initial sublist consisting of just 1's.

Now, I know that lambda expressions are not lists, though lists can be
encoded as lambda expressions. For finite lists, this all seem simple
enough, but in this case we seem to have a lambda expression that is
not a (finite) list, but that can nevertheless be "approximated" in
some3 sense by finte lists.

But I can't really put my finger on just what that sense might be.
> 
> Does this help?

Yes, it does. Very much so.
> 
>    -Paul
> 
> 



===
Gregory Woodhouse  <gregory.woodhouse at sbcglobal.net>


"Interaction is the mind-body problem of computing."

--Philip Wadler