Recursive Data Type
                           ROOTED BINARY TREES

Defined recursively follows:

  * A single node, $r$, is in $T$.

                            @                            

=====================================

If $t$ is an RBT, then the following are RBT's

  *  $\ms{makeleft}(t)$, 
         
           @
          /
         /
        /t\
        ---
overlay:                              \ms{makeright}(t)$
                                              @
                                               \
                                                \
                                               /t\
                                               ---
     
overlay: 

  *                 $\ms{makeboth}(t,t')$
                              @
                             / \
                        (Nick: finish up figure)
=========================================================
ANIMATION: grow this tree step-by-step:
 
                               An RBT Example

                                  @
                                 /
                                /
                               @
                              / \
                             /   \
                            /     \
                           @        @
                          / \      / 
                         /   \    /  
                        @     @  @
                                / \
                               /   \
                              @     @

======================================================

                 Recursive functions on RBT's

nodes: RBT --> Powerset(Nodes)

nodes(@) ::= {@},

nodes(makeleft(t)) ::= nodes(t) U {@}

      OVERLAY (italic): remember: @ is not supposed to be in nodes(t)

 overlay:

nodes(makeright(t)) ::= nodes(t) U {@}

nodes(makeboth(t1,t2)) ::= nodes(t1) U nodes(t2).

========================
Example

nodes(   @  )     ={@,@,@, NICK FILL IN}
        /
       /
      @
     / \
    /   \
   /     \
  @        @
 / \      / 
/   \    /  
@     @  @
       / \
      /   \
     @     @


========================================

depth: RBT --> N

depth(@) ::= 0

overlay
depth(makeleft(t)):: = 1+ depth(t)

overlay
depth(makeright(t)):: = 1+ depth(t)

overlay
depth(makeboth(t1,t2)):: = max(depth(t1),depth(t2))


===============================

Example

 depth(   @  )     =   4
         /
        /
       @
      / \
     /   \
    /     \
   @        @
  / \      / 
 /   \    /  
@     @  @
        / \
       /   \
      @     @

========================

Lemma:   | nodes(t) |   <= 2^{depth(t)}

overlay:

PROOF BY STRUCTURAL INDUCTION:

Base case (t = @).

     | nodes(t) | = 1 = 2^0 = 2^{depth(t)}.
                                       overlay   OK
===========================================

Induction Case (makeleft(t)).

ASSUME
  | nodes(t) |   <= 2^{depth(t)}

TO PROVE
 | nodes(makeleft(t)) |   <= 2^{depth(makeleft(t))}

-------------
overlay

| nodes(makeleft(t)) |   = | nodes(t) | +1   (by def of makeleft)

overlay 
                        <= 2^{depth(t)} +1   (induction hypothesis)

overlay                 <= 2^{depth(t)} + 2^{depth(t)}

                        =  2^{depth(t)+1

overlay                                  
                        = 2^{depth(makeleft(t))}  (by def of depth_)

overlay   makeleft case OK

==========================================
Induction Case (makeright(t)).

overlay   SAME

==========================

Induction Case (makeboth(t1,t2)).

ASSUME
  | nodes(t1) |   <= 2^{depth(t1)},
  | nodes(t1) |   <= 2^{depth(t1)}

TO PROVE
 | nodes(makeboth(t1,t2)) |   <= 2^{depth(makeboth(t1,t2))}

overlay

PROOF:

overlay
           VERY SIMILAR

================================
In-class Problem

PROBLEM 2 & 3

========================

Examples so far:

Can reduce structural induction to
Strong Induction on SIZE of parts.

overlay;

But what if the objects are all infinite?

overlay:

simple example: recursive definition of the set of functions on real
numbers from 18.01.

what is the "size" of the COSINE function?

============================
In-class Problem

                                PROBLEM 4

========================================

Can still replace structural induction by
ordinary (strong) induction on the

NUMBER OF STEPS (RULE APPLICATIONS) NEEDED TO
CONSTRUCT AN OBJECT OF THE RECURSIVELY DEFINED
SET.

overlay:
                                    number of steps
x, sin x, cos x, e^x :                     1

overlay

log x                                      2

cos (log x)                                4

(x cos(log x))                             6


===========================================================
                         Picture construction of

                              (x cos(log x))

  as a DERIVATION tree with 6 nodes:

                            product
                           /       \
                   identity         compose
                                    /   \
                                 cos     inverse
                                              \
                                              e^x
==========================================

                               ROOTED TREES

*   single node is an RT

*   if t1,t2,...,tn are RT's, so is

                               @
                        /     /       \
                   /         /                \
               /            /                      \
          /t1\            /t1\     ...              /tn\
          ----            ----                      ----  

====================================================================
                               ROOTED TREE

Nick: Insert FIGURE of some tree with about max depth four with selection
of subtrees: 4-sons, 3-sons, 2-sons, 1-son above something,
                     
overlay
In LISP

NICK: Insert LISP notation for the tree, eg,

`((() () () )   ( (() ()) (())  )  (() (((() () (()())))))  (((()())())()))

==============================================
In-class Problem

                                PROBLEM 5
===========================================================
GAME TREE

                                    *
1st moves:  (0,0) (0,1)  (1,0)   (1,1) (0,2) (2,0) (1, 2) (2, 1) (0, 3) ....
                    |      |     / |\ ...\
                  (0,0)  (0,0)  / /  | \...\
                               /  |  |  \ ... \
                          (0,0)(0,1)(0,2)(0,3)...(1,0)(2,0)...
                
overlay
INFINITELY WIDE

============================================
                            FINITE-PATH TREES

*   single node is an FP

*   if t1,t2,...,tn,... are FP's, so is

                               @
                        /     /       \
                   /         /                \

          /t1\            /t1\     ...              /tn\  ....
          ----            ----                      ----  

overlay
                   MAY HAVE INFINITELY MANY SUBTREES
=================================

           ROOTED TREES are FP's

                         WITH FINITELY MANY NODES

===========================
SLIDES OF FINITE-PATH TREES from slides5-3-from-5-2.ppt
...
=============================================
         BUT EVERY DOWNWARD PATH IN AN FP EVENTUALLY STOPS

Proof by Structural Induction on Def of FP

overlay:

BASE CASE ($t$ is one node): has only a 0-length path.

INDUCTION STEP ($t$ has subtrees.)
ASSUME in subtrees all down paths are finite.

Now path from root of $t$ goes to root of subtree.
Rest of the path in subtree must be finite by induction.
QED

========================================
In-class Problem

                                PROBLEMS 6 & 7