[Haskell-cafe] Detecting Cycles in Datastructures
Paul Hudak
paul.hudak at yale.edu
Fri Nov 18 15:45:13 EST 2005
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
More information about the Haskell-Cafe
mailing list