--- Lennart Augustsson <lennart@augustsson.net> wrote:
Unfolding Y is indeed part of the algorithm to generate the list. The lambda calculus is "just" another programming language, so why does this disturb you?
Well...think about this way. The function f i = [1, 1 ..]!!i is just a constant function expressed in a complicated way. Can I algoritmically determine that f is a constant function? For any particular value of i, the calculations you give demonstrate that f i = 1. It's a little less obvious that f really is constant. Yes, I know this can be proved by induction, but verifying a proof is not the same as discovering the theorem in the first place. I suppose the big picture is whether I can embed the theory of finite lists in the theory of infinite lists, preferably in such a way that the isomorphism of the theory "finite lists" with the embedded subtheory is immediately obvious. === Gregory Woodhouse <gregory.woodhouse@sbcglobal.net> "Interaction is the mind-body problem of computing." --Philip Wadler