\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}
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$.
\begin{definition}
\[
L \eqdef \set{x \in \set{\texttt{a},\texttt{b}}^* \suchthat
\#\text{\texttt{a}'s in } x = \#\text{\texttt{b}'s in } x}.
\]
\end{definition}
\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{axb}.  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, $T =
(V_T, E_T)$, with a necessarily unique ``root'' vertex $\rt(T)$, such that
every vertex is reachable by a directed path from the root.  Finite-Path
Trees from
\hyperref{http://theory.lcs.mit.edu/classes/6.042/fall02/handouts/lectures/ln5.pdf}
{def}{fptree}{Week 5 Notes}, for example, are the class of rooted trees
which do not have any infinite directed path from the root.

Another important class of 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}.

\begin{example}
We will define a special class of ordered binary trees called the \emph{recursive
ordered binary trees}, $\RBT$:

\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,
\end{enumerate}

\[
\ms{makeboth}(T_1,T_2) \eqdef (V_1 \union V_2 \union \set{\mathbf{n}}, E_1
\union E_2 \union \set{(\mathbf{n},\rt(T_1),\texttt{left}),
(\mathbf{n},\rt(T_2),\texttt{right})}) \in \RBT.
\]

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}

Note that $\RBT$ is precisely the set of \emph{finite} ordered binary
trees.  Properly speaking, we should prove this.  Namely, we should prove
that every $\RBT$ is finite,
\iffalse ---easily proved by structural induction on the definition of $\RBT$\fi
%
and prove that every finite ordered binary tree is an $\RBT$.
%
\iffalse ---easily proved by induction on the size of finite trees.\fi
We'll hold off on this, but will do a more interesting proof of this kind
for infinite trees in Theorem~\ref{rfp} below.

We can generalize $\RBT$'s to the class of \emph{Countable Ordered Trees},
$\CT$, in which each vertex may have any finite number, $n \ge 0$, of
edges consecutively labelled $1,2,\dots,n$ leaving it, or may even have an
infinite set of edges consecutively labelled with all the positive
integers.

\begin{example}
We recursively define the set, $\RCT$, of \emph{Recursive Countable Trees}
as follows:

\begin{enumerate}

\item
If $G$ is a graph with one vertex and no edges, then $G$ is a $\RCT$.

\item 
If $T_1=(V_1,E_1), T_2=(V_2,E_2), \dots$ is a finite or infinite sequence
of $\RCT$'s, such that $V_i$ and $V_j$ are disjoint for all $i \neq j$,
and $\mathbf{n}$ is a ``new'' node not in $\lgunion_1^\infty V_i$, then the
graph, $\mktree(T_1,T_2,\dots)$, made by adding an edge labelled
\texttt{i} from $\mathbf{n}$ to $\rt(T_i)$ for all $i > 0$ is a $\RCT$.
That is,
\[
\mktree(T_1,T_2,\dots) \eqdef (\lgunion_1^\infty V_i \union
\set{\mathbf{n}}, \lgunion_1^\infty E_i \union
\set{(\mathbf{n},\rt(T_i),i) \suchthat i \in \integers^{+}}) \in \RCT.
\]

\end{enumerate}

\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

\end{example}


\iffalse
So far we have constructed data types of expressions and trees using
concrete representations such as strings or graphs.  But what really
matters to us about these data types is \emph{how} they structured, rather
than \emph{what} they were made of.  This idea leads us to introduce
\emph{abstract}data types.

Abstract data types are defined in terms of \emph{constructor} and
\emph{selector} functions.  We'll illustrate this by defining
\emph{abstract lists}.  To do this, we need a constructor function,
$\mklist$, and two selector functions, $\fstlist$ and $\rstlist$.  We also
need a constant $\nillist$ -- which is also considered to be a constructor.
The idea is that $\mklist(a,\ell)$ makes a new list with $a$ as its first
element, and $\ell$ as the rest of the list.  In Lisp-like programming
languages, the $\mklist$ operation is called \texttt{cons}, $\fstlist$ is
\texttt{car}, and $\rstlist$ is \texttt{cdr}.

Lists are simply elements in the range of the constructors, but we don't
need to know what these elements actually are.  We only require that the
$\mklist$ constructor and its selectors satisfy the properties:
\begin{eqnarray}
\fstlist(\mklist(a,\ell)) & = & a,\\
\rstlist(\mklist(a,\ell)) & = & \ell.
\end{eqnarray}
We also require that $\nillist$ is a member of the domain of $\mklist$, and
that there is a predicate $\nillistq$ defined on the domain of $mklist$ such
that
\[
\nillistq(d) = \texttt{true} \quad \emph{iff} \quad d = \nillist.
\]
Finally, if we want to include in lists some non-list elements, called
\emph{atoms}, from some set, $A$, we also require that $A$ be a subset of
the domain of $\mklist$.  Now we're ready to define abstract lists:
\fi

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

\iffalse

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}

