Courtesy Apt, ETAC, Hoogerwoord, & Voermans

Courtesy Apt, ETAC, Hoogerwoord, & Voermans

This note deals with a problem posed to me by Apt when I visited him in Amsterdam. I mentioned the problem at the next session of the ETAC, where we did not solve it; Hoogerwoord, however, had suggested a structure of the argument and had provided a major building block. The next day, Voermans provided the missing ingredient and completed the proof.

We consider an expression built according to the following syntax

$$ \begin{array}{l} < e x p > := < a t o m > \mid \neg < e x p > \ | \vee < e x p > < e x p > | \wedge < e x p > < e x p > \ \end{array} $$

We are given the following rewrite rules

(0) $\neg \neg x \rightarrow x$ (1) $\neg \vee {xy} \rightarrow \land \neg x \sim y$ (2) $7 \land {xy} \rightarrow 7 \land {xy}$ (3) $\land x\lor y\;z \rightarrow \lor \land x\;y \land x\;z$ (4) $\land \lor x\underline{y}z \rightarrow \lor \land x\overline{z} \land y\underline{z}$

in which $x,y,z$ are subexpressions of type $< \exp \rangle$ . Our algorithm consists of repeatedly replacing a subexpression matching the left-hand side of a rewrite rule by the corresponding

right-hand side of that rule. The challenge is to prove that the algorithm terminates because, sooner or later, none of the rewrite rules is applicable any more.

We try to define a function $f$ from expressions to natural numbers - or, if the need arises, to a more general well-founded domain - such that the function value decreases when a rewrite rule is applied to the argument. Our first decision - taken for the sake of simplicity - is to define

$$ f. < a t o m > = c o n s t $$

we define

$$ \begin{array}{l} f _ {i} (7 x) = \mathrm {n e g .} (f _ {i} x) \ p. (v \times y) = d i s. (p. x, p. y) \ f \cdot (\wedge x y) = c o n. (f \cdot x, f \cdot y) \ \end{array} $$

the challenge is now to define const, neg, dis, and con in such a way that application of rewrite rules leads to a decrease of $f$ . Since rewrite rules can be applied to replace subexpressions , whereas the $f$ -value of the whole expression has to decrease, the functions neg,dis,and con have to be strongly monotonic in all their arguments,i.e.

(5) $p > {p}^{\prime } \land q > {q}^{\prime } \Rightarrow \neg \operatorname{eq}p > \operatorname{neg}q \land$

$$ \begin{array}{l} d i s. (p, q) > d i s. (p ^ {\prime}, q) \land \ d i s. (p, q) > d i s. (p, q ^ {\prime}) \land \ \operatorname {c o n.} (p, q) > \operatorname {c o n.} (p ^ {\prime}, q) \wedge \ c o n. (p, q) > c o n. (p, q ^ {\prime}) \ \end{array} $$

To begin with we focus our attention on

(3) and (4), which describe how $\wedge$ distributes

over v , viz. in the same way as * (times)

distributes over $+$ (plus). This last observation

suggests to choose for dis and con something

like $\operatorname{dis}\left( {p,q}\right) = p + q$ and $\operatorname{con}.\left( {p,q}\right) = p * q$

I wrote "something like" because the above

choice would leave the f-value under rewrites

(3) and (4) unchanged. Let us investigate with

$$ d i s. (p, q) = p + q, \mathrm {c o n .} (p, q) = p \times q - c $$

the requirement that (3) leads to a decrease of $p$ :

$$ \begin{array}{l} f. (\wedge \times \vee y z) > f. (\vee \wedge x y \wedge x z) \ = {\mathrm {d e f . o f} c o n; \mathrm {d e f . o f} d i s } \ f. x * f. (v y z) - c > f. (\wedge x y) + f. (\wedge x z) \ = {\mathrm {d e f . o p d i s}; \mathrm {d e f . o p c o n} } \ f _ {x} * (f _ {y} + f _ {z}) - c > f _ {x} * f _ {y} - c + f _ {x} * f _ {z} - c \ = {\mathrm {a l g e b r a} } \ c > 0 \ \end{array} $$

The requirement that application of (4)

leads to an f-decrease is equivalent to the

same $c > 0\;$ In order to ensure that $f$ -values

are natural we choose a natural const satisfying

$$ \mathrm {c o n s t} ^ {2} - c \geq \mathrm {c o n s t}. $$

These conditions can be satisfied, e.g. by $c = 1$ and $\mathrm{const} = 2$ . We are left with the obligation of constructing a neg, such that rewritings (0),

(1) and (2) decrease

From (0) we conclude the requirement

(6) $\;{neg.}\left( {{neg} \cdot p}\right) > p$

From (1) we conclude the requirement

(7) $\;{neg} \cdot \left( {p + q}\right) > {neg} \cdot p * {neg} \cdot q - c$

From (2) we conclude the requirement

(8) $\neg \operatorname{eq}.\left( {p * q - c}\right) > \operatorname{eq.}p + \operatorname{eq.}q$

These three requirements should be satisfied for $p \geq {const}$ and $q \geq {const}$ ,const being the minimum

(6) is satisfied if $\neg \operatorname{neg} p > p$ ; for monotonic neg satisfying $\neg \operatorname{neg} p > p$ , (8) is unlikely to present problems for larger arguments; (7) imposes a clear constraint, but since $c > 0$ ,

$$ \begin{array}{l l} & {\mathrm {s a t i s f i e s (7) . F o r c = 1 a n d c o n s t = 2 ,}} \ & {\mathrm {d = 2 i s t o o s m a l l - s i n c e 2 ^ {2 \times 2 - 1} = 2 ^ {2} + 2 ^ {2},}} \end{array} $$

(8) can be violated-; $d = 3$ , however, does the job. In short

$$ \begin{array}{l} f. < a t o m > = 2 \ f: (7 x) = 3 ^ {f \cdot x} \ f. (v \times y) = f. x + f. y \ f. (x y) = f. x * f. y - 1 \ \end{array} $$

is a witness demonstrating the existence of a variant function. Another witness is given by $c, \operatorname{const}, d = 1, 3, 2$

At the ETAC, I got stuck. I started with (0), (1) & (2), mapping the latter two on each other by ignoring the difference between $\land$ and $\lor$ ; subsequently introducing the ignored difference by taking (3) & (4) into account gave serious problems. The advantage of starting with (3) $\lambda$ (4) is that then $\neg$ is ignored automatically.

The reader is asked to realize how much the derivation has been eased by the introduction of the named functions const, neg, dis, & con .

Nuenen. 29 August 1991

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 USA