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

\renewcommand{\coursecopyrightnames}
{\href{http://theory.lcs.mit.edu/~meyer}{Prof.~Albert~R.~Meyer}}
%\renewcommand{\coursecopyrightyear}{2002}
%\graphicspath{/toc/a/class/6.042/fall02/problemrepository/figures/}

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


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

\begin{document}
\lecturenotes{5}{State Machines: Invariants and Termination}


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

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

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

\section{Die Hard}

In the movie Die Hard 3, Bruce Willis and Samuel Jackson are coerced by a
homicidal 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 are 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 will 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 = \set{(0,0)}$ (because both jugs start empty). 

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

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

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

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

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

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

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

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

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

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

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


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

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

In graph language, a (possibly infinite) path through the state machine
graph beginning at a start state corresponds to a possible system behavior
or process execution.  A state is reachable if there is a path
to it starting from one of the start states.  Formally,
\begin{definition}
An \emph{execution} is a (possibly infinite) sequence of states $q_0, q_1,
\ldots$ such that $q_0 \in Q_0$, and \iffalse $\forall i \geq 0\,
(q_i,q_{i+1}) \in \delta$, that is,\fi
\[
q_0 \rightarrow q_1 \rightarrow q_2 \cdots.
\]
A state is \emph{reachable} providing it 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 Hard Once and For All.  The problem is still to measure out
four gallons, but with a nine gallon jug instead of the five gallon one.
The states and transition relation are the same as for the Die Hard 3
machine, with all occurrences of ``5'' replaced by ``9.''

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

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

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

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

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

\section{Reachability and Invariants}

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

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

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

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

\subsection{The Robot}

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

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

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

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

Unfortunately, this is not going to work.  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 all start states.  But
the only start state is (0,0), and $P((0, 0))$ is true because $0 + 0$ is
even.

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

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

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

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

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

\section{Sequential algorithm examples}

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

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

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

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

In this section of Notes we will describe two classic examples
illustrating program verification via the Invariant Theorem: the Euclidean
Greatest Common Divisor (GCD) Algorithm and ``Fast'' exponentiation.

\subsection{Proving Correctness}

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

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

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

Partial correctness can commonly be proved using the Invariant Theorem.

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

Given two natural numbers, $a, b$, at least one of which is positive, the
three thousand year old Euclidean algorithm will compute their greatest
common divisor, $\gcd(a,b)$.  This is the largest integer that divides
both $a$ and $b$.

The algorithm uses two registers $x$ and $y$, initialized
at $a$ and $b$ respectively.  Then,
\begin{itemize}
\item if $y = 0$, \textbf{return} the answer $x$ and terminate,

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

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

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

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

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

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

\end{itemize}

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

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

\end{enumerate}

\subsubsection{Partial Correctness of GCD}

First let's prove that if GCD gives an answer, it is a correct answer.
Specifically, let $d \eqdef \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\ \ [\gcd(x,y) = d].
\]

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

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

\subsubsection{Termination of GCD}

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

To prove this, notice that $y$ gets strictly smaller after any one
transition.  That's because value of $y$ after the transition is the
remainder of $x$ divided by $y$, and this remainder is smaller than $y$ by
definition.  But the value of $y$ is always a natural number, so by the
Least Number Principle, it 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
terminated reachable state.

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.

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

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

To be precise about the claim, we model this algorithm with a state
machine:
\begin{enumerate}
\item $Q \eqdef\ \ \reals \cross \reals \cross \naturals$,
\item $Q_0 \eqdef\ \ \set{(a,1,b)}$,
\item transitions
\begin{equation*}
(x,y,z) \rightarrow
\begin{cases}
(x^2, y, \quotient(z,2)) & \text{if $z$ is positive and even},\\
(x^2, xy, \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 the machine will reach \emph{some} state in which it
returns the answer $d$.\footnote{In a nondeterministic machine, there
might be some states that returned the right answer, but also some that
returned the wrong answer, so proving that a nondeterministic machine not
only \emph{can} return a correct answer, but \emph{always} returns a
correct one, tends to be more of a burden than for deterministic
machines.}  Since the machine stops only when $z=0$---at which time it
returns $y$---all we need show 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$.

We claim that predicate, $P$, is an invariant, where
\[
P((x,y,z)) \eqdef\ \ [yx^z = d].
\]
This claim is easy to check, and we leave it to the reader.

Also, $P$ holds for the start state $(a,1,b)$ since $1\cdot a^b = a^b =d$
by definition.  So by the Invariant Theorem, $P$ holds for all reachable
states.  But only terminating states are those with $z = 0$, so if any
terminating state $(x,y,0)$ is reachable, then $y = yx^0 = d$ as required.
So we have proved partial correctness.

Note that as is often the case with induction proofs, the proof is
completely routine once you have the right invariant (induction
hypothesis).  Of course, the 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?  But notice that $z$ is a natural-number-valued
variable that gets smaller at every transition.  So again by the Least
Number Principle, we conclude that the algorithm will terminate.  In fact,
because $z$ generally decreases by more than one at each step, we can say
more:

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

\begin{optional}

\subsection{Extended GCD}

An important elementary fact from number theory is that the gcd of two
natural numbers can be expressed as an integer linear combination of them.
In other words,
\begin{theorem}\label{egcd}
\[
\forall m,n \in \naturals\, \exists k,l \in \integers\ \gcd(m,n) =  km+ln.
\]
\end{theorem}

We will prove Theorem~\ref{egcd} by extending the Euclidean Algorithm to
actually calculate the desired integer coefficients $k$ and $l$.  In
particular, given natural numbers $m,n$, with $n>0$, we claim the
following procedure\footnote{This procedure is adapted from Aho, Hopcroft,
and Ullman's text on algorithms.} halts with integers $k,l$ in registers
\texttt{K} and \texttt{L} such that
\[
km+ln = \gcd(m,n).
\]

Inputs: $m,n \in \naturals, n>0$.

Registers: \texttt{X,Y,K,L,U,V,Q}.

Extended Euclidean Algorithm:
\begin{center}
\begin{verbatim}
X := m; Y := n; K := 0; L := 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 := K,
  V := L,
  K := U - Q * K,
  L := V - Q * L};
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(m,n)$ is in \texttt{Y} at the end.  So
for all inputs $m,n$, this procedure terminates for the same reason as the
Euclidean algorithm: the contents, $y$, of register \texttt{Y} is a
natural number-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(m,n), \label{(a)}\\
Km+ Ln &=& Y,\text{ and }\label{(b)}\\
Um+Vn &=& 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,k,l,u,v$ be the contents of registers
\texttt{X,Y,K,L,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',k',l',u',v'$ of these registers at the next time the loop
is started.

Now according to the procedure, $u'=k,v'=l,x'=y$, so invariant~(\ref{(c)})
holds for $u',v',x'$ because of invariant~(\ref{(b)}) for $k,l,y$.  Also,
$k'= u - qk, l'= v - ql, y' = x - qy$ where $q = \quotient(x,y)$, so
\[
k'm+l'n = (u-qk)m + (v-ql)n =um+vn - q(km+ln) = x - qy = y',
\]
and therefore invariant (b) holds for $k',l',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=m, Y=n, K=0, L=1$
so $Km+Ln=0m+1n=n=Y$ so~(b) holds; also $U=1, V=0$ and $Um+Vn= 1m+0n=m =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(m,n) = \gcd(X,Y) = Y = Km + Ln.
\]
So we have the gcd in register \texttt{Y} and the desired coefficients in
\texttt{K}, \texttt{L}.

\end{optional}


\section{Derived Variables}

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

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

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

We can formulate our general termination method as follows:

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

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

Of course we could prove Theorem~\ref{th:decr} by induction on the value
of $f(q)$.  But think about what it says: ``If you start counting down at
some natural number $f(q)$, then you can't count down more than $f(q)$
times.''  Put this way, the theorem is so obvious that no one should feel
deprived that we are not bothering with 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 $\preceq$ is a
partial order on some set $A$, then define $\prec$ by the rule
\[
a\prec a' \ \eqdef\quad a \preceq a' \land a \neq a'.
\]
\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 $\preceq$ be partial order on a set, $A$.  A derived variable
$f : Q \to A$ is \emph{strictly decreasing} iff
\[
q \rightarrow q' \text{  implies  } f(q') \prec f(q).
\]
It is \emph{weakly decreasing} iff
\[
q \rightarrow q' \text{  implies  } f(q') \preceq f(q).
\]
\end{definition}
\emph{Strictly increasing} and \emph{weakly increasing} derived variables
are defined similarly.\footnote{Weakly increasing variables are often also
called \emph{nondecreasing}.  We will avoid this terminology to prevent
confusion between nondecreasing variables and variables with the much
weaker property of \emph{not} being a decreasing variable.}

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

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

