\problemdata
{S00 ps4}
{Russian peasant}
{computational processes}

\begin{problem}
%(Problem adapted from F97 pset 4)

The following algorithm, called the \emph{Russian peasants algorithm},
can be used to multiply any two natural numbers $x$ and $y$ using only
left bit-shift (i.e., multiply by 2) and right bit-shift (i.e., divide
by 2 and drop the remainder, if any) operations.  The answer is
accumulated in variable $a$; variables $r$ and $s$ are for temporary
storage.

\begin{tabbing}
XXX\=XXX\=XXX\=XXX\kill
$r:=x$; \\
$s:=y$; \\
$a:=0$;\\
do until $s=0$:\\
   \>if s is even then \\
   \>\>   $r := 2r$; \\
   \>\>   $s := s/2$;\\
   \>else \\
   \>\>   $a := a + r$; \\
   \>\>   $r := 2r$; \\
   \>\>   $s := (s-1)/2$;\\
\end{tabbing}
The answer $xy$ is the value left in the accumulator $a$ when the 
procedure terminates. 

\begin{problemparts}

\problempart Model the algorithm as a state machine.  
That is, define the states $Q$, the start states $Q_0$, and the steps
$\delta$.
\solution{

$Q=\{(r,s,a,x,y)|r,s,a,x,y\in \mathbb{N}\}$\\
$Q_0=\{(x,y,0,x,y)\}$\\
$\delta: (r,s,a,x,y)\rightarrow (r',s',a',x',y')$, where\\
$x'=x$, $y'=y$, $r'=2r$\\
Even $s$: $s'=s/2$, and $a'=a$\\
Odd $s$: $s'=(s-1)/2$, and $a'=a+r$\\
}

\problempart List the sequence of states that appears in an execution of the
algorithm for inputs $x=5$ and $y=9$.

\solution{
$(5,9,0,5,9)\rightarrow (10,4,5,5,9) \rightarrow (20,2,5,5,9) \rightarrow (40,1,5,5,9) \rightarrow (80,0,45,5,9)$
}

\problempart Prove that the algorithm gives the correct answer if it
terminates, that is, that $s = 0$ implies $a = xy$.
(Hint:  Use induction on the number of steps in the execution.  You
will have to strengthen the inductive hypothesis.)

\solution{
We prove the following invariant.

$P(r,s,a,x,y) = ``xy = rs+a$''.

{\bf Base case: }
For any initial state we have $P(x,y,0,x,y)$ which is true.

{\bf Inductive step:} Consider a transition from $(r,s,a,x,y)$ to
$(r',s',a',x',y')$.  We need to prove that $P(r,s,a,x,y) \rightarrow
P(r',s',a',x',y')$.

There are two cases based on the type of action, {\it even} or {\it odd}.

$\ms{even}$: \\
Doubling $r$ while halving $s$ doesn't change the product $rs$,
and $a$ doesn't change.  So $r's'+a' = rs+a = xy$.

$\ms{odd}$:\\ 
$r' = 2r$, $s' = {s - 1 \over 2}$, and $a' = a + r$.
So $r's' + a' = 2r{ s - 1 \over 2 } + a + r$.
Reorganizing terms yields $r's'+a' = rs+a = xy$.

The invariant is proved.  Now when $s=0$ this implies $a=xy$ and we have
our result.
}

\problempart Prove that the algorithm terminates. 

\solution{
We first notice the invariant that $s\geq 0$ for any reachable
execution state.  We could prove that this is an invariant by showing
it is true for the base case, $y\geq 0$, and furthermore, no
transition exists from a state with $s\geq 0$ to $s<0$ when $s$ is odd
or even.  A more advanced argument is to say that this is enforced by
the ``type'' of $s$, which is that $s\in \mathbb{N}$.

Now consider the value of $s$ during any valid execution.  Since
$s\geq 0$, as shown above, no transition increases $s$.  Furthermore,
for $s>0$, all transitions decrease $s$ by at least 1.  Thus for any
values of $x,y\in \mathbb{N}$, $s$ decreases to 0 in a finite number
of steps, and thus the program terminates in a finite number of steps.
}

\end{problemparts}
\end{problem}
