Mathematics for Computer Science

6.2. State Machines 133

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 (6.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 (6.4))

So in both cases, (6.5) holds, proving thatPis a preserved invariant.
Now it’s easy to prove partial correctness, namely, if the Fast Exponentiation
program terminates, it does so withabin registery. This works because obviously
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 ,
so 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 log 2 b
multiplications compared to the naive approach of multiplying byaa total ofb 1
times.
More precisely, it requires at most2.dlog 2 beC1/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 thandlog 2 beC 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.dlog 2 beC1/forb > 0
(see Problem 6.26).