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

On 5/2/05, Cale Gibbard wrote:

On 5/2/05, robert dockins 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.

As an added note before I take a nap, if you find that the proof requirement given this definition of length is too difficult, you could also use the definition that [] and _|_ both have length zero, (x:xs) has length one more than the length of xs, for finite and finitely defined lists, and infinite lists have length w. This will probably make the proof come out more easily (but both ways are equally valid, provided that you meet the proof requirements for mathematical induction). This way means that we will be allowed to make use of the fact that P holds for all finite and finitely defined lists in order to prove that it holds for infinite lists. As a tradeoff, there's more work in the induction step and base case, but it's likely the same kind of work we were already doing. - Cale