\documentclass[12pt]{article}
\usepackage{graphics}
\usepackage{macros-course-lectures}

\begin{document}

\lecture{notes5}{Structural Induction}{Oct 1, 2001}{\stamp}

% \section{Trees}

% The last lecture introduced the idea of a graph, a mathematical object
% used extensively in computer science. Now we will look at a
% particularly useful type of graph called a tree.

% Intutively a graph with very few edges cannot be connected. In the
% last lecture we have seen that $n-1$ edges are required for
% connectivity. There are many connected graphs with $n$ nodes and
% exactly $n-1$ edges. One example is the line graph with $n$ nodes.
% Another example is shown in figure \ref{fig:tree}. In general, such
% graphs are called trees.

% \begin{definition}
%   A \emph{tree} is a connected graph with no cycles.
% \end{definition}

% \begin{figure}
%   \centerline{\includegraphics[height=2in]{figures/tree}}
%   \caption{This tree has 11
%     \emph{leaves}, which are defined as vertices of degree at most one.
%     The remaining 7 vertices are called \emph{internal nodes}.}
%   \label{fig:tree}
% \end{figure}

% The vertices in a tree can be classified into two categories.
% Vertices of degree at most one are called \emph{leaves}, and vertices
% of degree greater than one are called \emph{internal nodes}.

% Trees are often drawn as in Figure~\ref{fig:tree} with the leaves on
% the bottom.  Keep this convention in mind; otherwise, phrases like
% ``all the vertices \emph{below}'' will be confusing. (The English
% mathematician Littlewood once remarked that he found such directional
% terms particularly bothersome, since he habitually read mathematics
% reclined on his back!)

% Trees arise in many problems.  Family trees are an example---each node
% is a person, and there is an edge between any parent and child.
% Similarly, the file structure in a computer system can often be
% represented by a tree.  In this case, each internal node corresponds
% to a directory, and each leaf corresponds to a file.  If one directory
% contains another, there there is an edge between the associated
% internal nodes.  If a directory contains a file, then there is an edge
% between the internal node and a leaf.  In both family trees and
% directories, there can be exceptions that make the graph not a
% tree---relatives can marry and have children, while directories
% sometimes use soft links to create multiple directory entries for a
% given file.

% Trees can actually be defined several different ways.
% \begin{theorem}
%   The following properties of a graph~$G$ are equivalent:
%   \begin{enumerate}
%   \item $G$ is a connected graph with no cycles 
%   \item $G$ is a connected graph that is disconnected by the removal of any
%     edge, \ie, a ``minimal'' connected graph.
%   \item $G$ is a graph with a unique simple path between every pair of
%     vertices
%   \end{enumerate}
% \end{theorem}
% Since the definitions are equivalent, any one of them could have been
% taken as the definition of a tree.

% Theorems asserting that several mathematical statements are equivalent
% are quite common.  One way to prove such a theorem would be to
% consider every pair of statements in turn and prove them equivalent.
% That is, we would prove $1 \Leftrightarrow 2$, $2 \Leftrightarrow 3$,
% and $3 \Leftrightarrow 1$.  This requires proving six implications,
% three in each direction.  

% This is overkill.  A simpler approach is to show $1 \Rightarrow 2$, $2
% \Rightarrow 3$, and $3 \Rightarrow 1$.  These three implications are
% sufficient to prove every pair of statements equivalent.  For example,
% $2 \Leftrightarrow 3$ follows because we prove $2 \Rightarrow 3$
% directly, and prove $3 \Rightarrow 2$ with the two steps $3
% \Rightarrow 1 \Rightarrow 2$.

% \begin{lemma}
%   $(3 \implies 1)$ A graph with a unique simple path between any pair of
%   nodes is connected and has no cycles.
% \end{lemma}
% \begin{proof}
%   It clearly meets the definition of connectivity.  To see there are
%   no cycles we argue by contradiction.  Suppose we have a (simple)
%   cycle $v_1,\ldots,v_k,v_1$.  Then there are 2 simple paths from
%   $v_1$ to $v_k$, namely $v_1,\ldots,v_k$ and the edge $\{v_1,v_k\}$.
% \end{proof}


% \begin{lemma}
%   $(1\implies 2)$ A connected graph with no cycles is disconnected by
%   the removal of any edge.
% \end{lemma}
% \begin{proof}
%   By contradiction.  Suppose we can delete the edge $\{u,v\}$ without
%   disconnecting the graph.  This means there is a path from $u$
%   to~$v$ that doesn't use $\{u,v\}$, and thus a simple path.  Adding
%   edge $\{u,v\}$ to a simple path that doesn't use $\{u,v\}$ creates a
%   cycle.  This contradicts the claim of no cycles.
% \end{proof}
% \begin{lemma} 
%   $(2 \implies 3)$
%   A connected graph that is disconnected by the removal of any edge has
%   a unique simple path between any pair of vertices.
% \end{lemma}
% \begin{proof}
%   Suppose there are two different simple paths from $u$ to~$v$.  Call
%   one $P_1$: $u=x_0,x_1,\ldots,x_k=v$.  Call the other $P_2$:
%   $u=y_0,\ldots,y_l=v$.  Let $i$ be the smallest such that $x_i \ne
%   y_i$ (why does this have to exist?).  We claim that we can remove
%   $\{y_{i-1},y_i\}$ without disconnecting~$G$.  To see this, consider
%   a pair of vertices $z$ and~$w$. There's a simple path between them
%   at the start.  It remains to show there's still a path (that doesn't
%   need to be simple) after removing $\{y_{i-1},y_i\}$.  We use proof
%   by cases.

%   Case 1:  $\{y_{i-1},y_i\}$ wasn't on the path.  Then the path remains
%   after removing $\{y_{i-1},y_i\}$.
  
%   Case 2: $\{y_{i-1},y_i\}$ was on the path.  We can assume that
%   $y_{i-1}$ is encountered first. So the path looked like
%   $z,\ldots,y_{i-1},y_i,\ldots,w$.  So there's a different path: go
%   from $z$ to $y_{i-1}$ on the first part of $z$-$w$ path, then from
%   $y_{i-1}$ to $u$ on the first part of $P_2$, then from $u$ to $v$ on
%   $P_1$, then from $v$ to $y_i$ on the second part of $P_2$, then from
%   $y_i$ to $w$ on the second part of the $z$-$w$ path. The
%   construction is illustrated in Fig.~\ref{fig:case2}.
%   \begin{figure}
%     \centerline{\includegraphics[height=.75in]{figures/notconnected}}
%     \caption{Although the edge $\{y_{i-1},y_i\}$ was on the path
%       from $z$ to~$w$, there is a path from $z$ to~$w$ also when
%       $\{y_{i-1},y_i\}$ has been removed. In the case shown above, the
%       path goes from $z$ to~$y_{i-1}$, then to~$u$, then to~$v$ along
%       the path $u=x_0,x_1,\ldots,x_{k-1},x_k=v$, then to~$y_i$, and
%       finally to~$w$.}
%     \label{fig:case2}
%   \end{figure}
% \end{proof}

% \subsection{Special Kinds of Trees}

% Two species of trees arise particularly often in computer science:
% rooted trees and binary trees. A \emph{rooted tree} is just a tree
% with one vertex designated as the ``root''. Given an ordinary tree,
% one can produce different rooted trees by choosing different vertices
% as the root. In a picture of a rooted tree, the topmost vertex usually
% represents the root. In a rooted tree we can say that there is a
% unique simple path from any vertex to the root. If $u$ is the first
% vertex on the unique simple path from vertex $v$ to the root, the $u$
% is called the \emph{parent} of $v$ and $v$ is called the \emph{child}
% of $u$.

% There is a special type of rooted tree called a binary tree.


\section{Structural Induction}
Structural induction is an elegant variant of induction for proving
things about recursively defined objects. Instead of using a number
$n$, the induction is based explicitly on the recursive structure of
the definition.

\subsection{Recursive Definitions}
A {\em recursive definition} says how to build something from
a simpler version of the same thing. They have two parts:
\begin{itemize}
\item Base case(s) that don't depend on anything else
\item Combination cases that depend on simpler cases
\end{itemize}

\noindent Here are several examples of recursive definitions:

\begin{description}

\item[The Factorial function:] A very useful function for counting and
probability.\footnote{In our definitions, we will frequently use the
symbol ``$=$'' in a special sense that means what appears on the left
is defined to be what appears on the right.  We expect you to
recognize from context which use we intend and, in the definitional
case, only to use the statement as a definition and not as an
algebraic statement.}\mbox{} 
\begin{itemize}
\item $0!=1$
\item $(n+1)! = (n+1)n!$ for $n \ge 1$.
\end{itemize}

