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

%\newcommand{\vl}{\text{value}}
\def\lexle{\mathrel{\preceq_{\text{lex}}}}
\def\lex<{\mathrel{\prec_{\text{lex}}}}
\def\coordle{\mathrel{\preceq_{\text{c}}}}
\def\coord<{\mathrel{\prec_{\text{c}}}}
\def\SS{\mathrel{\prec_{\text{SS}}}}
\def\succSS{\mathrel{\succ_{\text{SS}}}}
\def\Ack{{\text{Ack}}}
\def\RAck{{R_\text{Ack}}}

%\newlength{\prooflength}
%\newlength{\reasonlength}

\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{\tgn}{\text{\emph{total-girls-names}}}


\newcommand{\bins}{\set{0,1}*}
\newcommand{\aexp}{\text{Aexp}}
\newcommand{\tg}{\text{2PG}}


\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{4}{Structural Induction; State Machines}

\section{Recursive Data Types}

\emph{Recursive data types} play a central role in modern programming
languages.  From a Mathematical point of view, recursive data types are
what induction is about.  Recursive data types are specified by
\emph{recursive definitions} that say how to build something from it
parts.  These definitions have two parts:
\begin{itemize}
\item \textbf{Base case(s)} that don't depend on anything else.
\item \textbf{Constructor case(s)} that depend on previous cases.
\end{itemize}

\begin{example}\label{E}
Define a set, $E$, recursively as follows:
\begin{itemize}
\item \textbf{Base case:} $0 \in E$,\label{0E}
\item \textbf{Constructor cases:} if $n \in E$ and $n>0$, then
\begin{enumerate}
\item $n+2 \in E$, \label{+2E}
\item $-n \in E$.\label{-E}
\end{enumerate}
\end{itemize}
\end{example}

Using this definition, we can see that $0 \in E$ by the Base case, so $0 +
2 = 2 \in E$ by Constructor case~\ref{+2E}., and so $2+2 =4 \in E$, $4+2 =
6 \in E$, \dots, and in fact any nonnegative even number is in $E$ by
successive application of case~\ref{+2E}.  Also, by case~\ref{-E}.,
$-2,-4,-6,\dots \in E$.  So clearly all the even integers are 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 the Base and Constructor cases.  In
other words, $E$ will be exactly the set of even integers.

Another example is set, $M$, of strings of \emph{matched} right and left
parentheses.  These are the strings that would be obtained if we took a
sequence of fully parenthesized arithmetic (or Scheme) expressions and
erased all the characters except the parentheses.  Here's a recursive
definition:
\begin{example}\label{M}
Define the set, $M$, of strings of \emph{matched} right and left
parentheses recursively as follows:
\begin{itemize}

\item \textbf{Base case:} $\lambda \in M$, where $\lambda$ is the
\emph{empty} string,

\item \textbf{Constructor case:} if $s,t \in M$, then
$\texttt{(}s\texttt{)}t \in M$.

\end{itemize}
\end{example}

Here we're writing $\texttt{(}s\texttt{)}t$ to indicate the string that
starts with a left parenthesis, followed by the sequence of parentheses
(if any) in the string $s$, followed by a right parenthesis, and ending
with the sequence of parentheses in the string $t$.

Using this definition, we can see that $\lambda \in S$ by the Base case, so
\[
\texttt{(}\lambda\texttt{)}\lambda=\texttt{()}\in M
\]
by the Constructor case, and so
\begin{align*}
\texttt{(}\lambda\texttt{)}\texttt{()} &= \texttt{()()},\\
\texttt{(())}\lambda & = \texttt{(())},\\
                     & \texttt{(())()}
\end{align*}
are further strings in $M$ by repeated applications of the Constructor
case.

Arithmetic expressions are another important example of a recursive data
type.  We could define them as parenthesized strings with symbols for
arithmetic operators plus, times, etc., but a more useful representation
uses ``tagged'' data items reflecting how an expression should be parsed.
So we will define arithmetic expressions using pairs whose first elements
are symbolic tags like \texttt{integer} and \texttt{sum}.  In programming
jargon, we are working with the ``parse trees'' of the expressions rather
than the parenthesized strings.

