Mathematics for Computer Science

5.4. State Machines 141

Ifzis even, then we have thatxtDx^2 ;ytDy;ztDz=2. Therefore,zt 2 N
and

ytxtztDy.x^2 /z=2

Dyx^2 
z=2

Dyxz

Dab (by (5.4))

Ifzis odd, then we have thatxtDx^2 ;ytDxy;zt D.z1/=2. Therefore,
zt 2 Nand

ytxtztDxy.x^2 /.z1/=2

Dyx^1 C^2 
.z1/=2

Dyx^1 C.z1/

Dyxz

Dab (by (5.4))

So in both cases, (5.5) holds, proving thatPis a preserved invariant.
Now it’s easy to prove partial correctness: if the Fast Exponentiation program
terminates, it does so withabin registery. This works because 1
abDab, which
means that the start state,.a;1;b/, satisifiesP. By the Invariant Principle,Pholds
for all reachable states. But the program only stops whenzD 0. If a terminated
state.x;y;0/is reachable, thenyDyx^0 Dabas required.
Ok, it’s partially correct, but what’s fast about it? The answer is that the number
of multiplications it performs to computeabis roughly the length of the binary
representation ofb. That is, the Fast Exponentiation program uses roughly logb^6
multiplications, compared to the naive approach of multiplying byaa total ofb 1
times.
More precisely, it requires at most2.dlogbeC1/multiplications for the Fast
Exponentiation algorithm to computeabforb > 1. The reason is that the number
in registerzis initiallyb, and gets at least halved with each transition. So it can’t
be halved more thandlogbeC 1 times before hitting zero and causing the program
to terminate. Since each of the transitions involves at most two multiplications, the
total number of multiplications untilzD 0 is at most2.dlogbeC1/forb > 0(see
Problem 5.36).

(^6) As usual in computer science, logbmeans the base two logarithm, log 2 b. We use, lnbfor the
natural logarithm logeb, and otherwise write the logarithm base explicitly, as in log 10 b.