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)?
Forget all the other replies. :-) The *real* reason that induction is a valid method of proving properties of lists is that *lists are themselves defined inductively*. (Except they aren't in Haskell--but let's pretend we're talking about ML for the moment.)
In ML (with Haskell syntax), when you write
data Nat = Zero | Succ Nat
what it means is something like this:
1. Zero is in Nat.
2. If x is in Nat, then Succ x is in Nat.
3. Nat contains only such elements as can be proven to belong to it by
rules 1 and 2.For example, Succ Zero is in Nat. Proof: Zero is in Nat (1); if Zero is in Nat, then Succ Zero is in Nat (instantiation of (2)); Succ Zero is in Nat (modus ponens). Note that this mirrors the way the value is actually constructed in program code (the Curry-Howard isomorphism).
Now, suppose you've proven
A. P(Zero). B. P(x) => P(Succ x).
Let n be any element of Nat. By rule 3, there is a proof that n belongs to Nat. Take that proof, and replace every occurrence of "x is in Nat" with "P(x)". The result will be a proof of P(n).
In other words, the inductive structure of the type ensures that we can construct a proof of P(n) for any n in the type by gluing together a finite number of primitive pieces (one for each data constructor). This is why it's sufficient to prove just A and B, and why they have this particular form.
This doesn't work in Haskell because Haskell types aren't constructed in this way. It's harder to prove properties of types in Haskell (and fewer properties actually hold).
-- Ben _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
