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

[Daniel Fischer]

Am Montag, 2. Mai 2005 14:20 schrieb 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?

It is good. Best would be to have an extensive look and decide for yourself. 
But if that's not possible, I'd say, though rather expensive, it's worth the 
money. BTW, I don't know it, but the 'Haskell School of Expression' (by Paul 
Hudak, if I remember correctly) is said to be good, too, so you might want to 
take a look at both and compare.

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

Quite!
>
> > 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. :-)

Both do, but in Explanation 2, you omitted 'finite' a couple of times.

Let me rephrase it:
You prove P([]) and
(forall finite lists xs) (forall x) (P(xs) => P(x:xs)).

Then you can deduce P(ys) for all finite lists ys because all such are reached 
in a finite number of steps. (I tacitly assumed that all lists and elements 
are defined, the case of partially defined lists is treated later in the 
book.)
>
> 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.

Cheers back,
Daniel