\item[The Fibonacci numbers:]
These are interesting numbers that arise, e.g., in biology, where
they model some types of growth processes (plants, cells, rabbit
populations, etc.).  The Fibonacci numbers are written as $F_i$, $i
= 0, 1, 2, \ldots$.  They are defined recursively by:

  \begin{align*}
    F_0 &= 0\\ 
    F_1 &= 1\\ 
    F_i &= F_{i-1} + F_{i-2} \mbox{ for $i \geq 2$.} 
  \end{align*}

  Note there 2 base cases, since each combination relies on previous two
  values.

  What is $F_4$?  Well, $F_2 = F_0+F_1 = 1$, $F_3 = F_1+F_2 = 2$, so
  $F_4 = 3$.  The sequence starts out $0, 1, 1, 2, 3, 5, 8, 13,
  21,\ldots$.

\newpage

\item[ $\Sigma$ notation (the traditional style):] We've been using
  this notation informally already.
  \begin{itemize}
  \item $\Sigma_{i=1}^0 f(i) = 0$ \\
  \item $\Sigma_{i=1}^{n+1} f(i) = \Sigma_{i=1}^n f(i) + f(n+1)$. 
  \end{itemize}

\item[Simultaneous recursive definitions.]
  You can define several things at the same time, in terms of each
  other.  For example, we may define two functions $f$ and $g$ from
  $\naturals$ to $\naturals$, recursively, by:
  \begin{itemize}
  \item
    $f(0) = 1$
  \item
    $g(0) = 1$
  \item
    $f(n+1) = f(n) + g(n)$, $n \geq 0$
  \item
    $g(n+1) = f(n) \times g(n)$, $n \geq 0$
  \end{itemize}

\end{description}


We must take care that concepts defined by recursive definitions are
well-defined.  Below are some examples that aren't well-defined.

\begin{description}
\item[$f(n)=2+f(n-1)$.]
  This definition has no base case.
\item[\rm $f(1)=1$ and $f(n) = 1+f(n+1)$.]

  This still has no sufficient base case, because $f(n)$ is defined in
  terms of $f(n+1)$.  So for positive integers $n$ other than 1,
  $f(n)$ is defined in terms of ``more complex'' cases instead of
  simpler ones.  Note that if we had written $f(n+1) = f(n)-1$, we
  would have meant something different (we would be defining $f(n+1)$
  in terms of $f(n)$) and $f$ would have been well-defined for all
  positive integers.  Also, note that the first way makes $f$
  well-defined for all integers {\em less than} or equal to 1.

\item[\rm $f(1)=1$ and $f(n) = 3f(n/2)$.]  This doesn't give a definition
  for odd values of $n$, since $n/2$ is not a natural number in this
  case.