\section{The Stable Marriage Problem}

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

\subsection{The Problem}

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

The general goal is to marry off boys and girls so that everyone is happy;
we'll be more precise in a moment.  Every boy must marry exactly one girl
and vice-versa---no polygamy.

If we want these marriages to last, then we want to avoid an unstable
arrangement:

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

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

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

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

Now we can state the \emph{Stable Marriage Problem} precisely: find
spouses for everybody so that the resulting 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 is an algorithm classification that you can learn about
in an Algorithms course like 6.046.}  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 describe a
state machine model of the Marriage Problem, and show how to give precise
mathematical definitions of concepts we need to explain it, \eg who
serenades who, who's a favorite suitor, \etc It's probably a good idea to
skim the rest of this section and refer back to it only if a completely
precise definition is needed.

\begin{optional}
So let's begin by defining the problem.

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

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

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

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

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

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

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

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

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

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

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

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

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

\end{optional}

\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 derived variable $\tgn$ of a state, $q$, to be the
total number of list entries:
\[
\tgn(q) \eqdef\ \ \sum_{B \in \boys} \card{q(B)}.
\]
Then $\tgn$ is a strictly decreasing natural-number-valued derived
variable whose initial value, $\tgn(\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
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$.\footnote{The
formula would be:
\[
P(q) \eqdef\ \ [\forall B \in \boys\, \forall G \in \girls\; G \notin q(B)
              \qimplies B <_G \fav_q(G)],
\]
with $<_G$ extended to \boyn\ by the rule that $\none <_G B$ for all boys,
$B$.}
\end{quotation}
Why is $P$ invariant?  Well, we know from Lemma~\ref{ndfav} that $G$'s
favorite tomorrow will be at least as desirable as her favorite today, and
since her favorite today is more desirable than $B$, tomorrow's favorite
will be too.

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

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

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

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

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

\begin{proof}
Let Bob be some boy and Carole some girl that he does \emph{not} marry 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, 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 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}

