[Haskell-cafe] Formalizing lazy lists?

[Greg Woodhouse]

--- Lennart Augustsson <lennart at 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 at sbcglobal.net>


"Interaction is the mind-body problem of computing."

--Philip Wadler