\item[\rm A mystery.]  Mathematicians have been wondering about this one
  for a while:
  \begin{itemize}
  \item $f(1) = 1$
  \item If $n$ is even, then $f(n) = f(n/2)$.
  \item If $n$ is odd, then $f(n) = f(3n+1)$.
  \end{itemize}
  If $f$ is well defined, then $f(n)=1$ everywhere.  But nobody knows if
  the recursion always terminates (though it's been checked for many numbers).
\end{description}

A recursive definition usually leads to inductive
proofs---the induction follows the definition down to the base case.

% \section{Inductive Proofs on Recursive Definitions} 

% A recursive definition usually leads to inductive
% proofs---the induction follows the definition down to the base case.
% The examples in this section involve functions that are defined
% recursively.  

% \subsection{Fibonacci Numbers}

% The Fibonacci numbers (defined earlier) satisfy many cute identities,
% so they provide lots of fun for mathematicians.  For example:
% \begin{theorem}
%   $\forall n \geq 0 (\Sigma_{i=0}^n F_i^2 = F_n F_{n+1})$
% \end{theorem}

% Example: $n = 4$: \\
% $0^2 + 1^2 + 1^2 + 2^2 + 3^2 = 15 = 3 \cdot 5$.
% \\
% Let's try a proof by (standard, not strong) induction.  The theorem
% statement suggests trying it with $P(n)$ defined as:
% \[\sum_{i=0}^n F_i^2 = F_n F_{n+1}
% \]

% \structuredproof{
%   Prove: $\forall n \geq 0 (\Sigma_{i=0}^n F_i^2 = F_n F_{n+1})$ \\
%   1. (Base) $\Sigma_{i=0}^0 F_i^2 = F_0 F_1$ \\
%   2. (Inductive step) $\forall n \geq 0
%   (\Sigma_{i=0}^n F_i^2 = F_n F_{n+1} \Rightarrow
%   \Sigma_{i=0}^{n+1} F_i^2 = F_{n+1} F_{n+2})$ \reason{???}\\
%   3. QED               \reason{induction}\\
% }

% \noindent Now we stare at the gap between $P(n)$ and $P(n+1)$.
% $P(n+1)$ is given by a summation that's obtained from that for $P(n)$
% by adding one term; this suggests that, once again, we subtract.  The
% difference is just the term $F_{n+1}^2$.  Now, we are assuming that
% the original $P(n)$ summation totals $F_n F_{n+1}$ and want to show
% that the new $P(n+1)$ summation totals $F_{n+1} F_{n+2}$.  So we
% would {\em like\/} the difference to be
% \[
% F_{n+1} F_{n+2} - F_n F_{n+1}
% \]

% So, the actual difference is $F_{n+1}^2$ and the difference we want is
% $F_{n+1} F_{n+2} - F_n F_{n+1}$.  Are these the same\?  We want to
% check that:
% \[
% F_{n+1}^2 = F_{n+1} F_{n+2} - F_n F_{n+1}
% \]
% But this is true, because it is really the Fibonacci definition in
% disguise: to see this, divide by $F_{n+1}$.  \forstudents{Here's the complete
% proof:

% \structuredproof{
%   Prove: $\forall n \geq 0 (\Sigma_{i=0}^n F_i^2 = F_n F_{n+1})$ \\
%   1. (Base) $\Sigma_{i=0}^0 F_i^2 = F_0 F_1$ 
%   \reason{Both sides are $0$.} \\
%   2. (Inductive step) $\forall n \geq 0 
%   (\Sigma_{i=0}^n F_i^2 = F_n F_{n+1} \Rightarrow
%   \Sigma_{i=0}^{n+1} F_i^2 = F_{n+1} F_{n+2})$ \noreason \\
%   \> 1. Fix $n \geq 0$. \\
%   \> 2. Assume $\Sigma_{i=0}^n F_i^2 = F_n F_{n+1}$ \\
%   \> 3. $\Sigma_{i=0}^{n+1} F_i^2 = F_{n+1} F_{n+2}$ \\
%   \> \> 1. $\Sigma_{i=0}^{n+1} F_i^2 = \Sigma_{i=0}^n F_i^2 + F_{n+1}^2$
%   \reason{Summation has one extra term} \\
%   \> \> 2. $\Sigma_{i=0}^n F_i^2 + F_{n+1}^2 = F_n F_{n+1} + F_{n+1}^2$
%   \reason{Inductive hypothesis (2.2)} \\
%   \> \> 3. $F_n F_{n+1} + F_{n+1}^2 = F_{n+1}(F_n + F_{n+1})$
%   \reason{Algebra} \\
%   \> \> 4. $F_{n+1}(F_n + F_{n+1}) = F_{n+1} F_{n+2}$ 
%   \reason{Fibonacci definition} \\
%   \> \> 5. QED                         
%   \reason{Combining the equations} \\
%   \> 4. QED 
%   \reason{Implication, UG} \\
%   3. QED                           
%   \reason{Induction}\\
% }
% }

% \subsubsection{Another false theorem}

% Here is another false ``theorem''.  The fallacy is like the blocks
% example---we don't have enough base cases.

% \begin{falsethm}
%   All Fibonacci numbers are even.
% \end{falsethm}

% We try strong induction, where $P(n)$ is defined to be ``$F_n$ is
% even.'' 
% \structuredproof{
%   Prove: $\forall n \geq 0 [P(n)]$ \\
%   1. (Base) $P(0)$
%   \reason{$F_0 = 0$, which is even.} \\
%   2. (Inductive step) 
%   $\forall n \geq 0 [(\forall i, 0 \leq i \leq n (P(i))) \Rightarrow
%   P(n+1)]$
%   \reason{???} \\
%   3. QED      \reason{Strong induction}\\
% }

% The inductive step is supposed to prove that $F_{n+1}$ is even, using
% the fact that all smaller Fibonacci numbers are even.
% The idea is to express $F_{n+1}$ as usual, as $F_{n-1} + F_n$.
% Then use the strong inductive hypothesis to say that $F_{n-1}$ and $F_n$
% are both even.
% The sum is therefore also even.
% \\
% What's the error?  We proved:
% $P(0)$ \\
% $P(0) \wedge P(1) \Rightarrow P(2)$ \\
% $P(1) \wedge P(2) \Rightarrow P(3)$, etc. \\
% But we never proved $P(1)$.

% \subsubsection{A lower bound}

% Here's a correct strong-induction proof about Fibonacci numbers.  It
% shows a lower bound on their values.
% \begin{lemma}
%   $\forall n \geq 2 [F_n \geq (\frac{3}{2})^{n-2}]$
% \end{lemma}
% \begin{proof}
%   Use strong induction.
%   Let $P(n) = F_n \geq (\frac{3}{2})^{n-2}$
%   \begin{structproof}
%     Prove: $\forall n \geq 2 [P(n)]$\\
%     1. (Base) $P(2)$
%     \> \> \> \> \>  $F_2 = 1 = (\frac{3}{2})^0$ \\
%     2. (Base) $P(3)$ 
%     \> \> \> \> \>  $F_3 = 2 \geq (\frac{3}{2})^1$ \\
%     3. (Inductive step) $\forall n \geq 3 [(\forall  i, 2 \leq i \leq n (P(i))) \Rightarrow P(n+1)]$\\
%     \> 1. Fix $n \geq 3$ \\
%     \> 2. Assume $\forall  i, 2 \leq i \leq n (P(i))$ \\
%     \> 3. $P(n+1)$
%     \> \> \> \> ??? \\
%     \> 4. QED
%     \> \> \> \> Implication, UG \\
%     4. QED
%     \> \> \> \> \> Strong induction
%   \end{structproof}

%   \noindent
%   Now in proving the ??? we are only worrying about $n \geq 3$ and we may
%   assume the inequality for all $i$ from $2$ up to $n$, inclusive.
%   Because of the way Fibonacci numbers are defined, it turns out that the
%   ones we need are just $n$ and $n-1$.
%   Those are in the range for which we can assume the property. 
%   \begin{structproof}
%     \> 3. $P(n+1)$ \\
%     \> \> 1. $F_n \geq (\frac{3}{2})^{n-2}$
%     \> \> \> Inductive hypothesis 3.2 \\
%     \> \> 2. $F_{n-1} \geq (\frac{3}{2})^{n-3}$
%     \> \> \> Inductive hypothesis 3.2 \\
%     \> \> 3. $F_{n+1} = F_n + F_{n-1}$
%     \> \> \> Definition \\
%     \> \> 4. $F_{n+1}\geq (\frac{3}{2})^{n-2} + (\frac{3}{2})^{n-3}$ 
%     \> \> \> Plug the inequalities into the equation \\
%     \> \> 5. QED
%     \> \> \> Algebra \\
%     \> \> \> 1. $\frac{3}{2} + 1 \geq (\frac{3}{2})^2$
%     \> \> Arithmetic \\
%     \> \> \> 2. $(\frac{3}{2})^{n-2} + (\frac{3}{2})^{n-3} \geq (\frac{3}{2})^{n-1}$
%     \> \> Algebra \\
%     \> \> \> 3. $F_{n+1} \geq (\frac{3}{2})^{n-1}$
%     \> \> Algebra (3.3.4 and 3.3.5.2) \\
%     \> \> \> 4. QED
%     \> \> Definition of $P(n+1)$ 
%   \end{structproof}
% \end{proof}


% \subsection{Double Induction}

% Here's a trickier use of recursive definitions and induction, used
% twice, in a nested way, in the same proof.  Define a function of two
% natural number variables recursively as follows: \\ 
% $f(0,k) = 1$ for all $k \geq 0$. \\ 
% $f(n,0) = 1$ for all $n \geq 0$.\\ 
% For $n, k \geq 0,$ $f(n+1,k+1) = f(n,k+1) + f(n+1,k)$. \\ 
% \\
% Why does this define a function\?  We can see by looking at a table\.
% The first two rules fill in the first row and column, respectively\.
% For each other entry, you obtain the value by adding the upper and
% left neighbors\.  It is left to the reader to see that this defines a
% unique function, that is, fills in all the spaces, in exactly one way.
% \[
% \begin{array}{r|rrrrr}
%    & 0   & 1  &  2  &  3  &  4 \\
% \hline
% 0  & 1   & 1  &  1  &  1  &  1 \\
% 1  & 1   & 2  &  3  &  4  &  5 \\
% 2  & 1   & 3  &  6  & 10  & 15 \\
% 3  & 1   & 4  & 10  & 20  & 35 \\
% 4 & 1 & 5 & 15 & 35 & 70\\
% \end{array}
% \]
% If you turn this rectangle on its corner, you get the famous
% ``Pascal's triangle.''
% We will see these numbers later in the term (around lecture 16)\.  
% For now, here is a formula (which we pull out of thin air), giving the 
% exact value of the function on any pair of arguments:
% \[
% f(n,k) = \frac{(n+k)!}{n!\;
%   k!}.
% \]

% Here we are using the factorial function defined earlier.  As an
% example, 
% \[
% f(3,4) = \frac{7!}{3!4!} =
% \frac{7\cdot 6\cdot 5\cdot 4\cdot 3\cdot 2\cdot 1}{3\cdot 2\cdot
%   1\cdot 4\cdot 3\cdot 2\cdot 1} = 35.
% \]

% \begin{lemma}
%   $\forall n, k \in N [f(n,k) = \frac{(n+k)!}{n! k!}]$.
% \end{lemma}

% \noindent We can prove this by induction\.  But there are two
% variables, $n$ and $k$\.  So, we will do the proof in 2 levels\.  The
% main strategy is by induction on $n$\.  And for each particular $n$,
% we work by induction on $k$\.  We are doing induction inside an
% induction\.  Let's break up the statement to make the two levels
% clearer\.  The specific statement we want to prove is:
% \begin{lemma}
%   $\forall n [\forall k [f(n,k) = \frac{(n+k)!}{n! k!}]]$
% \end{lemma}

% \noindent Define $Q(n,k)$ to be the predicate $f(n,k) =
% \frac{(n+k)!}{n! k!}$\.  $Q(n,k)$ says that the value in position
% $(n,k)$ is correct (satisfies the formula)\.  Define $P(n)$ to be the
% statement $\forall k [Q(n,k)]$, that is, $\forall k [f(n,k) =
% \frac{(n+k)!}{n!  k!}]$\.  In English, $P(n)$ means that all the
% values in row $n$ are correct\.

% \forstudents{
% Now we use the standard induction pattern: 
% \begin{structproof}
%   Prove: $\forall n \geq 0 (P(n))$ \\
%   1. (Base) $P(0)$ \\
%   2. (Inductive step) $\forall n \geq 0 [P(n) \Rightarrow P(n+1)]$ \\
%   3. QED 
%   \> \> \> \> \> Induction
% \end{structproof}


% Expanding this pattern:
% \begin{structproof}
%   Prove: $\forall n \geq 0 [P(n)]$ \\
%   1. (Base) $P(0)$ \\
%   \> 1. $\forall k [f(0,k) = \frac{(0+k)!}{0!k!}]$
%   \> \> \> \> Both sides are 1 (for any $k$) \\
%   \> 2. QED 
%   \> \> \> \> Definition of $P(0)$ \\
%   2. (Inductive step) $\forall n \geq 0 [P(n) \Rightarrow P(n+1)]$ \\
%   \> 1. Fix $n \geq 0$. \\
%   \> 2. Assume $P(n)$, that is, row $n$ is correct. \\
%   \> 3. $P(n+1)$, that is, row $n+1$ is correct.      
%   \> \> \> \> ??? \\
%   \> 4. QED    
%   \> \> \> \> Implication, UG \\
%   3. QED                           
%   \> \> \> \> \> Induction 
% \end{structproof}

% Now, how to prove 3\?  It involves saying something about the whole
% row $n+1$\.  
% We use induction to handle all the elements in this row one at a
% time\.  
% Our goal 3 can be rewritten, using the definition of $P$ in terms of
% $Q$\.  
% Note that this is all talking just about the particular row $n+1$.

% \begin{structproof}
%   \> 3. $P(n+1)$ \\
%   \> \> 1. $\forall k [Q(n+1,k)]$ \\
%   \> \> \> 1. (Base) $Q(n+1,0)$ \\
%   \> \> \> 2. (Inductive step) $\forall k \geq 0 [Q(n+1,k) \Rightarrow Q(n+1,k+1)]$. \\
%   \> \> \> 3. QED  
%   \> \> Induction \\
%   \> \> 2. QED
%   \> \> \> Definition of $P(n+1)$
% \end{structproof}

% \noindent
% The base case for the inner induction follows by expanding the
% definition of $Q(n+1,0)$:
% \begin{structproof}
%   \> \> \> 1. (Base) $Q(n+1,0)$ \\
%   \> \> \> \> 1. $f(n+1,0) = \frac{(n+1+0)!}{(n+1)! 0!}$ 
%   \> Both sides are 1 \\
%   \> \> \> \> 2. QED
%   \> Definition of $Q(n+1)$
% \end{structproof}

% \noindent
% The inductive step involves a little algebra:
% \begin{structproof}
%   XXX\=XXX\=XXX\=XXX\=XXX\=XXXXXXXXXXXXXXXXXXXXX\=    \kill
%   \> \> \> 2. (Inductive step) $\forall k \geq 0 [Q(n+1,k) \Rightarrow Q(n+1,k+1)]$. \\
%   \> \> \> \> 1. Fix $k \geq 0$. \\
%   \> \> \> \> 2. Assume $Q(n+1,k)$. \\
%   \> \> \> \> 3. $Q(n+1,k+1)$ \\
%   \> \> \> \> \> 1. $f(n+1,k+1)= f(n,k+1) + f(n+1,k)$ \\
%   \> \> \> \> \> \> Definition of $f(n+1,k+1)$ \\
%   \> \> \> \> \> 2. $f(n+1,k) = \frac{(n+1+k)!}{(n+1)!k!}$ 
%   \> Inductive hypothesis 2.3.1.2.2, \\
%   \> \> \> \> \> \> definition of $Q(n+1,k)$. \\
%   \> \> \> \> \> 3. $f(n,k+1) = \frac{(n+k+1)!}{n!(k+1)!}$ 
%   \> Inductive hypothesis 2.2, \\
%   \> \> \> \> \> \> definition of $P(n,k+1)$. \\
%   \> \> \> \> \> 4. $f(n+1,k+1)=\frac{(n+k+1)!}{n!(k+1)!}+\frac{(n+1+k)!}{(n+1)!k!}
%   =\frac{(n+1+k+1)!}{(n+1)!(k+1)!}$ \\
%   \> \> \> \> \> \> Combining equations, algebra \\
%   \> \> \> \> \> 5. QED                   
%   \> Definition of $Q(n+1,k+1)$ \\
%   \> \> \> \> 4. QED
%   \> \> Induction
% \end{structproof}
% }

% The ``inner'' inductive hypothesis (the one involving $Q(n+1,k)$)
% is invoked to get information about the
% previous element in the same row, $n+1$\. 
% The ``outer'' inductive hypothesis (the one involving $P(n,*)$),
% is invoked to get information about element $k+1$ of the previous row\.
% (The proof uses UI in the invocation of the outer inductive hypothesis.)

\subsection{Recursive Structure Definitions}

So far we've been looking at recursively defined functions of the
natural numbers.  Recursive definitions are also a useful way to
describe other types of objects (structures) that are built up from
smaller pieces. Here are some recursively defined data types.

\begin{definition}
  The set $F$ of fully parenthesized Boolean algebra expressions
  satisfies:\footnote{Note that we are being careful to distinguish
  parentheses that are of the boolean expression (represented by
  square brackets) from parenthesis used in our proof formulas
  (represented by standard parentheses}.

  \begin{enumerate}
  \item The symbols $0$ and $1$ are in $F$. 
  \item If $e$ and $e'$ are in $F$ then the expression $[e \wedge e']$ is
    in $F$. 
  \item
    If $e$ and $e'$ are in $F$ then the expression $[e \vee e']$ is
    in $F$. 
  \item
    If $e$ is in $F$ then the expression $[\neg e]$ is in $F$. 
  \item
    $F$ contains nothing else. 
  \end{enumerate}
