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

[Jan-Willem Maessen]

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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe