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 $a{b}^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-iterstarts 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 $ ( a_c b_c ) {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.