On 11/13/10 8:15 AM, Will Sonnex wrote:
Infinite values (lazy-evaluation in general) also give Zeno a problem, since you can no longer use structure as a well-defined ordering for induction. A property such as "reverse (reverse xs) === xs" does not work for infinite lists, since you can successfully case-analyse values from "xs" but case-analysing "reverse (reverse xs)" will give an infinite loop. You could say the values are equal in some sense (maybe given infinite computation time) but they do not behave in the same way.
Generally speaking the solution for handling possibly infinite structures is to use coinduction rather than induction. The reason "reverse (reverse xs) === xs" doesn't work for (possibly)infinite lists is that we can't prove that reverse.reverse makes any progress (since reverse of an infinite list is bottom). But there are plenty of other things you could still prove for infinite structures, "map f (map g xs) === map (f.g) xs" for example. -- Live well, ~wren