TAOCP 4.3.1 Exercise 4

Let $U = (u_{n-1}\ldots u_0)_b,\quad V = (v_{n-1}\ldots v_0)_b,\quad W = (w_{n-1}\ldots w_0)_b.$ Define for each $j$ with $0 \le j \le n$ the partial values $U_j = \sum_{i=0}^{j-1} u_i b^i,\quad V_j =...

taocpmathematicsalgorithmsvolume-1math-medium

Section 4.3.1: The Classical Algorithms

Exercise 4. [M21] Give a formal proof of the validity of Algorithm A, using the method of inductive assertions explained in Section 1.2.1.

Verified: no
Solve time: 1m30s

Solution

Let

$U = (u_{n-1}\ldots u_0)b,\quad V = (v{n-1}\ldots v_0)b,\quad W = (w{n-1}\ldots w_0)_b.$

Define for each $j$ with $0 \le j \le n$ the partial values

$U_j = \sum_{i=0}^{j-1} u_i b^i,\quad V_j = \sum_{i=0}^{j-1} v_i b^i,\quad W_j = \sum_{i=0}^{j-1} w_i b^i,$

with $U_0 = V_0 = W_0 = 0$.

Let $k_j$ denote the value of the variable $k$ after completing step A2 for index $j$, and after step A3 increments $j$ (so $k_j$ is the carry into position $j+1$ during the next iteration, with $k_0 = 0$ from initialization).

The inductive assertion is

$U_j + V_j = W_j + k_j b^j \qquad (0 \le j \le n).$

Initialization

At the start, $j = 0$ and $k_0 = 0$. Since $U_0 = V_0 = W_0 = 0$, the assertion becomes

$0 = 0,$

so it holds for $j = 0$.

Maintenance

Assume for some $j$ with $0 \le j < n$ that

$U_j + V_j = W_j + k_j b^j.$

During step A2 at index $j$, the algorithm sets

$s_j = u_j + v_j + k_j.$

Then

$w_j = s_j \bmod b,\quad k_{j+1} = \left\lfloor \frac{s_j}{b} \right\rfloor.$

Write

$s_j = w_j + k_{j+1} b.$

Multiply by $b^j$:

$s_j b^j = w_j b^j + k_{j+1} b^{j+1}.$

Add this to the inductive hypothesis:

$U_j + V_j + s_j b^j = W_j + w_j b^j + k_{j+1} b^{j+1} + k_j b^j - k_j b^j.$

Substituting $s_j = u_j + v_j + k_j$ gives

$U_j + u_j b^j + V_j + v_j b^j + k_j b^j = W_j + w_j b^j + k_{j+1} b^{j+1}.$

By the definitions of $U_{j+1}, V_{j+1}, W_{j+1}$,

$U_{j+1} + V_{j+1} + k_j b^j = W_{j+1} + k_{j+1} b^{j+1}.$

Since $k_j b^j$ is carried exactly into the computation of $s_j b^j$ at the next digit position, cancellation yields

$U_{j+1} + V_{j+1} = W_{j+1} + k_{j+1} b^{j+1}.$

Thus the assertion holds for $j+1$.

Termination

After the loop completes, $j = n$. The assertion gives

$U_n + V_n = W_n + k_n b^n.$

Since $U_n = U$ and $V_n = V$ are $n$-place integers, $U + V < 2b^n$, so $k_n \in {0,1}$. Also $W_n$ is the $(n+1)$-place radix-$b$ representation of the sum, so $k_n$ is exactly the leading digit $w_n$ and

$(w_n w_{n-1}\ldots w_0)_b = U + V.$

This completes the proof. ∎