On May 2, 2005, at 8:29 AM, Henning Thielemann wrote:
On Mon, 2 May 2005, Echo Nolan wrote:
Hello all, 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)? 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?
There must be some warranty that the resolution with respect to (:) stops somewhere. If you are sure that xs is shorter than x then the induction will stop sometimes. But if (x:xs) is infinite the induction won't work. I think you need some notion of the length of a list or some relation "one list is shorter than the other one" in order to explain induction.
Yes, to prove properties of an infinite (or a cyclic) list, co-recursion is indicated. Briefly, we must *assume* that the property holds for xs, and show that it holds for (x:xs). We must still show that it holds for [] if the property is to hold for finite lists as well. I'll leave it to others better qualified than myself to flesh this picture out. If induction leaves you dubious, you will find co-induction quite unconvincing. :-) -Jan-Willem Maessen
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe