Structural induction

Introductory example

Define: a binary tree is either empty, called a leaf, or (make-node datum t1 t2), where t1,t2 are binary trees.

Prove: for any binary tree t, #leaves(t) = #nodes(t) + 1.

• Define #nodes(), #leaves() recursively.

How to prove?

• (Strong or weak) induction on #nodes.
• (Weak) induction on height.
• Somehow trying to pair up leaves and nodes, with one leaf unpaired. How in general, for arbitrary binary tree?
• Structural induction.

Example

Define: an n-ary tree is either empty, or (make-node datum ts), where ts is an n-tuple of n-ary trees.

Prove: For any n-ary tree, #nodes(t) ≤ n^height(t)-1

• Define n-ary tree recursively.
• Define #nodes(), height() recursively.

Semi-aside: other ways to prove same thing?

• As before, strong induction on #nodes or height.
• Note: induction on n not helpful.
• Prove inductively for complete n-ary trees, then argue arbitrary tree has no more nodes that complete tree.
• Prove as a sum of #nodes per level for either complete or general tree.

Example

Prove: For any propositional WFF f, #connectives(f) ≥ #propositions(f) - 1.

Proof has same number of base and inductive cases as the data definition.

Example

Define strings: For a set Σ (the alphabet), the set Σ^* ("strings over Σ") contains:

• λ (empty string)
• wa, where a ∈ Σ, and w ∈ Σ^*.

Define length.

Define concatenation: For v,w ∈ Σ^*, define vw ∈ Σ^* as follows:

• If w=λ, vw = v.
• if w=ua (for a letter a and a string u), vw = (vu)a.

Prove: length(vw) = length(v) + length(w).

• Use induction on what? v or w? Why?
• Induction on w matches the definition of concatenation. P(w) = "length(vw) = …" (for arbitrary string v).

Example

; append: list, list -> list
;
(define (append x y)
   (cond [(empty? x) y]
         [(cons?  x) (cons (first x)
                           (append (rest x) y))]))

Prove:

For any list a, (append a (append a a)) = (append (append a a) a)

Ironically, by proving a stronger statement, your life actually becomes easier! Prove:

For any lists a,b,c, (append a (append b c)) = (append (append a b) c).

First, must decide what to do induction on: a, b, or c?

Induction on a: let P(a) be "For all lists b,c, (append a (append b c)) = (append (append a b) c)".

Known as generalizing or loading the inductive hypothesis.

Why all these different forms of induction?

To ponder: Is weak induction on numbers enough?

Induction can be used on any data defined recursively (or inductively), i.e., anything tree-like.

Note: Other forms of induction, e.g., co-induction and transfinite induction, allow you to do different kinds of things. They are more advanced and much less useful in CS.

Structuring proofs correctly

Always start your proofs starting with the larger data.

E.g., let P(t) be "#nodes(t) ≤ 2^height(t)-1". We prove P(t) holds for all binary trees t by structural induction.

• More clear:
  • Case 1, t = empty: …
  • Case 2, t = (make-node datum t1 t2), where t1 and t2 are binary trees:
    By our inductive hypothesis, we know P(t1) and P(t2), that is …
• Less clear:
  • Case 1: P(empty): …
  • Case 2: Assume P(t1) and P(t2) hold, for some trees t1,t2. Then we show that P((make-node datum t1 t2)) holds: …

The first approach is better since it says "You give me any tree t, and I'll reason with it."

The second approach is round-about, saying "Well, if something holds for some smaller trees t1 and t2, then it holds for a tree made out of them." Left unstated is: "Oh, and this tree I made out of the t1,t2 happens to be representative of all trees. It captures all cases."