SICP Exercise 1.16
This exercise requires the design of a procedure that evolves an iterative
exponentiation process using successive squaring. It should use constant space
and a logarithmic number of steps. The hint is to note that $\left( b^{
\frac{n}{2} } \right)^2 = \left( b^2 \right)^{ \frac {n}{2} }$ and to
transform states such that $ab^n$ is invariant, and equal to
$b^n$ where a
is another state variable along with the base b
and exponent n
. Here is the implementation:
(define (even? x)
(= (remainder x 2) 0))
(define (expt b n)
(expt-iter 1 b n))
(define (expt-iter a b n)
(cond ((= n 0) a)
((even? n) (expt-iter a (square b) (/ n 2)))
(else (expt-iter (* a b) b (- n 1)))))
Here, expt-iter
starts with the state variables a = 1
, b
, the base, and
n
, the exponent.
We will the use the notation $a_0$, $b_0$,
$n_0$ to denote the initial values, and $a_c$,
$b_c$, $n_c$ to denote the current values,
of the state variables a
, b
and n
, respectively.
When the exponent n
falls to zero, our invariant says that $a_c {b_c}
^0 = a_c$ must equal the final result ${b_0}^{n_0}$. Hence
in this case, we return $a_c$, the current value of a
. The
correctness of this can be readily verified for $n_0 = 0$. For
other values of $n$, we need to prove that given any call to
expr-iter
with arguments $a_c$,
$b_c$, $n_c$ such that the invariant is preserved,
i.e., $ a_c { b_c }^{n_c} = {b_0}^{n_0}$, each arm of the cond
in
expt-iter
preserves the invariant through the next recursive call to itself.
For even values of $n$, we use the first part of the hint to reduce the exponent by half while squaring $b$. Let’s look at our invariant expression in this case. Suppose we are dealing with some even exponent $n_c = 2k$. Before our transformation, the invariant says that $a_c { b_c } ^{2k} = {b_0}^{n_0}$. After our transformation, the invariant is $a_c { {b_c}^2 }^k$, which is just a rearrangement of the invariant expression before the transformation, and hence, must also equal ${b_0}^{n_0}$.
For odd values of $n$, we transform by changing $a$ to be the product $ab$ while reducing $n$ by $1$. For some odd value of $n_c = 2k+1$, the invariant before the transformation is $a_c {b_c}^{2k+1}$. After the transformation, it becomes $ \left( a_c b_c \right) {b_c}^{2k} $, which is only a rearrangement of the previous term, implying that our transformation correctly preserves the invariant.
Maintaining an invariant across state transformations is a powerful way of designing iterative processes, and also makes it easy to reason for the correctness of the procedures behind such processes.