\begin{example}\label{A}
The set, $\aexp$, of \emph{Arithmetic expressions}
over a set of \emph{variables}, $V$,
is defined recursively as follows:
\begin{itemize}
\item \textbf{Base cases:}
\begin{enumerate}
\item If $n \in \integers$, then $\ang{\texttt{integer}, n} \in \aexp$.
\item If $v \in V$, then $\ang{\texttt{variable}, v} \in \aexp$.
\end{enumerate}
\item \textbf{Constructor cases:} if $e,e' \in \aexp$, then
\begin{enumerate}
\item $\ang{\texttt{sum}, e, e'} \in \aexp$,
\item $\ang{\texttt{product}, e, e'} \in \aexp$, and
\item $\ang{\texttt{minus}, e} \in \aexp$.
\end{enumerate}
\end{itemize}
\end{example}


\subsection{Structural Induction on Recursive Data Type Definitions}

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

To illustrate this, we'll prove that strings of matched parentheses always
have an equal number of left and right parentheses.  To do this, define a
predicate on strings
\[
P(s) \eqdef s \text{ has an equal number of left and right parentheses}.
\]
\begin{proof}

We'll prove that $\forall s \in M.\, P(s)$ by structural induction on the
definition of $M$, using $P(s)$ as the induction hypothesis.

\textbf{Base case:} $P(\lambda)$ holds because the empty string has zero
left and zero right parentheses.

\textbf{Constructor case:} For $r = \texttt{(}s\texttt{)}t$, we must show
that $P(r)$ holds, given that $P(s)$ and $P(t)$ holds.  So let $n_s$,
$n_t$ be, respectively, the number of left parentheses in $s$ and $t$.  So
the number of left parentheses in $r$ is $1+n_s+n_t$.

Now from the respective hypotheses $P(s)$ and $P(t)$, we conclude that the
number of right parentheses in $s$ and $t$, respectively, is also $n_s$
and $n_t$.  So the number of right parentheses in $r$ is $1+n_s+n_t$,
which is the same as the number of left parentheses.  This proves $P(r)$.
We conclude by structural induction that $\forall s \in M.\, P(s)$.
\end{proof}

Returning to the recursive definition of the set $E$ in Example~\ref{E},
the observation that all even integers are in $E$ was easy to see, and is
easy to prove by induction (with induction hypothesis $2n \in E \land -2n
\in E$).  To verify the observation $E$ actually equals the even numbers,
we need only show that every integer in $E$ is even.  This follows
trivially by structural induction with hypothesis:
\[
Q(n) \eqdef \text{$n$ is even}.
\]

\textbf{Base case}: $Q(0)$ holds since 0 is even.

\textbf{Constructor cases}: assuming $n \in E$ and $Q(n)$ holds, prove
that
\begin{enumerate}
\item $Q(n+2)$ holds.  This is immediate, since adding 2 to an even number
  gives an even number.
\item $Q(-n)$ holds.  This is also immediate, since $n$ is even iff $-n$ is even.
\end{enumerate}

We could understand induction on the length of strings as structural
induction if we think of the strings as being represented as tagged data:

\begin{definition}\label{A*}
The set, $A^*$, of strings over a set, $A$, called the \emph{alphabet},
is defined recursively as follows:
\begin{itemize}
\item \textbf{Base case:} $\ang{\texttt{emptystring}} \in A^*$.

\item \textbf{Constructor case:} if $s \in A^*$ and $a \in A$, then
$\ang{\texttt{successor-string},s,a}\in A^*$.

\end{itemize}
\end{definition}
Here, of course, $\ang{\texttt{emptystring}}$ is a tagged representation
of the emptystring, $\lambda$, and $\ang{\texttt{successor-string},s,a}$ is a
representation of the string, $sa$, equal to the string $s$, followed by
the character, $a$.

In fact, ordinary induction can be understood as an instance of structural
induction if we think of the nonnegative integers as being represented as
tagged data.  To start, we might represent 0 as a length one sequence
consisting of the tag \texttt{zero}:
\begin{definition}\label{tagn}
The nonnegative integers can be defined recursively as follows:
\begin{itemize}
\item \textbf{Base case}  $\ang{\texttt{zero}}\in \naturals$.
\item \textbf{Constructor case} if $n \in \naturals$, then
      $\ang{\texttt{successor},n}\in \naturals$.
\end{itemize}
\end{definition}

Similarly, 

Conversely, the simple structural inductions given above could be replaced
by induction on the ``size'' of the data items, or more generally, by
induction on the number of constructor steps needed to arrive at a data
item.  So for these examples, using structural induction instead of
ordinary induction is a matter of style.  But there are some important
recursive data types whose elements take an infinite number of steps to
build, and for these, structural induction cannot be replaced by ordinary
induction.  An example is the data type of \emph{two-person games of
perfect information}.

\subsubsection{Games as a Recursive Data Type}

Chess, checkers, and tic-tac-toe are examples of \emph{two-person
terminating games of perfect information}, ---$\tg$'s for short.  These
are games in which two players alternate moves that depend only on the
visible board position or state of the game.  ``Perfect information''
means that the players know the complete state of the game at each move.
(Most card games are \emph{not} games of perfect information because
neither player can see the other's hand.)  ``Terminating'' means that the
game cannot go on forever ---it must end after a finite number of
moves.\footnote{Since board positions can repeat in chess and checkers,
termination is enforced by rules that prevent any position from being
repeated more than a fixed number of times.  So the ``state'' of these
games is the board position \emph{plus} a record of how many times
positions have been reached.}

Chess, checkers, and tic-tac-toe all can end in a tie with no winner, but
for simplicity, we'll stick to games in which the only outcomes are a win
for one player and a loss for the other.  (No ``everybody wins''-type
games at MIT.) \texttt{:-)}

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

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

Familiar games like tic-tac-toe and chess have only a finite number of
possible moves at any stage, but some interesting games do have infinitely
many possible moves.  For example, there is a straightforward way to
generalize checkers for play on an $n \times n$ board.  Now we might
define the ``metacheckers'' game by letting the first metacheckers player
choose any integer $n \geq 8$, and having the players play an $n \times n$
checkers game with the second metagame player making the first move in the
chosen $n \times n$ game.

\iffalse Here's a contrived example we'll call the \emph{MN} Game: the
first player can pick any positive integer, $m$.  The second player may
then may pick any bigger integer, $n$.  After that, the players alternate
moves, picking on each move any positive integer less than $n$ that has
not been chosen previously.  The first person who has no remaining
possible move is the loser.

Of course you have an obvious winning strategy for the MN game: pick $n$
to be the smallest even integer $>m$.  On the other hand, even though you
are sure to win, I can delay your win as long as I like by choosing a very
large $m$.  \fi

Notice that at any point in the play of a $\tg$, the rest of the game is
itelf a $\tg$.  So a game can be represented by the set of subgames that
result from its possible first moves.  This observation makes it easy
---perhaps deceptively easy ---to define $\tg$'s as a tagged recursive
data type.

\begin{definition}
The set, $\tg$, of \emph{two-person terminating games of perfect
information} is defined recursively as follows:
\begin{itemize}
\item \textbf{Base cases:}
\begin{enumerate}
\item $\ang{\texttt{win}}\in \tg$.
\item $\ang{\texttt{lose}}\in \tg$.
\end{enumerate}
\item \textbf{Constructor case:} if $\mathcal{G}$ is a nonempty set of
$\tg$'s, then $\ang{\texttt{next-moves},\mathcal{G}}\in \tg$.
\end{itemize}
\end{definition}

Notice that in metacheckers there are not only an infinite number of
possible first moves, but there is no finite bound on how long a game will
take ---the first player can delay the end as long as he likes by
initially choosing a big enough board.  But metacheckers a terminating
game: it's impossible for the metachekers players to keep making moves
forever, even if they conspired to do so.

With such infinite games, there is no way to assign nonnegative integer
``sizes'' to games so that ordinary induction on game size becomes a
useful proof method.  But structural induction remains sound and easy to
apply.\footnote{The soundness of such infinite structural induction may
seem worrisome, but we'll accept it without proof.  There is a persuasive
way to justify it by generallizing the well-ordering principle to partial
orders, but we won't go into this in the Notes.}  We will use it to prove
the remarkable fact that in every game, there is a winning strategy for
one of the players.

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

Notice that although Theorem~\ref{fund} guarantees a winning strategy, it
gives no clue which player may have it.  For chess, the Subset takeaway
Game from a
\href{http://theory.csail.mit.edu/classes/6.042/spring06/cp2f.pdf}
{Friday, Week 2 Team Problem}, and many other familiar games, no one knows
which player has a winning strategy.

\begin{proof}
The proof is by structural induction on $\tg$'s.  The induction
hypothesis, $P(G)$, is that there is a winning strategy for game $G$.

\textbf{Base cases:}
\begin{enumerate}
\item $G=\ang{\texttt{win}}$.  Then $P(G)$ holds because the first player
 has the winning strategy: ``make the winning move.''
\item $G=\ang{\texttt{lose}}$.  Then $P(G)$ holds because the second
 player has a winning strategy: ``Let the first player make the losing
 move.''
\end{enumerate}

\textbf{Constructor case:} Suppose $G =
\ang{\texttt{next-moves},\mathcal{G}} \in \tg$.  By structural induction,
we may assume that $P(H)$ holds for every possible move $H \in
\mathcal{G}$.  There are two cases to consider:
\begin{itemize}
\item some $H_0 \in \mathcal{G}$ has a winning strategy for its second
  player. Then the first player in $G$ has a winning strategy: pick $H_0$
  and follow the second player's winning strategy in $H_0$.  So $P(G)$
  holds.

\item every $H \in \mathcal{G}$ has a winning strategy for its first
  player. Then the second player in $G$ has a winning strategy: if the
  first player's move in $G$ is to $H \in \mathcal{G}$, then follow the
  winning strategy for the first player in $H$.  So $P(G)$ holds.
\end{itemize}
So $P(G)$ holds in any case, which completes the proof of the Constructor
case.

It follows by structural induction that $P(G)$ holds for all $G \in \tg$.
\end{proof}


\iffalse

Another basic example of a recursive data type is the set, $\bins$, of
\emph{binary strings}, which we could define recursively as follows:
\begin{itemize}
\item \textbf{Base cases:} the empty sequence, $\lambda$, is an element of $\bins$.
\item \textbf{Constructor case:} If $s \in \bins$, then
\begin{enumerate}
 \item $s0 \in \bins$, and
 \item $s1 \in \bins$.
\end{enumerate}
\end{itemize}
This definition of $\bins$ assumes we already know that strings are
sequences of letters and digits, and that $s0$ is the sequence of letters
and digits in the string $s$ followed by the digit 0; similarly for $s1$.
In particular, $\lambda a = a$ is the length one sequence consisting of
just the letter or digit, $a$.
\fi


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

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

\end{example}


\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

\subsection{Functions on Recursively-defined Data Types}

Functions on recursively-defined data types can be defined recursively
using the same cases as the data type definition.  Namely, to define a
function, $F$, on a recursive data type, define the value of $F$ for the
base cases of the data type definition, and then define the value of $F$
in each constructor case in terms of the values of $F$ on the component
data items.

For example, from the recursive Definition~\ref{A*} of strings, we can
define:

\begin{definition}
The \emph{length}, $\lnth{s}$, of a string, $s$ is defined recursively by
the rules:
\begin{itemize}
\item $\lnth{\lambda} \eqdef 0$
\item $\lnth{sa} \eqdef 1+\lnth{s}$.
\end{itemize}
\end{definition}

\begin{definition}
The \emph{concatenation}, $st$, of a strings $s$ and $t$ over alphabet,
$A$, is defined recursively in $t$ by the rules:
\begin{itemize}
\item $s\lnth{\lambda} \eqdef 0$.
\item $s(ta) \eqdef (st)a$ for $a \in A$.
\end{itemize}
\end{definition}


For the set, $M$, of strings of matched parentheses, we 
define:
\begin{definition}
The \emph{depth}, $d(s)$, of a string, $s \in M$, is defined
recursively by the rules:
\begin{itemize}
\item $d(\lambda) \eqdef 0.$
\item $d(\texttt{(}s\texttt{)}t)
    \eqdef \max \set{d(s) + 1, d(t)}$
\end{itemize}
\end{definition}

textbox{\textbf{Warning:} When a recursive definition of a data type
allows the same element to be constructed in more than one way, the
definition is said to be \emph{ambiguous}.  A function defined recursively
from an ambiguous definition of a data type will not be well-defined
unless the values specified for the different ways of constructing the
element agree.}

We were careful to choose an \emph{un}ambigous definitions of the sets $M$
and $E$ to ensure that functions like $d$ defined recursively from their
definitions would always be well-defined.  Recursive definitions of tagged
data types, where the tag uniquely determines the rule used to construct
an element, are guaranteed to be unambiguous.


\subsubsection{Evaluation and Substitution}

We'll define some recursive functions on arithmetic expressions that
suggest the role of recursive definitions in computation.  For simplicity,
we'll work with arithmetic expressions with only one variable ---call it
$x$.  Now given such an expression, $e \in \aexp$, and an integer value,
$n$, for the variable, $x$, we can evaluate $e$ in the usual way to arrive
at an integer value, $\ms{eval}(e,n)$.  The $\ms{eval}$ function has a
familiar recursive definition:

\begin{definition}
The function $\ms{eval}$ is defined recursively on an expression, $e$, and
integer, $n$, as follows:

\begin{itemize}

\item $\ms{eval}(\ang{\texttt{integer}, k}, n) \eqdef k$,

\item  $\ms{eval}(\ang{\texttt{variable}, x}, n) \eqdef n$,

\item $\ms{eval}(\ang{\texttt{sum}, e, e'},n) =
  \ms{eval}(e,n)+\ms{eval}(e',n)$,

\item $\ms{eval}(\ang{\texttt{product}, e, e'},n) = \ms{eval}(e,n)\cdot
  \ms{eval}(e',n)$,

\item $\ms{eval}(\ang{\texttt{minus}, \ang{e}},n) = - \ms{eval}(e,n)$.
\end{itemize}
\end{definition}

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 the variable $x$ in $e$.  

\begin{definition}
The function $\ms{subst}$ is defined recursively on expressions $e$ and
$f$ as follows:

\begin{itemize}

\item $\ms{subst}(\ang{\texttt{integer}, k}, f) \eqdef k$,

\item  $\ms{subst}(\ang{\texttt{variable}, x}, f) \eqdef f$,

\item $\ms{subst}(\ang{\texttt{sum}, e, e'}, f) =
  \ang{\texttt{sum},\ms{subst}(e,f),\ms{subst}(e',f)}$,

\item $\ms{subst}(\ang{\texttt{product}, e, e'},f) =
  \ang{\texttt{product},\ms{subst}(e,f),\ms{subst}(e',f)}$,

\item $\ms{subst}(\ang{\texttt{minus}, \ang{e}},f) =  \ang{\texttt{minus},
  \ms{subst}(e,f)}$.
\end{itemize}
\end{definition}


Now suppose we substitute another expression, $f$, for all the $x$'s in
$e$ to obtain a new expression, $e' \eqdef \ms{subst}(e,f)$.  Now we could
evaluate $e'$ when $x$ has the value $n$ by directly applying \ms{eval}.
But another, usually more efficient, approach would be to find the value
of $f$ when $x$ has the value $n$, and then evaluate $e$ with $x$ given
the value obtained from $f$.\footnote{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.''}

For example, suppose (using ordinary formula notation for readability)
\begin{align}
e & \text{ is } x + x & \text{and}\\
f & \text{ is } 3x    & \text{so}\\
g & \eqdef \ms{subst}(e,f) = 3x + 3x.
\end{align}
Then in the evaluation of $g$ at $x=1$, two multiplications by 3 would be
performed.  But evaluating $f$ at $x=1$ involves only one multiplications
by 3, and then evaluating $e$ with $x= 3\cdot 1 = 3$ involves no further
multiplications.

We will prove that both approaches yield the same answer.  More precisely,
what we want to prove is
\begin{theorem}\label{environments}
For all expressions $e,f \in \aexp$ 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$.\footnote{This is an example
of why it's useful to notify the reader what the induction variable is
---in this case it isn't $n$.}

\textbf{Base cases}
\begin{itemize}

\item $e = \ang{\texttt{integer}, k}$.  Then the lefthand side of
equation~(\ref{eval-subst}) equals $k$ by this base case in the definition
of $\ms{subst}$, and the righthand side equals $k$ by this base case of
the definition of $\ms{eval}$.


\item $e = \ang{\texttt{variable}, x}$.  Then the lefthand side of
equation~\eqref{eval-subst} equals $\ms{eval}(f,n)$ by this base case in
the definition of $\ms{subst}$, and the righthand side also equals
$\ms{eval}(f,n)$ by this base case in the definition of
$\ms{eval}$.

\end{itemize}

\textbf{Constructor cases}:
\begin{itemize}

\item $e = \ang{\texttt{sum}, e_1, e_2}$.  By the structural induction
hypothesis~\eqref{eval-subst}, we may assume that for all $f \in \aexp$
and $n \in \naturals$,
\begin{equation}\label{hyp}
\ms{eval}(\ms{subst}(e_i,f),n)  =  \ms{eval}(e_i, \ms{eval}(f,n))
\end{equation}
for $i= 1,2$.  We wish to prove that
\begin{equation}\label{s+}
\ms{eval}(\ms{subst}(\ang{\texttt{sum}, e_1, e_2},f),n)  = 
   \ms{eval}(\ang{\texttt{sum}, e_1, e_2}, \ms{eval}(f,n)).
\end{equation}
But the lefthand side of~(\ref{s+}) equals
\[
\ms{eval}(\ang{\texttt{sum}, \ms{subst}(e_1,f), \ms{subst}(e_2,f)},n)
\]
by definition of $\ms{subst}$ for a sum expression, which equals
\[
\ms{eval}(\ms{subst}(e_1,f),n) + \ms{eval}(\ms{subst}(e_2,f),n)
\]
by definition of $\ms{eval}$ for a sum expression.  By induction
hypothesis~\eqref{hyp}, this equals
\[
\ms{eval}(e_1,\ms{eval}(f,n)) + \ms{eval}(e_2,\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.

\item  $e = \ang{\texttt{product}, e_1, e_2}$ or  $e =
  \ang{\texttt{minus}, e_1}$. Similar.

\end{itemize}

\end{proof}


\subsection{Recursive Functions on Natural Numbers}

Definition~\ref{tagn} of the nonnegative integers as a recursive tagged
data type justifies the familiar recursive definitions of functions on the
natural numbers.  Here are some examples.

\begin{description}
\item[The Factorial function], $\text{fac}(n)$, often written $n!$.  This is
function you will see a lot of later in the term.
\begin{itemize}
\item $\text{fac}(0) \eqdef 1$.
\item $\text{fac}(n+1) \eqdef (n+1)\text{fac}(n)$ for $n \ge 0$.
\end{itemize}

\item[The Fibonacci numbers.] These form interesting sequence of numbers
that arise, in biology, where they model some types of growth processes
(plants, cells, rabbit populations, etc.).  Letting $\text{fib}(n)$ be the
$n$th Fibonacci number, $\text{fib}$ can be defined recursively by:
\begin{align*}
\text{fib}(0) &\eqdef 0,\\ 
\text{fib}(1) &\eqdef 1,\\ 
\text{fib}(n) &\eqdef \text{fib}(n-1) + \text{fib}(n-2) &\mbox{for $n \geq 2$.} 
\end{align*}
Here the recursive step starts at $n=2$ with base cases for 0 and 1.  This
is needed since the constructor case relies on two previous values.

What is $\text{fib}(4)$?  Well, $\text{fib}(2) =
\text{fib}(1)+\text{fib}(0) = 1$, $\text{fib}(3) =
\text{fib}(2)+\text{fib}(1) = 2$, so $\text{fib}(4) = 3$.  The sequence
starts out $0, 1, 1, 2, 3, 5, 8, 13, 21,\dots$.

\item[Sum-notation], $S(n) \eqdef \sum_{i=1}^n f(i)$.
  \begin{itemize}
  \item $S(0) \eqdef 0$.
  \item $S(n+1) \eqdef  f(n+1) + S(n)$ for $n\geq 0$.
  \end{itemize}

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

\end{description}

\iffalse

\begin{optional}


We can use the recursive definition of a function to establish its
properties by structural induction.


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

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

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

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

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

\end{optional}
\fi

\subsubsection{Ill-formed Function Definitions}

There are some \hyperdef{ill}{formed}{blunders} to watchout for when
defining functions recursively.  Below are some function specifications
that resemble good definitions of functions on the natural numbers, but
they aren't.

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

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

\begin{eqnarray}\label{f3}
f_3(n) \eqdef
\begin{cases}
 0, & \text{if $n=0$,}\\
 f_3(n+1)+1, & \text{otherwise.}
\end{cases}
\end{eqnarray}
``Definition''~(\ref{f3}) impliles that $f_3(1) > f_3(2) > f_3(3) \cdots
>$, so $f_3(1)$ cannot equal any integer.  No total function on the
natural numbers can satisfy this definition.\footnote{It does uniquely
determine a \emph{partial} function on the natural numbers, namely,
$f_3(0) = 0$ and $f_3$ is undefined everywhere else, if we accept the
convention that $f(a)=f(b)$ holds when $f$ is not defined for both $a$ and
$b$.}

\begin{eqnarray}\label{f4}
f_4(n) \eqdef
\begin{cases}
 0, & \text{if $n=0$},\\
 f_4(n+1) &  \text{otherwise}.
\end{cases}
\end{eqnarray}
Any function that is 0 at 0 and constant everywhere else
satisfies~(\ref{f4}), so it does not uniquely define anything.

A mystery: Mathematicians have been wondering about this one for a while:
\begin{eqnarray}\label{f5}
f_5(n) \eqdef\begin{cases}
 1, & \text{if $n\le 1$},\\
 f_5(n/2) &  \text{if $n>1$ is even},\\
 f_5(3n+1)& \text{if $n>1$ is odd}.
\end{cases}
\end{eqnarray}
For example, $f_5(3)=1$ because
\[
f_5(3)\eqdef f_5(10)\eqdef f_5(5)\eqdef f_5(16)\eqdef f_5(8)\eqdef
f_5(4)\eqdef f_5(2)\eqdef f_5(1)\eqdef 1.
\]
The constant function equal to 1 will satisfy~\eqref{f5}, but it's not
known if another function does as well. The problem is that the third case
specifies $f_5(n)$ in terms of $f_5$ at arguments larger than $n$, and so
cannot be justified by induction on $\naturals$.  It's known that any
$f_5$ satisfying~\eqref{f5} equal 1 for all $n$ up to over a billion, and
it seems a good guess that the only $f_5$ that works is the constant
function equal to 1.

\textbf{Quick exercise:} Why does the constant function 1
satisfy~\eqref{f5}?

\iffalse

\section{Induction in Computer Science}

We've 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 on some data types with infinite
elements.  It is a technique which every Computer Scientist should firmly
grasp.
\fi

\section{State machines}

State machines are an abstract model of step-by-step processes, and
accordingly, they come up in many areas of Computer Science.  You may
already have seen them in a digital logic course, a compiler course, or a
probability course.

\subsection{Basic definitions}

A state machine is really nothing more than a binary relation on a set,
except that the elements of the set are called ``states'' and a pair
$(p,q)$ in the graph of the relation is called a ``transition.''  The
transition from state $p$ to state $q$ will be written $p \rightarrow q$.
A state machine also comes equipped with a designated \emph{start state}.

State machines used in digital logic and compilers usually have only a
finite number of states, but machines that model continuing computations
typically have an infinite number of states.  In many applications, the
states or transitions are labelled with tokens indicating inputs or
outputs, or numbers indicating costs, capacities or probabilities.  In
these Notes, we'll stick to unlabelled states and transitions.\footnote{We
do label states, as in Figure~\ref{fig:counter}, so we can talk about
them, but the labels aren't part of the state machine.}

\begin{example}
A bounded counter, which counts from $0$ to $99$ and overflows at 100.
The transitions arepictured in Figure~\ref{fig:counter}, with
start state zero.

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

This machine isn't much use once it overflows, since it has no way to get
out of its overflow state.

\end{example}

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

\begin{example}
\textbf In the movie \textit{Die Hard 3: With a Vengeance}, the characters
played by Samuel L. Jackson and Bruce Willis have to disarm a bomb planted
by the diabolical Simon Gruber:

\textbox{
\begin{list}{}{\itemsep=0in \leftmargin=0.25in \rightmargin=0.25in}

\item[\textbf{Simon:}] On the fountain, there should be 2 jugs, do you
see them?  A 5-gallon and a 3-gallon.  Fill one of the jugs with
exactly 4 gallons of water and place it on the scale and the timer
will stop.  You must be precise; one ounce more or less will result in
detonation.  If you're still alive in 5 minutes, we'll speak.

\item[\textbf{Bruce:}] Wait, wait a second. I don't get it. Do you get it?

\item[\textbf{Samuel:}] No.

\item[\textbf{Bruce:}] Get the jugs. Obviously, we can't fill the 3-gallon jug
with 4 gallons of water.

\item[\textbf{Samuel:}] Obviously.

\item[\textbf{Bruce:}] All right. I know, here we go. We fill the 3-gallon jug
exactly to the top, right?

\item[\textbf{Samuel:}] Uh-huh.

\item[\textbf{Bruce:}] Okay, now we pour this 3 gallons into the 5-gallon jug,
giving us exactly 3 gallons in the 5-gallon jug, right?

\item[\textbf{Samuel:}] Right, then what?

\item[\textbf{Bruce:}] All right. We take the 3-gallon jug and fill it a third
of the way...

\item[\textbf{Samuel:}] No!  He said, ``Be precise.''  Exactly 4
gallons.

\item[\textbf{Bruce:}] Sh - -.  Every cop within 50 miles is running his a - - off
and I'm out here playing kids games in the park.

\item[\textbf{Samuel:}] Hey, you want to focus on the problem at hand?

\end{list}
}

Fortunately, they find a solution in the nick of time.  We'll let the
reader work out how.

The \emph{Die Hard} series is getting tired, so we propose a final
\emph{Die Hard Once and For All}.  Here Simon's brother returns to avenge
him, and he poses the same challenge, but with the 5 gallon jug replaced
by a 9 gallon one.

We can model jug-filling scenarios with a state machine.  In the scenario
with a 3 and a 5 gallon water jug, the states will be pairs, $(b,l)$ of
real numbers such that $0 \leq b \leq 5, 0 \leq l \leq 3$.  We let $b$ and
$l$ be arbitrary real numbers.  (We can prove that the values of $b$ and
$l$ will only be nonnegative integers, but we won't assume this.)  The
start state is $(0,0)$, since both jugs start empty.

Since the amount of water in the jug must be known exactly, we will only
consider moves in which a jug gets completely filled or completely
emptied.  There are 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}


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.

\textbf{Quickie exercise:} Which states of the Die Hard 3 machine have
direct transitions to exactly two states?

\end{example}

\subsection{Reachability and Invariants}

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's characters will disarm the bomb if he can get to some
state of the form $(4, l)$.

A (possibly infinite) sequence of transitions through successive states
beginning at the start state corresponds to a possible system behavior;
such a sequence is called an \emph{execution} of the state machine.  A
state is called \emph{reachable} if it appears in some execution.  The
bomb in Die Hard 3 gets disarmed successfully because the state (4,3) is
reachable.

A useful approach in analyzing state machine is to identify
\emph{invariant} properties of states.
\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 Induction in a special form for state machines:
\begin{theorem}[Invariant Theorem]
Let $P$ be an invariant predicate for a state machine.  If $P$ holds for
the start state, then $P$ holds for all reachable states.
\end{theorem}

The Invariant Theorem follows by induction on the length of an execution.
It's obvious enough not to need proof.


\subsubsection{Die Hard Once and For All}

Now back to Die Hard Once and For All.  This time there is a 9 gallon jug
instead of the 5 gallon jug.  We can model this with a state machine whose
states and transitions are specified the same way 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.  We prove this
using the Invariant Theorem.  Namely, we define the invariant predicate,
$P((b.l))$, to be that $b$ and $l$ are nonnegative integer mulitples of 3.
So $P$ obviously holds for the state state $(0,0)$.

To prove that $P$ is an invariant, we assume $P((b,l)$ holds for some
state $(b.l)$ and show that if $(b,l) \rightarrow (b',l')$, then
$P(b',l')$.  The proof divides into cases, according to which transition
rule is used.  For example, suppose the transition followed from the
``fill the little jug'' rule.  This means $(b,l) \rightarrow (b,3)$.  But
$P((b,l)$ impiles that $b$ is an integer multiple of 3, and of course 3 is
an integer multiple of 3, so $P$ still holds for the new state $(b,3)$.
Another example is when the transition rule used is ``pour from big jug
into little jug'' for the subcase that $b + l > 3$.  Then state is $(b,l)
\rightarrow (b -( 3 -l), 3)$.  But since $b$ and $l$ are integer multiples
of 3, so is $b -( 3 -l)$.  So in this case too, $P$ holds after the
transition.

We won't bother to crank out the remaining cases, which can all be checked
with equal ease.  Now by the Invariant Theorem, we conclude that every
reachable state satisifies $P$.  But since no state of the form $(4,l)$
satisifies $P$, we have rigorously proved that Bruce dies once and for
all!

\subsubsection{A Robot on a Grid}

There is a robot.  It walks around on a grid, and at every step it moves
diagonally in a way that changes its position by one unit up or down
\emph{and} one unit left or right.  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 model the problem as a state machine and then prove a suitable
invariant.  A state will be a pair of integers corresponding to the
coordinates of the robots position.  State $(i,j)$ has transitions to
four different states: $(i \pm 1, j \pm 1)$.

The problem is now to choose an appropriate invariant predicate, $P$, that
is true for the start state $(0,0)$ and false for $(1, 0)$.  The Invariant
Theorem then will imply 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.  Consider the state $(2,1)$.  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 the start state $(0,0)$.
Clearly, $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$
or $i + j \pm 2$, all of which are even.
\end{proof}

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

\begin{notesproblem}
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).

\insolutions{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{notesproblem}

\subsection{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 transformed the field of programming language parsing; 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 theoretical 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 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 before Meyer understood Floyd's excitement
---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.  A eulogy describing Floyd's life and work by his closest
colleague, Don Knuth, can be found at
\href{http://www.acm.org/pubs/membernet/stories/floyd.pdf}
{\texttt{http://www.acm.org/pubs/membernet/stories/floyd.pdf}}.

\subsubsection{Proving Correctness}

Floyd distinguished 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 he 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 he meant.  The word
``partial'' comes from viewing a process that might not terminate as
computing a \emph{partial function}.  So partial correctness means that
when there is a result, it is correct, but the process might not always
produce a result, perhaps because it gets stuck in a loop.

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

Partial correctness can commonly be proved using the Invariant Theorem.
Termination can commonly be proved using the Well-ordering Principle.
We'll illustrate Floyd's ideas by verifying the Euclidean Greatest Common
Divisor (GCD) Algorithm.

\subsubsection{The Euclidean Algorithm}\label{euclid}

The Euclidean algorithm is a three thousand year old procedure to compute
the greatest common divisor, $\gcd(a,b)$ of integers $a$ and $b$.
We can represent this algorithm as a state machine.  A state will be a
pair of integers $(x,y)$ which we can think of as integer registers in a
register program.  The state transitions are defined by the rule
\begin{align*}
(x,y) & \rightarrow (y, \remainder(x,y)) & \text{if $y \neq 0$}.
\end{align*}
The algorithm terminates when no further transition is possible, namely
what $y=0$.  The final answer is in $x$.

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

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

\end{enumerate}

\paragraph{Partial Correctness of GCD}

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

\begin{proof}
Define the state predicate
\[
P((x,y)) \eqdef\ \ [\gcd(x,y) = d \text{ and } (x > 0 \text{ or } y > 0)].
\]

$P$ holds for the start state $(a,b)$, by definition of $d$ and the
requirement that at least one $b$ is positive.  Also, the invariance of
$P$ follows immediately from
\begin{lemma}
For all $m,n \in \naturals$ such that $n \neq 0$,
\begin{equation}\label{gcd}
\gcd(m,n) = \gcd(y,\remainder(m,n)).
\end{equation}
\end{lemma}
Lemma~\ref{gcd} is easy to prove, and we'll leave it to the reader (a
proof will appear in later Notes on elementary Number Theory).  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
$(x,y)$ is a terminal state, then $y=0$.  If this terminal state is
reachable, then the invariant holds for $(x,y)$.  This implies that
$\gcd(x,0) = d$ and that $x>0$.  We conclude that $x = \gcd(x,0) = d$.
\end{proof}

\paragraph{Termination of GCD}

Now we turn to the second property, that the procedure must terminate.  To
prove this, notice that $y$ gets strictly smaller after any one
transition.  That's because the 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
Well Ordering Principle, it reaches 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
state at which no further step is possible, that is, at which the
procedure terminates.

Note that this argument does not prove that the minimum value of $y$ is
zero, only that the minimum value occurs at termination.  But we already
noted that the only rule for termination is that $y=0$, so it follows that
the minimum value of $y$ must indeed be zero.

\subsubsection{The Extended Euclidean Algorithm}

An important fact about the $\gcd{a,b}$ is that it equals an integer
linear combination of $a$ and $b$, that is,
\begin{equation}\label{sa}
\gcd{a,b} = sa+ tb
\end{equation}
for some $s,t \in \naturals$.  We'll see some nice proofs of~\eqref{sa} in
later Notes, but there is also an extension of the Euclidean Algorithm
that efficiently, if obscurely, produces the desired $s$ and $t$.  In
particular, given natural numbers $x$,$y$, with $y>0$, we claim the
following procedure\footnote{This procedure is adapted from Aho, Hopcroft,
and Ullman's text on algorithms.}  halts with integers $s,t$ in registers
\texttt{S} and \texttt{T} satisfying~\eqref{sa}.

Inputs: $a,b \in \naturals, b>0$.

Registers: \texttt{X,Y,S,T,U,V,Q}.

Extended Euclidean Algorithm:
\begin{center}
\begin{verbatim}
X := a; Y := b; S := 0; T := 1; U := 1; V := 0; 
loop:
if Y|X, then halt
else
  Q := quotient(X,Y);
         ;;the following assignments in braces are SIMULTANEOUS
 {X := Y,
  Y := remainder(X,Y);
  U := S,
  V := T,
  S := U - Q * S,
  T := V - Q * T};
goto loop;
\end{verbatim}
\end{center}

Note that \texttt{X,Y} behave exactly as in the Euclidean GCD algorithm in
Section~\ref{euclid}, except that this extended procedure stops one step
sooner, ensuring that $\gcd(x,y)$ is in \texttt{Y} at the end.  So for all
inputs $x,y$, this procedure terminates for the same reason as the
Euclidean algorithm: the contents, $y$, of register \texttt{Y} is a
nonnegative integer-valued variable that strictly decreases each time
around the loop.

We claim that invariant properties that can be used to prove partial
correctness are:
\begin{eqnarray}
\gcd(X,Y) &=& \gcd(a,b), \label{(a)}\\
Sa+Tb &=& Y,\text{ and }\label{(b)}\\
Ua+Vb &=& X. \label{(c)}
\end{eqnarray}

To verify these invariants, note that invariant~(\ref{(a)}) is the same
one we observed for the Euclidean algorithm.  To check the other two
invariants, let $x,y,s,t,u,v$ be the contents of registers
\texttt{X,Y,S,T,U,V} at the start of the loop and assume that all the
invariants hold for these values.  We must prove that~(\ref{(b)})
and~(\ref{(c)}) hold (we already know~(\ref{(a)}) does) for the new
contents $x',y',s',t',u',v'$ of these registers at the next time the loop
is started.

Now according to the procedure, $u'=s,v'=t,x'=y$, so invariant~\eqref{(c)}
holds for $u',v',x'$ because of invariant~\eqref{(b)} for $s,t,y$.  Also,
$s'= u - qs, t'= v - qt, y' = x - qy$ where $q = \quotient(x,y)$, so
\[
s'a+t'b = (u-qs)a + (v-qt)b =ua+vb - q(sa+tb) = x - qy = y',
\]
and therefore invariant~\eqref{(b)} holds for $s',t',y'$.

Also, it's easy to check that all three invariants are true just before
the first time around the loop.  Namely, at the start $X=a, Y=b, S=0, T=1$
so $Sa+Tb=0a+1b=b=Y$ so~(b) holds; also $U=1, V=0$ and $Ua+Vb= 1a+0b=a =X$
so~(\ref{(c)}) holds.  So by the Invariant Theorem, they are true at
termination.  But at termination, the contents, $Y$, of register
\texttt{Y} divides the contents, $X$, of register \texttt{X}, so
invariants~(\ref{(a)}) and~(\ref{(b)}) imply
\[
\gcd(a,b) = \gcd(X,Y) = Y = Sa + Tb.
\]
So we have the gcd in register \texttt{Y} and the desired coefficients in
\texttt{S}, \texttt{T}.


\subsection{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 Well Ordering 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: \text{states } \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}$, where $x\text{-coord}((i, j))
\eqdef~i$.

We can formulate our general termination method as follows:

\begin{definition}
A derived variable $f : \text{states } \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$ is a strictly decreasing derived variable of a state machine that
takes only nonnegative integer values, then the length of any execution
starting at 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 too obvious to warrant 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 partial ordered sets.  It's useful to generalize the familiar
notations $\leq$ and $<$ for ordering the real numbers: if $\prec$ is a
strict partial order on some set, $A$, then define $\preceq$ to be the
corresponding \emph{weak} partial order
\[
a\preceq a' \ \eqdef\quad a \prec a' \lor a = a'.
\]
\iffalse
A relation like $\prec$ is called a \emph{strict} partial order.  It is
transitive, antisymmetric, and but \emph{non}reflexive in the strongest
sense: $a \not\prec a$ for every $a \in A$.\footnote{In other words, if $a
\prec b$, then it is not the case that $b \prec a$.  This property is also
called \emph{a}symmetry.}\fi

\begin{definition}
Let $\prec$ be a strict partial order on a set, $A$.  A derived variable
$f : Q \to A$ is \emph{strictly decreasing} with respect to $\prec$ 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.

\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.pdf}
\caption{\em Bob is married to Carol, and Ted is married to Alice, but Ted
prefers Carol to 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 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 first
published in a paper by D. Gale and L.S. Shapley in 1962.  At the time of
publication, Gale and Shapley were unaware of perhaps the most impressive
example of the algorithm.  It was used to assign 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?\footnote{``Greedy'' is not any
moral judgment.  It refers to algorithms that work by always choosing the
next state that makes the largest immediate progress.}  We simply 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$, try to show that neither of these two will be
involved in a rogue couple, and then solve the remaining problem by
induction.  Clearly Boy 1 will never leave his top pick, Girl $C$.  But
the problem with this approach is that we \emph{can't} be sure that Girl
$C$ won't be in a rogue couple.  Girl $C$ might very well dump Boy 1 --
she might even rate him last!

This turns out to be a tricky problem.  The best approach is to use a
mating ritual that is reputed to have been popular in some mythic past.

\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\dots, 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 should have clear mathematical
definitions of what we're talking about.  In this section we sketch how to
define a rigorous state machine model of the Marriage Problem.

So let's begin by formally 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.

To model the Mating Algorithm with a state machine we make a key
observation: 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 a state to some mathematical data structure providing this
information.  Namely, define a state to be the ``still-has-on-his-list''
relation, $R$, between boys and girls.  So $B\,R\,G$ means girl $G$ has not
been crossed off boy $B$'s list.

We start the Mating Algorithm with no girls crossed off.  So in the start
state is the \emph{complete bipartite} relation in which every boy is
related to every girl.

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.
Mathematically, the girl he is serenading is just the maximum girl under
$B$'s ordering $<_B$ among the girls on $B$'s list.  (If the list is
empty, he's not serenading anybody.)

We could go on to define a girl's favorite to be the maximum under her
preference ordering among the boys serenading her.  We could go on
similarly to specify the state transitions with precise mathematical
rules, but we won't bother.  The point is that if need be, we could define
everything using basic mathematical data structures like sets, functions,
and relations.  But let's stick with the intuitive vocabulary of boys and
girls and their preferences.

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

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

We still have to prove that the Mating Algorithm leaves everyone in a
stable marriage.  To do this, we note one very useful fact 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.  So day by day, her favorite suitor can stay the same or
get better, never worse.  In others words, a girl's favorite is a weakly
increasing variable with respect to her preference order on the boys.

Now we can verify the Mating Algorithm using a simple invariant predicate,
$P$, that captures what's going on:
\begin{quotation}\noindent
For every girl, $G$, and every boy, $B$, if $G$ is crossed off $B$'s list,
then $G$ has a favorite suitor and she prefers him over $B$.
\end{quotation}

Why is $P$ invariant?  Well, we know that $G$'s favorite tomorrow will be
at least as desirable to her 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: a boy only serenades one girl,
so 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 Bob be some boy and Carole be any girl that he is \emph{not} married
to on the last day of the Mating ritual.  We will prove that Bob and
Carole are not a rogue couple.  Since Bob was an arbitrary boy, 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.  Carole is not on Bob's list.  Then since invariant $P$
holds, we know that Carole prefers her husband to Bob.  So she's not going
to run off with Bob: the claim holds in this case.

\emph{Case} 2.  Otherwise, Carole is on Bob's list.  But since Bob is not
married to Carole, he must have chosen to serenade his wife instead of
Carole, so he must prefer his wife.  So he's not going to run off with
Carole: 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, we know
their suitors can only change for the better as the Algorithm progresses.

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 from the boy's point of view, the
girl he is serenading can only change for the worse.  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.
The mating algorithm actually does as well as possible for all the boys
and 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 pop star Ashlee Simpson: 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 Ashlee 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 Well Ordering 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 the
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}
