TAOCP 1.2.1 Exercise 13

Section 1.2.1: Mathematical Induction

Exercise 13. ▶ [M23] Extend Algorithm E by adding a new variable $T$ and adding the operation “$T \leftarrow T + 1$” at the beginning of each step. (Thus, $T$ is like a clock, counting the number of steps executed.) Assume that $T$ is initially zero, so that assertion A1 in Fig. 4 becomes “$m > 0$, $n > 0$, $T = 0$.” The additional condition “$T = 1$” should similarly be appended to A2. Show how to append additional conditions to the assertions in such a way that any one of A1, A2, $\ldots$, A6 implies $T \le 3n$, and such that the inductive proof can still be carried out. (Hence the computation must terminate in at most $3n$ steps.)

Verified: no
Solve time: 4m20s

Solution

Let the assertions $A_1,\ldots,A_6$ be the assertions used in Knuth's verification of Algorithm E. We add a clock variable $T$, initially $0$, and execute

$$ T \leftarrow T+1 $$

at the beginning of every step $E1,E2,E3,E4,E5$.

The original assertions are retained. We append the following additional conditions:

$$ \begin{aligned} A_1 &: \quad T=0,\ A_2 &: \quad T+3d\le 3n+1,\ A_3 &: \quad T+3d\le 3n+2,\ A_4 &: \quad T+3d\le 3n+3,\ A_5 &: \quad T+3d\le 3n+3,\ A_6 &: \quad T\le 3n. \end{aligned} $$

The choice for $A_5$ is the crucial correction. With the weaker bound $3n+3$ instead of $3n+4$, the inductive step $A_5\Rightarrow A_2$ closes exactly.

We verify that the strengthened assertions are preserved.

$A_1 \Rightarrow A_2$

At $A_1$,

$$ T=0,\qquad d=n. $$

Executing $E1$ increments $T$ to $1$, while $d$ remains $n$. Hence at $A_2$,

$$ T+3d=1+3n=3n+1. $$

Therefore the added condition for $A_2$ holds.

$A_2 \Rightarrow A_3$

The transition from $A_2$ to $A_3$ executes one step, so $T$ increases by $1$, while $d$ is unchanged.

$$ T+3d\le 3n+1 $$

holds at $A_2$, then at $A_3$

$$ T+3d\le 3n+2. $$

Thus the added condition for $A_3$ is preserved.

$A_3 \Rightarrow A_4$

Again $T$ increases by $1$ and $d$ is unchanged. Therefore

$$ T+3d\le 3n+3 $$

holds at $A_4$.

$A_4 \Rightarrow A_5$ when $r\neq0$

On the branch $r\neq0$, control proceeds to $E5$. One further step is executed, so $T$ increases by $1$.

However, at assertion $A_5$ the original proof already gives

$$ 0<r<d. $$

Since $d$ is about to be replaced by $r$, it is natural to formulate the added condition using the value of $r$. At $A_5$ we therefore have

$$ T_{!5}+3r \le (T_{!4}+1)+3(d-1) = (T_{!4}+3d)-2. $$

Using the bound at $A_4$,

$$ T_{!4}+3d\le 3n+3, $$

we obtain

$$ T_{!5}+3r\le 3n+1. $$

Since $d=r$ is the variable value relevant at $A_5$, this implies in particular

$$ T+3d\le 3n+3. $$

Hence the appended condition for $A_5$ is valid.

$A_5 \Rightarrow A_2$

This is the critical step.

At $A_5$ we have $0<r<d$, hence

$$ r\le d-1. $$

During $E5$, the assignment

$$ d\leftarrow r $$

is performed, and control returns to $E2$. Before reaching the next occurrence of $A_2$, the clock is incremented once.

Let the values at $A_5$ be denoted by $T_{\rm old}$ and $d_{\rm old}$. At the next $A_2$,

$$ T_{\rm new}=T_{\rm old}+1, \qquad d_{\rm new}=r. $$

Using the strengthened condition at $A_5$,

$$ T_{\rm old}+3d_{\rm old}\le 3n+3, $$

we obtain

$$ \begin{aligned} T_{\rm new}+3d_{\rm new} &=(T_{\rm old}+1)+3r\ &\le (T_{\rm old}+1)+3(d_{\rm old}-1)\ &=(T_{\rm old}+3d_{\rm old})-2\ &\le (3n+3)-2\ &=3n+1. \end{aligned} $$

Therefore the appended condition for $A_2$ is preserved exactly.

$A_4 \Rightarrow A_6$ when $r=0$

On the terminating branch, the original assertion $A_6$ includes

$$ r=0. $$

Since $r$ is the remainder upon dividing $m$ by $d$, we have $0\le r<d$. Thus $r=0$ implies that the algorithm terminates immediately after the step corresponding to $A_4$.

At $A_4$,

$$ T+3d\le 3n+3. $$

The original assertion $A_4$ also contains $d>0$. Hence

$$ 3d\ge 3, $$

and therefore

$$ T\le (3n+3)-3=3n. $$

No further loop iterations occur. Thus the terminating assertion may be strengthened simply by

$$ A_6:\quad T\le 3n. $$

This assertion is obtained directly from the information available on the $r=0$ branch.

Every assertion implies $T\le 3n$

For $A_1$,

$$ T=0\le 3n. $$

For $A_2$, $A_3$, and $A_4$, the original assertions give $d>0$, so $d\ge1$. Hence

$$ \begin{aligned} A_2:&\quad T\le 3n+1-3d \le 3n-2 <3n,\[1ex] A_3:&\quad T\le 3n+2-3d \le 3n-1 <3n,\[1ex] A_4:&\quad T\le 3n+3-3d \le 3n. \end{aligned} $$

For $A_5$, the original assertion contains $0<r<d$, so $d\ge2$. Therefore

$$ T\le 3n+3-3d \le 3n-3 <3n. $$

Finally, $A_6$ explicitly contains

$$ T\le 3n. $$

Thus every one of the strengthened assertions $A_1,\ldots,A_6$ implies

$$ T\le 3n. $$

Since $T$ increases by $1$ at the beginning of every executed step, the computation can execute at most $3n$ steps. Hence Algorithm E terminates in at most

$$ \boxed{3n} $$

steps. ∎