[Haskell-cafe] Clarification on proof section of HS: The Craft of FP

[robert dockins]

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