\section{Well-Founded Orderings and Termination}

\subsection{Another Robot}

\iffalse Begin by defining the trivial ``pick how long'' game: P1 picks $n
\in \naturals$, the P2 and P1 alternate making forced moves.  The game
ends after $n$ forced moves; the last person to move wins.  So P1 strategy
is ``pick and even number.''  Insert here the discussion of ``terminates,
but no bound on number of steps...'' used below.

May also tell the ``guess a bigger number game''joke.
\fi

Suppose we had a robot positioned at a point in the plane with natural
number coordinates, that is, at an integer lattice-point in the Northeast
quadrant of the plane.  At every second the robot must move a unit
distance South or West until it can no longer move without leaving the
quadrant.  It may also jump \emph{any} integer distance East, but at every
point in its travels, the number of jumps East is not allowed to be more
than twice the number of previous moves South.

For example, suppose the robot starts at the position (9,8).  It can now
move South to (9,7) or West to (8,8); it can't jump East because there
haven't been any previous South moves.

The robot's moves might continue along the following trajectory: South to
(9,7), East to (23,7), South to (23,6), East to (399,6), West to (398,6),
East to (511,6), West to (510,6), and East to $(10^5,6)$.  At this point
it has moved South twice and East four times, so it can't jump East again
until it makes another move South.

\begin{claim}\label{robotcl}
The robot will always get stuck at the origin.
\end{claim}

If we think of the robot as a nondeterministic state machine, then
Claim~\ref{robotcl} is a termination assertion.  The Claim may seem
obvious, but it really has a different character than the termination
results for the algorithms we've considered so far.  That's because, even
knowing that the starting position was (9,8), for example, there is no
way to bound the total number of moves the robot can make before it gets
stuck.  So we will not be able to prove termination using the
natural-number-valued decreasing variable method of Theorem~\ref{th:decr}.
The robot can delay getting stuck at the origin for as many seconds as it
wants; nevertheless, it can't avoid getting stuck eventually.

Does Claim~\ref{robotcl} still seem obvious?  Before reading further, it's
worth thinking how you might prove it.

\iffalse
First give simple proof using Least Num Principle, first on number of
South moves to show robot reaches row 0, then number of East moves in row
0, then number of West moves in row 0.  Then segue into well-founded
decreasing variables.
\fi

We will prove that the robot always gets stuck at the origin by
generalizing the decreasing variable method, but with decreasing values
that are more general than natural numbers.  Namely, the traveling robot
can be modeled with a state machine with states of the form $((x,y),s,e)$
where
\begin{itemize}
\item $(x,y) \in \naturals^2$ is the robot's position,
\item $s$ is the number of moves South the robot took to get to this
position, and
\item $e \le 2s$ is the number of moves East the robot took to get to this
position. 
\end{itemize}

Now we define a derived variable $\vl:\text{States}\to \naturals^3$:
\[
\vl(((x,y),s,e)) \ \eqdef\quad (y,2s-e,x),
\]
and we order the values of states with the \emph{lexicographic} order,
$\lexle$, on $\naturals^3$:
\begin{equation}\label{lex3}
(k,l,m) \lexle (k',l',m') \ \eqdef\quad k < k' \text{ or } (k=k' \text{
and } l < l') \text{ or } (k=k' \text{ and } l = l' \text{ and } m \le m')
\end{equation}

Let's check that values are lexicographically decreasing.  Suppose the
robot is in state $((x,y),s,e)$.
\begin{itemize}
\item If the robot moves West it enters state $((x-1,y),s,e)$, and
\[
\vl(((x-1,y),s,e)) = (y,2s-e,x-1) \lex< (y,s-2e,x) = \vl(((x,y),s,e)),
\]
as required.


