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

\lectureformat

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

\askaboutsolutions

\begin{document}

\lecture{notes6}{Computational Processes}{Oct 9, 2001}{\stamp}

\section{Modeling Processes}
The 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.

We will model algorithms and computational processes as \emph{state
machines}.  It's useful to distinguish two aspects of 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 does produce some output.  This
is called \emph{termination}.

\end{enumerate}

The most important idea for analyzing state machines is that of an
``invariant'', which describes a property of states that will remain true,
no matter how the state machine progresses.  You will see how invariants
can be used to prove partial correctness.  We'll also discuss some simple
methods for proving termination.

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{problems}
\problem Which states of the Die Hard 3 machine have direct transitions to
exactly two states?
\end{problems}

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!

\subsection{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{defin}
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{defin}

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.

\section{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 & \ints \cross \ints,\\
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{problems}
\problem
Consider two-dimensional board, represented by the integer grid. 
A robot 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).

\solnospace{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{problems}

\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 a month
ago (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 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 \nats \cross \nats$,

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

We will prove that this state machine correctly computes
$\ms{GCD}(a,b)$.  It is convenient to break this claim down into two
parts:

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

First let's prove the algorithm is correct.  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 \nats$ 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}

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}
Suppose $a \in \reals, b \in \nats$, and consider the following algorithm
to compute $a^b$: 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 \nats$,
\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.

\begin{problems}
\problem The naive way to compute $a^b$ would be to multiply $a$ by itself
$b$.  Our ``fast'' exponentiation algorithm is really much faster.  Prove
that it requires at most $2 \log_2 b$ multiplications to compute $a^b$ for
$b>1$.
\end{problems}

\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}.  We'll see that several derived variables are
helpful in explaining a very elegant procedure to solve the so-called
Stable Marriage Problem in the next section.

As an example, for the Die Hard machines above, 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}
Let $<$ be a partial order on a set, $A$.  A derived variable $f : Q \to
A$ is {\em decreasing} iff $q \rightarrow q'$ implies $f(q') \neq
f(q)\text{ and } f(q') < f(q)$.
\end{definition}

\begin{theorem}
\label{th:decr}
If $f : Q \to \nats$ is a 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 decreasing natural-number-valued derived variable for
some state machine, then every execution of that machine terminates.
\end{corollary}

One can define other useful flavors of derived variable, for example:

\begin{definition}
Let $<$ be a partial order on a set, $A$.  A derived variable
$f : Q \to A$ is \emph{nonincreasing} iff $q \rightarrow q'$ implies
$f(q') < f(q) \text{ or } f(q) = f(q')$.
\end{definition}
\emph{Increasing} and \emph{nondecreasing} derived variables are defined
similarly.

The existence of a natural-number-valued nonincreasing derived variable
does not guarantee that every execution terminates.  That's because a
derived variable that is constant is a special case of a nonincreasing
derived variable, and an infinite execution could proceed through states
in which the nonincreasing derived 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 nondecreasing 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 nondecreasing.

\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 \nats$
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 \in \sere_q(B) \neq \none}.
\]

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

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:
the formula:
\[
\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 $<_G$-nondecreasing 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 $<_B$-nonincreasing 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 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}
On the last day of the Mating ritual each girl has at most one suitor,
and if she has a suitor, that is whom she marries.  Since each boy
serenades at most one girl on any day, the suitors of different girls must
be different boys.  So the ritual yields a set of marriages between some
of the girls and an equal number of boys.  We have to show that all the
girls and all the boys are married on the last day.  Since there are the
same number of boys as girls, all we have to show is that either all the
boys are married or all the girls are.

Suppose, for the sake of contradiction, that some boy is not married.
That means his list is 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 is married to.  So all the boys must also be
married, a contradiction.
\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}
