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