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.