[Haskell-cafe] Clarification on proof section of HS: The Craft of
daniel.is.fischer at web.de
Mon May 2 09:46:57 EDT 2005
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.
> > 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
> 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.
More information about the Haskell-Cafe