Well, yes, but I'd argue that ordinary (transfinite) mathematical induction will work just fine here. It's just that the set we're doing mathematical induction over is one larger (in the ordinal sense) than usual. Let S = N union {w}, where N is the usual set of naturals and w is an additional new element. Adopt the usual well-ordering <= on N, and extend it to a new well-ordering by defining x <= w for every x.
Assign finite completely defined lists their usual lengths, and every _|_ terminated or infinite list, length w.
So every infinite object has a special length denoted "w". I assume we wish to make the following statements about "w"
w = w ~(w < w)
Without which "=" and "<" fail to have their intended meaning.
Suppose that if the statement P(x) holds for every x < y then it holds for y as well. Then P(y) holds by mathematical induction.
Then this induction hypothesis cannot apply to infinite lists. Suppose
xs is infinite. Then we assign it length "w". Now, (x:xs) is also infinite, and has length "w". But, ~(w < w), so we cannot conclude that P(x:xs) given P(xs).
One simply cannot reason based on the "size" of an infinite object in this way. You require a form of structural reasoning, and that means coinduction.
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
