\problemdata
{structural induction}
{trees}
{S00 tut2}

\begin{problem}
% structural induction

\mbox{}

\begin{problemparts}

\problempart

Give the structural inductive definition of the set $F$ of full
binary trees.
\solution{
\emph{Carl: I am not sure whether this is what Nancy and
    David wanted as an answer here since we give the student's the
    recursive definition in problem 1a.}

  Recall from lecture that we let $\ms{makeboth}(t,t')$, for $t, t'
  \in F$, denote the full binary tree made up of attaching the full
  binary trees $t$ and $t'$ respectively to a node, as done in the
  recursive definition of $F$.

  \begin{tabbing}
    XXX\=XXX\=XXX\=XXX\kill
    $\forall t \in F (P(t))$ \\
    1. (Base) $P(n)$, where $n$ is the single-node tree. \\
    2. (Inductive step) 
    $\forall t,t' \in F, (P(t) \wedge P(t') \Rightarrow P(\ms{makeboth}(t,t')))$ \\
    3. QED
  \end{tabbing}
}

\problempart

Define the function $\ms{numleaves}(t)$, for $t \in F$, giving the
number of ``leaves'' of the full binary tree $t$; that is,
$\ms{numleaves}(t)$, for $t \in F$, gives the number of nodes in $t$
that do not have children.  Your definition should be recursive, based
on the recursive definition of the set $F$.

\solution{
   We define the function $\ms{numleaves}(t)$, for $t \in F$, as
   follows:

   $\ms{numleaves}(\text{single node}) = 1$

   $\ms{numleaves}(\ms{makeboth}(t,t')) 
   = \ms{numleaves}(t) + \ms{numleaves}(t')$
}

\problempart

Define the function $\ms{numinternal}(t)$, for $t \in F$, giving the
number of ``internal'' nodes of the full binary tree $t$; that is,
$\ms{numinternal}(t)$, for $t \in F$, gives the number of nodes in $t$
that have children.  Your definition should be recursive, based on the
recursive definition of the set $F$.
\solution{

   We define the function $\ms{numinternal}(t)$, for $t \in F$, as
   follows:

   $\ms{numinternal}(\text{single node}) = 0$

   $\ms{numinternal}(\ms{makeboth}(t,t')) = 
   \ms{numinternal}(t) + \ms{numinternal}(t') + 1$
}

\problempart

Prove by structural induction that for any full binary tree $t$ in
$F$, $\ms{numleaves}(t) = 1 + \ms{numinternal}(t)$.
\solution{
This part is shown by structural induction on the recursion step.

   Let $P(t): \ms{numleaves}(t) = 1 + \ms{numinternal}(t)$.

   Use the structural inductive definition of part (a) to show the
   property is true.
}
\end{problemparts}
\end{problem}