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

\backwardscompatibility        % !! use for backwards compatibility
\renewcommand{\coursecopyrightnames}{Prof.~Albert~R.~Meyer}

\begin{document} 
\inclassproblems{5M}                    % !! start the paper


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

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


%Fast multiplication by adding and doubling from F97 pset4, problem 2.
%%%%%%%%%%%%%%%%%%%%%%% PROBLEM %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5

\begin{problem}
Consider the following multiplication algorithm, known as the ``Russian
peasant's multiplication'' to multiply numbers $a,b \in \naturals$.

The accumulator for the answer is register \texttt{p}; registers
\texttt{x}, \texttt{y} are for temporary storage.

\texttt{x:=}$a$; \texttt{y:=}$b$; \texttt{p:=}0;
\begin{verbatim}
Do until y=0:
 if even(y) then {x := 2x; y := y/2};
 if odd(y) then {p := p + x; x := 2x; y := (y-1)/2};
\end{verbatim}
We claim the product of $a$ and $b$ will be left in the accumulator
\texttt{p} when the procedure terminates.

Here is an example of the execution of the algorithm for $a=5, b = 9$:
\begin{verbatim}
                          x     y     p
                         -------------
                          5     9     0
                         10     4     5
                         20     2     5
                         40     1     5
                         80     0    45
\end{verbatim}

\begin{problemparts}

\problempart
Model the algorithm as a state machine.  

\solution{The state is the triple of values in \texttt{x, y}, and \texttt{p}.

There is just one start state: $(a,b,0)$.

There are two types of state transitions (even or odd) as described in the
algorithm.  Consider a transition from $(x,y,p)$ to $(x',y',p')$:

if $y$ is even:   $(x',y',p')$ = $(2x, y/2, p)$

if $y$ is odd:    $(x',y',p')$ = $(2x, (y-1)/2, p+x)$
}

\problempart
Prove that it is correct using an invariant.

\solution{
To prove correctness, we show that
\begin{lemma*}
The predicate $P(x,y,p) \eqdef\quad [ab = xy+p]$ is an invariant.
\end{lemma*}

\begin{proof}
Consider a transition from $(x,y,p)$ to $(x',y',p')$ and suppose
$P(x,y,p)$ holds, that is, $ab = xy+p$.  We must prove that $P(x',y',p')$
holds, that is, $ab = xy+p$.  There are two cases based on the type of
action, \emph{even} or {\it odd}.

\emph{even}: Doubling $x$ while halving $y$ doesn't change the product
$xy$, and $p$ doesn't change.  So $x'y'+p' = xy+p = ab$.

\emph{odd}: $x' = 2x$, $y' = (y - 1)/ 2$, and $p' = p + x$.  So
\[
x'y' + p' = 2x(y - 1)/ 2 + p + x = (xy-x) + p + x = xy+p = ab.
\]
\end{proof}

Also, $P$ holds for the start state $(a,b,0)$ because $ab+0 = ab$.  So by
the Invariant Theorem, we conclude:
\begin{corollary*}
If $y=0$ in a reachable state, then $p = ab$.
\end{corollary*}

\begin{proof}
By our invariant, we have
$P(x,0,p)$, that is $x0 + p = ab$, so $x=ab$.
\end{proof}
}

\problempart
Why is this algorithm guaranteed to terminate?  How many arithmetic
operations $(+, -, \times, / )$
does it perform on given inputs $a$ and $b$?

\solution{Notice that the value of $y$ is a nonnegative integer that
decreases at every step unless it is 0: if $y$ is even, it becomes $y/2$
and if $y$ is odd, it becomes $(y-1)/2$.  So $y$ will eventually become 0,
and the algorithm must terminate.

In fact, since $y$ is a least halved each time around the loop, there are
at most $\floor{\log_2 b}+1$ loop executions, and each execution involves
1 multiply (by 2), one division (by 2), one addition, and at most one subtraction.
}

\end{problemparts}
\end{problem}


\end{document}










