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

[Cale Gibbard]

This is, as others pointed out, an example of mathematical induction
at work. This is actually a slightly nontrivial instance of it, as
there is one more case than usual to be treated: lists can be
infinite. What happens to our proof when our list is infinite? Have we
really shown that the function works for all lists?

The answer is yes, the proof does work. Mathematical induction works
on what are called well-ordered sets. The naturals are just one
example. A set S with a relation <= is called well-ordered by <= if
the following hold:
1) <= is a partial order, that is:
 a) a <= a for every a in S (reflexivity)
 b) If a <= b and b <= a for any a,b in S, then a = b (antisymmetry)
 c) If a <= b and b <= c then a <= c for any a,b,c in S. (transitivity)
2) <= is additionally a total order, that is for any a and b in S,
we have a <= b or b <= a. (comparability)
3) Every nonempty subset T of S has a least element with respect to
<=. That is, there is some x in T such that for any a in T, we have x
<= a.

Note that the natural numbers are well-ordered by the usual <= under
this definition. Also, the lengths of lists, with the single infinity,
which I'll call w, under the ordering inherited from the naturals, and
x <= w for every x is still well ordered. (You might want to check
this) As an example, the set of integers with the usual ordering is
not well ordered.

Now suppose that F is some logical formula with a single free
variable, and that S is a well ordered set under the relation <=. Let
0 be the least element of S under this relation.

Additionally, suppose that F(0) is true (this is actually implied by
the following), and that if F(x) is true for all x < y in S,  then
F(y) is true as well. (x < y means that x <= y, and x /= y)

We will show that F(x) is true for all x in S by way of contradiction.

Suppose that there is some x such that F(x) is false. Consider the set
of all such x in S, that is {x | not F(x)}. This set is nonempty by
assumption, so it has a least element, say c.

Then for any x < c, F(x) must hold, because otherwise c would not be
the least element where F fails to be true. So, for every x < c, F(x)
is true, and by assumption F(c) must be true as well. But F(c) was
supposed to be false, which is a contradiction.

So our extra assumption that there was an x for which F(x) was false
must be wrong. So F(x) must be true for all x in S.

So, that's induction for sets of any size. It's possible to go a
little farther with it, but I think this is more than enough.

So there you have it, a proof that mathematical induction works. You
might want to check that the lengths of lists (including the infinite
length w) are well ordered.

I hope this helps.
 - Cale Gibbard

On 5/2/05, Echo Nolan <hellish at comcast.net> wrote:
> Hello all,
>         My copy of HS: The Craft Of FP just arrived and I was reading
> section 8.5 about induction. On page 141, Simon Thompson gives a
> method of proving properties of functions on lists:
>         1) Prove that the property holds for the null list
>         2) Prove that the property holds for (x:xs) under the assumption
>                 that the property holds for xs.
> 
>         My question is this: what is the proof of (P([]) and ( P(xs) => P(x:xs))) => P(xs)?
> In other words, how does proof of the property on empty lists and proof
> that the property holds on (x:xs) under the assumption that it holds on
> xs give proof that it holds on all lists? Isn't there a recursive
> dependency here? You are defining the proof for lists with at least one
> element based on the assumption that it holds for all lists, right? How
> does this get you a proof of the general property if it depends on the
> assumption of the general property?
> 
> Regards and thanks,
> Echo Nolan.
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
> 
> 
> 
>