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

[Cale Gibbard]

On 5/2/05, Cale Gibbard <cgibbard at gmail.com> wrote:
> 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.

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