1.18 Exercise 1.18

(define (fast-times-iter a b)   (define (loop x a b)     (cond ((= b 0) x)           ((even? b) (loop x (double a) (halve b)))           (else (loop (+ a x) a (- b 1)))))   (loop 0 a b))

fast-times-iter works by using an inner procedure loop of three arguments x, a, and b, holding the invariant that AB = x + ab.

The first call to loop has the arguments 0, A, and B, making the invariant hold trivially.

Inside loop, there are three cases. If b is positive and even, then loop is recursively called with the arguments x, 2a, and b/2, and the invariant still holds. If b is positive and odd, then the recursive arguments are a + x, a, and b - 1. Since x + ab = (x + a) + a(b-1), the invariant holds. If b is zero, then x is returned. Since x + a(0) = x, x will have the value AB. Therefore, fast-times-iter is correct.