Structural induction is a correct and useful proof method on recursive
data types even when they are infinite.  For example, using structural
induction on the definition of $\RCT$'s, we can easily prove that every
$\RCT$ is a Finite-path Countable Ordered Tree.

\iffalse
But there is one technical point to notice before we prove this.  Namely,
Finite-path Trees were actually defined to be graphs.  But Countable Trees
were defined abstractly, so they may not be graphs at all.  To be
accurate, we should say that the \emph{graph} of an Abstract Countable
Tree is a Finite-path Tree\footnote{To be thorough, we should recursively
define a function \emph{graph} mapping countable trees to their
representations as graphical trees.  This is straightforward to do, as any
concerned reader can easily confirm.}\fi


\begin{theorem}\label{rfp}
Every $\RCT$ is a
\hyperref{http://theory.lcs.mit.edu/classes/6.042/fall02/handouts/lectures/ln5.pdf}
{def}{fptree}{Finite-Path \CT}.
\end{theorem}

\begin{proof}
Define
\[
P(T) \eqdef \text{$T$ is a Finite-path \CT}.
\]
We prove that $P(T)$ holds for all $T \in \RCT$ by Structural Induction
on the definition of $\RCT$.

\textbf{Base case} ($T$ has one vertex) $T$ is a $\CT$ by definition of
$\CT$.  There is only an ``empty'' of length zero in $T$.  So $T$ is also
Finite-path.

\textbf{Inductive step} ($T = \mktree(T_1,T_2,\dots)$).  By structural
induction hypothesis, we may assume that $P(T_i)$ holds for all $T_i$.

By definition of $T$, the edges from the root of $T$ are labelled with
consecutive integers.  Any other vertex of $T$ is a vertex in $V_i$ which
is labelled with consecutive integers because $T_i \in \CT$ by hypothesis.
Hence $T \in \CT$.

Also by definition of $T$, the second node on any path from the root of
$T$ must be the root some $T_i$.  The rest of the path is a directed path
from the root of $T_i$, and so is finite because $T_i$ is Finite-path by
induction hypothesis.  So the whole path from the root of $T$ is also
finite.

\end{proof}

This proof by Structural Induction may seem obvious, but it is actually
different in character from all the other 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 a Recursive Countable Tree can be built
by combining an infinite sequence of subtrees, which in total already take
an infinite number of rule applications, the number of rule applications
to construct a single $\RCT$ may not be finite.  So ordinary induction on
the number of rule applications to construct a recursively defined object
won't work.  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 correct proof method, even for data
types like $\RCT$ that build up elements in an infinite number of steps.

\begin{problem} Prove the converse of Theorem~\ref{rfp}:

\begin{theorem}
Every Finite-path $\CT$ is a $RCT$.
\end{theorem}

\hint Suppose not, and consider a minimal Finite-path $\CT$ (under the
well-founded ``strict-subtree'' partial order on Finite-path trees defined
in Week 5 Notes) that is not in $\RCT$.
\end{problem}

\iffalse
Maybe discuss recursive functions on recursive trees, \eg a recursively
defined Winning Strategy for game trees, or a recursively defined value
for games trees (where leaves are labelled with $\reals^{+}$; may need to
restrict to countable trees to have strategies arbitraril close to the
value).
\fi



\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 Definition~\ref{SL} of $S$ above?

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

\section{Ill-formed Definitions}

We must take care that functions defined recursively are well-defined.
Below are some function specifications that look like definitions but
aren't.

\begin{description}
\item[$f(n)=2+f(n-1)$.]
This ``definition'' has no base case.  If some function, $f$, satisfied this
equatioin, so would a function obtained by adding a constant, $k$, to the
value of $f$.  So this ``definition'' does not uniquely define $f$.

\item[\rm\em $f(n) = 0$ if $n$ is divisible by 2, $f(n) = 1$ if $n$ is
divisible by 3, and $f(n) = 2$ otherwise.]
%if $n$ is not divisible by 2 or 3.]
This ``definition'' is inconsistent: it requires $f(6) = 0$ and $f(6) 
=1$, so it doesn't define anything.

\item[\rm\em $f(0) = 0$, otherwise $f(n) = f(n+1)+1$.]  From this
``definition,'' it follows that $f(1) > f(2) > f(3) \linebreak[2] >
\dots$, so $f(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, the function that
is 0 at 0 and undefined everywhere else.

\item[\rm\em $f(0) = 0$, otherwise $f(n) = f(n+1)$.]  Lots of total
functions satisfy the equations in the ``definition.''  Namely, any
function that is 0 at 0 and constant eveywhere else.

\item[\rm\em 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}
This ``definition'' of $f$ 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$ is a function
that satisfies the above equations, then $f(n)= 1$ for all $n$ up to at
least a billion, and it's a good guess that the only $f$ that works is the
constant function equal to 1.  But nobody knows if there is more than one
function satisfying these equations.
\end{description}


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



