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

[Daniel Fischer]

Am Dienstag, 3. Mai 2005 03:48 schrieben Sie:
> Daniel Fischer writes:
> > Due to lazyness, we can have infinite lists (and other infinite
> > structures) in Haskell (of course, in finite time, only a finite
> > portion of those can be evaluated), e.g. ns = [1 .. ] :: [Integer] is
> > an infinite list which is often used. And now consider the property P
> > that there exists a natural number n so that the list l has length n.
> >
> > Obviously P holds for all finite lists, but not for the infinite list
> > ns.
>
> You can avoid some problems like that by using lazy naturals, e.g.:
>
>     data Nat = Zero | Succ Nat
>
>     instance Eq Nat where m == n = compare m n == EQ
>
>     instance Ord Nat where
>         compare Zero     Zero     = EQ
>         compare Zero     (Succ _) = LT
>         compare (Succ _) Zero     = GT
>         compare (Succ m) (Succ n) = compare m n
>
>     infinity = Succ infinity
>
>     length []     = Zero
>     length (x:xs) = Succ (length xs)
>
> Everything terminates, as long as you don't try to compare two infinite
> values.

Mea culpa,

I probably should have stated it quite explicitly:
this example was intended to illustrate the difference between finite and 
infinite lists with respect to inductive proofs.

The proof scheme

(1) P([])
(2) (forall xs) (forall x) (P(xs) => P(x:xs))

yields an induction over the natural numbers:
let Q(n) = for all lists xs of length n, P(xs) holds.

Then (1) --> (i) Q(0),
(2) --> (ii) (forall n) (Q(n) => Q(n+1)).

But by step (ii) we only reach successor ordinals, so, as Cale Gibbard pointed 
out, to handle infinite lists we must take the step to transfinite induction, 
for 'w' (closest Ascii character to omega) is a limit ordinal.

The scheme for transfinite induction is

(i) Q(0)
(iia) [(forall n) (n < m => Q(n))] => Q(m)

as stated by Cale. This reaches all ordinals.
My example has the property that (ii) holds, but (iia) doesn't.

Conclusion: to handle infinite lists, we must extend our toolkit - replacing 
(ii) by (iia) isn't the only possibility, of course.

Cheers,
Daniel