To print this page, print the following version: This Page (2up Postscript)

Prog	procedure RecA( m:int )     if m=1 then         put "Bye"     else         put "Hi"         RecA(m-1)     end if end RecA	procedure RecB( m:int )     if m=1 then         put "Bye"     else         put "Hi"         RecB(m-1)         RecB(m-1)     end if end RecB	procedure RecC( m:int )     if m=1 then         put "Bye"     else         put "Hi"         RecC(m div 2)     end if end RecC	procedure RecD( m:int )     if m=1 then         put "Bye"     else         put "Hi"         RecD (m div 2)         RecD((m+1) div 2)     end if end RecD
1) Rec ~	rec1	rec2	rec1	rec2
20 m ~	n	n	lenght of box	lenght of box
3) B(m) ~	number of leaves	number of leaves	number of leaves	number of leaves
4) Recur. Relation	B(1) = 1 B(m) = B(m-1)	B(1) = 1 B(m) = 2* B(m-1)	B(1) = 1 B(m) = B(floor(m/2))	B(1) = 1 B(m) = B(floor(m/2))+B(ceil(m/2))
5) Closed	B(m) = 1	B(m) = 2^(m-1)	B(m) = 1	B(m) = m
6) Check	1 = 1 1 = 1	2^(1-1) = 1 2^([m]-1) = 2 * 2^([m-1]-1)	1 = 1 1 = 1	1 = 1 m = floor(m/2)+ceil(m/2)
7) H(m) ~	number of interal nodes	number of interal nodes	number of interal nodes	number of interal nodes
8) Recur. Relation	H(1) = 0 H(m) = 1 + H(m-1)	H(1) = 0 H(m) = 1 + 2* H(m-1)	H(1) = 0 H(m) = 1 + H(floor(m/2))	H(1) = 0 H(m) = 1 + H(floor(m/2))+H(ceil(m/2))
9) H(m) =	H(m) = m-1	H(m) = 2^(m-1) - 1	H(m) = floor(log_2(m))	H(m) = m - 1
10) Check	1-1 = 0 [m]-1 = 1 + [m-1]-1	2^(1-1) - 1 = 0 2^([m]-1) - 1 = 1 + 2 *[2^([m-1]-1) - 1]	log(1) = 0 log([m]) = 1 + log([m/2])	1 = 1 m = 1 + [floor(m/2)-1] + [ceil(m/2)-1]

Note that (m div 2) = floor(m/2), ((m+1) div 2) = ceiling(m/2), and (m div 2) + ((m+1) div 2) = m.

• Question: Sum and Mult are designed to finalize the input polynomials f and g. Why is this done? Could the sum be made, without copying records, while keeping f and g pointing at the same polynomials? What are the dangers of this?
  

Answered in handout for ass4.

7) Formal Proof of Correctness

The following is an outline of a proof of correctness for a recursive program. Fill in the missing details required to prove the correctness of your program EvalRec.

For every integer k >=0, let S(k) be the formal statement that "The routine EvalRec returns the correct value for every value of x, y, and z and for every polynomial (pointed to by n) that has k nodes in it."

The overall goal is to prove that EvalRec returns the correct answer on every input. It is sufficient to prove that "forall k>=0 S(k)".

The method is proof by Strong Induction:
       i.e. prove that for every k>=0, [S(0) and ... and S(k-1)] => S(k)
       Note for k=0, the assumption is empty and you must prove S(0).

Let k be an arbitrary integer >= 0. Assume by way of strong induction that [S(0) and ... and S(k-1)].

SubGoal: Use the assumption to prove S(k).
Let x', y', and z' be arbitrary integers and let n' point at an arbitrary polynomial with k nodes.

SubSubGoal: Prove that EvalRec( x',y',z',n') returns the correct answer.
Because we have limited information about k, x', y', z', and n', it is best to brake the different possibilities into cases.

If an undefined variable is found oot will give an error message. Hence, assume all values are defined.

Case k=0 ie n=nil) The polynomial is not initialize. In this case, the program prints and error mesage as required by the post-conditions.

Case k=1) A polynomial consisting of single node will have n->left=nil. Hence, the Operand() test will succeed. If this operand is "x", "y", "z", or a real, then the progam returns the appropriate value. Otherwise, an appropriate error message is printed.

