CS212 Fall 1998
Structural Induction

Inductively Defined Sets

Recall from the handout on induction that induction is a method of proving statements about inductively defined sets. A set is inductively defined when it is generated from some base elements using some set of constructor operations.

We have seen many examples of induction on the natural numbers N = {0,1,2,...}. This set has a unique base element 0 and constructor operation inc that produces x+1 from x.

There are lots of other inductively defined sets. Another example of an inductively defined set is the set of lists in Dylan. For lists, the base element is the empty list () and the constructor is the pairing operator pair. Every list is constructed from () and some finite sequence of applications of pair.

We can prove facts about lists by induction on the length of the list, which essentially maps the argument into an induction on N. The basis handles lists of length 0, of which there is only one, namely (). The induction step assumes that the fact we are trying to prove is true for all lists of length less than n, then uses that assumption to establish that it is true for lists of length n.

Another approach is to do induction on lists directly, without talking about their length. This kind of induction is often called structural induction, although it is really no different from induction on N. This is possible because lists are inductively defined: there is a natural smallest list (), and all other lists are formed by pairing a new element with a smaller list.

Induction Principles

Every inductively defined set has its own induction principle that can be used in inductive proofs. For the natural numbers N, the induction principle is:

Suppose P is a property of numbers. If we can prove

  1. P is true of 0
  2. for any n, if P is true of all numbers less than n, then P is true of n
then we can conclude that P is true of all numbers n.

We often don't need the full power of the induction hypothesis ``P is true of all numbers less than n.'' Many times just knowing that P is true of n-1 is sufficient to establish that it is true of n. Thus the following weaker version of the induction principle is often sufficient:

Suppose P is a property of natural numbers. If we can prove

  1. P is true of 0
  2. for any n, if P is true of n, then P is true of n+1
then we can conclude that P is true of all natural numbers n.

The former version is often called strong induction principle and the latter the weak induction principle, although they are in fact equivalent in deductive power.

The Induction Principle for Lists

As in the handout on lists, we will write s.l for the pair with head s and tail l, i.e. the result of evaluating (pair s l), and () for the empty list, i.e. the result of evaluating '().

For lists, the appropriate induction principle is:

Suppose P is a property of lists. If we can prove

  1. P is true of ()
  2. for any list l and any object s, if P is true of l, then P is true of s.l
then we can conclude that P is true of all lists.

This is very similar to the weak induction principle for N. Note that there is no mention of length. One can argue the validity of this principle informally, the way we did for N, or one can prove its validity using induction on the length of lists.

An Example

Recall from the handout on lists the copy procedure for copying lists:

(define (copy <function>) (method ((l <list>)) (if (null? l) '() (pair (head l) (copy (tail l)))))) In that handout, we gave a proof by induction on length that this procedure was correct. Now let's try a proof by structural induction of the same thing.

We would like to show that for all lists l, 

(copy l) ==> l
Basis

We want to show (copy '()) ==> () Using the substitution model with apply steps omitted, (copy '()) ==> ((method ((l <list>)) (if (null? l) '() (pair (head l) (copy (tail l))))) '()) ==> (if (null? ()) '() (pair (head ()) (copy (tail ())))) ==> ()
Induction step

Assume that 
(copy l) ==> l
(this is the induction hypothesis), and let s be an arbitrary object. We wish to show that 
(copy s.l) ==> s.l
Again, using the substitution model with apply steps omitted, 
(copy s.l)
==> ((method ((l <list>))
       (if (null? l) '() (pair (head l) (copy (tail l))))) s.l)
==> (if (null? s.l) '() (pair (head s.l) (copy (tail s.l))))
==> (pair (head s.l) (copy (tail s.l)))
==> (pair s (copy l))  by the contract for lists
==> (pair s l)         by the induction hypothesis
==> s.l
By the induction principle for lists, we can now conclude that 
(copy l) ==> l
for all lists l.

Note that we never mentioned length anywhere in this argument.

Binary Trees

A binary tree can be represented as a class of objects composed of a left and right child: (define-class <btree> (<object>) (left <object>) (right <object>))

Each child will itself either be another (sub)tree or will be a leaf--some value stored at a terminal node of the tree. We will define a leaf to be anything that is not of type <btree>.

(define (leaf? <function>) (method ((x <object>)) (not (instance? x <btree>)))) We will denote by l.r the <btree> with left subtree l and right subtree r. We can create this tree using make: 
(make  left: l right: r) ==> l.r
The contract for binary trees is 
(left l.r) = l
(right l.r) = r

The depth of a binary tree is defined inductively: a leaf has depth zero, and the depth of l.r is defined to be 1 + max(depth l, depth r). Intuitively, if we envision a tree as a rooted graph-like structure, then the depth is the length of the longest path from the root to a leaf. (Food for thought: why might the inductive definition of depth be better to work with than the informal graph-theoretic definition?)

One can prove properties of binary trees by induction on depth. This essentially maps the argument into an induction on N. Here we would be using depth in the same way we used length for lists. This works because the depth of a tree is always strictly greater than the depth of its subtrees.

However, one can also use structural induction on trees directly. Such arguments rely on the following induction principle for binary trees:

Suppose P is a property of binary trees. If we can prove

  1. P is true of all leaves
  2. for any binary trees l and r, if P is true of l and r, then P is true of l.r
then we can conclude that P is true of all binary trees.

Another Example

Consider the following simple procedure to count the number of leaves in a binary tree:

(define (count-leaves <function>) (method ((tree <object>)) (if (leaf? tree) 1 (+ (count-leaves (left tree)) (count-leaves (right tree))))))

Let us show by structural induction that for any binary tree s with n leaves, 

(count-leaves s) ==> n
Basis

If s is a leaf, then by the substitution model, 
(count-leaves s)
==> (if (leaf? s)
         1
         (+ (count-leaves (left s))
            (count-leaves (right s))))
==> 1
Induction step

Assume (count-leaves l) and (count-leaves r) correctly count the leaves of the trees l and r, respectively. This is the induction hypothesis. We want to show that (count-leaves l.r) correctly counts the leaves of l.r.

Let n(l) be the number of leaves of l, and let n(r) be the number of leaves of r. Then the number of leaves of l.r is n(l.r) = n(l) + n(r), because a leaf of l.r is either a leaf of l or a leaf of r, but not both. Using the subtitution model, 

(count-leaves l.r)
==> (if (leaf? l.r)
        1
        (+ (count-leaves (left l.r))
        (count-leaves (right l.r))))
==> (+ (count-leaves (head l.r))
       (count-leaves (tail l.r)))  since l.r is not a leaf
==> (+ (count-leaves l)
       (count-leaves r))           by the contract for binary trees
==> (+ n(l) n(r))                  by the induction hypothesis
==> n(l) + n(r)
which is equal to n(l.r).

CS212 home page

Last Modified: 10/1/98 by dck