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

[Cale Gibbard]

On 5/2/05, robert dockins <robdockins at fastmail.fm> wrote:
> > 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).
> 
I didn't claim that this what we need to prove in this case. We need
to prove that P holds on lists of length w given that it holds on
lists of every finite length.

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