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. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