\item If the robot jumps East it enters a state $((z,y),s,e+1)$ for some
$z>x$.  Now
\[
\vl(((z,y),s,e+1)) = (y,2s-(e+1),z) = (y,2s-e-1,z),
\]
but since $2s-e-1 < 2s-e$, the rule~(\ref{lex3}) implies that
\[
\vl(((z,y),s,e+1)) = (y,2s-e-1,z)  \lex< (y,2s-e,x) = \vl(((x,y),s,e)),
\]
as required.

\item If the robot moves South it enters state $((x,y-1),s+1,e)$, and
\[
\vl(((x,y-1),s+1,e)) = (y-1,2(s+1)-e,x) \lex< (y,s-2e,x) = \vl(((x,y-1),s+1,e)),
\]
as required.

\end{itemize}

So indeed state-value is a decreasing variable under lexicographic order.
We'll show in the next section that it is impossible for a
lexicographically-ordered values to decrease an infinite number of times.
That's just what we need to finish verifying Claim~\ref{robotcl}.


\subsection{Well-founded Partial Orders}

\begin{definition}\label{wfpo}
Let $\preceq$ be a partial order and $S$ be a subset of its domain.  An
element $m \in S$ is minimal in $S$ iff no other element in $S$ is $\preceq
m$.  A partial order $\preceq$ is \emph{well-founded} iff every nonempty
subset of its domain has a minimal element.
\end{definition}

\iffalse
That is, $m \in S$ is minimal if $m' \preceq m$ implies that $m' =
m$ for all $m' \in S$.\fi

So saying that the natural numbers are well-founded under $\le$ is
equivalent to the Least Number Principle, but well-foundedness makes sense
much more generally than for just natural numbers.

Remember that a minim\emph{um} element of $S$ is one that is $\preceq$ all
the elements in $S$.  We saw in
\hyperref{http://theory.lcs.mit.edu/classes/6.042/fall03/handouts/ln3.pdf}
{rule}{minel}{Week 3 Notes} that every finite partial order must have a
minimal element.  The various scheduling/precedence partial orders in
earlier Notes typically had several minimal elements and therefore didn't
have a minimum element.

\textbf{Quick Exercise:} Give an example of a partial order with a
\emph{unique} minim\emph{al} element but no minim\emph{um} element.

\solution{The set of all real numbers totally ordered by $\le$ has no
minimal element.  We can regard $\le$ as a partial order on $\reals \union
\set{i}$, where $i$ is the complex number $\sqrt{-1}$, by agreeing that $i$
is not comparable to every real number.  This makes $i$ the unique minimal
element -- it's also the unique maximal element -- but there is no minimum
element.}

There is another helpful way to characterize well-founded partial orders:
\begin{lemma}
\label{d-chain}
A partial order is well-founded iff it has no infinite decreasing chain.
\end{lemma}

Saying that the partial order $\preceq$ has no infinite decreasing chain
means there is no infinite sequence $p_1,p_2,\dots,p_n\dots$ of elements
in $P$ such that
\[
p_1 \succ p_2 \succ \dots \succ p_n \dots.
\]
Here we're using the notation ``$p \succ q$'' to mean [$q \preceq p$ and $q
\neq p$].  That's so we can read the decreasing chain left to right, as
usual in English.

\begin{proof}
(\textbf{left to right}) (By contradiction) If there was such an infinite
decreasing sequence, then the set of elements in the sequence itself would
be a nonempty subset without a minimal element.

(\textbf{right to left}) (By contradiction) Suppose $\preceq$ was not
well-founded.  So there is some set subset $S \subseteq \domain{\preceq}P$,
such that $S$ has at least one element, $s_1$, but $S$ has no minimal
element.  In particular, since $s_1$ is not minimal, there must be
\emph{another} element $s_2 \in S$ such that $s_1 \succ s_2$.  Similarly,
since $s_2$ is not minimal, there must be still another element $s_3 \in S$
such that $s_2 \succ s_3$.  Continuing in this way, we can construct an
infinite decreasing chain $s_1 \succ s_2 \succ s_3 \cdots$ in $S$.
\end{proof}

An immediate corollary of Lemma~\ref{d-chain} is
\begin{corollary}\label{fin-wf}
Every finite partial order is well-founded.
\end{corollary}

\begin{problem}
Let $D$ be the usual \emph{dictionary order} on finite sequences of letter
of the alphabet.  Show that neither $D$ nor $D^{-1}$ is well-founded.

\solution{\[
a\ D\ aa\ D\ aaa D\dots
\]
is an infinite $D$-increasing sequence, and so is an infinite
$D^{-1}$-decreasing sequence, proving that $D^{-1}$ is not well-founded.
To show $D$ is not well-founded, we describe 
an infinite $D^{-1}$-increasing sequence:
\[
b\ D^{-1}\ ab\ D^{-1}\ aab\  D^{-1}\ aaab \dots.
\]
}
\end{problem}

