[Haskell-cafe] Formalizing lazy lists?

[Lennart Augustsson]

Greg Woodhouse wrote:
> 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?

In general, no.  Even in this case I'm pretty sure you'll need induction
somewhere.


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

I don't think you'll find such an embedding that is "satisfying", i.e.,
that gives you much insight.  Reasoning about total functions on
finite lists can be done with sets (and set theory), reasoning about
partial functions and/or lazy lists needs domains.
An example
	reverse . reverse = id
is true for all finite lists, but not true for any infinite lists
(nor any partial lists).
(What remains true for all lists is that
	reverse . reverse <= id
where <= is the usual domain ordering.)

	-- Lennart