[Haskell-cafe] Re: Induction (help!)

[Achim Schneider]

PR Stanley <prstanley at ntlworld.com> wrote:

> 
> > > Hi
> > > I don't know what it is that I'm not getting where mathematical
> > > induction is concerned. This is relevant to Haskell so I wonder if
> > > any of you gents could explain in unambiguous terms the concept
> > > please. The wikipedia article offers perhaps the least obfuscated
> > > definition I've found so far but I would still like more clarity.
> > > The idea is to move onto inductive proof in Haskell. First,
> > > however, I need to understand the general mathematical concept.
> > >
> > > Top marks for clarity and explanation of technical terms.
> > >       Thanks
> > > Paul
> > >
> >Induction -> from the small picture, extrapolate the big
> >Deduction -> from the big picture, extrapolate the small
> >
> >Thus, in traditional logic, if you induce "all apples are red",
> >simple observation of a single non-red apple quickly reduces your
> >result to "at least one apple is not red on one side, all others may
> >be red", i.e, you can't deduce "all apples are red" with your
> >samples anymore.
> 
>          Paul: surely, you wouldn't come up with an incorrect premise 
> like "all apples are red" in the first place.
> Sorry, still none the wiser
> Cheers,
> Paul

well, "all 'apples' are 'red'" is the proof you want to make. And it can
be correctly induced, if and only if you can prove that

a) all 'apples' share the same behaviour regarding the property 'colour'
b) one 'apple''s colour property is 'red'

which leads you directly to 
c) every 'apple' (that is, potentially infinite many) 'apples' are
'red'.

if b) concludes that one 'apples''s colour property is not 'red', of
course, you can't say "all 'apples' are 'red'" and still write QED
beneath your proof without having to admit that that wasn't what you
wanted to demonstrate.

As an example, you might construct a proof that every faculty of any
number is positive:


fac 0 = 1
fac n | n > 0 = n * (fac (n-1))
fac _ = undefined

You don't have to go on to proving an infinite number of possible
inputs, you only have to prove 

1) that 1 is positive (by definition)
2) that any number greater than 0 is positive (by definition)
3) that multiplication of two positive numbers results in a positive
number (by definition)
4) that only positive numbers get multiplicated (by analysing
haskell's semantics, read: data flow). 

So, as soon as you have proved the properties of the fixed point, the
whole, infinite set is proven.

-- 
(c) this sig last receiving data processing entity. Inspect headers for
past copyright information. All rights reserved. Unauthorised copying,
hiring, renting, public performance and/or broadcasting of this
signature prohibited.