[Haskell-cafe] Induction (help!)

[Daniel Fischer]

Am Dienstag, 6. Mai 2008 23:34 schrieb PR Stanley:
> 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).
> 	Paul: I was hoping that understanding the classic mathematical
> concept would help me appreciate the structural computer science)
> variation better.

Understanding either will help understanding the other, they're the same idea 
in different guise.

> I don't know what it is about induction that I'm
> not seeing. It's so frustrating! Deduction in spite of the complexity
> in some parts makes perfect sense. This, however, is a different beast!
>
> 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".
> 	Paul: By 'correct' presumably you mean sound.
>
> 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.
> 	Paul: I'd presume 'proof' here means applying the function to one
> leaf to see if it returns 1. If I'm not mistaken this is establishing
> the base case.

Yes, right.

>
>      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).
> 	Paul: How did you arrive at this decision? Why can we assume that P
> holds fr all its subtrees?

It's the induction hypothesis.
We could paraphrase the induction step as "If P holds for all cases of lesser 
complexity than x, then P also holds for x".
In this example, the subtrees have lesser complexity than the entire tree (you 
could define complexity as depth).
The induction step says "assuming P(l) and P(r), we can deduce P(Branch l r)", 
or, as a formula,
forall l, r. ([P(l) and P(r)] ==> P(Branch l 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.
> 	Paul: Is this the function definition for countLeaves?
>
> 	This is analogous to proving P(n) => P(n+1) in the case of naturals.
> 		Paul:I thought P(n) was the induction hypothesis and P(n+1) was the
> proof that the formula/property holds for the subsequent element in
> the sequence if P(n) is true. I don't see how countLeaves l and
> countLeaves r are analogous to P(n) and P(n+1).

(countLeaves l == number of leaves in l) and (countLeaves r == number of 
leaves in r) together are analogous to P(n).
Proving
forall l, r. ([P(l) and P(r)] ==> P(Branch l r))
is analogous to proving
forall n. [P(n) ==> P(n+1)].

Let me phrase mathematical induction differently.
To prove
forall natural numbers n. P(n)
, it is sufficient to prove
1) P(0)
and
2) forall n. [P(n) implies P(n+1)]
. And structural induction for lists:
To prove 
forall (finite) lists l . P(l)
, you prove
1L) P([ ])   -- the base case is the empty list
2L) forall x, l. [P(l) ==> P(x:l)]
and for trees:
to prove
forall trees t. P(t)
, you prove
1T) forall i. P(Leaf i)
2T) forall l, r. ([P(l) and P(r)] ==> P(Branch l r)).

In all three cases, the pattern is the same. The key thing is number 2, which 
says if P holds for one level of complexity, then it also holds for the next 
level of complexity. In the domino analogy, 2) says that the dominos are 
placed close enough, so that a falling domino will tip its neighbour over.
Then 1) is tipping the first domino over.


>
> 		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
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe