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

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

%\newcommand{\xara}[1]{\texttt{\textbf{#1}}}
%for color: 
\newcommand{\xara}[1]{\texttt{\textbf{\color{blue}{#1}}}}

\newlength{\prooflength}
\newlength{\reasonlength}
\def\bparts{\begin{problemparts}}
\def\eparts{\end{problemparts}}
\def\ppart{\problempart}

\providecommand{\boys}{\text{the-Boys}}
\providecommand{\girls}{\text{the-Girls}}
\providecommand{\qst}{\text{$q_0$}}
\providecommand{\none}{\texttt{none}}
\providecommand{\girln}{\text{$\girls \union \set{\none}$}}
\providecommand{\boyn}{\text{$\boys \union \set{\none}$}}
\providecommand{\sere}{\text{\emph{serenading}}}
\providecommand{\suit}{\text{\emph{suitors}}}
\providecommand{\fav}{\text{\emph{favorite}}}
\providecommand{\nex}{\text{\emph{next}}}
\providecommand{\size}{\text{\emph{size}}}

\begin{document}
\lecturenotes{5}{Recursive Definitions and State Machines}

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

\begin{example}
Another important example is a \emph{binary tree}.

The set, $T$, of \emph{rooted binary trees} is defined recursively as
follows:
\begin{enumerate}
\item
A single node, $r$, is in $T$.
\item 
If $t$ is in $T$, then $\ms{makeleft}(t)$ is in $T$,\label{ml}
\item
if $t$ is in $T$, then $\ms{makeright}(t)$ is in $T$,\label{mr}
\item
if $t$ and $t'$ are in $T$, then $\ms{makeboth}(t,t')$ is in $T$.
\end{enumerate}

In this definition, $\ms{makeleft}(t)$ returns the structure formed from
$t$, a single new node $n$, and an arrow labeled ``left'' from $n$ to
$t$. %as in Figure~ref{fig:makeleft}

Similarly, $\ms{makeright}(t)$ returns the structure formed from $t$,
a single new node $n$, and an arrow labeled ``right'' from $n$ to $t$.
%as in Figure~ref{fig:makeright}

Finally, $\ms{makeboth}(t,t')$ returns the structure formed from $t$,
$t'$, and a single new node $n$, with an arrow labeled ``left'' from $n$
to $t$ and another arrow labeled ``right'' from $n$ to $t'$.
%as in Figure~ref{fig:makeboth}

A {\em full binary tree} is a tree in which every node is either a single
node or has both a left and right subtree.
%as in Figure~ref{fig:fillbin}
In other words rules~\ref{ml}. and~\ref{mr}. are removed from the
definition given above.

\end{example}

\begin{example}
The set, $L(A)$, of \emph{lists} over atom set $A$ satisfies:
\begin{enumerate}
\item \texttt{()}, the \emph{empty list}, is in $L(A)$,
\item if $\ell \in L(A)$ and $a \in A$, then $\ms{makelist}(a,l)$ is in $L(A)$,
\item if $\ell_1$ and $\ell_2$ are in $L(A)$, then 
$\ms{makelist}(\ell_1, \ell_2)$ is in $L(A)$.
\end{enumerate}

Conceptually, $\ms{makelist}(a,l)$ makes a new list with $a$ as its first
element, and $l$ as the rest of the list.  In Lisp-like programming
languages, the $\ms{makelist}$ operation is called \texttt{cons}.
\end{example}

\begin{example}
Define the set, $R(A)$, of \emph{Rooted Trees with leaf-set $A$}
as follows:
\begin{enumerate}
\item\label{tuple} If $n \geq 0$ and $t = \langle t_1,t_2,\dots,t_n
\rangle$ is an $n$-tuple of elements $t_i \in A \union R(A)$ for $1 \leq i
\leq n$, then $t \in R(A)$.
\end{enumerate}

Did we forget the ``base case'' for starting off this set of trees?  No,
we didn't.  If we apply rule~\ref{tuple}. with $n=0$, we can conclude that
the 0-tuple, $\langle\rangle$, is in $R(A)$, and once we have that, we're
off and running.

Formally, the tree $t = \langle t_1,t_2,\dots,t_n \rangle$ is just a tuple,
but we would represent it by a graphical tree consisting of a \emph{root
node} with an edge to root nodes of each of the $n$ trees
$t_1,t_2,\dots,t_n$.
%as in Figure~\ref{rooted-tree}
\end{example}

\begin{example}
As a final example we recursively define the set, $T(A)$, of
\emph{Finite-path Trees with leaf-set $A$} as follows:
\begin{enumerate}
\item If $t = \langle t_1,t_2,\dots \rangle$ is a sequence (possibly
empty, possibly infinite) of elements in $t_i A\cup T(A)$, then $t\in
T(A)$.
\end{enumerate}

So Rooted Trees are simply the Finite-path Trees that have only finitely
many nodes.
\end{example}


\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)$: 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 an equal number of left brackets.

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

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

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

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

\begin{proof}

Define $P(t)$: Binary tree $t$ has exactly $1$ fewer edges than nodes.  We
use the notation $\ms{nodes}(t)$ for the nodes in $t$, and
$\abs{\ms{nodes}(t)}$ for the number of nodes; likewise for
$\ms{edges}(t)$.  The key is that the inductive steps all preserve the
``deficit'' of 1.

For instance, combining two trees involves adding two edges and one node;
since each subtree had a ``deficit'' of 1, this maintains the deficit of~1.

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

\textbf{Inductive step} ($\ms{makeleft}(t)$).  
Assume $P(t)$ to prove $P(\ms{makeleft}(t))$.  That is, assuming
\begin{equation}\label{t1n}
|\ms{edges}(t)|+1 = |\ms{nodes}(t)|,
\end{equation}
show that
\begin{equation}\label{mlf}
|\ms{edges}(\ms{makeleft}(t))|+1 = |\ms{nodes}(\ms{makeleft}(t))|.
\end{equation}
But
\begin{equation}\label{e+1}
|\ms{edges}(\ms{makeleft}(t))| = |\ms{edges}(t)| + 1,
\end{equation}
since $\ms{makeleft}$ adds one edge.  Combining~(\ref{e+1}) with the
hypothesis~(\ref{t1n}) yields
\begin{equation}
|\ms{edges}(\ms{makeleft}(t))| = |\ms{nodes}(t)|.
\end{equation}
and adding ones to both sides of this equation gives
\begin{equation}\label{elt}
|\ms{edges}(\ms{makeleft}(t))| +1 = |\ms{nodes}(t)|+1.
\end{equation}
But
\begin{equation}\label{n+1}
|\ms{nodes}(\ms{makeleft}(t))| = |\ms{nodes}(t)| + 1,
\end{equation}
since $\ms{makeleft}$ adds one node, and combining~(\ref{n+1})
and~(\ref{elt}) immediately implies~(\ref{mlf}).

\textbf{Inductive step} ($\ms{makeleft}(t)$). 
Assume $P(t)$ to prove $P(\ms{makeright}(t))$.  Same as previous case
with $\ms{makeright}$ replacing $\ms{makeleft}$.

\textbf{Inductive step}  ($\ms{makeboth}(t,t')$).
Assume $P(t) \wedge P(t')$ to prove
$P(\ms{makeboth}(t,t'))$.    That is,  assuming
\begin{eqnarray}
|\ms{edges}(t)|+1 & = &|\ms{nodes}(t)|\\
|\ms{edges}(t')|+1 & = & |\ms{nodes}(t')|,
\end{eqnarray}
prove
\begin{equation}\label{mtt}
|\ms{edges}(\ms{makeboth}(t,t'))|+1 = |\ms{nodes}(\ms{makeboth}(t,t'))|.
\end{equation}
The similar proof is left to the reader.
\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}

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 formal definition of what
we previously used intuitively to be the number of nodes in the tree
$t$), by: 
\begin{enumerate}
\item  $\ms{numnodes}(\mbox{single node}) \eqdef 1$,
\item  $\ms{numnodes}(\ms{makeleft}(t)) \eqdef \ms{numnodes}(t) + 1$,
\item   $\ms{numnodes}(\ms{makeright}(t)) \eqdef \ms{numnodes}(t) + 1$,
\item   $\ms{numnodes}(\ms{makeboth}(t,t')) \eqdef \ms{numnodes}(t)
  +\ms{numnodes}(t') + 1$.
\end{enumerate}

Similarly,  define $\ms{numedges}(t)$: 
\begin{enumerate}
\item   $\ms{numedges}(\mbox{single node}) \eqdef 0$,
\item   $\ms{numedges}(\ms{makeleft}(t)) \eqdef \ms{numedges}(t) + 1$,
\item   $\ms{numedges}(\ms{makeright}(t)) \eqdef \ms{numedges}(t) + 1$,
\item   $\ms{numedges}(\ms{makeboth}(t,t')) \eqdef \ms{numedges}(t) +
  \ms{numedges}(t') + 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}

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 finite-path 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$ 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 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 examples that aren't well-defined.

\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 on Finite-path Trees}

Finite-path Trees are named after their crucial property: even though such
trees may by infinite, they do not have any infinite path ``down'' from
the root.  Note that even though a Finite-path Tree has no infinite path
down, it may have paths of all finite lengths, and so it would still be
``infinitely deep.''  For example, it may have a subtree with one node, a
second subtree consisting of a single path of length one, a third subtree
consisting of a path of length two, and so on, as illustrated in
Figure~\ref{fptree}.

\begin{figure}[htbp]
%\centering \includegraphics[height=2in]{figures/fptree}
\begin{center}
\input{figures/fptree.latex}
\end{center}
\caption{A Finite-path Tree with unbounded depth.}\label{fptree}
\end{figure}

We can prove the finite-path property easily by structural induction:

\begin{theorem}
Every path down from the root of a Finite-path Tree is finite.
\end{theorem}

\begin{proof}
Define
\[
P(t) \eqdef \text{every path down from the root of $t$ is finite}.
\]
We prove that $P(t)$ holds for all $t \in T(A)$ by structural induction on
the definition of $T(A)$.  There is a small quibble: the theorem will not
hold if $A$ includes trees with infinite paths.  For simplicity, we'll
assume that $A$ consists solely of a one-node tree.

Remember, the definition of Finite-path Trees did not use a separate
case, so the proof only has an induction step, with ``base'' cases
appearing as subcases of the induction step.

\textbf{Inductive step} ($t \in T(A)$).  Assume that $P(t')$ holds for all
subtrees, $t'$, connected to the root of $t$, to prove $P(t)$.

\textbf{Case 1} ($t$ is the empty tree.)  Then $t$ has no paths at all.

\textbf{Case 2} ($t$ has one node.)  Then $t$ has only an empty path
of length 0.

\textbf{Case 3:} ($t$ has subtrees.)
Any path from the root of $t$ must go to a root of a subtree $t'$.  The
rest of the path must be a path down from the root of $t'$, which is
finite by induction hypothesis.

\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 Finite-path 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 Finite-path Tree may not be finite.  So ordinary
induction on a finite number of rule applications won't be a replacement.
As a matter of fact, Mathematical Logicians have proved that this kind
structural induction is actually \emph{strictly more powerful} than
ordinary induction.  But nevertheless, Structural Induction is a
completely correct proof method, even for data types like Finite-path
Trees that have infinite elements.


\section{Induction and Recursive Algorithms}

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

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

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

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

\section{Modeling Processes}
The second topic for the week will be the application of induction and
other proof techniques to the design and analysis of algorithms and
systems.  We will focus on the problem of proving that some simple
algorithms behave correctly.

\emph{Proving} the correctness of a program is a quite different activity
than debugging and testing a program.  Since programs are typically
intended to handle a huge, if not infinite, number of different inputs,
completely testing a program on all inputs is rarely feasible, and partial
testing always leaves open the possibility that something will go wrong in
the untested cases.  A proof of correctness ensures there are no such
loopholes.  Correctness proofs for hardware and software are playing a
growing role in assuring system quality, especially for systems performing
critical tasks such as flying airplanes, controlling traffic, and handling
financial transactions.

Before we get into the abstract definitions, it will help to look at a
couple of entertaining examples.

\section{Die Hard}

In the movie Die Hard 3, Bruce Willis and Samuel Jackson are coerced by a
homocidal maniac into trying to disarm a bomb on a weight-sensitive
platform near a fountain.  To disarm the bomb, they need to quickly
measure out exactly four gallons of water and place it on the platform.
They have two empty jugs, one that holds three gallons and one that holds
five gallons, and an unlimited supply of water from the fountain.  Their
only options are to fill a jug to the top, empty a jug completely, or pour
water from one jug to the other until one is empty or the other is full.
They do succeed in measuring out the four gallons while carefully obeying
these rules.  You can figure out how (or go see the movie or
\S \ref{do-four} below).

But Bruce is getting burned out on dying hard, and according to rumor, is
contemplating a sequel, Die Once and For All.  In this film, they will
face a more devious maniac who provides them with the same three gallon
jug, but with a \emph{nine} gallon jug instead of the five gallon one.  The
water-pouring rules are the same.  They must quickly measure out exactly
four gallons or the bomb will go off.

This time the task is impossible---whether done quickly or slowly.  We
can prove this without much difficulty.  Namely, we'll prove that it is
impossible, by any sequence of moves, to get exactly four gallons of water
into the large jug.

A sequence of moves is constructed one move at a time.  This suggests a
general approach for proofs about sequential processes: to show that some
condition always holds during the executions of a process, use induction
on the number, $n$, of steps or operations in the executions.  For Die
Hard, we can let $n$ be the number of times water is poured.

All will be well if we can prove that neither jug contains four gallons
after $n$ steps for all $n \geq 0$.  This is already a statement about
$n$, and so it could potentially serve as an induction hypothesis.  Let's
try lunging into a proof with it:

\begin{theorem}\label{dies}
Bruce dies once and for all.
\end{theorem}

Let $P(n)$ be the predicate that neither jug contains four gallons of
water after $n$ steps.  We'll try to prove $\forall n\, P(n)$ using
induction hypothesis $P(n)$.

In the base case, $P(0)$ holds because both jugs are initially empty.  In
the inductive step, we assume that neither jug has four gallons after $n$
steps and try to prove that neither jug has four gallons after $n+1$
steps.

Now we are stuck; the proof cannot be completed.  The fact that neither
jug contains four gallons of water after $n$ steps is not sufficient to
prove that neither jug can contain four gallons after $n+1$ steps.  For
example, after $n$ steps each jug might hold two gallons of water.
Pouring all water in the three-gallon jug into the nine-gallon jug would
produce four gallons on the $n+1$st step.

What to do?  We use the familiar strategy of strengthening the induction
hypothesis.  Some experimentation suggests strengthening $P(n)$ to be the
predicate that after $n$ steps, the number of gallons of water in each jug
\emph{is a multiple of three}.  This is a stronger predicate: if the
number of gallons of water in each jug is a multiple of three, then
neither jug contains four gallons of water.  This strengthened induction
hypothesis does lead to a correct proof of the theorem.

To be precise about this proof, we'll model the situation using a
\emph{state machine}.

\section{State machines}

\subsection{Basic definitions}

Mathematically speaking, a state machine is just a binary relation on
states, where the pairs in the relation correspond to the allowed
steps of the machine.  In addition, a state machine has some states
that are designated as start states---the ones in which it is allowed
to begin executing.

\begin{definition} A \emph{state machine} has three parts:
\begin{enumerate}
\item a nonempty set, $Q$, whose elements are called \emph{states},
\item a nonempty subset $Q_0 \subseteq Q$, called the set of \emph{start states},
\item a binary relation, $\delta$, on $Q$, called the \emph{transition
relation}.
\end{enumerate}
\end{definition}

Another view is that a state machine is really nothing more than a digraph
whose nodes are the states and whose arrows were determined by the
transition relation.  Reflecting this view, we often write $q \rightarrow
q'$ as alternative notation for the assertion that $(q,q') \in \delta$.
The only extra state machine component beyond the digraph is its
designated set of ``start'' nodes.

State machines come up in many areas of Computer Science.  You may have
seen variations of this definition in a digital logic course, a compiler
course, or a theory of computation course.  In these courses, the machines
usually have only a \emph{finite} number of states.  Also, the edges in
the state graphs are usually labelled with input and/or output tokens.  We
won't need inputs or output for the applications we consider.

\subsection{Examples}

Here are some simple examples of state machines.

\begin{example}
A bounded counter, which counts from $0$ to $99$ and overflows at 100.
The state graph is shown in Figure~\ref{fig:counter}.

\begin{figure}[htbp]
\centering \includegraphics[height=1in]{figures/counter}
%\centerline{\psfig{figure=figures/counter.eps,height=1in}}
\caption{\em The state graph of the 99-bounded counter.}
\label{fig:counter}
\end{figure}

Formally, the state machine modeling the 99-counter has:
\begin{itemize}
\item 
$Q \eqdef \set{ 0, 1, 2, \dots, 99, \texttt{overflow}}$,

\item $Q_0 \eqdef \set{ 0 }$,

\item $\delta = \set{ (0,1), (1,2), (2,3), \dots,
(99,\texttt{overflow}),(\texttt{overflow},\texttt{overflow})}$.  
Note the self-loop (transition to itself) for the overflow state.

\end{itemize}

\end{example}

\begin{example}
An unbounded counter is similar, but has an infinite state set, yielding
an infinite digraph.  This is harder to draw \texttt{:-)}
\end{example}

\begin{example}
The Die Hard 3 situation can be formalized as a state machine as well.
\begin{itemize}
\item 
$Q \eqdef \set{ (b,l) \in \reals^2 \suchthat 0 \leq b \leq 5, 0 \leq l
\leq 3 }$.  Note that $b$ and $l$ are arbitrary real numbers, not
necessarily integers.  After all, Bruce could scoop any unmeasured amount
of water into a bucket.

\item $Q_0 = \{ (0,0) \}$ (because both jugs start empty). 

\item $\delta$ has several kinds of transitions: 
\begin{enumerate}

\item  Fill the little jug: $(b,l) \rightarrow (b,3)$ for $l < 3$.

\item  Fill the big jug: $(b,l) \rightarrow (5,l)$ for $b<5$.

\item  Empty the little jug: $(b,l) \rightarrow (b,0)$ for $l>0$.

\item  Empty the big jug: $(b,l) \rightarrow (0,l)$ for $b>0$.

\item  Pour from the little jug into the big jug: for $l>0$,
\begin{equation*}
(b,l) \rightarrow
\begin{cases}
(b+l, 0) & \text{if $b + l \le 5$,}\\
(5, l - (5 - b)) & \text{otherwise.}
\end{cases}
\end{equation*}

\item Pour from big jug into little jug: for $b>0$,
\begin{equation*}
(b,l) \rightarrow
\begin{cases}
(0, b+l) & \text{if $b + l \le 3$,}\\
(b - (3 -l), 3) & \text{otherwise.}
\end{cases}
\end{equation*}
\end{enumerate}
\end{itemize}
\end{example}

Note that in contrast to the 99-counter state machine, there is more than
one possible transition out of states in the Die Hard machine.

\begin{problem}
Which states of the Die Hard 3 machine have direct transitions to
exactly two states?
\end{problem}

A machine is called \emph{deterministic} if its execution behavior is
uniquely determined: there is only one start state and there is at most
one transition out of every state.\footnote{In the case of state machines
with inputs, a machine is deterministic when its execution is uniquely
determined by the inputs it receives, but different inputs may lead to
different executions.}  Otherwise, it is \emph{nondeterministic}.  So the
Die Hard machine is nondeterministic, and the counter machines are
deterministic.  Formally,

\begin{definition}
A state machine $(Q,Q_0,\delta)$ is \emph{deterministic} iff the
transition relation, $\delta$, is the graph of a partial function on $Q$,
and there is exactly one start state.  Otherwise, the machine is
\emph{nondeterministic}.
\end{definition}


\subsection{Executions of state machines}\label{do-four}

The Die Hard 3 machine models every possible way of pouring water among
the jugs according to the rules.  Die Hard properties that we want to
verify can now be expressed and proved using the state machine model.  For
example, Bruce will disarm the bomb if he can \emph{reach} some state of
the form $(4, l)$.

In graph language, a (possibly infinite) path through the state machine
graph beginning at a start state corresponds to a possible system behavior
or process execution.  A state is reachable if there is a path
to it starting from one of the start states.  Formally,
\begin{definition}
An \emph{execution} is a (possibly infinite) sequence $q_0, q_1, \ldots$
such that $q_0 \in Q_0$, and $\forall i \geq 0\, (q_i,q_{i+1}) \in \delta$.
A state is \emph{reachable} if appears in some execution.
\end{definition}

\begin{example}
We said that Bruce and Samuel successfully disarm the bomb in Die Hard 3.
In particular, the state (4,3) is reachable:

\begin{center}
\begin{tabular}{lc}
action & state\\
\hline start & (0,0),\\
fill the big jug & (5,0), \\
pour from big to little & (2,3), \\
empty the little & (2,0), \\
pour from big into little & (0,2), \\
fill the big jug, &(5,2),  \\
pour from big into little & (4,3).
\end{tabular}
\end{center}
\end{example}

\subsection{Die Hard Once and For All}

Now back to Die Once and For All.  The problem is still to measure out
four gallons, but with a nine gallon jug instead of the five gallon one.
The states and transition relation are the same as for the Die Hard 3
machine, with all occurrences of ``5'' replaced by ``9.''

Now reaching any state of the form $(4,l)$ is impossible.  To prove this
carefully, we define $P(n)$ to be the predicate:
\begin{quote}
At the end of any $n$-step execution, the number of gallons in
each jug is an integer multiple of 3 gallons.
\end{quote}
We prove $\forall n\, P(n)$ by induction.

\textbf{Base case} $n=0$: $P(n)$ holds because each jug contains 0 gallons
and $0 = 0 \cdot 3$ is an integer multiple of 3.

\textbf{Induction step}: Assume that $n \ge 0$ and some length $n$
execution ends with $b$ gallons in the big jug and $l$ in the little
jug.  We may assume by induction that $P(n)$ holds, namely, that $b$ and
$l$ are integer multiples of 3.  We must prove $P(n+1)$.  In particular,
all we have to show is that after one more step, the amounts in the jugs
are still integer multiples of 3.

The proof is by cases, according to which transition rule is used in the
next step.  For example, using the ``fill the little jug'' rule for the
$n+1$st transition, we arrive at state $(b,3)$.  We already know that $b$
is an integer multiple of 3, and of course 3 is an integer multiple of 3,
so the new state $(b,3)$ has integer multiples of 3 gallons in each jug,
as required.  Another example is when the transition rule used is ``pour
from big jug into little jug'' for the subcase that $b + l > 3$.  Then the
$n+1$st state is $(b -( 3 -l), 3)$.  But since $b$ and $l$ are integer
multiples of 3, so is $b -( 3 -l)$.  So in this case too, both jugs will
contain an integer multiple of 3 gallons.

We won't bother to crank out the remaining cases, which can all be checked
with equal ease.  This completes the proof of Theorem~\ref{dies}: Bruce
dies once and for all!

\section{Reachability and Invariants}

The induction proof about the Once and For All machine follows a proof
pattern that is often used to analyze state machine behavior.  Namely, we
showed that the integer-multiple-of-3 property held at the start state and
remained \emph{invariant} under state transitions.  So it must hold at all
reachable states.  In particular, since no state of the form $(4, l)$
satisfies the invariant, no such a state can be reachable.

\begin{definition}
An {\em invariant} for a state machine is a predicate, $P$, on states,
such that whenever $P(q)$ is true of a state, $q$, and $q \rightarrow r$
for some state, $r$, then $P(r)$ holds.
\end{definition}

Now we can reformulate the Induction Axiom specially for state machines:
\begin{theorem}[Invariant Theorem]
Let $P$ be an invariant predicate for a state machine.  If $P$ holds for
all start states, then $P$ holds for all reachable states.
\end{theorem}

The truth of the Invariant Theorem is as obvious as the truth of the
Induction Axiom.  We could prove it, of course, by induction on the length
of finite executions, but we won't bother.

\subsection{The Robot}

There is a robot.  He walks around on a grid and at every step he moves
one unit north or south \emph{and} one unit east or west.  (Read the last
sentence again; if you do not have the robot's motion straight, you will
be lost!)  The robot starts at position $(0, 0)$.  Can the robot reach
position $(1, 0)$?

To get some intuition, we can simulate some robot moves.  For example,
starting at (0,0) the robot could move northeast to (1,1), then southeast
to (0,2), then southwest to (-1, 1), then southwest again to (-2, 0).

Let's try to model the problem as a state machine and then prove a
suitable invariant:
\begin{eqnarray*}
Q & \eqdef & \integers \cross \integers,\\
Q_0 & \eqdef & \set{ (0, 0)},\\
\delta & \eqdef & \set{ ((i, j),(i', j'))
\suchthat i' = i \pm 1 \land j' = j \pm 1}.
\end{eqnarray*}

The problem is now to choose an appropriate predicate, $P$, on states and
prove that it is an invariant.  If this predicate is true for the start
state (0,0) and false for $(1, 0)$, then follows that the robot can never
reach $(1, 0)$.  A direct attempt at an invariant is to let $P(q)$ be
the predicate that $q \neq (1, 0)$.

Unfortunately, this is not going to work.  Clearly $P((2,1))$ holds because
$(2,1) \neq (1, 0)$.  And of course $P((1,0))$ does not hold.  But $(2,1)
\rightarrow (1,0)$, so this choice of $P$ will not yield an invariant.

We need a stronger predicate.  Looking at our example execution you might
be able to guess a proper one, namely, that the sum of the coordinates is
even!  If we can prove that this is an invariant, then we have proven that
the robot never reaches $(1, 0)$ because the sum $1+0$ of its coordinates
is not an even number, but the sum $0+0$ of the coordinates of the start
state is an even number.

\begin{theorem}
The sum of the robot's coordinates is always even.
\end{theorem}

\begin{proof}
The proof uses the Invariant Theorem.

Let $P((i, j))$ be the predicate that $i + j$ is even.

First, we must show that the predicate holds for all start states.  But
the only start state is (0,0), and $P((0, 0))$ is true because $0 + 0$ is
even.

Next, we must show that $P$ is an invariant.  That is, we must show that
for each transition $(i, j) \rightarrow (i', j')$, if $i + j$
is even, then $i' + j'$ is even.  But $i' = i \pm 1$ and $j' = j \pm 1$ by
definition of the transitions.  Therefore, $i' + j'$ is equal to $i + j -
2$, $i + j$, or $i + j + 2$, all of which are even.
\end{proof}

\begin{corollary}
The robot cannot reach $(1, 0)$.
\end{corollary}

\begin{problem}
A robot moves on the two-dimensional integer grid.  It starts out at
$(0,0)$, and is allowed to move in any of these four ways:
\begin{enumerate}
\item (+2,-1)   Right 2, down 1
\item (-2,+1)   Left 2, up 1 
\item (+1,+3) 
\item (-1,-3) 
\end{enumerate}

Prove that this robot can never reach (1,1).

\showsolution{
A simple invariant that does the job is defined on states
$(i,j)$ by the predicate: $i + 2j$ is an integer multiple of $7$.
}
\end{problem}

\section{Sequential algorithm examples}

The Invariant Theorem was formulated by Robert Floyd at Carnegie Tech in
1967\footnote{The following year, Carnegie Tech was renamed Carnegie-Mellon
Univ.}.  Floyd was already famous for work on formal grammars that had wide
influence in the design of programming language syntax and parsers; in
fact, that was how he got to be a professor even though he never got a
Ph.D.

In that same year, Albert R. Meyer was appointed Assistant Professor in the
Carnegie Tech Computation Science department where he first met Floyd.
Floyd and Meyer were the only theoreticians in the department, and they
were both delighted to talk about their many shared interests.  After just
a few conversations, Floyd's new junior colleague decided that Floyd was
the smartest person he had ever met.

Naturally, one of the first things Floyd wanted to tell Meyer about was
his new, as yet unpublished, Invariant Theorem.  Floyd explained the
result to Meyer, and Meyer could not understand what Floyd was so excited
about.  In fact, Meyer wondered (privately) how someone as brilliant as
Floyd could be excited by such a trivial observation.  Floyd had to show
Meyer a bunch of examples like the ones that follow in these notes before
Meyer realized that Floyd's excitement was legitimate --- not at the truth
of the utterly obvious Invariant Theorem, but rather at the insight that
such a simple theorem could be so widely and easily applied in verifying
programs.

Floyd left for Stanford the following year.  He won the Turing award ---
the ``Nobel prize'' of Computer Science --- in the late 1970's, in
recognition both of his work on grammars and on the foundations of program
verification.  He remained at Stanford from 1968 until his death in
September, 2001.

We now describe two classic examples illustrating program verification via
the Invariant Theorem.

\subsection{The Euclidean Algorithm}

Given two natural numbers, $a, b$, at least one of which is positive, the
three thousand year old Euclidean algorithm will compute their GCD.  The
algorithm uses two registers $x$ and $y$, initialized at $a$ and $b$
respectively.  Then,
\begin{itemize}
\item if $y = 0$, \textbf{return} the answer $x$ and terminate,

\item else \emph{simultaneously} set $x$ to be $y$, set $y$ to be
the remainder of $x$ divided by $y$, and repeat the process.
\end{itemize}

\begin{example} 
Find $\text{GCD}(414,662)$:
\begin{enumerate}
\item $\text{rem}(414, 662) = 414$ so repeat with $(662,414)$,
\item $\text{rem}(662, 414) = 248$, so repeat with $(414,248)$,
\item $\text{rem}(414, 248) = 166$, so repeat with $(248,166)$, 
\item $\text{rem}(248, 166) = 82$, so repeat with $(166,82)$,
\item $\text{rem}(166, 82) = 2$, so repeat with $(82,2)$,
\item $\text{rem}(82, 2) = 0$, so repeat with $(2,0)$,
\item return 2.
\end{enumerate}
So $\text{GCD}(414,662) = 2$. 
\end{example}

We can present this algorithm as a state machine:
\begin{itemize}

\item $Q \eqdef \naturals \cross \naturals$,

\item $Q_0 \eqdef \set{(a,b)}$,

\item state transitions are defined by the rule
\begin{align*}
(x,y) & \rightarrow (y, \text{rem}(x,y)) & \text{if $y \neq 0$}.
\end{align*}

\end{itemize}

Next we consider how to prove that this state machine correctly computes
$\ms{GCD}(a,b)$.

\subsection{Proving Correctness}

It's generally useful to distinguish two aspects of state machine or
process correctness:

\begin{enumerate}
\item the property that the final results, if any, of the process satisfy
system requirements.  This is called \emph{partial correctness}.  You
might suppose that if a result was only partially correct, then it might
also be partially incorrect, but that's not what's meant here.  When there
is a result, it is correct, but the process might not always produce a
result.  For example, it might run forever on some input without producing
an output.  The word ``partial'' comes from viewing such a process as
computing a \emph{partial function}.

\item the property that the process always finishes or is guaranteed to
produce some desired output.  This is called \emph{termination}.
\end{enumerate}

Partial correctness can commonly be proved using the Invariant Theorem.

\subsection{Correctness of GCD}

We want to prove:
\begin{enumerate}
\item starting from $x = a$ and $y = b$, if we ever finish, then we have
the right answer.  That is, at termination, $x = \text{GCD}(a,b)$.  This
is a \emph{partial correctness} claim.

\item we do actually finish.  This is a process \emph{termination} claim.

\end{enumerate}

\subsubsection{Partial Correctness of GCD}

First let's prove that if GCD gives an answer, it is a correct answer.
Specifically, let $d \eqdef \text{GCD}(a,b)$.  We want to prove that
\emph{if} the procedure finishes in a state $(x,y)$, then $x = d$.

\begin{proof}
So define the state predicate
\[
P((x,y)) \eqdef\ \ [\text{GCD}(x,y) = d].
\]

$P$ holds for the start state $(a,b)$, by definition of $d$.
Also, $P$ is an invariant because
\[
\text{GCD}(x,y) = \text{GCD}(y,\text{rem}(x,y))
\]
for all $x,y \in \naturals$ such that $y \neq 0$ (see Rosen Lemma 2.4.1).  So
by the Invariant Theorem, $P$ holds for all reachable states.

Since the only rule for termination is that $y=0$, it follows that if
state $(x,y)$ is terminated, then $y=0$.  So if this terminated state is
reachable, then we conclude that $x = \text{GCD}(x,0) = d$.
\end{proof}

\subsubsection{Termination of GCD}

Now we turn to the second property, that the procedure must reach a
terminated state. 

To prove this, notice that $y$ gets strictly smaller after any one
transition.  That's because value of $y$ after the transition is the
remainder of $x$ divided by $y$, and this remainder is smaller than $y$ by
definition.  But the value of $y$ is always a natural number, so by the
Least Number Principle, it must have a minimum value among all its values
at reachable states.  But there can't be a transition from a state where
$y$ has its minimum value, because the transition would decrease $y$ still
further.  So the reachable state where $y$ has its minimum value is a
terminated reachable state.

\subsection{Fast Exponentiation}
The most straightforward to compute the $b$th power of a number, $a$, is
to multiply $a$ by itself $b$ times.  This of course requires $b-1$
multiplications.  There is another way to do it using considerably fewer
multiplications.  This algorithm is called \emph{Fast Exponentiation}:

Given inputs $a \in \reals, b \in \naturals$,
initialize registers $x,y,z$ to $a,1,b$ respectively,
and repeat the following sequence of steps until termination:
\begin{itemize}
\item if $z=0$ \textbf{return} $y$ and terminate
\item $r := \text{remainder}(z,2)$
\item $z := \text{quotient}(z,2)$
\item if $r = 1$, then $y := xy$
\item $x := x^2$
\end{itemize}
We claim this algorithm always terminates and leaves $y = a^b$.

To be precise about the claim, we model this algorithm with a state
machine:
\begin{enumerate}
\item $Q \eqdef \reals \cross \reals \cross \naturals$,
\item $Q_0 \eqdef \set{(a,1,b)}$,
\item transitions
\begin{equation*}
(x,y,z) \rightarrow
\begin{cases}
(x^2, y, \text{quotient}(z,2)) & \text{if $z$ is positive and even},\\
(x^2, xy, \text{quotient}(z,2)) & \text{if $z$ is positive and odd}.
\end{cases}
\end{equation*}
\end{enumerate}

Let $d \eqdef a^b$.  Since the machine is obviously deterministic, all we
need to prove is that a state of the form $(x,d,0)$ is reachable.

We'll begin by proving partial correctness: \emph{if} a state of the form
$(x,y,0)$ is reachable, then $y = d$.

Now it's easy to check that the predicate, $P$, is an
invariant, where
\[
P((x,y,z)) \eqdef\ \ [yx^z = d].
\]
Also, $P$ holds for the start state $(a,1,b)$ by definition of $d$.  So by
the Invariant Theorem, $P$ holds for all reachable states.  The only
terminating states are those with $z = 0$, so if a terminating state
$(x,y,0)$ is reachable, then $y = yx^0 = d$.  So we have proved partial
correctness.

Note that as is often the case with induction proofs, the proof is trivial
once you have the right invariant (induction hypothesis), but the trivial
proof is not much help in understanding how someone discovered the
algorithm and its invariant.  To learn more about that, you'll have to
study Algorithms, say by taking 6.046.

What about termination?  We have to prove that a terminated state is
reachable.  But notice that $z$ is a natural-number-valued variable that
gets smaller at every transition.  So there must be a minimum value for
$z$ among the reachable states, and this minimum can only occur at a
terminated state.  So we conclude that the algorithm will always
terminate.  In fact, we can say more:

\begin{problem}
Prove that it requires at most $2 \log_2 b$ multiplications to compute
$a^b$ for $b>1$.
\end{problem}

\section{Derived Variables}

The preceding termination proofs involved finding a natural-number-valued
measure to assign to states.  We might call this measure the ``size'' of
the state.  We then showed that the size of a state decreased with every
state transition.  By the Least Number Principle, the size can't decrease
indefinitely, so when a minimum size state is reached, there can't be any
transitions possible: the process has terminated.

More generally, the technique of assigning values to states --- not
necessarily natural numbers and not necessarily decreasing under
transitions --- is often useful in the analysis of algorithms.
\emph{Potential functions} play a similar role in physics.  In the context
of computational processes, such value assignments for states are called
\emph{derived variables}.

For example, for the Die Hard machines we could have introduced a
derived variable, $f:Q \to \reals$, for the amount of water in both
buckets, by setting $f((a, b)) \eqdef a + b$.  Similarly, in the robot
problem, the position of the robot along the $x$-axis would be given by
the derived variable $x\text{-coord}((i, j)) \eqdef i$.

We can formulate our general termination method as follows:

\begin{definition}
A derived variable $f : Q \to \reals$ is \emph{strictly decreasing} iff
\[
q \rightarrow q' \text{  implies  } f(q') < f(q).
\]
\end{definition}

\begin{theorem}
\label{th:decr}
If $f : Q \to \naturals$ is a strictly decreasing derived variable of a
state machine, then the length of any execution starting at a start state
$q$ is at most $f(q)$.
\end{theorem}

Of course we could prove Theorem~\ref{th:decr} by induction on the value
of $f(q)$.  But think about what it says: ``If you start counting down at
some natural number $f(q)$, then you can't count down more than $f(q)$
times.''  Put this way, the theorem is so obvious that no one should feel
deprived that we are not writing out a proof.

\begin{corollary}
If there exists a strictly decreasing natural-number-valued derived
variable for some state machine, then every execution of that machine
terminates.
\end{corollary}

We now define some other useful flavors of derived variables taking values
over posets.  It's useful to generalize the familiar notations
$\leq$ and $<$ for ordering the  real numbers: 
if $\preceq$ is a partial order on some set $A$, then define $\prec$ by
the rule
\[
a\prec a' \eqdef\quad a \preceq a' \land a \neq a'.
\]
A relation like $\prec$ that is transitive and antisymmetric but such that
$a$ is never $\prec a$ is called a \emph{strict} partial order.

\begin{definition}
Let $\preceq$ be partial order on a set, $A$.  A derived variable
$f : Q \to A$ is \emph{strictly decreasing} iff
\[
q \rightarrow q' \text{  implies  } f(q') \prec f(q).
\]
It is \emph{weakly decreasing} iff
\[
q \rightarrow q' \text{  implies  } f(q') \preceq f(q).
\]
\end{definition}
\emph{Strictly increasing} and \emph{weakly increasing} derived variables
are defined similarly.\footnote{Weakly increasing variables are often also
called \emph{nondecreasing}.  We will avoid this terminology to prevent
confusion between nondecreasing variables and variables with the much
weaker property of \emph{not} being a decreasing variable.}

The existence of a natural-number-valued \emph{weakly} decreasing derived
variable does not guarantee that every execution terminates.  That's
because an infinite execution could proceed through states in which a
weakly decreasing variable remained constant.

Predicates can be viewed as the special case of derived variables that
only take the values 0 and 1.  If we do this, then invariants can be
characterized precisely as \emph{weakly increasing} 0-1-valued derived
variables.  Namely, for any predicate, $P$, on states, define a derived
variable, $f_P$, as follows:
\begin{equation*}
f_P(q) \eqdef
\begin{cases}
0 & \text{if $P(q)$ is false}, \\
1 & \text{otherwise}.
\end{cases}
\end{equation*}
Now $P$ is an invariant if and only if $f_P$ is weakly increasing.
\footnote{It may seem natural to call a variable whose values do not
change under state transitions an ``invariant variable.''  We will avoid
this terminology, because the weakly increasing variable $f_P$ associated
with an invariant predicate, $P$, is not necessarily an invariant
variable.}

\section{The Stable Marriage Problem}

Okay, frequent public reference to derived variables may not help your
mating prospects.  But they can help with the analysis!

\subsection{The Problem}

Suppose that there are $n$ boys and $n$ girls.  Each boy ranks all of the
girls according to his preference, and each girl ranks all of the boys.
For example, Bob might like Alice most, Carol second, Hildegard third,
etc.  There are no ties in anyone's rankings; Bob cannot like Carol and
Hildegard equally.  Furthermore, rankings are known at the start and stay
fixed for all time.

The general goal is to marry off boys and girls so that everyone is happy;
we'll be more precise in a moment.  Every boy must marry exactly one girl
and vice-versa --- no polygamy.  If we want these marriages to last, then
we want to avoid an unstable arrangement:

\begin{definition}
A set of marriages is {\em unstable} if there is a boy and a girl who
prefer each other to their spouses.
\end{definition}

For example, suppose that Bob is married to Carol, and Ted is married to
Alice.  Unfortunately, Carol likes Ted more than Bob \emph{and} Ted likes
Carol more than Alice.  The situation is shown in Figure~\ref{fig:hots}.
So Carol and Ted would both be happier if they ran off together.  We say
that Carol and Ted are a \emph{rogue couple}, because this is a situation
which encourages roguish behavior.

\begin{figure}[htbp]
\centering \includegraphics[height=1.5in]{figures/hots}
\caption{\em Bob is married to Carol, and Ted is married to Alice, but Ted
prefers Carol his mate, and Carol prefers Ted to her mate.  So Ted and
Carol form a rogue couple, making their present marriages unstable.}
\label{fig:hots}
\end{figure}

\begin{definition}
A set of marriages is {\em stable} if there are no rogue couples or,
equivalently, if the set of marriages is not unstable.
\end{definition}

Now we can state the \emph{Stable Marriage Problem} precisely: find
spouses for everybody so that the resulting the set of marriages is
stable.  It is not obvious that this goal is achievable!  In fact, in the
gender blind \emph{Stable Buddy} version of the problem, where people of
any gender can pair up as buddies, there may be no stable pairing!
However, for the ``boy-girl'' marriage problem, a stable set of marriages
does always exist.

Incidentally, although the classical ``boy-girl-marriage'' terminology for
the problem makes some of the definitions easier to remember (we hope
without offending anyone), solutions to the Stable Marriage Problem are
really useful.  The stable marriage algorithm we describe was discovered
independently and first published in a paper by D. Gale and L.S. Shapley
in 1962.  The most impressive example of the algorithm is in assignment of
residents to hospitals by the National Resident Matching Program (NRMP)
that actually predates their paper by ten years.  Acting on behalf of a
consortium of major hospitals (playing the role of the girls), the NRMP
has, since the turn of the twentieth century, assigned each year's pool of
medical school graduates (playing the role of boys) to hospital
residencies (formerly called ``internships'').  Before the procedure
ensuring stable matches was adopted, there were chronic disruptions and
awkward countermeasures taken to preserve assignments of graduates to
residencies.  The stable marriage procedure was discovered and applied by
the NRMP in 1952.  It resolved the problem so successfully, that the
procedure continued to be used essentially without change at least through
1989.\footnote{Much more about the Stable Marriage Problem can be found in
the very readable mathematical monograph by Dan Gusfield and Robert
W. Irving,
\href{http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=7676}{The
Stable Marriage Problem: Structure and Algorithms}, MIT Press, Cambridge,
Massachusetts, 1989, 240 pp.}

%%insert rest of story from gusfield book pp3--4??

Let's find a stable set of marriages in one possible situation, and then
try to translate our method to a general algorithm.  The table below shows
the preferences of each girl and boy in decreasing order.

\begin{eqnarray*}
boys & \quad & girls \\
1 : C B E A D & \quad & A : 3 5 2 1 4 \\
2 : A B E C D & \quad & B : 5 2 1 4 3 \\
3 : D C B A E & \quad & C : 4 3 5 1 2 \\
4 : A C D B E & \quad & D : 1 2 3 4 5 \\
5 : A B D E C & \quad & E : 2 3 4 1 5
\end{eqnarray*}

How about we try a greedy strategy?  We take each boy in turn and pack
him off with his favorite among the girls still available.  This gives
the following assignment.

\begin{eqnarray*}
1 \rightarrow C \\
2 \rightarrow A \\
3 \rightarrow D \\
4 \rightarrow B \\
5 \rightarrow E \\
\end{eqnarray*}

To determine whether this set of marriages is stable, we have to check
whether there are any rogue couples.  Boys 1, 2, and 3 all got their top
pick among the girls; none would even think of running off.  Boy 4 may be
a problem because he likes girl $A$ better than his mate, but she ranks
him dead last.  However, boy 4 also likes girl $C$ better than his mate,
and she rates him above her own mate.  Therefore, boy 4 and girl $C$ form
a rogue couple!  The marriages are not stable.  We could try to make ad
hoc repairs, but we're really trying to develop a general strategy.

Another approach would be to use induction.  Suppose we pair boy 1
with his favorite girl, $C$, show that these two will not join a rogue
couple, and then solve the remaining problem by induction.  Clearly
boy 1 will never leave his top pick, girl $C$.  But girl $C$ might
very well dump him-- she might even rate him last!

This turns out to be a tricky problem.  The best approach is to use a
mating ritual that was popular back in the 50's.

\subsection{The Mating Algorithm}

We'll describe the algorithm as a Mating Ritual that takes place over
several days.  The following events happen each day:

{\bf Morning: } Each girl stands on her balcony.  Each boy stands under
the balcony of his favorite among the girls on his list, and he serenades
her.  If a boy has no girls left on his list, he stays home and does his
6.042 homework.

{\bf Afternoon: } Each girl who has one or more suitors serenading her,
says to her favorite suitor, ``Maybe... come back tomorrow.''  To the
others, she says, ``No.  I will never marry you!  Take a hike!''

\textbf{Evening}: Any boy who is told by a girl to take a hike, crosses that
girl off his list.

\textbf{Termination condition}: When every girl has at most one suitor,
the ritual ends with each girl marrying her suitor, if she has one.

% Show example

There are a number of facts about this algorithm that we would like to
prove:

\begin{itemize}
\item The algorithm terminates.
\item Everybody ends up married.
\item The resulting marriages are stable.
\end{itemize}

Furthermore, we would like to know if the algorithm is fair.  Do both boys
and girls end up equally happy?

\subsection{The State Machine Model}

Before we can prove anything, we need clear mathematical definitions of
what we're talking.  So let's begin by defining the problem.

\begin{definition}
A Marriage Problem consists of two disjoint sets of size $n \in \naturals$
called \boys\ and \girls.  The members of \boys\ are called \emph{boys},
and members of \girls\ are called \emph{girls}.  For each boy, $B$, there
is a strict total order, $<_B$, on \girls, and for each girl, $G$, there
is a strict total order, $<_G$, on \boys.
\end{definition}

The idea is that $<_B$ is boy $B$'s preference ranking of the girls.  That
is, $G_1 <_B G_2$ means that $B$ prefers girl $G_2$ to girl $G_1$.
Similarly, $<_G$ is girl $G$'s preference ranking of the boys.

Next we model the Mating Algorithm with a state machine $(Q, Q_0,
\delta)$.  A key observation is that to determine what happens on any day
of the ritual, all we need to know is which girls are on which boys'
lists that day.  So we define the boys' lists to be the states of our
machine.  Formally,
\[
Q \eqdef [\boys \to \power(\girls)]
\]
where $[\boys \to \power(\girls)]$ is the set of all total functions
mappings boys to sets of girls.  Here the idea is that if $q: \boys
\to \power(\girls)$ is a state, then $q(B)$ is the set of girls that boy
$B$ has left on his list, that is, the girls he \emph{not} crossed off
yet.

We start the Mating Algorithm with no girls crossed off.  So in the start
state, $\qst$, every girl is on every boy's list.  Formally,
\begin{align*}
\qst(B) & \eqdef  \girls, & \text{for all boys, $B$}, \\
Q_0  & \eqdef \set{\qst}.
\end{align*}

According to the Mating ritual, on any given morning, a boy will
serenade the girl he most prefers among those he has not as yet crossed
out.  If he has crossed out all the girls, then we'll say he is serenading
\none, where \none\ can be any convenient mathematical object that is not
equal to any girl or boy.  So we can define the derived variable $\sere_q$
to be a function mapping each boy to the girl (or \none) he is serenading
in state $q$.  There is a simple way to define $\sere_q:\boys \to \girln$
using the $\max$ operator for the boy's preference order.  Namely,
\[
\sere_q(B) \eqdef
\begin{cases}
\max_B q(B) &\text{if } q(B) \neq \emptyset,\\
\none & \text{otherwise}.
\end{cases}
\]
where $\max_B(S)$ is the maximum element in a nonempty set, $S \subseteq
\girls$ ordered by $<_B$.

Another useful derived variable is the set of suitors who are serenading a
girl on a given morning.  That is, the derived variable is the function
$\suit_q:\girls \to \power(\boys)$ mapping each girl to her set of
suitors:
\[
\suit_q(G) \eqdef \set{B \in \boys \suchthat G = \sere_q(B)}.
\]

The final derived variable we need is the favorite suitor of
each girl on a given evening.  That is, $\fav_q:\girls \to \boyn$ is
defined by the rule:
\[
\fav_q(G) \eqdef 
\begin{cases}
\max_G \suit_q(G) & \text{if } \suit_q(G) \neq \emptyset,\\
\none & \text{otherwise}.\\
\end
{cases}
\]

Notice that no boy is the favorite of two girls, because a boy serenades
only one girl at a time.

Now we're ready to define the transitions.  A state changes in the evening
when some of the boys cross the girl they are serenading off their lists.
If a boy is serenading a girl and he is not her favorite suitor, then he
crosses her off.  If the boy is not serenading any girl (because his list
is empty), or if he is the current favorite of the girl he is serenading,
then he doesn't cross anyone off his list.  So for any state, $q$, this
uniquely defines tomorrow morning's state, $\nex_q$.\footnote{The
preceding description of $\nex_q$ in words is a good mathematical
definition.  But for people who prefer formulas, here's one:
\[
\nex_q(B) \eqdef
\begin{cases}
q(B) - {\sere_q(B)} &
      \text{if } \sere_q(B) \neq \none \text{ and } B \neq \fav_q(\sere_q(B)),\\
q(B) & \text{otherwise}.
\end{cases}
\]}

Notice that $\nex_q$ is always defined, so we still have to say when to
terminate.  The rule is to terminate when every girl has at most one
suitor -- that's who she will marry.  But this is exactly the situation
when it is no longer possible for any boy to cross any girl off his list,
which means that $\nex_q = q$.  So we define the transition relation by
the rule
\[
q \rightarrow q' \text{  if and only if  } [q' = \nex_q \text{ and } q
\neq q'].
\]

There's one very useful fact to notice about the ritual: if a girl has a
favorite boy suitor on some morning of the ritual, then that favorite
suitor will still be serenading her the next morning --- because his list
won't have changed.  So she is sure to have today's favorite boy among her
suitors tomorrow.  That means she will be able to choose a favorite suitor
tomorrow who is at least as desirable to her as today's favorite.

It's helpful if we agree to include \none\ as a least preferred object by
every boy and girl.  This allows us to say that, even if a girl has no
suitor today, she will be no worse off tomorrow.  So day by day, her
favorite suitor can stay the same or get better, never worse.  In others
words, we have just proved the following:
\begin{lemma}\label{ndfav}
$\fav_q(G)$ is a weakly $<_G$-increasing derived variable, for every girl, $G$.
\end{lemma}

Similarly, a boy keeps serenading the girl he most prefers among those on
his list until he must cross her off, at which point he serenades the next
most preferred girl on his list.  So we also have:
\begin{lemma}\label{niser}
$\sere_q(B)$ is a weakly $<_B$-decreasing derived variable, for every boy, $B$.
\end{lemma}

\subsection{Termination}

It's easy to see why the Mating Algorithm terminates: every day at least
one boy will cross a girl off his list.  If no girl can be crossed off any
list, then the ritual has terminated.  But initially there are $n$ girls
on each of the $n$ boys' lists for a total of $n^2$ list entries.  Since
no girl ever gets added to a list, the total number of entries on the
lists decreases every day that the ritual continues, and so the ritual
can continue for at most $n^2$ days.\footnote{Here's the version with
formulas.  Define the \emph{size} of a state, $q$, to be the total number
of list entries:
\[
\size(q) \eqdef \sum_{B \in \boys} \card{q(B)}.
\]
Then $\size$ is a strictly decreasing natural-number-valued derived
variable whose initial value, $\size(\qst)$, is
\[
\sum_{B \in \boys} \card{\girls} = \card{\boys}\cdot \card{\girls} = n^2.
\]
So by Theorem~\ref{th:decr}, the state machine terminates in at most $n^2$
steps.}

\subsection{They All Live Happily Every After...}

We still have to prove that the Mating Algorithm leaves everyone in a
stable marriage.  One simple invariant predicate, $P$, captures what's
going on:
\begin{quotation}\noindent
if some girl, $G$, is not on the list of some boy, $B$, then $G$ has a
favorite suitor and she prefers him over $B$.\footnote{The formula would
be:
\[
P(q) \eqdef [\forall B \in \boys\, \forall G \in \girls\; G \notin q(B)
              \implies B <_G \fav_q(G)],
\]
with $<_G$ extended to \boyn\ by the rule that $\none <_G B$ for all boys,
$B$.}
\end{quotation}
Why is $P$ invariant?  Well, we know from Lemma~\ref{ndfav} that $G$'s
favorite tomorrow will be at least as desirable as her favorite today, and
since her favorite today is more desirable than $B$, tomorrow's favorite
will be too.

Notice that $P$ also holds on the first day, since every girl is on every
list.  So by the Invariant Theorem, we know that $P$ holds on every day
that the Mating ritual runs.  Knowing the invariant holds when the
Mating Algorithm terminates will let us complete the proofs.

\begin{theorem}
Everyone is married by the Mating Algorithm.
\end{theorem}

\begin{proof}
Suppose, for the sake of contradiction, that some boy is not married on
the last day of the Mating ritual.  So he can't be serenading anybody,
that is, his list must be empty.  So by invariant $P$, every girl has a
favorite boy whom she prefers to that boy.  In particular, every girl has
a favorite boy that she marries on the last day.  So all the girls are
married.  What's more there is no bigamy: we know that no two girls have
the same favorite.

But there are the same number of girls as boys, so all the boys must be
married too.
\end{proof}

\begin{theorem}
The Mating Algorithm produces stable marriages.
\end{theorem}

\begin{proof}
Let $B_1$ and $B_2$ be any two distinct boys, and suppose on the last day
of the Mating ritual, $B_1$ is married to girl $G_1$ and $B_2$ is married
to girl $G_2$.  We claim $B_1$ and $G_2$ are not a rogue couple.  Since
$B_1$ could be any of the boys, it follows that no boy is part of a rogue
couple.  Hence the marriages on the last day are stable.

To prove the claim, we consider two cases:

\emph{Case} 1.  $G_2$ is not on $B_1$'s list.  Then since invariant $P$
holds, we know that $G_2$ prefers her favorite $B_2$ over $B_1$.  So she's
not going to run off with $B_1$: the claim holds in this case.

\emph{Case} 2.  Otherwise, $G_2$ is on $B_1$'s list.  But since $B_1$ is
married to $G_1$, he has chosen to serenade $G_1$ instead of $G_2$, so he
must prefer $G_1$ over $G_2$.  So he's not going to run off with $G_2$:
the claim also holds in this case.
\end{proof}

\subsection{...And the Boys Live Especially Happily}

Who is favored by the Mating Algorithm, the boys or the girls?  The girls
seem to have all the power: they stand on their balconies choosing the
finest among their suitors and spurning the rest.  What's more, their
suitors can only change for the better as the Algorithm progresses
(Lemma~\ref{ndfav}).  And from the boy's point of view, the girl he is
serenading can only change for the worse (Lemma~\ref{niser}).  Sounds like
a good deal for the girls.

But it's not!  The fact is that from the beginning the boys are serenading
their first choice girl, and the desirability of the girl being serenaded
decreases only enough to give the boy his most desirable possible spouse.
So the mating algorithm does as well as possible for all the boys and
actually does the worst possible job for the girls.

To explain all this we need some definitions.  Let's begin by observing
that while the mating algorithm produces one set of stable marriages,
there may be other ways to arrange stable marriages among the same set of
boys and girls.  For example, reversing the roles of boys and girls will
often yield a different set of stable marriages among them.

\begin{definition}
If there is some stable set of marriages in which a girl, $G$, is married
to a boy, $B$, then $G$ is said to be a \emph{possible spouse} for $B$, and
likewise, $B$ is a \emph{possible spouse} for $G$.
\end{definition}

This captures the idea that incompetent nerd Ben Bitdiddle has no chance
of marrying movie star Heather Graham: she is not a possible spouse.  No
matter how the cookie crumbles, there will always be some guy that she
likes better than Ben and who likes her more than his own mate.  No
marriage of Ben and Heather can be stable.

Note that since the mating algorithm always produces one stable set of
marriages, the set of possible spouses for a person --- even Ben --- is
never empty.

\begin{definition}
A person's \emph{optimal} spouse is the possible spouse that person most
prefers.  A person's \emph{pessimal} spouse is the possible spouse that
person least prefers.
\end{definition}

Here is the shocking truth about the Mating Algorithm:

\begin{theorem}
The Mating Algorithm marries every boy to his optimal mate and every girl
to her pessimal mate.
\end{theorem}

\begin{proof}
The proof is in two parts.  First, we show that every boy is married to
his optimal mate.  The proof is by contradiction.

Assume for the purpose of contradiction that some boy does not get his
optimal girl.  There must have been a day when he crossed off his optimal
girl --- otherwise he would still be serenading her or some even more
desirable girl.

By the Least Number Principle, there must be a first day when a boy
crosses off his optimal girl.  Let $B$ be one of these boys who first
crosses off his optimal girl, and let $G$ be $B$'s optimal girl.

According to the rules of the ritual, $B$ crosses off $G$ because she has
a favorite suitor, $B'$, whom she prefers to $B$.  So on the morning of
day that $B$ crosses off $G$, her favorite $B'$ has not crossed off his
own optimal mate.  This means that $B'$ must like $G$ more than any other
possible spouse.  (Of course, she may not be a possible spouse; she may
dump him later.)

Since $G$ is a possible spouse for $B$, there must be a stable set of
marriages where $B$ marries $G$, and $B'$ marries someone else.  But $B'$
and $G$ are a rogue couple in this set of marriages: $G$ likes $B'$ more
than her mate, $B$, and $B'$ likes $G$ more than the possible spouse he is
married to.  This contradicts the assertion that the marriages were
stable.

Now for the second part of the proof: showing that every girl is
married to her pessimal mate.  Again, the proof is by contradiction.

Suppose for the purpose of contradiction that there exists a stable set of
marriages, $\mathcal{M}$, where there is a girl, $G$, who fares worse than
in the Mating Algorithm.  Let $B$ be her spouse in the Mating Algorithm.
By the preceding argument, $G$ is $B$'s optimal spouse.  Let $B'$ be her
spouse in $\mathcal{M}$, a boy whom she likes even less than $B$.  Then
$B$ and $G$ form a rogue couple in $\mathcal{M}$: $B$ prefers $G$ to his
mate, because she is optimal for him, and $G$ prefers $B$ to her mate,
$B'$, by assumption.  This contradicts the assertion that $\mathcal{M}$
was a stable set of marriages.
\end{proof}

\end{document}
