Next: Abstraction and Class Definitions Up: CS212 Preliminary Exam I Previous: Higher-Order Functions (10 points)

Induction (20 points)

A proper binary tree of integers is defined inductively as follows:

• '() (null) is a proper binary tree of integers.
• If t and s are proper binary trees of integers, and i is an integer, then (pair i (pair t s)) is a proper binary tree of integers.

The following function computes the ``mirror image of a proper tree of integers where the left and right sub-trees are swapped (and their sub-trees are swapped, etc.):

   (define (mirror <function>)
     (method ((t <object>))
       (if (null? t) '()
           (bind (((i <integer>) (head t))
                  ((left <object>) (head (tail t)))
                  ((right <object>) (tail (tail t))))
             (pair i (pair (mirror right) (mirror left))))

You are to formally prove by structural induction and the substitution model that the property P(x) (defined below) holds for all proper binary integer trees x:

P(x) is (mirror (mirror x)) evaluates to x.

Be sure to cover the base case and the inductive case. For the inductive case, be sure to state your induction hypothesis (what you're assuming) and what you're trying to show. Also, be sure to note where you are using your induction hypothesis to justify your argument. You may abbreviate steps in the substitution model as long as it is clear what is going on.

Base case ( P('()) ).

(mirror (mirror '())) ->*

(mirror (if (null? '()) '()
               (bind (((i <integer>) (head '()))
                      ((left <object>) (head (tail '())))
                      ((right <object>) (tail (tail '()))))
                 (pair i (pair (mirror right) (mirror left))))) ->*

(mirror '()) ->*

(if (null? '()) '()
       (bind (((i <integer>) (head '()))
              ((left <object>) (head (tail '())))
              ((right <object>) (tail (tail '()))))
        (pair i (pair (mirror right) (mirror left))))) ->*

'()

Inductive case: Assume P(x) and P(y) and that i is an integer. We will show that P(pair i (pair x y)) holds.

(mirror (mirror (pair i (pair x y)))) ->
(mirror ((method ((t <object>))
            (if (null? t) '()
               (bind (((i <integer>) (head t))
                      ((left <object>) (head (tail t)))
                      ((right <object>) (tail (tail t))))
                 (pair i (pair (mirror right) (mirror left)))))) (pair i (pair x y)))) ->*
(mirror (if (null? (pair i (pair x y))) '()
               (bind (((i <integer>) (head (pair i (pair x y))))
                      ((left <object>) (head (tail (pair i (pair x y)))))
                      ((right <object>) (tail (tail (pair i (pair x y))))))
                 (pair i (pair (mirror right) (mirror left)))))) (pair i (pair x y)))) ->*
...
(mirror (pair i (pair (mirror y) (mirror x)))))) ->*
...
(pair i (pair (mirror (mirror x)) (mirror (mirror y)))) ->* (By IH)
(pair i (pair x y))

Next: Abstraction and Class Definitions Up: CS212 Preliminary Exam I Previous: Higher-Order Functions (10 points)