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

[Daniel Carrera]

Hi Echo,

I'm totally new at Haskell btw. But I'll comment a bit. :-)

> My copy of HS: The Craft Of FP just arrived

Is it good? Do you recommend it? Should I get a copy too?

> 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.

Cool. Mathematical induction. I can see how that would be a sueful skil 
for an FP programmer.

> 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?

I'll offer two explanations. Hopefully one will make sense. :-)

Explanation 1:

Fact (*): You proved P(xs) => P(x:xs).

step 0: prove for the empty list.
step 1: given (*) and step 0, you get the result for a 1-item list.
step 2: given (*) and step 1, you get the result for a 2-item list.
...
step n: given (*) and step n-1, you get the result for a n-item list.

Explanation 2:

Start with any list xs, it can be written in the form (y:ys). So if you 
prove the property for ys you're done, right? Continue this recursively, 
removing one entry on each round. Eventually you'll hit an empty list. 
But you proved the property for the empty. So, recursively, you've 
proven it for all lists.

Hope that helps.

This is called mathematical iduction. It is one of the most popular 
methods of proving theorems in mathematics.


Cheers,
Daniel.