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