An easy way to construct well-founded partial orders is by taking products
of well-founded partial orders.  For example, the natural numbers are
well-founded under $\le$, so the product partial order $(\le \cross \le)$ on
pairs of natural numbers is going to be well-founded.

\iffalse

But why stop at $n$ when we can be much more general without being any more
complicated?

The idea is that a Cartesion product, $A_1 \cross A_2 \cross \dots \cross
A_n$ of sets $A_1,A_2, \dots, A_n$ consists of all the $n$-tuples
$\ang{a_1,a_2,\dots,a_n}$ such that $a_i \in A_i$ for $1 \le i \le n$.  But
any such $n$-tuple can be represented by the function, $f$, where $f(i)
\eqdef a_i$.

GO ON TO DEFINE: a \emph{dependent-type} is a set-valued total function.
For example, for $r \in \reals$, define the dependent-type, $F_0$, by the
rule:
\[
F_0(r) \eqdef \set{t \in \reals \suchthat t \neq r}.
\]

If $F$ is a dependent-type, then an \emph{element of type, $F$,} is
defined to be a total function, $f$, with the same domain as $F$, and such
that
\[
\forall a \in \domain(F)\ f(a) \in F(a).
\]

AND SO ON...
\fi

To prove this, we first generalize coordinatewise and lexicographic
partial order to pairs of elements from \emph{any} partial orders, not
just natural numbers.

\begin{definition}\label{lex-coord-def}
Let $\preceq_1$ and $\preceq_2$ be a partial orders with domains $A_1$ and
$A_2$.

