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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
