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