[Haskell-cafe] Detecting Cycles in Datastructures
Greg Woodhouse
gregory.woodhouse at sbcglobal.net
Fri Nov 18 15:03:03 EST 2005
--- Paul Hudak <paul.hudak at yale.edu> wrote:
>
> I suspect from your other post that you haven't seen the standard
> trick of encoding infinite data structures as fixpoints. Suppose you
> have a lambda calculus term for cons, as well as for the numeral 1.
> Then the infinite list of ones is just:
>
Not in quite those terms. Intuitively, I think of the infinite data
stucture here as being a kind of a "completion" of the space of
ordinary (finite) graphs to a space in which th given function actually
does have a fixed point.
> 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.
>
===
Gregory Woodhouse <gregory.woodhouse at sbcglobal.net>
"Interaction is the mind-body problem of computing."
--Philip Wadler
More information about the Haskell-Cafe
mailing list