\problemdata
{S00 ps4.5}
{computational processes}

\begin{problem}
%[[[Taken from spring99, handout26, pset 4]]]
Suppose that the following procedure is used to
raise a real number $x$ to the non-negative integral power $y$.  
\begin{itemize}
\item Do the assignments $a := x, b := y, p := 1$.
\item Repeat the following steps:
  \begin{itemize}
  \item If $b$ is 0, output $p$ and terminate.
  \item If $b$ is even, do the assignment $a := a^2$ (that is, set the next
        value of $a$ to be the square of the current value), and also do
        $b := b/2$.
  \item If $b$ is odd, do $p := p \cdot a$ and $b := b - 1$.
  \end{itemize}
\end{itemize}

%[[[Shishir:  I pulled in the solution from the old handout, editing it
%slightly.  But I did this quickly.  Please read carefully,
%including checking that the presentation is consistent with the way the
%material is being presented in lecture this year.  My notes are in
%files ``lecture7, lecture 8, lecture9'' in the lectures directory.
%Also, formatting of solutions isn't consistent with what we're doing
%this year---please fix.  Same comments for the rest of this pset.]]]

\begin{problemparts}
\problempart Model the procedure with a state machine.

\solution{

The state can be represented with a triple of numbers $a,b,p$:
\[Q = \{a, b, p\} \subset
(\reals \times \naturals \times \reals)
\]
The initial state is
\[
q_0 = (x,y,1)
\]
There are two transitions:
\begin{eqnarray*}
(a, b, p) &\rightarrow& (a^2, b/2, p) \,\,\mbox{ if $b$ is even and $b > 0$}
\\
(a, b, p) &\rightarrow& (a, b-1, ap) \,\,\mbox{ if $b$ is odd}
\end{eqnarray*}
The terminating condition is $b=0$, and then the state machine outputs~$p$.
\end{solution}
}



\problempart Formulate an invariant relating $a, b, x, y$, and $p$ that
holds in every state.  Your invariant should imply that if
$b = 0$, then $p = x^y$.

\solution{

The invariant is expressed by the following predicate $P(\cdot)$ which
takes a state of the machine as an argument:
\[
P(a,b,p)=\mbox{``\,\,$a^bp=x^y$\,\,''}
\]
Note that if $b=0$ and $P(a,b,p)$ then $a^bp=p=x^y$.
}


\problempart Prove that the invariant holds.

\solution{
We use the Invariant Theorem.
Clearly, $P(q_0)$ holds:
\[
P(q_0)=\mbox{``\,\,$(x^y)*1=x^y$\,\,''}
\]
Now, we show that if $P(q)$ and $(q,q')$ is a valid transition then
$P(q')$: 

Take some $q=(a,b,p)$ and assume $P(q)$, i.e. that $a^bp=x^y$.  $q'=(a',b',p')$
could be a state following $q$ if one of the two cases holds:
\begin{itemize}
\item 
If $b>0$ and $b$ even then $(a',b',p')=(a^2,b/2,p)$, and then
\[
(a')^{b'}p'=(a^2)^{(b/2)}p=a^bp=x^y
\]
where the last equation follows from $P(q)$.  Hence, in this case
$P(q')$ is true.
\item
If $b$ odd then $(a',b',p')=(a,b-1,ap)$, and then
\[
(a')^{b'}p'=a^{b-1}ap=a^bp=x^y
\]
where again, the last equation follows from $P(q)$.  Hence, in this case
$P(q')$ is true as well.
\end{itemize}
}


\problempart Prove that the procedure terminates.

\solution{
We need to show that in any live execution, $b$ eventually reaches
$0$, because that's the termination condition.  Let's argue the
following facts:
\begin{enumerate}
\item 

It is an invariant of this state machine that $b$ is an integer.  It
starts as an integer $y$, and the two transitions preserve that: If
$b\in\integers$ and $b$ is even then $b/2\in\integers$.  Similarly,
if $b\in\integers$ then $(b-1)\in\integers$.

\item

$b$ cannot be a negative number.  We can show that by a contradiction:
If $b$ ever reached a negative number, since $b$ starts from a
nonnegative integer $y$, there must be a transition where $b$ went
below $0$, i.e. a transition from $b\geq{0}$ to $b'<0$.  But that's impossible
with our transitions:  
\begin{itemize}
\item
If $b\geq{0}$ then $b/2\not<{0}$
\item
If $b\geq{0}$ and $b\neq{0}$ then $b-1\not<0$.
\end{itemize}

\item
$b$ decreases in every transition (obviously, if $b>0$ than $b/2<b$
and $b-1<b$).
\end{enumerate}

Facts (1), (2) and (3) imply that $b$ must attain the value $b=0$ and
trigger the state machine to terminate.

Formally, it the the well-ordering principle that we use here: From
facts (1) and (2) it follows that for any execution of this state
machine, the set of values of variable $b$ is a subset of $\naturals$.
Therefore, from the well-ordering principle, it must have the smallest
element $b_0$. 

We claim that $b_0$ must be $0$.
If not, then since the execution is live, another step must
follow, which (by fact (3)) implies that the next value of $b$ must be
smaller.  But we have assumed that $b_0$ is the smallest value
attained by $b$.
This is a contradiction, which implies that $b_0=0$. 

Therefore, the procedure must terminate.

}

\end{problemparts}
\end{problem}

