ATAC’s proof of Scholten’s theorem

ATAC's proof of Scholten's theorem

In a recent letter, W.H.J. Fegen wrote me that C.S. Scholten had offered the following theorem to the ETAC.

(o) Let predicate transformers $p$ and $q$ satisfy

$$ [ p. X \vee Y ] = [ X \vee q. Y ] \quad \mathrm {f o r a l l} X, Y; $$

(1) let, for all $X$ ,h. $X$ be the weakest solution

$$ \begin{array}{r l} {\mathcal {P}} & \ & {\quad \mathcal {Y}: [ Y = X \land p. Y ] \quad ;} \end{array} $$

(2) let, for all $X$ , $k \in X$ be the weakest solution

$$ \begin{array}{r l} {\mathrm {o f}} & \ & {Y: [ Y \equiv X \land q. Y ]} \end{array} $$

Then predicate transformers $h$ and $k$ satisfy

(3) $\left\lbrack {h.A \vee B}\right\rbrack \equiv \left\lbrack {A \vee k.B}\right\rbrack \;$ for all $A,B$ .

This note records the proof that the ATAC designed on its session of 28 March 1989. We first give the three crucial lemmata, postponing their discussion until later.

From (0) one can conclude

Lemma 0 Predicate transformers $p,q$ are universally conjunctive

and the generalization of (0)

Lemma 1 (An:osn: $\left\lbrack {{p}^{n} \cdot X \vee Y}\right\rbrack \equiv \left\lbrack {X \vee {q}^{n}Y}\right\rbrack$ ) for

all $X, Y$

From Lemma 0 follows the monotonicity of $p, q$ and hence, on account of Knaaster-Tarski, the existence of $h$ and $k$ . From Lemma 0 follows the and-continuity of the right-hand sides of (1) and (2), which leads to

Lemma 2 For all $X$

$$ [ h, X \equiv (\underline {{A}} n: 0 \leq n: p ^ {n}. X) ] \quad a n d, s i m i l a r l y, $$

$$ [ k, X \equiv (\neg n: 0 \leq n: q ^ {n}: X) ] \quad . $$

Proof of (3) We observe for any $A,B$

$$ [ h, A \lor B ] $$

$$ \begin{array}{l} = {\text {L e m m a} 2 } \ [ (\underline {{A}} n: p ^ {n} A) \vee B ] \ = {\vee \overline {{\mathrm {o v e r}}} A } \ [ (\underline {{A}} _ {n}: p ^ {n}. A \vee B) ] \ = {\mathrm {i n t e r c h a n g e} } \ (\underline {{A}} n: [ p ^ {n}. A \vee B ]) \ = {\mathrm {L e m m a} 2 } \ (A n: [ A \vee q ^ {n}. B ]) \ = {\mathrm {i n t e r c h a n g e} } \ [ (A n: A \vee q ^ {n}. B) ] \ = {\vee o v e r A } \ [ A \vee (\overline {{A}} n: q ^ {n}. B) ] \ = {\mathrm {L e m m a} 2 } \ [ A \vee k. B ] \ \end{array} $$

(End of Proof of (3).)

We shall not repeat here the proof of Lemma 0, which we have given many times; we only recall that, like the proof of (3), it relies on the dis- tribution of $v$ over $\mathbb{H}$ and the interchange of "everywhere" with universal quantification.

Proof of Lemma 1. By induction over $n$ .

We observe that for $n = 0$ -and for $n = 1!$

(4) $\left\lbrack {{p}^{n} \cdot X \vee Y}\right\rbrack \equiv \left\lbrack {X \vee {q}^{n}Y}\right\rbrack \;\left{ {\text{ for all }X,Y.}\right.$

Next we observe for any $X, Y$

$$ \begin{array}{l} [ p ^ {n + 1}. X \vee Y ] \ = {d e f. o f f u n c t i o n a l i t e r a t i o n } \ [ p ^ {n}. (p. x) \vee Y ] \ = {(\mathrm {4}) \mathrm {w i t h} X := p. X } \ [ p. X \vee q ^ {n}. Y ] \ = {0) w i t h Y := q ^ {n}. Y } \ [ X \vee q. (q ^ {n}. Y) ] \ = {\mathrm {d e f . o f f u n c t i o n a l i t e r a t i o n} } \ [ X \vee q ^ {n + 1}, Y ] \ \end{array} $$

(End of Proof.)

Remark Functional iteration can be defined recur. sively by ${f}^{n + 1} \cdot X = f \cdot \left( {{f}^{n} \cdot X}\right)$ or ${f}^{n + 1} \cdot X = {f}^{n} \cdot \left( {{f}^{n} \cdot X}\right)$ ; note that the above proof uses both definitions. (End of Remark.)

