1.16 Exercise 1.16

(define (fast-expt-iter b n)   (define (loop a b i)     (cond ((= i 0) a)           ((even? i) (loop a (square b) (/ i 2)))           (else (loop (* a b) b (- i 1)))))   (loop 1 b n))

During the execution of this procedure, the invariant that B^n = ab^i holds (where b is the value of b in recursive calls to loop and B is the original value). a begins as 1 and b begins as b, making this trivial.

In every call of the loop, i is either even or odd. If it is even, then loop is called again with the arguments a, b^2, and i / 2. Since ab^i = a(b^2)^(i/2), the invariant still holds. Alternatively, if i is odd, then loop is called with arguments a * b, b, and i - 1. Since ab^i = (a*b)b^(i-1), the invariant also still holds.

loop stops recursing when i is equal to zero and returns a. In this case, b^i will be equal to 1. Since the invariant still holds, we can conclude that a holds the desired value of B^n. We conclude that fast-expt-iter is correct.