[Haskell-cafe] Induction (help!)

[Luke Palmer]

After you grok induction over the naturals, you can start to think
about structural induction, which is usually what we use in
programming.  They are related, and understanding one will help you
understand the other (structural induction actually made more sense to
me when I was learning, because I started as a programmer and then
became a mathematician, so I thought in terms of data structures).

So let's say you have a tree, and we want to count the number of
leaves in the tree.

    data Tree = Leaf Int | Branch Tree Tree

    countLeaves :: Tree -> Int
    countLeaves (Leaf _) = 1
    countLeaves (Branch l r) = countLeaves l + countLeaves r

We want to prove that countLeaves is correct.   So P(x) means
"countLeaves x == the number of leaves in x".

First we prove P(Leaf i), since leaves are the trees that have no
subtrees.  This is analogous to proving P(0) over the naturals.

    countLeaves (Leaf i) = 1, by definition of countLeaves.
    "Leaf i"  has exactly one leaf, obviously.
    So countLeaves (Leaf i) is correct.

Now to prove P(Branch l r), we get to assume that P holds for all of
its subtrees, namely we get to assume P(l) and P(r).  You can think of
this as constructing an algorithm to prove P for any tree, and we have
"already proved" it for l and r in our algorithm.  This is analogous
to proving P(n) => P(n+1) in the case of naturals. So:

   Assume P(l) and P(r).
   P(l) means "countLeaves l == the number of leaves in l"
   P(r) means "countLeaves r == the number of leaves in r"
   countLeaves (Branch l r) = countLeaves l + countLeaves r, by definition.
   And that is the number of leaves in "Branch l r", the sum of the
number of leaves in its two subtress.
   Therefore P(Branch l r).

Now that we have those two cases, we are done; P holds for any Tree whatsoever.

In general you will have to do one such proof for each case of your
data structure in order to prove a property for the whole thing.  At
each case you get to assume the property holds for all substructures.

Generally not so many steps are written down.  In fact in this
example, most people who do this kind of thing a lot would write
"straightforward induction", and that would be the whole proof :-)

The analogy between structural induction and induction over the
naturals is very strong; in fact induction over the naturals is just
induction over this data structure:

    data Nat = Zero | Succ Nat

Hope this helps.

Luke

On Tue, May 6, 2008 at 7:15 AM, Daniel Fischer <daniel.is.fischer at web.de> wrote:
> Am Dienstag, 6. Mai 2008 11:34 schrieb PR Stanley:
>
> > 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
>  >
>
>  Mathematical induction is a method to prove that some proposition P holds for
>  all natural numbers.
>
>  The principle of mathematical induction says that if
>  1) P(0) holds and
>  2) for every natural number n, if P(n) holds, then also P(n+1) holds,
>  then P holds for all natural numbers.
>
>  If you choose another base case, say k instead of 0, so use
>  1') P(k) holds,
>  then you can deduce that P holds for all natural numbers greater than or equal
>  to k.
>
>  You can convince yourself of the validity of the principle the following ways:
>  Direct:
>  By 1), P(0) is true.
>  Specialising n to 0 in 2), since we already know that P(0) holds, we deduce
>  that P(1) holds, too.
>  Now specialising n to 1 in 2), since we already know that P(1) is true, we
>  deduce that P(2) is also true.
>  And so on ... after k such specialisations we have found that P(k) is true.
>
>  Indirect:
>  Suppose there is an n1 such that P(n1) is false.
>  Let n0 be the smallest number for which P doesn't hold (there is one because
>  there are only finitely many natural numbers less than or equal to n1.
>  Technical term: the set of natural numbers is well-ordered, which means that
>  every non-empty subset contains a smallest element).
>  If n0 = 0, 1) doesn't hold, otherwise there is a natural number n (namely
>  n0-1), for which P(n) holds but not P(n+1), so 2) doesn't hold.
>
>
>  Example:
>  The sum of the first n odd numbers is n^2, or
>  1 + 3 + ... + 2*n-1 = n^2.
>
>  1) Base case:
>  a) n = 0: the sum of the first 0 odd numbers is 0 and 0^2 = 0.
>  b) n = 1: the sum of the first 1 odd numbers is 1 and 1^2 = 1.
>
>  2) Let n be an arbitrary natural number. We prove that if the induction
>  hypothesis - 1 + 3 + ... + 2*n-1 = n^2 - holds, then
>  1 + 3 + ... + 2*(n+1)-1 = (n+1)^2 holds, too.
>
>  1 + 3 + ... + 2*(n+1)-1
>         = (1 + 3 + ... + 2*n-1) + 2*(n+1)-1
>         = n^2 + 2*(n+1) -1       -- by the induction hypothesis
>         = n^2 + 2*n + 1
>         = (n+1)^2
>  cqfd.
>
>  Hope this helps,
>  Daniel
>
>
>
>
>  _______________________________________________
>  Haskell-Cafe mailing list
>  Haskell-Cafe at haskell.org
>  http://www.haskell.org/mailman/listinfo/haskell-cafe
>