Proof of Lemma 2 The proof consists of showing that

(i) $\left( {{An} : 0 \leq n : {p}^{n} \cdot X}\right)$ solves

(5) $Y : \left\lbrack {Y \equiv X \land P,Y}\right\rbrack ,$ and that (ii) any solution 2 of (5) satisfies $\left\lbrack {Z \Rightarrow \left( {\underline{A}n : 0 \leq n : {p}^{n} \cdot X}\right) }\right\rbrack$

${ad}\left( i\right)$ $X \land p.\left( {\underline{A}n : 0 \leq n : {p}^{n} \cdot X}\right)$

$$ \begin{array}{l} = {p \mathrm {u n i v e r s a l l y c o n j u n c t i v e} } \ = {\mathrm {d e f . o f f u n c t i o n a l i t e r a t i o n} } \ p ^ {0}. X \wedge (\underline {{A}} n: 0 \leq n: p ^ {n + 1}. X) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} n: 0 \leq n: p ^ {n}. X) \ \end{array} $$

ad(ii) We observe for any solution $z$ of (s)

$\left\lbrack {Z \Rightarrow X}\right\rbrack$ and (8) $\left\lbrack {z \Rightarrow p,z}\right\rbrack$

Hence

$$ [ Z \Rightarrow (\underline {{A}} n: p ^ {n}. X) ] $$

$\Leftrightarrow { \left( 7\right)$ and monotonicity of $A$ and of ${p}^{n}}$

$$ [ z \Rightarrow (\underline {{A}} n: p ^ {n}. z) ] $$

$= \left{ {{pred}\;{c}_{al} \cup {cal} \cup s}\right}$

$$ (A _ {n}: [ Z \Rightarrow p ^ {n}. Z ]) $$

which is shown by mathematical induction. We

observe $\left\lbrack {Z \Rightarrow {p}^{0} \cdot Z}\right\rbrack$ and

$$ [ 2 \Rightarrow p ^ {n + 1}. 2 ] $$

$$ \begin{array}{l} \Leftrightarrow \quad {\mathrm {t r a n s i t i v i t y} o f \Rightarrow } \ [ z \Rightarrow p. z ] \wedge [ p. z \Rightarrow p ^ {n + 1}. z ] \ = {(\mathbf {8}) } \ [ p, 2 \Rightarrow p ^ {n + 1}, 2 ] \ \Leftrightarrow {m o n o t o n i c i t y o f p } \ [ z \Rightarrow p ^ {n}. z ] \ \end{array} $$

(End of Proof of Lemma 2)

Remark Originally we intended to prove Lemma 2 using the well-known closed form for the weakest fixpoint of an and-continuous function. However, $p$ being universally conjunctive, it turned out to be simpler not to use that closed form and to prove Lemma 2 from first principles. (End of Remark.)

The reason for devoting a note to this theorem of Scholten's is that my first effort to prove it went awry; in my first effort, I used my standard heuristics, which were thus shown not to be infal- lible. I tried -h.A and k.B being given as ex- treme solutions-to prove (3) by mutual implication and tried to show LHS $\Rightarrow$ RHS

$$ \begin{array}{l} [ A \vee k. B ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ \neg A \Rightarrow k, B ] \ \Leftrightarrow {k, B \text {i s t h e w e a k e s t} \text {s o l . o f} Y: [ Y \Rightarrow B \wedge q. Y ] \ [ \neg A \Rightarrow B \land q. (\neg A) ] \ \end{array} $$

$$ \begin{array}{l} = {\text {p r e d i c a t e c a l c u l u s} } \ [ A \vee B ] \wedge [ A \vee q. (i A) ] \ = {(0) } \ [ A \vee B ] \wedge [ p. A \vee r. A ] \ \Leftrightarrow {\mathrm {b e c a u s e o f (1)} [ h. A \Rightarrow A ]; \mathrm {p r e d i c a t e c a l u l u s} } \ [ h. A \lor B ] \land [ A \Rightarrow p. A ] \ \end{array} $$

and there I was stuck: I had no way of meeting the remaining proof obligation $\left\lbrack {h.A \vee B}\right\rbrack \Rightarrow \left\lbrack {A \Rightarrow p.A}\right\rbrack$ . The moral of the story is probably (possibly?) that we have to consider the truth of [A v k.B] for values of ?A that fail to solve the tolerant equation of which k.B is the weakest solution.

After this failure, the ATAC tried to establish (3) directly by equational reasoning. It has the added advantage of not destroying the symmetry between the two sides of (3); moreover, (0), which has to be used, has the same form.

Inks Lake State Park

31 March 1989

prof. dr. Edsger W. Dgkstra

Department of Computer Sciences

The University of Texas at Austin

Austn. TX 78712 - 1188

USA