[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, I also omited the word "countable". I figure it's understood
> >>>>>since computers only deal with finite data. And given an infinite
> >>>>>list, any finite "head" of it would meet the criteria, so the
> >>>>>distinction is moot. Unless Haskell has some neat property I am not
> >>>>>aware of :-)
> >>
> >>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.
> >>
> >
> > This property clearly violates the assumption for mathematical
> > induction that if P(x) is true for all x < y, then P(y) is true.
> 
> The problem here is that the haskell [] type is not actually an
> inductive type, but a coinductive type (which means one can construct
> infinite objects of that type).  The proof tools available to work with
> coinductive types differ somewhat from the tools used on inductive
> types.  In "Craft of FP", the author works with scheme, which has eager
> evaluation and thus cannot construct objects with coinductive type: thus
> the usual, familiar induction principles just work.  Haskell has lazy
> evaluation which allows the construction and manipulation of
> coinductive-typed objects.
> 
> Short story: when working with finite objects, regular induction works.
>   When working with infinite objects, be careful and read up on coinduction.
> 

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.

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.

This does indeed add an additional case to check relative to induction
over just the naturals, that is that if P(x) holds for every x in N,
then we must check that P(w) holds.

In general, this may or may not be a special case, though in the case
of lists, it almost certainly will be.
 - Cale