\end{definition}

\begin{definition}
  The set $S$ of (finite length) strings over alphabet $A$ satisfies: 
  \begin{enumerate}
  \item  $\lambda$, the empty string, is in $S$.
  \item  If $s$ is in the set $S$ and $a \in A$, then $sa$ is in $S$.\\
  ($sa$ is called the \emph{concatenation} of the string $s$ and the 
  letter $a$.)
  \item $S$ contains nothing else. 
  \end{enumerate}
\end{definition}
This is a recursive description (definition) of the set of strings.
Notice that it includes every finite length string.  Moreover, every
string has a unique derivation using these rules --- this isn't
strictly necessary, but is often convenient in proofs.\\

Another important example is a {\em binary tree}.

\begin{definition}
  The set $T$ of binary trees satisfies: 
  \begin{enumerate}
  \item
    A single node $n$ is in $T$.
  \item 
    If $t$ is in $T$, then \ms{makeleft}$(t)$ is in $T$. 
  \item
    If $t$ is in $T$, then \ms{makeright}$(t)$ is in $T$. 
  \item
    If $t$ and $t'$ are in $T$, then \ms{makeboth}$(t,t')$ is in $T$. 
  \end{enumerate}

In this definition, \ms{makeleft}$(t)$ returns the structure formed
from $t$, a single new node $n$, and an arrow labeled ``left'' from
$n$ to $t$, is also in $T$. \ms{makeright}$(t)$ returns the structure
formed from $t$, a single new node $n$, and an arrow labeled ``right''
from $n$ to $t$, is also in $T$. \ms{makeboth}$(t,t')$ returns the
structure formed from $t$, $t'$, and a single new node $n$, with an
arrow labeled ``left'' from $n$ to $t$ and another arrow labeled
``right'' from $n$ to $t'$, is also in $T$. A {\em full binary tree}
is a tree in which every node is either a single node or has both a
left and right subtree; in other words rules 2 and 3 are removed from
the definition given above.

\end{definition}

\newcommand{\makelist}{\mathop{\mbox{makelist}}}

Finally, here is a definition of lists for 6.001:
\begin{definition}
  The set $L$ of lists over atom set $A$ satisfies:
  \begin{enumerate}
  \item $()$, the empty list, is in $L$.
  \item If $\ell \in L$ and $a \in A$, then $\makelist(a,l)$ is in $L$.
  \item If $\ell_1$ and $\ell_2$ are in $L$, then 
        $\makelist(\ell_1, \ell_2)$ is in $L$.
  \item $L$ contains nothing else
  \end{enumerate}
\end{definition}

Conceptually, $\makelist(a,l)$ makes a new list with $a$ as its first
element, and $l$ as the rest of the list.

\subsection{Structural Induction on Recursive Data Type Definitions}

Structural induction is used to prove a property $P$ of all the elements
of some recursively-defined data type. The proof consists of two steps: 
\begin{itemize}
\item Prove $P$ for the ``base cases'' of the definition. 
\item Prove $P$ for the result of any combination rule, assuming that it
  is true for all the parts.  
\end{itemize}

Structural induction looks like a new inference rule, but it isn't: it
is standard (strong) induction on the \emph{number of formation steps}
it takes to build the object at hand out of the basic objects of the
recursive definition. For example, for a proof using the binary tree
definition, the induction steps would look something like this:

% For Boolean expressions:
%                                 %[[[Victor: slide]]]
% \begin{structproof}
%   Prove: $\forall e \in F (P(e))$ \\
%   1. (Base) $P(0)$ \\
%   2. (Base) $P(1)$ \\
%   3. (Inductive step) 
%   $\forall e, e' \in F (P(e) \wedge P(e') \Rightarrow P([e \wedge e']))$\\
%   4. (Inductive step) 
%   $\forall e, e' \in F (P(e) \wedge P(e') \Rightarrow P([e \vee e']))$ \\
%   5. (Inductive step) 
%   $\forall e \in F (P(e) \Rightarrow P([\neg e]))$\\
%   6. QED
%   \> \> \> \> \> Structural induction on Boolean expressions
% \end{structproof}
%
% For binary trees:
                                %[[[Victor: slide]]]
\begin{structproof}
  Prove: $\forall t \in T \; (P(t))$ \\
  1. (Base) $P(n)$, where $n$ is the single-node tree. \\
  2. (Inductive step) 
  $\forall t \in T \; (P(t) \Rightarrow P(\ms{makeleft}(t)))$ \\
  3. (Inductive step) 
  $\forall t \in T \; (P(t) \Rightarrow P(\ms{makeright}(t)))$ \\
  4. (Inductive step) 
  $\forall t,t' \in T \; (P(t) \wedge P(t') \Rightarrow P(\ms{makeboth}(t,t')))$ \\
  5. QED
  \> \> \> \> \> Structural induction on binary trees
\end{structproof}

% For strings over alphabet $A = \{ 0,1 \}$:
%                                 %[[[Victor: slide]]]
% \begin{structproof}
%   Prove: $\forall s \in S (P(s))$ \\
%   1. (Base) $P(\lambda)$ \\
%   2. (Inductive step) $\forall s \in S (P(s) \Rightarrow P(s 0))$ \\
%   3. (Inductive step) $\forall s \in S (P(s) \Rightarrow P(s 1))$ \\
%   4. QED
%   \> \> \> \> \> Structural induction on strings.
% \end{structproof}
% You can see how this would extend to different alphabets.

\subsubsection{Examples}

Here's example for each of the data types: 

\begin{theorem}
  Every Boolean expression has the same number of left and right parentheses. 
\end{theorem}
\begin{proof}
  Define $P(e)$: Expression $e$ has the same number of left and right
  parentheses.
                                %[[[Victor: slide]]]
  \begin{structproof}
    Prove: $\forall e \in F \; (P(e))$ \\
    1. (Base) $P(0)$ 
    \> \> \> \> \> The expression $0$ has no parens. \\
    2. (Base) $P(1)$ 
    \> \> \> \> \> No parens \\
    3. (Inductive step) 
    $\forall e, e' \in F \; (P(e) \wedge P(e') \Rightarrow P([e \wedge e'])$\\
    \> 1. Fix $e, e' \in F \;$. \\
    \> 2. Assume $P(e) \wedge P(e')$, that is, each of $e$ and $e'$ has the
    same number \\
    \> \quad of left and right parens. \\
    \> 3. $P([e \wedge e'])$, that is, the expression $e \wedge e'$ has the
    same number of \\
    \> \quad left and right parens. \\
    \> \> \> \> \> By inductive hypothesis (3.2), and the fact \\ 
    \> \> \> \> \> that we're adding one left and one right \\
    \> \> \> \> \> paren. \\
    \> 4. QED 
    \> \> \> \> Implication, UG \\
    4. (Inductive step) 
    $\forall e, e' \in F \; (P(e) \wedge P(e') \Rightarrow P([e \vee e'])$
    \\
    \> \> \> \> \> Similar to the previous case. \\
    5. (Inductive step) 
    $\forall e \in F \; (P(e) \Rightarrow P([\neg e])$
    \> \> \> \> \> Similar to the previous case. \\
    6. QED
    \> \> \> \> \> Structural induction on Boolean expressions
  \end{structproof}
\end{proof}

\begin{theorem}
  The number of edges in any binary tree is exactly one fewer than the
  number of nodes. 
\end{theorem}
\begin{proof}
  Define $P(t)$: Binary tree $t$ has exactly $1$ fewer edges than nodes.
  We are using the notation $\ms{nodes}(t)$, $\ms{edges}(t)$. 
  The key is that the inductive steps all preserve the ``deficit'' of
  1. 
  For instance, combining two trees involves adding two edges and one
  node; since each subtree had a ``deficit'' of 1, this maintains the
  deficit of 1:
                                %[[[Victor: slide]]]
  \begin{structproof}
    Prove: $\forall t \in T \; (P(t))$ \\
    1. (Base) $P(n)$, where $n$ is the single-node tree. 
    \> \> \> \> \> $0$ edges and $1$ node \\
    2. (Inductive step) 
    $\forall t \in T \; (P(t) \Rightarrow P(\ms{makeleft}(t))$ \\
    \> 1. Fix $t$. \\
    \> 2. Assume $P(t)$, that is, $|\ms{edges}(t)|+1 = |\ms{nodes}(t)|$. \\
    \> 3. $P(\ms{makeleft}(t))$, that is,
    $|\ms{edges}(\ms{makeleft}(t))|+1 = |\ms{nodes}(\ms{makeleft}(t))|$. \\
    \> \> 1. $|\ms{edges}(\ms{makeleft}(t))| = |\ms{edges}(t)| + 1$ \\
    \> \> 2. $|\ms{nodes}(\ms{makeleft}(t))| = |\ms{nodes}(t)| + 1$. \\
    \> \> 3. QED
    \> \> \> Algebra, using 2.2, 2.3.1, 2.3.2 \\
    \> 4. QED
    \> \> \> \> Implication, UG \\
    3. (Inductive step) 
    $\forall t \in T \; (P(t) \Rightarrow P(\ms{makeright}(t))$ 
    \> \> \> \> \> Similar to the previous case. \\
    4. (Inductive step) 
    $\forall t, t' \in T \; (P(t) \wedge P(t') \Rightarrow P(\ms{makeboth}(t,t'))$ \\
    \> 1. Fix $t$. \\
    \> 2. Assume $P(t) \wedge P(t')$, that is, $|\ms{edges}(t)|+1 =
    |\ms{nodes}(t)|$ and $|\ms{edges}(t')|+1 =|\ms{nodes}(t')|$. \\
    \> 3. $P(\ms{makeboth}(t,t'))$, that is,
    $|\ms{edges}(\ms{makeboth}(t,t'))|+1 = |\ms{nodes}(\ms{makeboth}(t))|$. \\
    \> \> 1. $|\ms{edges}(\ms{makeboth}(t,t'))| = |\ms{edges}(t)| +
    |\ms{edges}(t')| + 2$ \\
    \> \> 2. $|\ms{nodes}(\ms{makeboth}(t,t'))| = |\ms{nodes}(t)| +
    |\ms{nodes}(t')| + 1$. \\
    \> \> 3. QED
    \> \> \> Algebra, using 4.2, 4.3.1, and 4.3.2 \\
    \> 4. QED
    \> \> \> \> Implication, UG \\
    5. QED
    \> \> \> \> \> Structural induction on binary trees
  \end{structproof}
\end{proof}


\subsubsection{A string Theorem}

Here is a more complex proof, illustrating a combination of structural
induction and strengthening the hypothesis.

%%\forstudents{
\begin{theorem}
  In a string of $0$s and $1$s, the number of occurrences of the pattern
  $01$ is less than or equal to the number of occurrences of $10$, plus
  one.
\end{theorem}

Let's try to prove this by structural induction.  First we must
define $P(s)$.  Let's write $\ms{num}(pat,s)$ as the number of
occurrences of the pattern string pat in s.  Now our inductive
hypothesis is
\[
P(s): \ms{num}(01,s) \leq \ms{num}(10,s) + 1. 
\]
If you try to prove this by structural induction, you will get
stuck.
Why\? 
Consider what happens when you add $1$ at the end.  
This could increase the number of $01$s without increasing the number of
$10$s. 

So, to prove by structural induction on strings, let's strengthen the
hypothesis by adding another clause.  If a string ends in $0$ then
the number of $01$s is less than or equal to the number of $10$s.
That solves the problem by weakening what we have to show when the
string ends in $1$.  But maybe it causes another problem somewhere
else.  Let's give it a try: \\ 
\\
Redefine $P(s)$: \\
$\ms{num}(01,s) \leq \ms{num}(10,s) + 1$, \\
and \\
If $s$ ends in $0$ then $\ms{num}(01,s) \leq \ms{num}(10,s)$. \\
\\
This means that, for each inductive step, we have two things to show:
                                %[[[Victor: slide]]]
\structuredproof{
  Prove: $\forall s \in S \; (P(s))$ \\
  1. (Base) $P(\lambda)$ 
  \> \> \> \> \> \reason{No patterns of either kind.} \\
  2. (Inductive step) $\forall s \in S \; (P(s) \Rightarrow P(s 0))$ \\
  \> 1. Fix $s$. \\
  \> 2. Assume $P(s)$. \\
  \> 3. $P(s 0)$ \\
  \> \> 1. $\ms{num}(01,s0) \leq \ms{num}(10,s0) + 1$. 
  \> \> \> \reason{???} \\
  \> \> 2. If $s 0$ ends in $0$ then $\ms{num}(01,s0) \leq
  \ms{num}(10,s0)$. \noreason \\
  \> \> \> \> \> \reason{???} \\
  \> \> 3. QED
  \> \> \> \reason{Conjunction} \\
  \> 4. QED 
  \> \> \> \> \reason{Implication, UG} \\
  3. (Inductive step) $\forall s \in S \; (P(s) \Rightarrow P(s 1))$ \\
  \> 1. Fix $s$. \\
  \> 2. Assume $P(s)$. \\
  \> 3. $P(s 1)$ \\
  \> \> 1. $\ms{num}(01,s1) \leq \ms{num}(10,s1) + 1$. 
  \> \> \> \reason{???} \\
  \> \> 2. If $s 1$ ends in $0$ then $\ms{num}(01,s1) \leq
  \ms{num}(10,s1)$.\noreason \\
  \> \> \> \> \> \reason{???} \\
  \> \> 3. QED
  \> \> \> \reason{Conjunction} \\
  \> 4. QED 
  \> \> \> \> \reason{Implication, UG} \\
  4. QED
  \> \> \> \> \> \reason{Structural induction on strings.}\\
}

First let's consider $s1$. This is the case that looks dangerous,
because it might increase the number of $01$s.  We have to prove two
statements.  The second is easy, because the new string doesn't end in
$0$.  We say it's ``vacuously true''.

The first statement now takes some work. 
We might be adding to the number of $01$s.  
However, if we do, the previous string must have ended with $0$. 
Then the inductive hypothesis says that the previous string had to
satisfy the stronger inequality in the second statement. 
Adding one to the LHS of the stronger inequality yields the weaker
inequality we want.

The following proof fragment considers cases based on whether $s$ ends
in $0$ or not.  If not, it might end in $1$, or might be empty (don't
forget this possibility).

\begin{structproof}
  \> 3. $P(s 1)$ \\
  \> \> 1. $\ms{num}(01,s1) \leq \ms{num}(10,s1) + 1$. \\
  \> \> \> 1. If $s$ ends in $0$ then $\ms{num}(01,s1) \leq\ms{num}(10,s1) + 1$. \\
  \> \> \> \> 1. Assume $s$ ends in $0$. \\
  \> \> \> \> 2. $\ms{num}(01,s) \leq \ms{num}(10,s)$ 
  \> Inductive hypothesis (3.2), part 2. \\
  \> \> \> \> 3. $\ms{num}(01,s1) = \ms{num}(01,s) + 1$ 
  \> Adding one more $01$. \\
  \> \> \> \> 4. $\ms{num}(10,s1) = \ms{num}(10,s)$ \\
  \> \> \> \> 5. $\ms{num}(01,s1) \leq\ms{num}(10,s1) + 1$. 
  \> Algebra (combining 3.3.1.1.2, ...3, and ...4) \\
  \> \> \> \> QED 
  \> Implication \\
  \> \> \> 2. If $s$ ends in $1$ then $\ms{num}(01,s1)\leq\ms{num}(10,s1) + 1$. \\
  \> \> \> \> \> Inductive hypothesis, part 1; no new $01$s. \\
  \> \> \> 3. If $s = \lambda$ then $\ms{num}(01,s1) \leq\ms{num}(10,s1)+ 1$. \\
  \> \> \> \> \> $s1$ is just $1$, which has no $01$s. \\
  \> \> \> 4. QED 
  \> \> Cases \\
  \> \> 2. If $s 1$ ends in $0$ then $\ms{num}(01,s1) \leq \ms{num}(10,s1)$. \\
  \> \> \> \> \> Vacuously true, because $s1$ doesn't end in $0$. \\
  \> \> 3. QED
  \> \> \> Conjunction \\
\end{structproof}
Of course, you could also expand the step for $s$ ending in $1$ into a
careful series of inequalities.
\\

Now consider $s0$.  We hope that what we did to make the $s1$ case
work doesn't mess up the $s0$ case.  But we have to check.

The first statement is easy.  It follows from the first statement of
the inductive hypothesis for $s$, because we are not increasing the
number of $01$s.  But now the second statement takes more work.  The
difficulty is that the new string ends in $0$, which means that we
have to show the stronger inequality in the second statement.  But to
do this, we might only have the weaker inequality for the previous
string.  The argument again depends on what the previous string $s$
ended with.  So again, we consider cases, based on whether $s$ ends in
$0$ or $1$, or is empty.  If $s$ ends in $0$ we rely on the second
statement of the inductive hypothesis for $s$ (with the stronger
inequality), whereas if $s$ ends in $1$ we rely on the first statement
(with the weaker inequality).  In this case, we have to ``turn the
weaker inequality into the stronger inequality''.

\structuredproof[38ex]{
  \> 3. $P(s 0)$ \\
  \> \> 1. $\ms{num}(01,s0) \leq \ms{num}(10,s0) + 1$.
  \reason{Induct. hypothesis, part 1; no new $01$s.} \\
  \> \> 2. If $s 0$ ends in $0$ then $\ms{num}(01,s0) \leq\ms{num}(10,s0)$. \\
  \> \> \> 1. $\ms{num}(01,s0) \leq \ms{num}(10,s0)$. \\
  \> \> \> \> 1. If $s$ ends in $0$ then $\ms{num}(01,s0)
  \leq\ms{num}(10,s0)$. \noreason \\
  \reason{Induct. hypothesis, part 2; no new $01$s} \\
  \> \> \> \> 2. If $s$ ends in $1$ then $\ms{num}(01,s0)
  \leq\ms{num}(10,s0)$. \noreason \\ 
  \> \> \> \> \> 1. Assume $s$ ends in $1$. \\
  \> \> \> \> \> 2. $\ms{num}(01,s) \leq \ms{num}(10,s) + 1$. 
  \reason{Inductive hypothesis, part 1} \\
  \> \> \> \> \> 3. $\ms{num}(01,s0) = \ms{num}(01,s)$ \\
  \> \> \> \> \> 4. $\ms{num}(10,s0) = \ms{num}(10,s) + 1$ 
  \reason{Exactly one new occurrence of $10$.} \\
  \> \> \> \> \> 5. $\ms{num}(01,s0) \leq \ms{num}(10,s0)$ 
  \reason{Algebra} \\
  \> \> \> \> \> 6. QED
  \reason{Implication} \\
  \> \> \> \> 3. If $s = \lambda$ then $\ms{num}(01,s0) \leq
  \ms{num}(10,s0)$. \noreason \\ 
  \> \> \> \> \> \> 
\reason{$s0$ is just $1$, which has no $01$s or $10$s.} \\
  \> \> \> \> 4. QED 
  \> \> \reason{Cases} \\
  \> \> \> 2. QED
  \> \> \reason{Propositional reasoning (truth table)} \\
  \> \> 3. QED 
  \> \> \> \reason{Conjunction}\\
}

If you actually write out all these cases in the proof, you will
notice that some facts are stated repeatedly, e.g., that when you add
a $0$ to the end of a string you are not increasing the number of
$01$s.  To avoid having to state these facts several times, you can
move them earlier in the proof.
%%}

\subsection{Recursively-defined Functions on 
            Recursively-defined Data Types}

Recursive definitions provide a natural way to define functions whose
domains are recursively-defined data types.
\\
\begin{example}(Boolean Expressions)
  Define $\ms{eval}$, a function from Boolean expressions to $\{ 0, 1
  \}$, by: 
\begin{quote}
  $\ms{eval}(0) = 0$ \\
  $\ms{eval}(1) = 1$ \\
  $\ms{eval}([e \wedge e']) = 1$ if $\ms{eval}(e) = \ms{eval}(e') = 1$, $0$ otherwise. \\
  $\ms{eval}([e \vee e']) = 0$ if $\ms{eval}(e) = \ms{eval}(e') = 0$, $1$ otherwise. \\
  $\ms{eval}([\neg e]) = 0$ if $\ms{eval}(e) = 1$, $1$ otherwise. 
\end{quote}
\end{example}

\begin{example} (Strings)
For strings over alphabet $A$, define the function $\ms{length}(s)$ as
follows:
\begin{quote}
$\ms{length(\lambda)}=0$ (the empty string)\\
$\ms{length}(sa) = \ms{length}(s)+1$ for string $s$ and $a\in A$.\\
\end{quote}
\end{example}

\begin{example} (Binary Trees)
  Define the function $\ms{numnodes}(t)$ (a formal definition of what
  we previously used intuitively to be the number of nodes in the tree
  $t$), by: 
\begin{quote}
  $\ms{numnodes}(\mbox{single node}) = 1$ \\
  $\ms{numnodes}(\ms{makeleft}(t)) = \ms{numnodes}(t) + 1$ \\
  $\ms{numnodes}(\ms{makeright}(t)) = \ms{numnodes}(t) + 1$ \\
  $\ms{numnodes}(\ms{makeboth}(t,t')) = \ms{numnodes}(t)
  +\ms{numnodes}(t') + 1$ 
\end{quote}

Similarly,  define $\ms{numedges}(t)$: 
\begin{quote}
  $\ms{numedges}(\mbox{single node}) = 0$ \\
  $\ms{numedges}(\ms{makeleft}(t)) = \ms{numedges}(t) + 1$ \\
  $\ms{numedges}(\ms{makeright}(t)) = \ms{numedges}(t) + 1$ \\
  $\ms{numedges}(\ms{makeboth}(t)) = \ms{numedges}(t) +
  \ms{numedges}(t') + 2$ 
\end{quote}
\end{example}

We can use structural induction to prove properties of functions
defined in this way.
For example, we can reprove the relationship between numbers of nodes
and edges in terms of the formal functions $\ms{numnodes}$ and
$\ms{numedges}$.
(The argument is pretty much the same as before, just using the formal
function definitions instead of relying on our understanding of the
sizes of sets.) \\

%%\forstudents{
Define $P(t)$: 
$\ms{numnodes}(t) = \ms{numedges}(t) + 1$. 
                                %[[[Victor: slide]]]
\begin{structproof}
  Prove: $\forall t \in T \; (P(t))$ \\
  1. (Base) $P(t_0)$, where $t_0$ is the single-node tree. 
  \> \> \> \> \> By definition, $\ms{numnodes}(t_0) = 1$ \\
  \> \> \> \> \> and $\ms{numedges}(t_0) = 0$ \\
  2. (Inductive step) 
  $\forall t \in T \; (P(t) \Rightarrow P(\ms{makeleft}(t))$ \\
  \> 1. Fix $t$. \\
  \> 2. Assume $P(t)$, that is, $\ms{numedges}(t)+1 = \ms{numnodes}(t)$. \\
  \> 3. $P(\ms{makeleft}(t))$, that is,
  $\ms{numedges}(\ms{makeleft}(t))+1 = \ms{numnodes}(\ms{makeleft}(t))$. \\
  \> \> 1. $\ms{numedges}(\ms{makeleft}(t)) = \ms{numedges}(t) + 1$ \\
  \> \> \> \> \> Definition of $\ms{numedges}$ \\
  \> \> 2. $\ms{numnodes}(\ms{makeleft}(t)) = \ms{numnodes}(t) + 1$ \\
  \> \> \> \> \> Definition of $\ms{numnodes}$ \\
  \> \> 3. QED
  \> \> \> Algebra \\
  \> 4. QED \\
  3. (Inductive step) 
  $\forall t \in T \; (P(t) \Rightarrow P(\ms{makeright}(t))$ 
  \> \> \> \> \> Similar to the previous case. \\
  4. (Inductive step) 
  $\forall t, t' \in T \; (P(t) \wedge P(t') \Rightarrow P(\ms{makeboth}(t,t'))$ \\
  \> 1. Fix $t$. \\
  \> 2. Assume $P(t) \wedge P(t')$, that is, \\
  \> \quad $\ms{numedges}(t)+1 = \ms{numnodes}(t)$ and $\ms{numedges}(t')+1 =\ms{numnodes}(t')$. \\
  \> 3. $P(\ms{makeboth}(t,t'))$, that is,
  $\ms{numedges}(\ms{makeboth}(t,t'))+1 = \ms{numnodes}(\ms{makeboth}(t))$. \\
  \> \> 1. $\ms{numedges}(\ms{makeboth}(t,t')) = \ms{numedges}(t) +
  \ms{numedges}(t') + 2$ \\
  \> \> \> \> \> Definition of $\ms{numedges}$ \\
  \> \> 2. $\ms{numnodes}(\ms{makeboth}(t,t')) = \ms{numnodes}(t) +
  \ms{numnodes}(t') + 1$ \\
  \> \> \> \> \> Definition of $\ms{numnodes}$ \\
  \> \> 3. QED
  \> \> \> Algebra \\
  \> 4. QED \\
  5. QED
  \> \> \> \> \> Structural induction on binary trees
\end{structproof}
%%}

We've connected structural induction to recursive definitions.  In a
sense, this connection also holds for the natural numbers.  One can
think of the natural numbers as a recursively defined set
($0\in\naturals$, and if $n\in\naturals$ then $n+1 \in \naturals$),
and of normal induction as a structural induction on this recursive
definition.

\section{Induction and Recursive Algorithms}

We've spent a lot of time studying induction.  This is because
induction comes up all the time in analyzing computation.  Why?  Well,
induction is a ``one step at a time'' proof method.  Computations also
evolve ``one step at a time.''

In fact, many of our inductive proofs can be seen as \emph{algorithms}
for solving a problem.  And many of our recursive definitions can be
seen as algorithms for computing a value. For example, we proved ``any
$2^n$ by $2^n$ board can be tiled with Ls''.  If you look at the
inductive proof, we actually gave a \emph{procedure} for carrying out
that tiling.  We break the board in four, tile each piece, and merge
the tilings.  What kind of algorithm is this? It's \emph{recursive:}
it calls itself on smaller subproblems.  Similarly the inductive proof
for Nim gave a game-winning algorithm. The recursive definitions of
the Fibonacci numbers is also expressing a recursive algorithm for
computing them.

Just about any inductive proof that a problem has a solution is in
fact providing a recursive algorithm for solving the problem.

Similarly, when you have a recursive algorithm that you think solves
some problem, induction is the usual way to prove that it works.

%%% THIS SHOULD PROBABLY BE IN NEXT WEEK???

% \subsection{RSA}

% RSA is at the core of many of the secure communication protocols we
% use today (SSL, etc).  RSA works by treating any given message
% (sequence of bits) as a big number $x$ and applying a mathematical
% function that ``hides'' the number $x$ unless you know a secret key.

% More precisely, it computes the remainder $r$ of $x^a$ on division by
% $b$, where $a$ and $b$ are two specially constructed \emph{large}
% numbers.  It turns out that if someone is given $r$ and knows the
% right secret about the origin of $a$ and $b$, they can ``invert'' the
% exponentiation and get $x$.  But if you don't have the secret, the
% inversion seems to be very hard.

% So, how can we compute the exponentiation?\\
% The most obvious way is to work from the \emph{recursive definition}:
% \begin{itemize}
% \item $x^0=1$
% \item $x^{n}=x\cdot x^{n-1}$
% \end{itemize}
% This is a definition of $x^n$, but also suggests a recursive algorithm
% for computing it:
% \begin{structproof}
%   Procedure $\ms{Exp}(x,n)$\\
%   \\
%   {\bf if} $n=0$\\
%   \> return 1\\
%   {\bf else}\\
%   \> return $x*\ms{Exp}(x,n-1)$
% \end{structproof}
% Now it's pretty ``obvious'', but how would you \emph{prove} that
% algorithm $\ms{Exp}$ returns the right answer?\\
% Well, it doesn't always: what happens if you call $\ms{Exp}(5,-2)$?
% $\ms{Exp}(8,2.5)$?\\ 
% (Trying to prove correctness can reveal implicit assumptions.  We
% assume $n$ is a natural number).

% \begin{theorem}
%   For all $x,n \in \nats$, a call to $\ms{Exp}(x,n)$ returns $x^n$
% \end{theorem}
% Note: the procedure $\ms{Exp}$ above can be thought of as (i) a
% computational process or (ii) a recursive function definition (defined
% as the output of the computational process).  We need to prove that it
% defines the \emph{same} function as $x^n$.

% We are actually claiming two distinct things in the theorem:
% \begin{description}
% \item[Termination.] The algorithm returns something (i.e., doesn't run
%   forever). 
% \item[Correctness.] The algorithm returns the \emph{right} something.
% \end{description}
% \begin{proof}
%   By induction on $n$.  The base case, that $\ms{Exp}(x,0)$ returns
%   $x^0=1$, follows by inspection: on that call, the ``if'' condition is
%   satisfied, so we return 1.  For the inductive step, assume
%   $\ms{Exp}(x,n)$ returns $x^n$ and prove correctness for $n+1$.
%   Consider the call 
%   to $\ms{Exp}(x,n+1)$.  $n+1>0$, so the ``else'' clause is invoked.  We
%   call $\ms{Exp}(x,n)$ which, by assumption, returns $x^n$.  We multiply
%   that quantity by $x$, yielding $x^{n+1}$, and return it.  This proves
%   that $\ms{Exp}(x,n+1)$ terminates and returns the right value.
% \end{proof}

% OK, we've shown the procedure returns the right answer.
% Is it a good implementation?
% How many multiplications are done to compute $x^n$?  By induction,
% there are $n$ multiplications.
% Remember those ``128 bit keys'' we weren't allowed to export to
% foreign countries?  That
% means the number $n$ has about 128 bits.
% So we will be doing about $2^{128}$ multiplications.
% We'll still be working on it when 6.042 finishes...

% \subsection{Fast Exponentiation}

% Let's cut down on the number of multiplies.  Suppose we want to
% compute $x^a$ and $a$ is even, say $2c$.  So we want to compute
% $x^a=x^{2c}$.  Is there any obvious way to beat $a$ multiplies?
% Yes. Note
% $x^{2c}=(x^c)^2$.  So let's compute $x^c$ ($c$ multiplies) and then
% square it (1 multiply). This totals $c+1 =1+ a/2$ multiplies.

% What if $a$ is odd? 

% Let's generalize this idea to an algorithm:

% \begin{proofoverhead}
%   Procedure $\ms{FastExp}(x,n)$\\
%   \\
%   {\bf if} $n=0$\\
%   \> return 1\\
%   {\bf else}\\
%   \> {\bf if} $n$ is even\\
%   \> \> let $y=\ms{FastExp}(x,n/2)$\\
%   \> \> return $y^2$\\
%   \> {\bf else}\\
%   \> \> let $y=\ms{FastExp}(x,(n-1)/2)$\\
%   \> \> return $x*y^2$
% \end{proofoverhead}

% \begin{theorem}
%   For all $x,n \in \nats$, a call to $\ms{FastExp}(x,n)$ returns $x^n$
% \end{theorem}
% \begin{proof}
%   We'll use induction again.  The base case ($n=0$) follows by
%   inspection as before.  So let's prove the inductive step.

%   What kinds of subproblems are we going to use to prove it works for
%   $n$?  {\bf Not} just $n-1$, so let's use strong induction.

%   Since it keeps the notation simpler, we will prove $P(n)$ from
%   smaller cases instead of $P(n+1)$.  Suppose the inductive
%   hypothesis is true for every $k < n$, let's prove it for $n$.
%   Suppose we call $\ms{FastExp}(x,n)$.  We can assume $n\ne 0$ (we
%   already did a proof for 0) so the {\bf else} clause is selected in
%   the algorithm.  We consider two cases.

%   If $n$ is even (say $n=2m$) then we  call
%   $\ms{FastExp}(x,m)$.   By strong induction this returns $x^m$, which
%   we assign to $y$.
%   Then we return $y=(x^m)^2=x^{n}$ as required, so the proof works for
%   this case.

%   If $n$ is odd (say $n=2m+1$) then we call   $\ms{FastExp}(x,m)$ and
%   set $y$ to the result.  
%   Then we return $x*y^2=x*(x^m)^2=x^{2m+1}=x^n$.
%   So the proof works in this case too.
%   These are all the cases.  QED.
% \end{proof}

% How many multiplications does {\bf this} algorithm do?

% \begin{theorem}
%   If $n$ has $b$ bits, then $\ms{FastExp}(x,n)$ performs at most $2b$
%   multiplications.  
% \end{theorem}
% \begin{proof}
%   Induction on $b$.\\
%   Base case:  If $b=0$, then $n=0$ and we return without doing
%   any multiplications.  So the base case is true.
%   Inductive step: assuming it true for $b$ bits, consider a $b+1$-bit
%   number $n$.\\
%   We execute a recursive call to   $\ms{FastExp}$ on either $n/2$
%   or $(n-1)/2$, depending whether $n$ is odd or even.\\
%   Both of these numbers have at most $b$ bits.\\
%   So by induction, the recursion does at most $2b$ multiplications.\\
%   Then we do either one more (even case) or two more (odd case). So at
%   most two more.\\
%   Overall, at most $2b+2 = 2(b+1)$ multiplications.  QED.
% \end{proof}

% Using this algorithm, a 128-bit key means only 256 multiplications:
% quite an improvement!


% \subsection{Greatest Common Divisor}

% \begin{definition}
% Given 2 positive natural numbers, $a, b \in N^+$, their \emph{greatest
%   common divisor (GCD)} is the largest number that divides both
% without remainder.
% \end{definition}

% (Recall the notation: $a \mid b$ means $a$ divides $b$.)

% Finding the  GCD is a problem that must be solved to generate the
% ``secret'' used to decrypt RSA messages.

% One of the first recorded algorithms---Euclid's algorithm---finds
% greatest common divisors.  Here is a key lemma for ``simplifying''
% the problem:

% \begin{lemma}
%   Given $x>y$, let $r=x-y$.  Then any common divisor of $x$ and $y$ is
%   also a common divisor of $y$ and $r$, and vice versa.
% \end{lemma}
% \begin{corollary}
%   GCD$(x,y)=$GCD$(y,r)$
% \end{corollary}
% \begin{proof} (of the corollary).  The pair s$(x,y)$ and $(y,r)$ have exactly
%   the same set of divisors (by lemma).  Thus, the biggest number in
%   each set, namely the greatest common divisor, is the same.
% \end{proof}
% \begin{proof} (of the lemma).  We prove one direction: that any
%   divisor of $x$ and $y$ also divides $r$.  Suppose $d \mid x$ and $d
%   \mid y$.  So $x=zd$ and $y=wd$.  Thus $r=x-y=d(z-w)$ so $d \mid r$,
%   meaning $d$ is a common divisor of $y$ (by assumption) and $r$ (by
%   deduction).  The other direction of proof is similar.
% \end{proof}

% From this lemma we get Euclid's algorithm:
% \begin{structproof}
%   Procedure $\ms{Euclid}(x,y)$\\
%   \\
%   {\bf if} $x=0$ return $y$\\
%   {\bf else if} $y=0$ return $x$\\
%   {\bf else if} $x > y$ return $\ms{Euclid}(y,x-y)$\\
%   {\bf else} return $\ms{Euclid}(x,y-x))$
% \end{structproof}

% Example: \\
% Find $\ms{GCD}(112, 84)$ = ? \\
% Step 1: $112 - 84 = 28$, reduce to $(28,84)$. \\
% Step 2: $84 - 28 = 56$, reduce to $(28,56)$. \\
% Step 3: $56 - 28 = 28$, reduce to $(28,28)$. \\
% Step 4: $28 - 28 = 0$, reduce to $28,0$\\
% Now done, answer is $28$. \\
% \\

% Let's prove this algorithm does the right thing.
% First faint worry: maybe we've got an infinite recursion?
% The first thing to prove for any algorithm: it \emph{terminates}

% \begin{lemma}
%   For any natural number inputs $x$ and $y$, $\ms{Euclid}(x,y)$ returns
%   a value.
% \end{lemma}
% Why do we think this is true intuitively?  Because the arguments
% ``shrink'' on each recursive call and eventually reach 0.  Induction
% lets us formalize this.
% \begin{proof}
%   Induction on $x+y$.  More formally, we prove by strong induction on
%   $n$ that for all inputs $x$ and $y$ such that $x+y=n$, the algorithm
%   terminates.

%   Base case: if $x+y=0$, then $x$ is 0 so we return  immediately.

%   Inductive step.  Assume the claim for $x+y<n$ and prove it for
%   $x+y=n$.
%   Now consider two cases.  Either $x \ge y$ or $y \ge x$.  

%   Suppose first that $x \ge y$. So consider two subcases.  If $y=0$,
%   then we return immediately and the inductive step is proved.  If $y
%   > 0$, then we make a recursive call with arguments $y$ and $x-y <
%   x-0 =x$. So the sum of the two new arguments is less than
%   $x+y=n$. So the inductive hypothesis holds: the recursive call
%   returns a value. So our original call returns (the same) value.

%   What about the second case ($y \ge x$)?  Well, I would have to write
%   the same proof all over again, swapping $x$ and $y$ everywhere.  To
%   avoid such tedium, we say ``without loss of generality, assume $x
%   \ge y$.  This is code for ``the other case works exactly the same
%   way'' and completes the proof.
% \end{proof}

% \begin{lemma}
%   For any natural number inputs $x$ and $y$, $\ms{Euclid}(x,y)$
%   returns GCD$(x,y)$.
% \end{lemma}
% \begin{proof}
%   We'll use induction on $x+y$ as before.  The base case of $x+y=0$ is
%   trivial (assuming we define GCD$(0,0)$ to be 0, which seems fair).

%   For the inductive step where $x+y= n > 0$, assume without loss of
%   generality that $x \ge y$.  If $y=0$, we return $x$, which is the
%   correct answer.  If $y>0$, then we return the result of a recursive
%   call on $\ms{Euclid}(y,x-y)$.  This means (by strong induction) that
%   we return GCD$(y,x-y)$.  But we proved in a lemma above that
%   GCD$(x,y)=$GCD$(y,x-y)$. So we are returning the right value, namely
%   GCD$(x,y)$.
% \end{proof}

% One might be concerned about the GCD$(0,0)$ definition.  Technically
% every number is a common divisor of 0 and 0, so it should be infinite?

% But this turns out not to matter.  We never actually make a recursive
% call to $(0,0)$---as soon as one argument is 0, we terminate.  

% So even though we still need a base case for the induction pattern, we
% never actually apply that base case.  Instead our real base case is
% implicit in the ``subcase'' of the inductive step where one argument
% is 0.

% This is an example of a hack to the definition or algorithm that makes
% the proof cleaner.  If we wanted to avoid considering GCD$(0,0)$, we
% could prove by induction that any call to $\ms{Euclid}(x,y)$ that
% \emph{does not have both arguments equal to 0} returns the correct
% value.  However, we would then have to waste time on our induction
% step checking that this extra condition was still satisfied in the
% recursion.  By making an arbitrary, unimportant definition of
% GCD$(0,0)$, we save ourselves some work.

% As described, Euclid's algorithm may perform as many as $x$
% substractions (when $y=1$).  A small variation on our
% algorithm---using remainder on division by $y$ instead of subtracting
% $y$---can dramatically speed up the algorithm. It turns out that
% with this change, only $2\log x$ divisions are needed to solve the
% problem.

\end{document}
% LocalWords:  UG XXX XXXXXXXXXXXXXXXXXXXX UI ors nots makeleft makeright paren
% LocalWords:  makeboth parens LHS Ls GCD subcases subcase
