TAOCP 4.3.1 Exercise 14
Let U=(u_{m-1}\ldots u_1u_0)_b,\qquad V=(v_{n-1}\ldots v_1v_0)_b, and let
Section 4.3.1: The Classical Algorithms
Exercise 14. ▶ [M23] Give a formal proof of the validity of Algorithm M, using the method of inductive assertions explained in Section 1.2.1. (See exercise 1.)
Verified: no
Solve time: 45s
Solution
Let
$$ U=(u_{m-1}\ldots u_1u_0)b,\qquad V=(v{n-1}\ldots v_1v_0)_b, $$
and let
$$ W^{(j)}=(w_{m+n-1}\ldots w_1w_0)_b $$
denote the contents of the array $w$ at the beginning of step M2 for a given value of $j$.
We shall prove the validity of Algorithm M by exhibiting inductive assertions for the loops on $j$ and $i$.
Assertion for the outer loop
At the beginning of step M2 with index $j$ ($0\le j\le n$),
$$ W^{(j)} = U\sum_{r=0}^{j-1} v_r b^r . \tag{1} $$
For $j=0$, step M1 has set all digits $w_t$ equal to zero; hence
$$ W^{(0)}=0 = U\sum_{r=0}^{-1} v_r b^r, $$
so (1) is true initially.
Assume that (1) holds for some $j<n$. We must show that after steps M2-M6 have been executed for this value of $j$, the resulting array satisfies
$$ W^{(j+1)} = U\sum_{r=0}^{j} v_r b^r . \tag{2} $$
Two cases arise.
If $v_j=0$, step M2 sets $w_{j+m}\leftarrow0$ and passes directly to M6. Since
$$ U v_j b^j =0, $$
the represented number is unchanged, and therefore
$$ W^{(j+1)}=W^{(j)} = U\sum_{r=0}^{j-1} v_r b^r = U\sum_{r=0}^{j} v_r b^r . $$
Thus (2) holds.
It remains to consider the case $v_j\neq0$.
Assertion for the inner loop
During execution of steps M3-M5, define
$$ P_i=\sum_{r=0}^{i-1} u_r b^r . $$
At the beginning of step M4 with index $i$ ($0\le i\le m$), the digits satisfy
$$ \sum_{t=0}^{i+j-1} w_t b^t + k,b^{i+j} = W^{(j)} + v_j b^j P_i . \tag{3} $$
For $i=0$, step M3 sets $k\leftarrow0$. Since $P_0=0$, (3) becomes
$$ 0+0=W^{(j)}+0 $$
when restricted to the positions that may subsequently change, so the assertion is true initially.
Assume that (3) holds for some $i<m$. Let
$$ t=u_i v_j+w_{i+j}+k. $$
Step M4 sets
$$ w_{i+j}\leftarrow t\bmod b, \qquad k\leftarrow\lfloor t/b\rfloor . $$
Hence
$$ t=(t\bmod b)+b\lfloor t/b\rfloor , $$
so the quantity
$$ w_{i+j}+kb $$
after the update equals its value before the update plus $u_i v_j$.
Multiplying by $b^{i+j}$, we obtain
$$ (w_{i+j}^{\text{new}}+k^{\text{new}}b)b^{i+j} = (w_{i+j}^{\text{old}}+k^{\text{old}}b)b^{i+j} + u_i v_j b^{i+j}. $$
Combining this with (3) yields
$$ \sum_{t=0}^{i+j} w_t b^t + k,b^{i+j+1} = W^{(j)} + v_j b^j \left( P_i+u_i b^i \right). $$
Since
$$ P_i+u_i b^i=P_{i+1}, $$
the assertion becomes
$$ \sum_{t=0}^{i+j} w_t b^t + k,b^{i+j+1} = W^{(j)} + v_j b^j P_{i+1}, $$
which is precisely (3) with $i$ replaced by $i+1$. Therefore the inner-loop assertion is preserved.
When the loop terminates, $i=m$. Since
$$ P_m=U, $$
assertion (3) gives
$$ \sum_{t=0}^{m+j-1} w_t b^t + k,b^{m+j} = W^{(j)} + U v_j b^j . $$
Step M5 stores $w_{m+j}\leftarrow k$. Therefore
$$ W^{(j+1)} = W^{(j)} + U v_j b^j . \tag{4} $$
Substituting the outer-loop hypothesis (1) into (4),
$$ W^{(j+1)} = U\sum_{r=0}^{j-1} v_r b^r + U v_j b^j = U\sum_{r=0}^{j} v_r b^r . $$
Thus (2) holds, completing the induction for the outer loop.
Termination
After the final execution of M6, we have $j=n$. By the outer-loop assertion,
$$ W^{(n)} = U\sum_{r=0}^{n-1} v_r b^r . $$
But
$$ \sum_{r=0}^{n-1} v_r b^r = V, $$
hence
$$ W^{(n)}=UV. $$
Therefore the digits
$$ (w_{m+n-1}\ldots w_1w_0)_b $$
represent exactly the radix-$b$ product of
$$ (u_{m-1}\ldots u_1u_0)_b $$
and
$$ (v_{n-1}\ldots v_1v_0)_b. $$
Algorithm M is therefore correct.
This completes the proof.
∎