The \emph{coordinatewise partial order}, $\coordle$, is defined to be the
\hyperref{http://theory.lcs.mit.edu/classes/6.042/fall03/handouts/ln3.pdf}
{def}{productrel}{product relation}, $(\preceq_1 \cross \preceq_2)$, defined
in Week 3 Notes.

The \emph{lexicographic partial order}, $\lexle$, for $\preceq_1$ and
$\preceq_2$ is defined by the conditions:
\begin{eqnarray*}
%\label{lexc2}
\domain{\lexle} &\eqdef& A_1 \cross A_2\\
(a_1,a_2) \lexle (b_1,b_2) & \qiff & a_1 \prec_1 b_1\text{ or } (a_1=b_1 \text{
and } a_2 \preceq_2 b_2).
\end{eqnarray*}

\end{definition}

Note that calling these relations ``partial orders'' is accurate: we know
from
\hyperref{http://theory.lcs.mit.edu/classes/6.042/fall03/handouts/ln3.pdf}
{def}{productrel}{Week 3 Notes} that products preserve partial orderings,so
$\coordle$ is indeed a partial order.  It's similarly easy to verify that
$\lexle$ is also a partial order.

But not only are these relations really partial orders, but they will also
be well-founded providing $\preceq_1$ and $\preceq_2$ are well-founded.
Namely,

\begin{theorem}\label{lex-coord-thm}
Let $\preceq_1$ and $\preceq_2$ be well-founded partial orders.  Then
\begin{enumerate}

\iffalse
\item\label{Lpo} so are $\lexle$ and $\coordle$.  Moreover,
\fi

\item\label{Lexwf} $\lexle$ is well-founded,

\item\label{Cwf} $\coordle$ is well-founded,

\item\label{Lto} if $\preceq_1$ and $\preceq_2$ are both total orders,
then so is $\lexle$.
\end{enumerate}
\end{theorem}

\begin{proof}

To prove part~\ref{Lexwf}., suppose $\emptyset \neq S \subseteq A_1 \cross
A_2$.  We want to prove that $S$ has a minimal element.

We begin by noting that
\[
S_1 \eqdef\ \set{a_1 \in A_1 \suchthat (a_1,a_2) \in S \mbox{ for some }
a_2 \in A_2}
\]
is a nonempty subset of $A_1$, and so has a
$\preceq_1$-minimal element, $m_1$.  This means the set
\[
S_{12} \eqdef\ \set{a_2 \in A_2 \mid (m_1,a_2) \in S}
\]
is a nonempty subset of $A_2$ and so has a $\preceq_2$-minimal element,
$m_2$.  We claim that $(m_1,m_2)$ is a minimal element of $S$ under
$\lexle$.

To check this, note first that $(m_1,m_2) \in S$ by definition.  So to show
it is minimal, we need only show that if
\begin{eqnarray}
(a_1,a_2) & \in & S,\text{ and }\label{aaS}\\
(a_1,a_2) & \preceq_{\text{lex}} & (m_1,m_2)\label{mmaa}
\end{eqnarray}
then
\begin{eqnarray}\label{aamm}
(a_1,a_2) = (m_1,m_2).
\end{eqnarray}
But
\begin{align}
a_1 & \in S_1
       & \text{by~(\ref{aaS}) and def.\ of $S_1$},\label{e0}\\
a_1 & \preceq_1 m_1
       & \text{by~(\ref{mmaa}) and def.\ of $\lexle$},\label{e1}\\
a_1 & =_1 m_1
      &  \text{by~(\ref{e0}),~(\ref{e1}),
               and minimality of $m_1$ in $S_1$},\label{e2}\\
a_2 & \in S_{12}
        &  \text{by~(\ref{aaS}),~(\ref{e2}) and def.\ of $S_{12}$},\label{e3}\\
a_2 & \preceq_2 m_2
      & \text{by~(\ref{mmaa}),~(\ref{e2}), and def.\ of $\lexle$},\label{e4}\\
a_2 & = m_2
      & \text{by~(\ref{e3}),~(\ref{e4}), and minimality of $m_1$ in
       $S_{12}$}. \label{e5}
\end{align}

Now~(\ref{aamm}) follows from~(\ref{e2}) and~(\ref{e5}), completing
the proof of part~\ref{Lexwf}.

Now notice that this argument above also holds if we replace $\lexle$ by
$\coordle$, allowing us to conclude that $(m_1,m_2)$ is also a minimal
element of $S$ under $\coordle$.  This proves part~\ref{Cwf}.

Part~\ref{Lto}.\ follows straightforwardly from the definitions, and we
leave its proof to the reader.
\end{proof}

Of course, the values of states for the robot in the previous section were
triples not pairs, but we can easily define the lexicographic partial order
on $n$-tuples for any $n\ge 1$.  Namely, 
\begin{definition}\label{lexn}
Suppose $\preceq_1,\dots, \preceq_n$ are partial orders with domains $A_1,
\dots, A_n$, and define the partial order, $\lexle$, with domain, $A_1 \cross
\cdots \cross A_n$, recursively in $n$:
\begin{eqnarray*}
\ang{a_1} \lexle \ang{b_1} &\qiff& a_1 \preceq_1 b_1\\
\ang{a_1,\dots,a_n,a_{n+1}} \lexle \ang{b_1,\dots,b_n,b_{n+1}} &\qiff&
  a_1 \preceq_1 b_1 \land
    \ang{a_2,\dots,a_{n+1}} \lexle \ang{b_2,\dots,b_{n+1}}
\end{eqnarray*}
\end{definition}
Theorem~\ref{lex-coord-thm} now generalizes straightforwardly to
$n$-tuples.  In particular, we conclude that since $\le$ is a well-founded
total order on $\naturals$, lexicographic order is a well-founded total
order on $\naturals^n$ for all $n \ge 1$.

Now notice that the lexicographic order on $\naturals^3$ defined in the
previous section (by the condition~(\ref{lex3})) is exactly the same as
$\lexle$ on $\naturals^3$ according to Definition~\ref{lexn}.

But we already proved that the value of the robot's state decreases at
every step.  And we have just proved that the order on these values is
well-founded.  So Lemma~\ref{d-chain} implies that the values cannot keep
decreasing forever.  That means the robot cannot keep moving forever: it
must always terminate.

\subsection{Terminating Games of Perfect Information}

% F99, H42-tut11

The idea of well-founded partial orders will allow us to prove a
fundamental theorem about games like chess, checkers, or tic-tac-toe.
These are games in which two players alternate moves that depend only on
the visible board position or state of the game.  Such games are
technically called \emph{two person games of perfect information} because
the players know the complete state of the game.  (Most card games are
\emph{not} games of perfect information because neither player can see the
other's hand.)

Two person games of perfect information can be represented abstractly by
their ``game trees.''  The root of a game tree corresponds to the start
position of the game.  It has a child for each position after a possible
starting move of the first player.  Each of these children in turn has
children (these are grandchildren of the root) corresponding to the
positions of the game after possible moves by the second player, and so
on.

For example, in the game tree for tic-tac-toe, the root has nine children
corresponding to the nine boxes that the first player could mark with an
``X.''  Each of these nodes has eight children corresponding to the eight
remaining boxes which the second player could mark with an ``O,'' and so on.

%%%PICTURE WOULD BE GOOD

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

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

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

\end{problem}

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

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

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

\begin{theorem}\label{fund}
\textbf{Fundamental Theorem for two-person games of perfect information}:
For games in which every play is finite and ends in win or lose, there is
a winning strategy for one of the players.
\end{theorem}

Although Theorem~\ref{fund} guarantees a winning strategy, it gives no
clue which player may have it.  For chess, no one knows which player has a
winning strategy.

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

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

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

\end{problem}

Familiar games like tic-tac-toe and chess have finite game-trees, but not
all games do.  For example, a problem in Recitation 4 will be to work out a
winning strategy for a ``choose-a-pair'' game in which moves to any
natural-number-valued point in the plane are possible.  The game tree for
this choose-a-pair game is infinite.  In fact, the tree is infinitely
``wide.''  Namely, there are nodes that have an infinite number of
children.  The root is such a node, since the first move can be made to any
pair of natural numbers.  There is no finite bound on the length of plays,
so the tree is also infinitely ``deep.''

But even though the choose-a-pair tree is infinite, it turns out that every
choose-a-pair play terminates.  Abstractly, this means that although the
tree has \emph{longer and longer finite paths} down from the root, it has
\emph{no infinite paths} from the root.

\hyperdef{def}{fptree}{
\begin{definition}
A rooted tree is called \emph{finite-path} iff it has no infinite paths
away from the root.
\end{definition}}

A simple finite-path tree of unbounded depth is illustrated in
Figure~\ref{fin-path-tree}.  It consists of a root with an infinite number
of children, where each child is at the top of a finite chain of
descendents one longer than the previous child's.

\begin{figure}[htbp]
\centering \input{figures/fptree.pic}
%\centering \includegraphics[height=3in]{figures/fptree}
\caption{\emph{A finite-path tree with paths of every finite length.}}
\label{fin-path-tree}
\end{figure}

So the two-person games of perfect information in which every play
eventually ends in win or lose are precisely those games whose game trees
are finite-path.  These are the games to which the Fundamental Theorem
applies.

Let $\prec$ be the binary relation on rooted trees ``is (isomorphic to) a
\emph{proper} subtree of.''  More precisely, $T_1 \prec T_2$ iff there is
a \emph{non-root} vertex $v$ of $T_2$ such that $T_1$ is isomorphic to the
subtree of $T_2$ rooted at $v$.

\begin{theorem}\label{fpwpo}
The relation $\prec$ is a well-founded, strict partial order on finite-path
trees.
\end{theorem}

Assuming Theorem~\ref{fpwpo} for the moment, we can prove the Fundamental
Theorem~\ref{fund}.

\begin{proof} (of Theorem~\ref{fund}).

Suppose to the contrary that there is a game with a finite-path game tree
that has no winning strategy.  In particular, the set of finite-path game
trees without winning strategies is nonempty, so by Theorem~\ref{fpwpo}
there is a minimal such game tree under the ``proper subtree'' partial
order.

Let $T$ be a minimal tree without a winning strategy for either player.
Now if $C$ is a child of the root of $T$, then $C \prec T$ by definition.
But each child, $C$, is also a game tree, and since $T$ is minimal, there
must be a winning strategy for one of the players in the game starting at
the root of $C$.

Suppose some child, $C_0$, defines a game with a winning strategy for its
second player.  Then Player 1 on $T$ has a winning strategy: choose $C_0$
on the first move, and then follow the second player's winning strategy on
$C_0$.  Since there is no such winning strategy on $T$, it must be that
every child $C$ defines a game with a winning strategy for the first player
in the game starting at its root.  But that means that the Player 2 on $T$
has a winning strategy: if Player 1 on $T$ picks $C$, then Player 2 will
follow the winning strategy for the first player on $C$.  This contradicts
the hypothesis that $T$ has no winning strategy.
\end{proof}

To finish the story, we have have to prove that the relation $\prec$ is a
strict partial order on finite-path trees.

\begin{proof}
(of Theorem~\ref{fpwpo})

\begin{itemize}
\item
The relation $\prec$ is transitive: Suppose a copy of $T_1$ is a subtree of
$T_2$; then there is path, $P$, from the root of the $T_1$-copy to the root of
$T_2$.  Suppose also that a copy of $T_2$ is a subtree of $T_3$; then there is
path, $Q$, from the root of the $T_2$-copy to the root of $T_3$.  Now the
$T_2$-copy has a copy of the $T_1$-copy as a subtree; call this subtree $T'_1$.
So the path $P$ has a copy, $P'$, from the root of $T'_1$ to the root of the
$T_2$-copy.  This means that the path $P'$ followed by the path $Q$ leads from
the root of $T'_1$ to the root of $T_3$.  So indeed, there is a copy of $T_1$,
namely $T'_1$, which is a proper subtree of $T_3$.

\item
The relation $\prec$ is asymmetric: Suppose not.  That is, suppose (a copy of)
$T_1$ is a proper subtree of $T_2$ and also $T_2$ is a proper subtree of $T_1$.
Then $T_1$ has a copy of itself as a proper subsubtree\iffalse , as illustrated
in Figure 1, attached\fi. Therefore there is a path---which must be of length
two or more---from the root of $T_1$ to the root of the copy of $T_1$.  This
path extends to a path of length four or more to the root of the copy in the
copy, and then extends to the root of the copy in the copy in the copy\dots.
In this way we can find an infinite path from the root of $T_1$, contradicting
the assumption that $T_1$ is finite-path.

\item The relation $\prec$ is well-founded on finite-path trees.

Suppose not.  Then, by Lemma~\ref{d-chain} there must be an infinite
$\prec$-decreasing sequence of distinct elements.  That is, an infinite
sequence $T_1 \succ T_2 \succ T_3 \succ \dots$ of distinct finite-path
trees.  By definition, $T_n \succ T_{n+1}$ means there is a path from the
root of $T_n$ to a vertex which is the root of an isomorphic copy of
$T_{n+1}$.  It's convenient to assume that $T_{n+1}$ itself---rather than
an isomorphic copy---is the subtree of $T_n$ \iffalse as illustrated in
Figure 2\fi.  This assumption is justified because we could always replace
$T_{n+1}$ in the sequence above with the actual subtree of $T_n$
isomorphic to it.

Now $T_n \succ T_{n+1}$ implies there is a path $P_n$ (necessarily of
length one or more) from the root of $T_n$ to the root of $T_{n+1}$.  But
then $P_1$ followed by $P_2$ followed by $P_3$ \dots is an infinite path
from the root of $T_1$, contradicting the hypothesis that $T_1$ is
finite-path.  Hence there cannot be such an infinite decreasing sequence
of finite-path trees, and this implies that the partial order, $\prec$, on
finite-path trees is well-founded.

\end{itemize}

\end{proof}

\begin{problem}
Here is a generalization of the ``choose-a-pair'' game to
``choose-a-tuple''.  The rules are:

Player 1 chooses any integer $n\geq 1$.  Then Player 2 chooses any
$n$-tuple of natural numbers.  After that, the players alternate moves,
choosing as a move any $n$-tuple, $t$, of natural numbers such that no
previous move is $\coordle t$.  A player wins when the other player
chooses the origin (0,\dots,0).

For example, Player 1 might begin by choosing $n=3$.  Then Player 2 might
choose the 3-tuple (8, 9, 10).  Possible subsequent choices might then be
\[
(7,8,9), (0,1,67), (83, 0,0), (1,0,0), (0,0,1) (0,1,0)
\]
This finally leaves Player 1 with only the move (0,0,0), and the game now
ends with his loss.

\bparts

\ppart Prove that every choose-a-tuple play must end.

\ppart Conclude that one of the players has a winning strategy.

\ppart Which one?  (This is an Open Problem -- the 6.042 staff doesn't know
the answer.)

\eparts

\end{problem}

\iffalse

\subsection{The Gale Subset Game}

%from Spring98 H07-rec1

The \emph{Gale game}\footnote{J. Daniel Christensen and Mark Tilford,
``David Gale's Subset Take-Away Game,'' American Mathematical Monthly
v.105 (Jan.1998)} is played on the set of integers $A_n \eqdef
\set{1,\dots,n}$.  Two players alternate moves.  A {\em move} is a choice
of a \emph{strict} subset, $B \subset A_n$, (\viz $B \not = A_n$), subject
to the constraint that $B$ may not contain any subset chosen at a previous
move.  The player who first chooses the empty set is the loser.

For example, when $n=4$, the moves might be:
\[
\begin{array}{ccccccccc}
player: & 1 &2 & 1 &2 & 1 &2 & 1 &2\\
move:   &\set{1,2} &\set{3,4} & \set{1,3} & \set{2,4} & \set{1} & \set{2} & \set{3} & \set{4}\\
\end{array}
\]
At this point, the first player has no valid move and therefore loses.

{\em Gale's Conjecture} is that the second player has a winning strategy.

(a) Prove Gale's Conjecture for the games with $n=2$ and 3.

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

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

\medskip
(b) Must every Gale game end with a winner (remember, chess games don't)?
What is the length of the longest, and shortest, possible games on
$\set{1,\dots,n}$?  Explain.

{\bf Solution}:
The game will always end with a winner, because there are a finite number
of legal moves in any game, and no move can be reused.  Therefore the game
will come to an end after a number of steps at most equal to the number of
possible moves.

The set $A$ with $n$ elements has $2^n$ different subsets.  Since choosing
$\emptyset$ and $A$ itself is not allowed in the game, there are exactly
$2^n-2$ possible moves.  So the longest possible game would have at most
$2^n-2$ moves.  It is possible to have this many moves in a game: the
players could choose all the subsets of size of $n-1$ first, followed by
those with size of $n-2$, and so on, down to subsets with size of 1.  Such
a sequence of moves is allowed because all the moves prior to any given
move in the sequence are subsets at least as large as the given move, so
none of them is contained in the given move.

The shortest possible game would last for $n$ steps. In such a game the
players always choose subsets containing one element.  When all the $n$
such sets are chosen, no more valid moves remain.  It is not possible to go
below $n$ steps because the $n$ subsets with size 1 can always be picked
if they are not picked before.

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

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

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

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

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

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

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

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

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

\fi

\end{document}
