[Haskell-cafe] Detecting Cycles in Datastructures

[Greg Woodhouse]

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