Case k>1 and n->left~=nil) Because n->left~=nil, the Operand() test will fail and the code will recurse on EvalRec(n->left) and EvalRec(n->right). These sub-trees will have strictly fewer than k nodes, because they do not include the root. Hence by the induction assumption, we know that EvalRec returns the correct evaluation of these sub-polynomials (or gives the correct error message if the sub-polynomial is not valid). To be valid, the given polynomial must be the +, -, *, or / of these two sub-polynomials. In these cases, the program returns the correct +, -, *, or / of the sub-anwers. If the root is other than +, -, *, or /, then the appropriate error message is given.

Case k>1 and n->left=nil) For there to be more then one node, n->right must point at them. This is not a valid polynomial. Ideally an error message should be given. In the program, the Operand() tests will pass. If the root node is "x", "y", "z", or a real, then give an answer, not noticing that n->right is pointing at something. Otherwise, an appropriate error message is printed.

Because all the possibilities have been proven, the SubSubGoal is complete.

Because we proved the SubGoal for arbitrary values of x, y, z, and n, it must be true for all values. This completes the SubGoal.

Because we assumed [S(0) and ... and S(k-1)] and then proved S(k), it follows that [S(0) and ... and S(k-1)] => S(k). Because we did this for an arbitrary value of k>=0, it must be true for all values of k>=0.

By the method of Strong Induction, we can conclude that "forall k>=0 S(k)", i.e. EvalRec works.

8) Tracing the execution of the recursive program PrettyPut

       PrettyPut  ________________________________
                 | no parameters                 |
                 | puts the polynomial pointed   |
                 | to by poly                    |
                 |_______________________________|
                                |
       PPutRec   _______________V________________
                 |dir = root                    |
                 |prefix =                       |
                 | ""                            |
                 |print:                         |
                 |       |-- 1                   |
                 | -- * -|                       |
                 |       |           |-- 2       |
                 |       |     |- * -|           |
                 |       |     |     |     |-- 3 |
                 |       |     |     |- + -|     |
                 |       |     |           |-- 4 |
                 |       |- + -|                 |
                 |             |-- 5             |
                 |_______________________________|
                     |                      |
_____________________V___________ __________V______________________ 
|dir = left                     | |dir = right                    |
|prefix =                       | |prefix =                       | 
| bbbbbb                        | | bbbbbb                        | 
|print:                         | |print:                         |
|       |-- 1                   | |       |           |-- 2       |
|_______________________________| |       |     |- * -|           |
                                  |       |     |     |     |-- 3 |
                                  |       |     |     |- + -|     |
                                  |       |     |           |-- 4 |
                                  |       |- + -|                 |
                                  |             |-- 5             |
                                  |_______________________________|
                                      |                       |
                             _________|                       |
_____________________________V___ ____________________________V____
|dir = left                     | |dir = right                    |
|prefix =                       | |prefix =                       |
| bbbbbb|bbbbb                  | | bbbbbbbbbbbb                  |
|print:                         | |print:                         |
|       |           |-- 2       | |             |-- 5             |
|       |     |- * -|           | |_______________________________|
|       |     |     |     |-- 3 |                                 
|       |     |     |- + -|     |
|       |     |           |-- 4 |
|_______________________________|
    |                       |
    |                       |__________
____V____________________________ ____V____________________________
|dir = left                     | |dir = right                    |
|prefix =                       | |prefix =                       |
| bbbbbb|bbbbbbbbbbb            | | bbbbbb|bbbbb|bbbbb            |
|print:                         | |print:                         |
|       |           |-- 2       | |       |     |     |     |-- 3 |
|_______________________________| |       |     |     |- + -|     |
                                  |       |     |           |-- 4 |
                                  |_______________________________|
                                      |                       |
                             _________|                       |
_____________________________V___ ____________________________V____
|dir = left                     | |dir = right                    |
|prefix =                       | |prefix =                       |
| bbbbbb|bbbbb|bbbbb|bbbbb      | | bbbbbb|bbbbb|bbbbbbbbbbb      |
|print:                         | |print:                         |
|       |     |     |     |-- 3 | |       |     |           |-- 4 |
|_______________________________| |_______________________________|