Induction

Consider the following code, which defines a tree and some operations on it:

(defstruct <tree> left right)

(define (leaf? t) (not (tree? t)))

(define (count-leaves t)
   (if (leaf? t)
       1
       (+ (count-leaves (get-tree-left t))
          (count-leaves (get-tree-right t)))))

Consider a binary tree t, with left and right subtrees t.l and t.r respectively. The depth of t is defined to be one larger than the depth of its deeper subtree, that is depth(t) = 1 + max(depth(t.l), depth(t.r)). When t is a leaf node, meaning it has neither left nor right subtrees, its depth is 0.

Assume that for a binary tree t, represented using the structure <tree> , that (leaf? t) is true only when t is a leaf node. Moreover assume that when (leaf? t) is false that (left t) = t.l and (right t) = t.r, that is that the accessors return the left and right subtrees respectively.

Using induction and the substitution model, prove that (count-leaves t) counts the number of leaf nodes in any tree t. We will break the question up into three parts: what you are inducting over, the induction hypothesis, and then the proof itself.

1. What are you inducting over?
   
   
   
2. Give a clear, concise statement of your induction hypothesis.
   
   
   
3. Give an inductive proof that (count-leaves t) counts the number of leaf nodes in any tree t. Remember to have clear, separate base case and induction step. Use the induction hypothesis you gave above.
   
   
   
   
   
   

Solution

Return to CS 212 Prelim 1 - Fall 1996