\documentclass[11pt,twoside]{article}
\usepackage{latex-macros/course}

\renewcommand{\coursecopyrightnames}
{\href{http://theory.lcs.mit.edu/~meyer}{Prof.~Albert~R.~Meyer}}
%\renewcommand{\coursecopyrightyear}{2002}


\newcommand{\mklist}{\text{makelist}}
\newcommand{\mktree}{\text{maketree}}
\newcommand{\subtrees}{\text{subtrees}}
\newcommand{\mkleaf}{\text{makeleaf}}
\newcommand{\leafv}{\text{leaf-value}}
\newcommand{\leafq}{\text{leaf?}}


\newcommand{\fstlist}{\text{list-first}}
\newcommand{\rstlist}{\text{list-rest}}
\newcommand{\nillist}{\text{()}}
\newcommand{\nillistq}{\text{list-nil?}}
\newcommand{\List}{\text{List}}

%\newcommand{\ms}[1]{\mathop{\text{#1}}}
\newcommand{\ms}[1]{\text{#1}}

\newcommand{\xara}[1]{\texttt{\textbf{\color{blue}{#1}}}}
\newcommand{\RBT}{\text{RecBinT}}
\newcommand{\FBT}{\text{FullBinT}}
\newcommand{\rt}{\text{root}}
%\newcommand{\rootr}{\text{FinT}}
\newcommand{\CT}{\text{CT}}
\newcommand{\RCT}{\text{RecCT}}


\begin{document}
\lecturenotes{6}{Recursive Definitions and Structural Induction}

\section{Recursive Definitions}
Recursive definitions say 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 case(s) that depend on simpler cases.
\end{itemize}

Here are some examples of recursive definitions:

\begin{example}
Define a set, $E$, recursively as follows:
\begin{enumerate}
\item $0 \in E$,\label{0E}
\item if $n \in E$, then $n+2 \in E$,\label{+2E}
\item if $n \in E$, then $-n \in E$.\label{-E}
\end{enumerate}

Using this definition, we can see that since $0 \in E$ by~\ref{0E}., it
follows from~\ref{+2E}. that $0 + 2 = 2 \in E$, and so $2+2 =4 \in E$,
$4+2 = 6 \in E$, \dots, and in fact any nonegative even number is in $E$.
Also, by~\ref{-E}., $-2,-4,-6,\dots \in E$.

Is anything else in $E$?  The definition doesn't say so explicitly, but
an implicit condition on a recursive definition is that the only way
things get into $E$ is as a consequence of ~\ref{0E}.,~\ref{+2E}.,
and~\ref{-E}.  So clearly $E$ is exactly the set of even integers.
\end{example}

\begin{example}\label{SLex}
Define a set, $S$, of strings of \texttt{a}'s and \texttt{b}'s recursively
as follows:
\begin{enumerate}
\item $\lambda \in S$, where $\lambda$ is the \emph{empty} string,\label{lam}
\item if $x \in S$, then $\texttt{a}x\texttt{b} \in S$, \label{axb}
\item if $x \in S$, then $\texttt{b}x\texttt{a} \in S$,\label{bxa}
\item if $x,y \in S$, then $xy \in S$.\label{xy}
\end{enumerate}
\end{example}

Here we're writing $xy$ to indicate the \emph{concatenation} of the
strings $x$ and $y$, namely, $xy$ is the string that starts with the
sequence of \texttt{a}'s and \texttt{b}'s in $x$ followed by the
\texttt{a}'s and \texttt{b}'s in $y$.

Using this definition, we can see that since $\lambda \in S$ by~\ref{lam}.,
it follows from~\ref{axb}. that
$\texttt{a}\lambda\texttt{b}=\texttt{ab}\in S$, so $\texttt{aabb}\in S$ 
by~\ref{axb}. and $\texttt{baba}\in S$ by~\ref{bxa}.  Likewise,
$\texttt{b}\lambda\texttt{a}=\texttt{ba}\in S$ by~\ref{bxa}., so
$\texttt{abab}\in S$ by~\ref{axb}. and $\texttt{bbaa}\in S$
by~\ref{bxa}.  Also, since $\texttt{ab}\in S$ and $\texttt{ba}\in S$,
we have $\texttt{abba}\in S$ as well as as $\texttt{baab}\in S$
by~\ref{xy}.

Notice that every string in $S$ has an equal number of \texttt{a}'s and
\texttt{b}'s.  This is easy to prove by  induction on how a string
gets to be in $S$.  Let
\[
L \eqdef \set{x \in \set{\texttt{a},\texttt{b}}^* \suchthat
\#\text{\texttt{a}'s in } x = \#\text{\texttt{b}'s in } x}.
\]

\begin{lemma}\label{SL}
\[
S \subseteq L.
\]
\end{lemma}
\begin{proof} Let $P(n)$ be the predicate that if any string,
$s$, is in $S$ as a consequence of $n$ applications of
rules~\ref{axb}.,~\ref{bxa}., and~\ref{xy}., then $s \in L$.  We will
prove that $P(n)$ holds for all $n \in \naturals$ by strong induction.

\textbf{Base case} ($n=0$).
The only way to get an $s \in S$ without using any of the
rules~\ref{axb}.,~\ref{bxa}., and~\ref{xy}., is by rule~\ref{lam}., so $s
= \lambda$ and $s$ indeed has an equal number of \texttt{a}'s and
\texttt{b}'s, namely zero of each.

\textbf{Inductive step} ($n\geq 0$).  
Assume $P(0), \dots, P(n)$ to prove $P(n+1)$.

So suppose $s \in S$ as a consequence of $n+1$ applications of
rules~\ref{axb}.,~\ref{bxa}., and~\ref{xy}.

\emph{Case 1:} The ($n+1$)st rule was~\ref{axb}.  That is $s = \texttt{a} x
\texttt{b}$ for some $x$ that is in $S$ as a consequence of $n$
applications of~\ref{axb}.,~\ref{bxa}., and~\ref{xy}.  By induction
hypothesis, $x$ has an equal number of \texttt{a}'s and \texttt{b}'s, say
$k$ of each.  Then, $s$ also has an equal number of \texttt{a}'s and
\texttt{b}'s, namely $k+1$ of each, so $s \in L$.

\emph{Case 2:} The ($n+1$)st rule was~\ref{bxa}.  Symmetric to Case 1.

\emph{Case 3:} The ($n+1$)st rule was~\ref{xy}.  So $s = xy$ where $x$ and
$y$ are each in $S$ as a consequence of at most $n$ applications
of~\ref{axb}.,~\ref{bxa}., and~\ref{xy}.  By induction hypothesis, $x$ has
the same number, say $k_x$, of \texttt{a}'s and \texttt{b}'s, and $y$ has
the same number, say $k_y$, of \texttt{a}'s and \texttt{b}'s.  So $xy$ has
has an equal number of \texttt{a}'s and \texttt{b}'s, namely $k_x + k_y$
of each, and again $s \in L$ as required.
\end{proof}

It's also not hard to show that every string with an equal number of
\texttt{a}'s and \texttt{b}'s is in $S$:
\begin{problem}
Prove that $L = S$.
\end{problem}

\solution{We already know that $S \subseteq L$, so all we need show is
that every string, $x \in L$ is also in $S$.  We do this
by strong induction on the length, $\abs{x}$, or $x$.  

Namely, use the strong induction
hypothesis 
\[
P(n) \eqdef\quad \forall x \in L\ \abs{x} = n \implies x \in S.
\]
\begin{proof}

\textbf{Base case} ($n=0$).
$P(0)$ holds because the zero-length string,
$\lambda$, is in $S$ by definition of $S$.

\textbf{Inductive step} ($n\geq 0$).  Assume $P(k)$ for all $k \leq n$ to
prove $P(n+1)$.  So let $x \in L $ be of length $n+1$.

\textbf{Case 1:} Some proper prefix of $x$ is in $L$.  That is, $x = yz$
for some $y \in L, z \in \set{\texttt{a},\texttt{b}}^*$ with $0 < \abs{y}
< \abs{x}$.  It follows that also $0 < \abs{z} < \abs{x}$ and $z \in L$.
By strong induction hypothesis, we conclude that $y,z \in S$, so by
rule~\ref{xy}., $x = yz \in S$, as required.

\textbf{Case 2:} Reading the symbols in $x$ from left to right, the number
of \texttt{a}'s read remains larger than the number of \texttt{b}'s until
all of $x$ is read.  So $x$ must be of the form $\texttt{a} y \texttt{b}$
for some $y \in L$.  By strong induction hypothesis we conclude that $y
\in S$, so by rule~\ref{axb}., $x = \texttt{a} y \texttt{b} \in S$, as
required.

\textbf{Case 3:} Same a Case~2, with \texttt{a}'s and \texttt{b}'s
reversed.

\end{proof}}

\begin{example}
The set, $F$, of \emph{Fully Bracketed Arithmetic Expressions in
$x$} is a set of strings over the alphabet
$\set{\xara{]},\xara{[},\xara{+},\xara{-},\xara{*}, \xara{x}}$
defined recursively as follows:

\begin{enumerate}
\item The symbols $\xara{0,1,x}$ are in $F$.
\item If $e$ and $e'$ are in $F$, then the string $\xara{[}e \xara{+}
e'\xara{]}$ is in $F$,
\item
if $e$ and $e'$ are in $F$ then the string $\xara{[}e \xara{*} e'\xara{]}$ is
in $F$,
\item
if $e$ is in $F$ then the string $\xara{[}\xara{-} e\xara{]}$ is in $F$.
\end{enumerate}
\end{example}

Several basic examples of recursively defined data types are based on
\emph{rooted trees}.  These are possibly infinite directed trees with a
unique ``root'' vertex such that every vertex is reachable by a directed
path from the root.

One important class of rooted trees are the \emph{ordered binary trees}.
These are possibly infinite rooted trees with labelled edges, such that at
most two edges leave each vertex.  If two edges leave a vertex, one is
labelled \texttt{left} and the other is labelled \texttt{right}.  If one
edge leaves a vertex, it is labelled either \texttt{left} or
\texttt{right}.  We will define a special class of ordered binary trees
called the \emph{recursive ordered binary trees}, $\RBT$:

\begin{example}
$\RBT$'s are defined recursively as follows:
\begin{enumerate}

\item
If $G$ is a graph with one vertex and no edges, then $G$ is a $\RBT$.
That is, $(\set{v}, \emptyset) \in \RBT$ and $\rt((\set{v}, \emptyset)) =
v$.

\item \label{ml}
If $T=(V,E)$ is in $\RBT$, and $\mathbf{n}$ is a ``new'' node not in $V$,
then the graph, $\ms{makeleft}(T)$, made by adding an edge labelled
\texttt{left} from $\mathbf{n}$ to $\rt(T)$ is a $\RBT$.  That is,
\[
\ms{makeleft}(T) \eqdef (V \union \set{\mathbf{n}}, E \union
 \set{(\mathbf{n},\rt(T),\texttt{left})}) \in \RBT,
\]
where $(v,w,\ell)$ is the directed edge from vertex $v$ to
vertex $w$ with label $\ell$.

\item \label{mr} Same as above, with ``right'' in place of ``left.''

\item If $T_1=(V_1,E_1)$ and $T_2=(V_2,E_2)$ are in $\RBT$, $V_1$ and
$V_2$ are disjoint, and $\mathbf{n}$ is a ``new'' node not in $V_1 \union
V_2$, then the graph, $\ms{makeboth}(T_1,T_2)$, made by adding an edge
labelled \texttt{left} from $\mathbf{n}$ to $\rt(T_1)$ and an edge
labelled \texttt{right} from $\mathbf{n}$ to $\rt(T_2)$ is a $\RBT$.  That
is, $\ms{makeboth}(T_1,T_2) \in \RBT$, where
\begin{eqnarray*}
\lefteqn{\ms{makeboth}(T_1,T_2)}\\ &\eqdef& (\set{\mathbf{n}} \union V_1
\union V_2, E_1 \union \set{(\mathbf{n},\rt(T_1),\texttt{left})} \union
E_2 \union \set{(\mathbf{n},\rt(T_2),\texttt{right})}).
\end{eqnarray*}
\end{enumerate}

These cases are illustrated in Figure~\ref{fig:bintree}, with edges
labelled ``left'' shown going down to the left, and edges labelled
``right'' shown going down to the right.

\begin{figure}
\begin{center}
\input{figures/btree.pic}
\end{center}
\caption{Building a binary tree: (a)~$\ms{makeleft}(T)$,
(b)~$\ms{makeright}(T)$, and (c)~$\ms{makeboth}(T_1,T_2)$.}
\label{fig:bintree}
\end{figure}

A special case of $\RBT$'s are the \emph{full} ordered binary trees,
$\FBT$.  These are $\RBT$'s in which every node is either a \emph{leaf}
(\ie has out-degree zero) or has both a left and right subtree (see
Figure~\ref{fig:fullbintree}).  In other words rules~\ref{ml}.\
and~\ref{mr}.\ in the definition of $\RBT$ are not used in defining the
subset $\FBT \subset \RBT$.

\begin{figure}
\begin{center}
\input{figures/fbtree.pic}
\end{center}
\caption{A full binary tree.}
\label{fig:fullbintree}
\end{figure}
\end{example}

It's easy to prove by structural induction that every $\RBT$ is finite.
We'll skip the details, since we'll do a more interesting proof of this
kind for infinite trees in Theorem~\ref{fprgt} below.  It's also easy to
prove by strong induction on the size of finite trees that every finite
ordered binary tree is an $\RBT$.  In other words, $\RBT$ is precisely the
set of \emph{finite} ordered binary trees.

\iffalse
\begin{enumerate}
\item 

\item If $\ang{t_1,t_2,\dots,t_n,\dots}$ is a (finite or
infinite) sequence of elements in $\CT(A)$, then
$\mktree(\ang{t_1,t_2,\dots,t_n,\dots})$ is in $\CT(A)$.
\end{enumerate}


So Abstract Finite Trees are simply the Abstract Countable Trees that have
only finitely many nodes.
\fi


\iffalse
\begin{example}
The set, $\List$, of \emph{pure lists} is defined recursively by:
\begin{enumerate}
\item The 0-tuple, $\nillist$, is in $\List$.
\item If $\ell_1$ and $\ell_2$ are in $\List$, then the pair $(\ell_1,
\ell_2)$ is in $\List$.
\end{enumerate}

In Lisp-like programming languages, the pairing operation is called
\texttt{cons} and the 0-tuple is called \texttt{nil}.

\end{example}


We can define trees abstractly in a similar way, using constructors
$\mkleaf$ and $\mktree$ and corresponding selectors, $\leafv$ and
$\subtrees$, and predicate, $\leafq$.

\begin{example}
Define the set, $\rtr(A)$, of \emph{Abstract Finite Trees with
leaf-values $A$} as follows:
\begin{enumerate}
\item $\mkleaf(a)$ is in $\rtr(A)$ for every $a \in A$.

\item\label{tuple} If $\ang{t_1,t_2,\dots,t_n}$ is an $n$-tuple of
elements in $\rtr(A)$ for some some $n>0$, then
$\mktree(\ang{t_1,t_2,\dots,t_n})$ is in $\rtr(A)$.
\end{enumerate}

Here, the selectors are supposed to satisfy
\begin{eqnarray*}
\leafv(\mkleaf(a)) & = & a\\
\subtrees(\mktree(p)) & = & p,
\end{eqnarray*}
for every $a \in A$ and tuple, $p$, of elements in $\rtr(A)$.  Also, the
predicate $\leafq$ has domain $\rtr(A)$ and satisfies
\[
\leafq(t) = \texttt{true} \quad \emph{iff} \quad \exists a \in A\ t = \mkleaf(a).
\]

Although an abstract tree might be constructed out of something other than
a graph, we will draw them as tree graphs.  That is, we would draw
$\mktree(\ang{t_1,t_2,\dots,t_n})$ as a graph consisting of a \emph{root
node} with edges to the root nodes of graphs picturing each of the $n$
subtrees $t_1,t_2,\dots,t_n$ (see Figure~\ref{fig:rooted-tree}).
\begin{figure}
\begin{center}
\input{figures/rtree.pic}
\end{center}
\caption{Graph for an Abstract Finite tree $t = \mktree(\ang{t_1,t_2,\dots,t_n})$.}
\label{fig:rooted-tree}
\end{figure}

\end{example}
\fi


\section{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}

For example, structural induction on Fully Bracketed Arithmetic
Expressions takes the form:

\begin{proof}
To prove $\forall e \in F\ P(e)$, show:

\textbf{Base} ($e= \xara{0}$).  $P(\xara{0})$ holds.

\textbf{Base} ($e= \xara{1}$).  $P(\xara{1})$ holds.

\textbf{Base} ($e= \xara{x}$).  $P(\xara{x})$ holds.

\textbf{Inductive step} ($\xara{[}e \xara{+} e'\xara{]}$).
Assume $P(e)$ and $P(e')$ to prove $P(\xara{[}e \xara{+}
e'\xara{]})$.

\textbf{Inductive step} ($\xara{[}e \xara{*} e'\xara{]}$).
Assume $P(e)$ and $P(e')$ to prove $P(\xara{[}e \xara{*}
e'\xara{]})$.

\textbf{Inductive step} ($\xara{[-}e \xara{]}$).
Assume $P(e)$ to prove $P(\xara{[-}e \xara{]})$.
\end{proof}

Here's an actual example:

\begin{theorem}
Every Fully Bracketed Arithmetic Expression has the same number of left
and right brackets.
\end{theorem}

\begin{proof}
This is just like the proof of Lemma~\ref{SL} above, except we proved
Lemma~\ref{SL} by ordinary strong induction explicitly on the number of
rules used to contruct on element.  Here we use structural induction,
which lets us carry out the proof without having to count rule
applications.

Define $P(e) \eqdef\ $ expression $e$ has the same number of left
brackets, \xara{]}, and right brackets, \xara{[}.

\textbf{Base Cases} 
($e = \xara{0}$, $e= \xara{1}$, or $e = \xara{x}$). 
The expression $e$ has no brackets.

\textbf{Inductive step} 
($\xara{[}e \xara{+} e'\xara{]}$).
Assume $P(e)$ and $P(e')$ to prove $P(\xara{[}e \xara{+}
e'\xara{]})$.

But $P(e)$ implies $e$ has $k_e$ left brackets and $k_e$ right brackets
for some $k_e \in \naturals$; likewise $e'$ has $k_{e'}$ left brackets and
$k_{e'}$ right brackets.  So $\xara{[}e \xara{+} e'\xara{]}$ has $k_e+
k_{e'} +1$ right brackets and the same number of left brackets.

\textbf{Inductive step} ($\xara{[}e \xara{*} e'\xara{]}$).  
Similar.

\textbf{Inductive step} ($\xara{[-}e\xara{]}$).
Similar.
\end{proof}

\section{Induction on Trees}

Here's a proof using structural induction on binary trees:

\begin{theorem}\label{binary-edges-nodes}
The number of edges in any $\RBT$ is exactly one fewer than the
number of vertices. 
\end{theorem}

\begin{proof}

Define\[
P(T) \eqdef \quad T=(V,E) \in \RBT  \text{ and } \card{V}-1=\card{E}.
\]

\textbf{Base Case} ($T$ is the single-node tree). 
There are $0$ edges and $1$ node, so $P(T)$ holds.

\textbf{Inductive step} ($T= \ms{makeleft}(S)$).  Assume $P(S)$ to prove
$P(T)$.  That is, assuming
\begin{equation}\label{t1n}
\card{V_S}-1=\card{E_S},
\end{equation}
show that
\begin{equation}\label{mlf}
\card{V_T}-1=\card{E_T}
\end{equation}
But
\begin{align}
E_T =& E_S \union \set{(\mathbf{n},\rt(S),\texttt{left})} \qquad \text{so,} \notag\\
\card{E_T}  =& \card{E_S} +1, \label{e+1}
\end{align}
and
\begin{align}
\card{E_T} =& \card{V_S}, \qquad \text{(by~(\ref{e+1}) and~(\ref{t1n})), so}, \notag\\
\card{E_T}+1 =& \card{V_S}+1. \label{elt}
\end{align}
But
\begin{align}
V_T =& V_S \union \set{\mathbf{n}}, \qquad \text{so} \notag\\
\card{V_T} =& \card{V_S} + 1 \label{n+1}
\end{align}
Combining~(\ref{n+1}) and~(\ref{elt}) immediately implies~(\ref{mlf}).

\textbf{Inductive step} ($T = \ms{makeright}(S)$).  Same as previous case with
``right'' replacing ``left.''

\textbf{Inductive step} ($T= \ms{makeboth}(T_1,T_2)$).  Assume $P(T_1)$
and $P(T_2)$ to prove $P(T)$.  That is, assuming
\begin{eqnarray}
\card{E_{T_i}} & = &\card{V_{T_i}}-1,
\end{eqnarray}
for $i=1,2$, prove
\begin{equation}\label{mtt}
\card{E_{T}}  = \card{V_{T}}-1,
\end{equation}
The similar proof for this case is left to the reader.
\end{proof}

\section{Games Trees}

Recursive Game Trees (RGT's) are another recursively-defined data type that
can be used to define games like chess, checkers, or tic-tac-toe.  These
are games in which two players alternate moves that depend only on the
visible board position or state of the game.  Such games are technically
called \emph{two person terminating games of perfect information}.
``Perfect information'' means that the players know the complete state of
the game at each move.  (Most card games are \emph{not} games of perfect
information because neither player can see the other's hand.)
``Terminating'' means that the game must end with a winner---it is
impossible to continue play forever.

\begin{problem}
Why must every play of chess eventually end?

\solution{
Chess has a rule that if any position is repeated twice, then the play
ends in a draw (``stalemate'')---which we would count as a win for the
second player.  Since there are only finitely many board positions in
chess, and none can occur more than two times before the play ends, a play
can last at most $2n+1$ moves, where $n$ is the total number of possible
board positions---which is enormously large by the way.  In practice, the
nature of chess causes plays to end in under 100 moves.

\iffalse
How about checkers?  I don't know if checkers has a similar rule.  If not,
a play could continue forever by having opposing kings cycle around each
other.
\fi
}

\end{problem}

A two person games of perfect information is represented abstractly by a
game tree whose root corresponds to the start position of the game.  The
root has a child for each position after a possible starting move of the
first player.  Each of these children in turn has children (these are
grandchildren of the root) corresponding to the positions of the game after
possible moves by the second player, and so on.

For example, in the game tree for tic-tac-toe, the root has nine children
corresponding to the nine boxes that the first player could mark with an
``X.''  Each of these nodes has eight children corresponding to the eight
remaining boxes which the second player could mark with an ``O,'' and so
on.  Paths from root to leaf are of length at most nine, because every
TIC-TAC-TOE game ends after at most nine moves.


%%%PICTURE WOULD BE GOOD

In general, each node corresponds to a state of the game, and its children
correspond to the states which result from each of the possible moves by
the player whose turn it is.  The leaves of the tree correspond to
situations where no moves are possible---the game is over.  A path from
the root to a leaf describes an individual game or \emph{play} of the
game.  (In English, ``game'' can be used in two senses: we can say that
chess is a game, and we can also play a game of chess.  The first usage
refers to the game tree, and the second usage refers to what we call a
``play.'')

\begin{problem}
How many children does the root of a game tree for chess have?  What is
the first level of the tree where two nodes on that level have different
numbers of children?

\solution{20 moves from the root (level 0), namely 16 pawn moves and 4
knight moves.  Same at level 1 for the second player.  But at level 2,
corresponding to first player's second move, there are different numbers
of choices.}

\end{problem}

In many games like tic-tac-toe or chess, a play may end with a draw, but
it's slightly simpler to develop our game theory if we forbid draws (for
example, we could rule that all draws count as wins for the second
player).  So we label the leaves of the game tree with \texttt{win} or
\texttt{lose} indicating the outcome for the first player.  (A win for one
player is a loss for the other---no ``everybody wins''-type games at
MIT. \texttt{:-)}

A \emph{strategy} for a player in a game specifies which move the player
should make in any state in which it is that player's turn to move.  A
\emph{winning} strategy ensures that the player will win no matter what
moves the other player makes.

In tic-tac-toe for example, most elementary school children figure out
strategies for both players that each ensure that the other player can
never get ``tic-tac-toe''.  If we count a play that ends without a
tic-tac-toe as a win for the second player, then the strategy which
prevents the first player from getting ``tic-tac-toe'' is a winning
strategy for the second player.  (Of course the first player can win if
his opponent plays childishly, but not if the second player follows the
winning strategy.)

Familiar games like tic-tac-toe and chess have finite game-trees, but not
all games do.  Here's a simple, if silly example called the \emph{MN} Game:
I go first and pick any integer, $m > 0$.  The second move is yours and you
may pick any natural number $n>m$.  After that we alternate picks, each of
us picking on our turn any positive integer less than $n$ that has not been
chosen previously.  The first person who has no move left on their turn is
the loser.  Of course you have an obvious winning strategy for the MN game:
pick $n$ to be the smallest even integer $>m$.  On the other hand, even
though you are sure to win, I can delay your win as long as I like by
choosing a very large $m$.

Notice that there are an infinite number of possible first moves, and for
each first move, and infinite number of possible second moves.  So if we
represented the MN game as a tree, it would be infinitely ``wide.''

In general, we define Recursive Game Trees, and their roots, as follows:

\begin{definition}
\begin{enumerate}

\item A single node, $\mathbf{n}$, labelled \texttt{win} or \texttt{lose}
is an \emph{RGT} and its \emph{root} is $\mathbf{n}$.

\item 
If $\mathcal{G}$ is a nonempty finite or infinite set of pairwise disjoint
RGT's (that is, if $G_1\neq G_2 \in \mathcal{G}$, then $G_1$ and $G_2$ have
no nodes in common), and $\mathbf{n}$ is a ``new'' node not in any RGT in
$\mathcal{G}$, then the graph with an edge from $\mathbf{n}$ to the root of
$G$ for each $G \in \mathcal{G}$ is an RGT, and its root is $\mathbf{n}$.

\end{enumerate}

\end{definition}

For example, the game tree for the MN game has a root with edges going to
the roots of an infinite number of Game Trees $G_1,G_2,\dots$ corresponding
to each possible value of $m$ the first player can choose.  The root of
each subtree $G_m$ has edges going to the roots of an infinite number of
finite Game Trees $H_{m+1},H_{m+2},\dots$ corresponding to the value of $n$
chosen by the second player.  There are $n-2$ edges from the root of the
Game Tree $H_n$ each corresponding to one of the integers the first player
can choose on his second move.  These edges each lead to the root of a tree
with $n-3$ edges, and so on.  If $n$ is even, all the leaves of $H_n$ are
labelled \texttt{lose}, and all are labelled \texttt{win} if $n$ is odd.

So the MN Game Tree is ``infinitely wide,'' namely, there are nodes that
have an infinite number of children.  Also, there is no finite bound on the
length of plays, so the tree is also ``infinitely deep.''  But notice that
although there are finite paths from the root of the MN tree of every
finite length greater than 1, there is \emph{no single infinite path} from
the root.  This reflects the fact that every MN game must end after a
finite number of moves.  An infinite path would correspond to an infinite
sequence of moves that never ended at a win or loss.

The Gale Subset Game described below is very similar to the MN game but is
much more challenging.  In fact, no winning strategy (for either player) is
known for the Gale game.

\subsection{The Gale Subset Game [optional]}
\begin{optional}

Like the MN game, in the \hyperdef{gale}{gale}{\emph{Gale Subset
Game}}\footnote{J. Daniel Christensen and Mark Tilford, ``David Gale's
Subset Take-Away Game,'' American Mathematical Monthly v.105 (Jan.1998)}
the first player chooses any positive integer $m$, and the second player
chooses any integer $n>m$.  After that the players alternate moves, where
a move consists of picking a proper subset $B \subset \set{1,\dots,n}$
(that is, $B \neq \set{1,\dots,n}$) such that $B$ does not contain any
subset chosen at a previous move.  The player who first chooses the empty
set is the loser.

For example, if the first player picks $m=3$, and the second player picks
$n=4$, the subsequent moves might be:
\[
\begin{array}{ccccccccc}
\text{player:} & 1 &2 & 1 &2 & 1 &2 & 1 &2\\
\text{move:}   &\set{1,2} &\set{3,4} & \set{1,3} & \set{2,4} & \set{1} & \set{2} & \set{3} & \set{4}
\end{array}
\]
At this point, the first player must choose the empty set and therefore
loses.

{\em Gale's Conjecture} is that the second player has a winning strategy.
The truth of the Conjecture remains unknown.

\begin{notesproblem}

\bparts

\ppart Prove Gale's Conjecture for the games with $m=1$ and $n=2$ or 3.

\solution{When $n=2$, $A=\set{1,2}$.  The first player can only choose a
singleton set consisting of one of the two elements.  The second player
just chooses the other one and wins.

When $n=3$, the first player can have two choices: choosing a subset
containing 1 element or 2 elements.  Whatever the first player's choice is,
the second player simply picks the complement of the first player's choice.
The game is then reduced to the case when $n=2$. Therefore, Gale's
Conjecture holds for $n=2,3$.}

\ppart Suppose the second player picks the integer $n$.  What is the
length of the shortest possible game in which no player chooses the empty
set when another move is possible?  What is the length of the longest
possible game?  Conclude that every Gale game must end.

\solution{The game will always end with a winner, because after $n > m$ is
chosen by the second player, there are only $2^n -1$ sets that are legal
picks by the players on their subsequent turns.  Therefore the game must
end after $\leq 2^n -1$ more moves.

It is possible to have this many moves in a game: the players could choose
all the subsets of size of $n-1$ first, followed by those with size of
$n-2$, and so on, down to subsets with size of 1.  Such a sequence of moves
is allowed because all the moves prior to any given move in the sequence
are subsets at least as large as the given move, so none of them is
contained in the given move.

The shortest possible game would last for $n+1$ steps. In such a game the
players always choose subsets containing one element.  When all the $n$
such sets are chosen, the only valid move is the empty set, and the game
ends.  It is not possible to end in fewer than $n+1$ moves because the $n$
subsets with size 1 can always be picked if they have not been picked
before.}

\ppart Try to prove Gale's Conjecture for $n=4$.  \hint You will be
overwhelmed with cases if you don't identify ``symmetric'' cases.  For
example, if player 1's first move is $\set{1,2,3}$, and you work out how
player 2 will win, then you can adapt your strategy to work against {\em
any} first move consisting of a set of size three, by permuting the roles
of~1, 2, 3, and~4.

\solution{There are three cases for the move of the first player
when the game starts:

\begin{enumerate}
\item The first player chooses a subset of 1 element.  The second player
then should choose the complement of the first player's choice.  The game
then becomes the same as playing the $n=3$ game on the set just chosen by
the second player.

\item The first player chooses a subset of 3 elements.  The second player
should choose the complement of the first player's choice.  The game then
becomes the same as playing the $n=3$ game on the set just chosen by the
first player.

\item The first player chooses a subset of 2 elements $C_1=\set{a,b}$.  The
second player then picks the complement of the first player's choice,
$C_2=\set{c,d}$.  We then have the following cases:
\begin{enumerate}

\item If the first player choose a subset of one element contained in
$C_1$ or $C_2$, say, $\set{a}$, the second player can choose the subset containing
only the element which remains in the same set, i.e., $\set{b}$.  The game
is then reduced to the case when $n=2$.

\item
If the first player chooses a subset of two elements --- necessarily one
element from $C_1$ and the other from $C_2$, say, $\set{a,c}$.  The second
player chooses the complement of it, $\set{b,d}$.  We have two remaining
possible subcases:
\begin{enumerate}

\item If the first player chooses one of the remaining sets of size two,
say $\set{a,d}$, player two should choose its complement, $\set{b,c}$.  The
remaining possible moves are the four sets of size 1, where the second
player clearly wins after two more rounds.

\item If the first player chooses a set of 1 element in $C_1$ or $C_2$,
say, $\set{a}$, player two should choose the set containing only the element
remaining in the set, i.e., $\set{b}$.  The game is then reduced to the case
when $n=2$.
\end{enumerate}
\end{enumerate}
\end{enumerate}
Therefore, player also has a winning strategy in the Gale game for $n=4$. 
}

\eparts
\end{notesproblem}
\end{optional}


\subsection{Finite Path Trees}

The recursive definition of RGT's guarantees that they describe terminating
games.  That is, an RGT has \emph{no} infinite path away from its root.  We
can prove this easily by structural induction on the definition iof RGT's.
A tree with no infinite path away from its root is called a
\hyperdef{def}{fptree}{\emph{finite-path}} trees.

\begin{lemma}\label{fprgt}
Every RGT is a finite-path tree.
\end{lemma}

\begin{proof}
The proof is by structural induction on the definition of RGT, with
hypothesis $P(G)$ being that $G$ is a finite path tree.

\textbf{Base case} ($G$ is a one node tree).  There is only an ``empty''
path of length zero in $G$, so $G$ is trivially finite-path.

\textbf{Inductive step} ($G$ has root $\mathbf{n}$ with edges to the roots
of a set, $\mathcal{G}$, of RGT's).  By structural induction hypothesis, we
may assume that every $G' \in \mathcal{G}$ is finite-path.

Now suppose to the contrary that there was an infinite path from the root
of $G$.  By definition of $G$, any such path begins with an edge from the
root of $G$ to the root of some tree $G' \in \mathcal{G}$ and continues
from the root of $G'$.  But this continuation is an infinite path in $G'$,
contradicting the fact that $G'$ is finite-path.  So there cannot be an
infinite path away from the root of $G$, which proves $P(G)$.

\end{proof}


This proof by structural induction was really easy, but may seem a little
odd, since we are not used to using induction to prove things about
infinite objects.  In fact, this proof really is different in character
from all the previous structural induction proofs.

Namely, all the other proofs could be reformulated as ordinary induction on
the number of rule applications used in constructing an element of the
recursive data type.  But because an RGT can be built in one step from an
infinite set of subtrees---which in total already take an infinite number
of rule applications---the number of rule applications to construct a
single RGT may not be finite.  So ordinary induction on the number of rule
applications to construct a recursively defined object won't
work.\footnote{As a matter of fact, Mathematical Logicians have proved that
this kind structural induction on infinite data objects is actually
\emph{strictly more powerful} than ordinary induction.}  But nevertheless,
structural induction is a completely sound proof method, even for data
types like RGT's that build up elements in an infinite number of steps.

We remark that, conversely, every finite path tree is an RGT (if we label
its leaves)---a fact we'll prove next week.


\subsection{The Fundamental Theorem for Games}

It is remarkable that there is a winning strategy for every two-person
terminating game of perfect information.

\begin{theorem}\label{fund}
\textbf{Fundamental Theorem}: In every two-person terminating game of
perfect information, there is a winning strategy for one of the players
\end{theorem}

Notice that although Theorem~\ref{fund} guarantees a winning strategy, it
gives no clue which player may have it.  For chess, the Gale Game, and many
other familiar games, no one knows which player has a winning strategy.
\begin{proof}
The proof is by structural induction on the definition of the RGT for the
game.  The induction hypothesis, $P(G)$ is that there is a winning strategy
for the game defined by $G$.

\textbf{Base case} ($G$ is a one node tree).  If the root of $G$ is
labelled \texttt{win}, then the first player has a winning strategy: don't
move.  If the root of $G$ is labelled \texttt{lose}, then the second player
has the same winning strategy.

\textbf{Inductive step} ($G$ has root $\mathbf{n}$ with edges to the roots
of a set, $\mathcal{G}$, of RGT's).  By structural induction hypothesis, we
may assume that for each $G' \in \mathcal{G}$, one player or the other has
a winning strategy.  We now consider two cases.

\emph{Case 1:} There is a tree, $G' \in \mathcal{G}$, with a winning
strategy for the second player.  Then there is a winning strategy for the
first player in game $G$: move first to the root of $G'$ and then follow
the winning strategy for the second player in the game defined by $G'$.

\emph{Case 2:} No tree in $\mathcal{G}$ has a winning strategy for the
second player.  Since by induction there is a winning strategy for each
tree in $\mathcal{G}$, it follows that there must be a winning strategy for
the first player in each of the games defined by trees in $\mathcal{G}$.
Then there is a winning strategy for the second player in game $G$: suppose
the first player's initial move leads to the root of some $G'\in
\mathcal{G}$.  Then follow the winning strategy for the first player in the
game defined by $G'$.

So in either case, one of the players has a winning strategy for $G$, that
is, $P(G)$ holds.

\end{proof}

\iffalse

\subsubsection{A String Theorem}

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

\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) \eqdef$
\begin{eqnarray*}
\ms{num}(01,s) & \leq & \ms{num}(10,s) + 1, \text{ and}\\
\leftenq{\text{If $s$ ends in $0$ then}}\\
\ms{num}(01,s) & \leq  &\ms{num}(10,s).
\end{eqnarray*} 
 
This means that, for each inductive step have two things to show.

\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) \implies 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) \implies 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{proof}
  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{proof}
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.
\fi


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

\subsection{Some Recursively Defined Functions}
Recursive definitions provide a natural way to define functions whose
domains are recursively-defined data types.

\begin{example} (Binary Trees)

Define the function $\ms{numnodes}(T)$ (a recursive definition of
$\card{V_T}$ for a $\RBT$ as follows:
\begin{enumerate}
\item  $\ms{numnodes}(\mbox{single node}) \eqdef 1$,
\item  $\ms{numnodes}(\ms{makeleft}(S)) \eqdef \ms{numnodes}(S) + 1$,
\item   $\ms{numnodes}(\ms{makeright}(S)) \eqdef \ms{numnodes}(S) + 1$,
\item   $\ms{numnodes}(\ms{makeboth}(T_1,T_2)) \eqdef \ms{numnodes}(T_1)
  +\ms{numnodes}(T_2) + 1$.
\end{enumerate}

Similarly,  define $\ms{numedges}(T)$: 
\begin{enumerate}
\item   $\ms{numedges}(\mbox{single node}) \eqdef 0$,
\item   $\ms{numedges}(\ms{makeleft}(S)) \eqdef \ms{numedges}(S) + 1$,
\item   $\ms{numedges}(\ms{makeright}(S)) \eqdef \ms{numedges}(S) + 1$,
\item $\ms{numedges}(\ms{makeboth}(T_1,T_2)) \eqdef \ms{numedges}(T_1) +
\ms{numedges}(T_2) + 2$.
\end{enumerate}
\end{example}


\begin{example}(Arithmetic Expressions)
Given a value, $n$, for the variable, $x$, we can easily calculate
the numerical value of any expression, $e$, in the set, $F$, of Fully
Bracketed Arithmetic Expressions in $x$.  The function,
$\ms{eval}(e,n)$, giving the value of expression $e$ when $x$ has
value $n$ has a simple recursive definition based on the definition of the
recursive data type $F$.  Namely, define
\begin{enumerate}
\item  $\ms{eval}(\xara{0}, n) \eqdef 0$,
\item  $\ms{eval}(\xara{1}, n) \eqdef 1$,
\item  $\ms{eval}(\xara{x}, n) \eqdef n$,
\item  $\ms{eval}(\xara{[}e \xara{+} e'\xara{]}, n) \eqdef \ms{eval}(e,n)
+ \ms{eval}(e',n)$,
\item  $\ms{eval}(\xara{[}e \xara{*} e'\xara{]},n) \eqdef
\ms{eval}(e,n) \cdot \ms{eval}(e', n)$,
\item  $\ms{eval}(\xara{[}\xara{-} e\xara{]},n) = -\ms{eval}(e,n)$.
\end{enumerate}

Another useful operation on arithmetic expressions is substituting one
into another.  Let $\ms{subst}(e,f)$ be the result of substituting
expression $f$ for all occurrences of \xara{x} in $e$.  The function
$\ms{subst}$ also has a simple definition based on the
definition of the recursive data type $F$.  Namely, define
$\ms{subst}(e,f)$ recursively in $e$ as follows:
\begin{enumerate}
\item  $\ms{subst}(\xara{0}, f) \eqdef 0$,
\item  $\ms{subst}(\xara{1}, f) \eqdef 1$,
\item  $\ms{subst}(\xara{x}, f) \eqdef f$,
\item  $\ms{subst}(\xara{[}e \xara{+} e'\xara{]}, f) \eqdef
\xara{[} \ms{subst}(e,f) \xara{+} \ms{subst}(e',f) \xara{]}$,
\item  $\ms{subst}(\xara{[}e \xara{*} e'\xara{]}, f) \eqdef
\xara{[} \ms{subst}(e,f) \xara{*} \ms{subst}(e',f) \xara{]}$,
\item  $\ms{subst}(\xara{[}\xara{-} e\xara{]},f) = 
\xara{[}\xara{-} \ms{subst}(e,f) \xara{]}$.
\end{enumerate}

\end{example}

\subsection{Recursive Function Definitions}

In general, we can define a function, $f$, on a recursively defined data
type by defining $f$ on each of the elements in the base cases of the
definition.  Then define $f(d)$ in terms of $f(d_1), f(d_2), \dots$ where
$d$ is an element built from elements $d_1,d_2,\dots$ by a combination
rule.  One warning though: $f$ is only guaranteed to be well-defined if
each element, $d$, can be constructed in \emph{only one way}: only by a
unique combination rule applied to unique elements $d_1,d_2,\dots$.  So
this kind of recursive definition will work fine for Fully Bracketed
Arithmetic Expressions, binary trees, lists, and recursive trees, but
might \emph{not} yield a well-defined function if the definition of $f$
was based on the recursive definition we gave for the set, $S$, of strings
with an equal number of \texttt{a}'s and \texttt{b}'s.  The reason is that
some strings in $S$ can be constructed in more than one way.

\begin{problem}
\begin{problemparts}
\ppart What is the smallest string in $S$ which can be constructed in two
different ways using the definition of $S$ in Example~\ref{SLex}?

\ppart Find a recursive definition of $S$ similar to the one above,
but under which every string in $S$ is constructed in exactly one way.
\end{problemparts}
\end{problem}

\subsection{Proving Properties of Recursive Functions}

When we have a recursive definition of a function on a recursive data
type, we can use structural induction to prove properties of the function.
We already did this in proving Theorem~\ref{binary-edges-nodes} relating
the number of edges and nodes in a binary tree.  A more interesting
example using structural induction on the definition of Fully Bracketed
Arithmetic Expressions to prove a fundamental relationship between
numerical and symbolic calculation.

Namely, suppose we have an arithmetic expression $e$ with variable $x$ and
we substitute another expression, $f$, for all the $x$ in $e$ to obtain a
new expression, $e' \eqdef \ms{subst}(e,f)$.  Now suppose we want to
evaluate $e'$ when $x$ has the value $n$.  One way to do it would simply
be to evaluate $e'$ recursively, ignoring the way that $e'$ was obtained
from $e$ and $f$.  But another, usually more efficient, approach would be
to find the value of $f$ when $x$ has the value $n$, and then evaluate $e$
when $x$ is given the value obtained from $f$.  In Lisp programming
terminology, the first approach corresponds to evaluation using a
``substitution model,'' and the second approach corresponds to evaluation
using an ``environment model.''  We will prove that both models yield the
same answer.  More precisely, what we want to prove is

\begin{theorem}\label{environments}
For all expressions $e,f \in F$ and $n \in \integers$,
\begin{equation}\label{eval-subst}
\ms{eval}(\ms{subst}(e,f),n) = \ms{eval}(e, \ms{eval}(f,n)).
\end{equation}
\end{theorem}

\begin{proof}
The proof is by structural induction on $e$.

\textbf{Base cases} ($e = \xara{0}$, $e= \xara{1}$).  Then the
lefthand side of equation~(\ref{eval-subst}) equals $e$ by the base cases
of the definition of $\ms{subst}$, and the righthand side equals $e$ by the
base cases of the definition of $\ms{eval}$.

\textbf{Base case} ($e = \xara{x}$).  Then the lefthand side of
equation~(\ref{eval-subst}) equals $\ms{eval}(f,n)$ by the base case for
\xara{x} of the definition of $\ms{subst}$, and the righthand side
equals $\ms{eval}(f,n)$ by the base case for \xara{x} of the definition
of $\ms{eval}$.

\textbf{Inductive step} ($\xara{[}e \xara{+} e'\xara{]}$).
Assume that for all $f \in F$ and $n \in \naturals$,
\begin{eqnarray}
\ms{eval}(\ms{subst}(e,f),n) & = & \ms{eval}(e, \ms{eval}(f,n))\label{Pe}\\
\ms{eval}(\ms{subst}(e',f),n) & = & \ms{eval}(e', \ms{eval}(f,n)),\label{Pep}
\end{eqnarray}
to prove that
for all $f \in F$ and $n \in \naturals$,
\begin{equation}\label{s+}
\ms{eval}(\ms{subst}(\xara{[}e \xara{+} e'\xara{]},f),n)  = 
   \ms{eval}(\xara{[}e \xara{+} e'\xara{]}, \ms{eval}(f,n))
\end{equation}

But the lefthand side of~(\ref{s+}) equals
\[
\ms{eval}(\xara{[} \ms{subst}(e,f) \xara{+} \ms{subst}(e',f) \xara{]},n)
\]
by definition of $\ms{subst}$ for a sum expression, which equals
\[
\ms{eval}(\ms{subst}(e,f),n) + \ms{eval}(\ms{subst}(e',f),n)
\]
by definition of $\ms{eval}$ for a sum expression.  By induction
hypothesis, this equals
\[
\ms{eval}(e,\ms{eval}(f,n)) + \ms{eval}(e',\ms{eval}(f,n)),
\]
which equals the righthand side of~(\ref{s+}) by definition of $\ms{eval}$
for a sum expression.  This proves~(\ref{s+}) in this case.

\textbf{Inductive step} ($\xara{[}e \xara{*} e'\xara{]}$).  Similar.

\textbf{Inductive step} ($\xara{[-}e\xara{]}$).  Similar.
\end{proof}


\subsection{Recursive Functions on Natural Numbers}

The recursive definitions of functions on recursively defined data types
also applies to recursively defined functions on the natural numbers.  One
can think of the natural numbers, $\naturals$, as recursively defined by
\begin{enumerate}
\item $0 \in \naturals$,
\item if $n\in\naturals$, then $n+1 \in \naturals$.
\end{enumerate}
Now ordinary induction is exactly structural induction based on this
recursive definition.  Treating the natural numbers as a recursively
defined data type also justifies the use of familiar recursive definitions
of functions on the natural numbers.
\begin{description}

\item[The Factorial function:] A very useful function for counting and
probability.
\begin{itemize}
\item $0!\eqdef 1$
\item $(n+1)! \eqdef (n+1)n!$ for $n \ge 0$.
\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 &\eqdef 0,\\ 
F_1 &\eqdef 1,\\ 
F_i &\eqdef F_{i-1} + F_{i-2} \mbox{ for $i \geq 2$.} 
\end{align*}
Note there are two base cases, since each combination relies on previous two
values.

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

\item[ $\Sigma$ notation (the traditional style):] We've been using
  this notation informally already.
  \begin{itemize}
  \item $\Sigma_{i=1}^0 f(i) \eqdef 0$, \\
  \item $\Sigma_{i=1}^{n+1} f(i) \eqdef \Sigma_{i=1}^n f(i) + f(n+1)$, for $n\geq 0$. 
  \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) \eqdef 1$,
  \item
    $g(0) \eqdef 1$,
  \item
    $f(n+1) \eqdef f(n) + g(n)$, for $n \geq 0$,
  \item
    $g(n+1) \eqdef f(n) \times g(n)$, for $n \geq 0$.
  \end{itemize}
\end{description}

We can use the recursive definitions of functions in proving their
properties.

\begin{optional}

As an illustration, we'll prove a cute identity involving Fibonacci
numbers.  Fibonacci numbers provide lots of fun for mathematicians because
they satisfy many such identities.
\begin{proposition}
  $\forall n \geq 0 (\Sigma_{i=0}^n F_i^2 = F_n F_{n+1})$.
\end{proposition}

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}.
\]

\textbf{Base case} ($n=0$). 
$\Sigma_{i=0}^0 F_i^2 \eqdef (F_0)^2 = 0 = F_0 F_1$ because
$F_0 \eqdef 0$.

\textbf{Inductive step} ($n\geq 0$).  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}$.

\end{optional}

\section{Ill-formed Definitions}

We must take care that functions defined recursively are
\hyperdef{ill}{formed}{well-defined}.  Below are some function
specifications that look a little like good definitions of functions on the
natural numbers, but they aren't.

\begin{eqnarray}\label{f1}
f_1(n)\eqdef2+f_1(n-1).
\end{eqnarray}
This ``definition'' has no base case.  If some function, $f_1$,
satisfied~(\ref{f1}), so would a function obtained by adding a constant,
$k$, to the value of $f_1$.  So ``definition''~(\ref{f1}) does not
uniquely define $f_1$.

\begin{eqnarray}\label{f2}
f_2(n) \eqdef \begin{cases}
0, &  \text{if $n$ is divisible by 2,}\\
1, &  \text{if $n$ is divisible by 3,}\\
2, & \text{otherwise.}
\end{cases}
\end{eqnarray}
This ``definition'' is inconsistent: it requires $f_2(6) = 0$ and $f_2(6)
=1$, so~(\ref{f2}) doesn't define anything.

\begin{eqnarray}\label{f3}
f_3(n) \eqdef
\begin{cases}
 0, & \text{if $n=0$,}\\
 f_3(n+1)+1, & \text{otherwise.}
\end{cases}
\end{eqnarray}
From ``definition''~(\ref{f3}), it follows that $f_3(1) > f_3(2) > f_3(3)
\cdots >$, so $f_3(1)$ cannot equal any integer.  No total function on the
natural numbers can satisfy this definition.  However, it does uniquely
determine a \emph{partial} function on the natural numbers, namely,
$f_3(0) = 0$ and $f_3$ is undefined everywhere else.

\begin{eqnarray}\label{f4}
f_4(n) \eqdef
\begin{cases}
 0, & \text{if $n=0$},\\
 f_4(n+1) &  \text{otherwise}.
\end{cases}
\end{eqnarray}
Lots of total functions satisfy ``definition''~(\ref{f4}).  Namely, any
function that is 0 at 0 and constant eveywhere else.

A mystery: Mathematicians have been wondering about this one for a while:
\begin{eqnarray}\label{f5}
f_5(n) \eqdef\begin{cases}
 1, & \text{if $n\le 1$},\\
 f_5(n/2) &  \text{if $n>1$ is even},\\
 f_5(3n+1)& \text{if $n>1$ is odd}.
\end{cases}
\end{eqnarray}
For example,
\[
f_5(3)=f_5(10)=f_5(5)=f_5(16)=f_5(8)=f_5(4)=f_5(2)=f_5(1)=1.
\]
This ``definition'' of $f_5$ in some cases defines $f(n)$ in terms of $f$
applied to arguments larger than $n$, and so cannot be justified by
induction on $\naturals$.  It has been proven that if $f_5$ satisfies the
above equations, then $f_5(n)= 1$ for all $n$ up to at least a billion.
It's a good guess that the only $f_5$ that works is the constant function
equal to 1.  But nobody knows if there is a function $f_5$
satisfying~(\ref{f5}) other than the constant function 1.


\section{Induction in Computer Science}

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

Structural induction on recursive definitions lets us go beyond simple
natural number counting.  We can explain how to define recursive functions
on recursive data types.  And we can prove properties of recursively
defined data and functions by structural induction on the definition of
the data type.  We even noted that Structural Induction is technically
more powerful than ordinary induction.  It is a technique which every
Computer Scientist should firmly grasp.

\end{document}



