A sequel to EWD822 (with C.S.Scholten)

by Edsger W. Dijkstra and C.S. Schoften

In EWD822 it was boldly stated that $wp(S,?)$ is infinitely conjunctive. Neither there, nor in "A Discipline of Programming" this has been proved. It follows from our exercises with wlp in EWD816; the purpose of this note is to explore more direct proofs. Out of methodological interest we investigated what a proof looks like if $wp(DO,R)$ is defined as the strongest solution of

(0) $X : \left\lbrack {X = \left( {¬ B \vee {wp}\left( {S,X}\right) }\right) ∧ \left( {B \vee R}\right) }\right\rbrack$

In our exploration we shall not require $wp(S,?)$ in (0) to be or-continuous; as a result, our conclusions will also have a bearing on the case of unbounded nondeterminacy. We shall, however, use that $wp(S,?)$ is infinitely conjunctive.

To begin with, we observe that (0) is of the form

(1) $X : \left\lbrack {X = b \times R}\right\rbrack$

in which $b$ is "infinitely doubly conjunctive", i.e. satisfies

(2) $\left[ b \left(\underset{i \mid X i}{A} \right)\left(\underset{i \mid Y i}{A} \right. = \left(\underset{i \mid X i}{A} \cdot b \left(X i\right)\right) \right]$ for all predicate sequences $X_{i}$ and $Y_{i}$ (i≥0).

This is a consequence of the general formula

(3) $\left[(\underline{A} i: (¬ B \vee X i) \wedge (B \vee Y i)) = (¬ B \vee (\underline{A} i: X i)) \wedge (B \vee (\underline{A} i: Y i))\right]$

and the fact that $w p\left( {S,?}\right)$ is infinitely conjunctive. From its being infinitely doubly conjunctive it follows that $b$ is infinitely conjunctive,and hence conjunctive and monotonic,in both its arguments.Another consequence is

(4) [ P ⇒ Q ] ⇒ [ b (X ∧ Y) P = b X P ∧ b Y Q ].

Our target is now to prove Lemma 0, which expresses the infinite conjunctivity of $wp(DO, R)$ defined as strongest solution of (0).

Lemma 0. Let the (two-argument) predicate transformer be infinitely doubly conjunctive. Let $R_i$ ( $i ≥ 0$ ) be an infinite sequence of predicates. Let $P$ be the strongest solution of

(5) X: [ b X (\underline {{A}} i: R i) = X ] ;

let ${Qj}\left( {j ≥ 0}\right)$ be the strongest solution of

(6) X: [ b X (R _ {j}) = X ]

Then $\left\lbrack {P = \left( {\underline{A}j : Qj}\right) }\right\rbrack$ .

Proof. Since $b$ is monotonic in its first argument -see EWD822-, $P$ is also the strongest solution of

(5 ^ {\prime}) X: [ b X (\underset {i} {A _ {i}}; R _ {i}) ⇒ X ] .

Similarly, ${Qj}$ is also the strongest solution of

(6) X: [ b X (R _ {j}) ⇒ X ]

Apparently unavoidable, the proof consists of two parts: we have to show that $\left( {\underline{A}}{j}\right) \left( {Q}{j}\right)$ is a solution of (5)-or (5')- and that it is its strongest one; we have chosen (5')

The first part is straightforward: we have for any $z$

\begin{array}{l} [ z = b (\underline {{A}} _ {j}: Q _ {j}) (\underline {{A}} _ {i}: R _ {i}) ] \ = {b i s \mathrm {i n f i n i t e l y d o u b l y c o n j u n c t i v e} } \ [ z = (\underline {{A}} _ {j}: b (\underline {{O}} _ {j}) (\tilde {R} _ {j})) ] \ ⇒ {(6 ^ {\prime}) } \ [ z ⇒ (\underline {{A}} j: Q j) ] \ \end{array}

Hence $\left( {\underline{A}j : Qj}\right)$ is a solution of $\left( {5}^{\prime }\right) ;P$ being its strongest solution,we have proved $\left\lbrack {P ⇒ \left( {\underline{A}j : Qj}\right) }\right\rbrack$ .

Note. In the above appeal to (6') we have only used that ② $j$ is a solution of (6'). (End of Note.)

The difficulty of the second part, viz. the proof of $\left\lbrack {\left( {A}_{j} : Qj}\right) ⇒ P}\right\rbrack$ ,is the exploitation of the fact that the Qj are the strongest solutions of (6) and (6). To this end we observe first

\begin{array}{l} [ (A _ {i}: Q _ {i}) ⇒ P ] \ = {\mathrm {p r e d i c a t e c a l c u l u s , f o r s o m e c h o s e n} j } \ [ Q _ {i} ∧ (A _ {i}: Q _ {i}) ⇒ P ] \ = {\mathrm {d e f i n i t i o n o f i m p l i c a t i o n a n d d e M o r g a n} } \ [ Q j ⇒ (\underline {{E}} _ {i}: ¬^ {\prime} Q _ {i}) v P ] ; \ \end{array}

Qj being defined as the strongest solution of (6'), the last line can be proved by showing that (Eq : 7 Q i) v P is a solution of (6')

true

\begin{array}{l} = {\text {p r e d i c a t e c a l c u l u s} } \ [ (A _ {i}: Q _ {i}) ∧ P ⇒ P ] \ ⇒ {b \mathrm {i s m o n o t o n i c i n i s f i r s f i r s t a r g u m e n t} } \ [ b ((A _ {i}: Q _ {i}) \wedge P) (A _ {i}: R _ {i}) ⇒ b P (A _ {i}: R _ {i}) ] \ ⇒ {P i s a s o l u t i o n o f (5 ^ {\prime}) } \ [ b ((A _ {i}: Q _ {i}) ∧ P) (A _ {i}: R _ {i}) ⇒ P ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ b ((E _ {i}: ¬ Q _ {i}) \vee P) \wedge (A _ {i}: Q _ {i})) (A _ {i}: R _ {i}) ⇒ P ] \ = {(4), \mathrm {s i n c e f o r s o m e c h o s e n} j [ (\underline {{A}} i: \mathbb {R} i) ⇒ \mathbb {R} j ] } \ [ b (\underline {{E}} c: ¬ Q _ {i}) v P) (R _ {j}) \wedge b (\underline {{A}} c: Q _ {i}) (\underline {{A}} c: R _ {i}) ⇒ P ] \ = {b i s \mathrm {i n f i n i t e l y d o u b l y c o n j u n c t i v e} } \ [ b ((E _ {i}: ¬ Q _ {i}) \vee P) (R _ {j}) \wedge (\underline {{A}} _ {i}: b (Q _ {i}) (R _ {i})) ⇒ P ] \ = {Q _ {s} a r e s o l u t i o n s o f (6) } \ [ b ((E i: ¬ Q i) \vee P) (R j) \wedge (\underline {{A}} i: Q i) ⇒ P ] \ = {d e f i n i t i o n o f i m p l i c a t i o n a n d d e M o r g a n s \ [ b (\underline {{E}} _ {i}: ¬ Q _ {i}) v P) (R _ {j}) ⇒ (\underline {{E}} _ {i}: ¬ Q _ {i}) v P ] \ \end{array}

Note From the above proof it follows that for $\left\lbrack {\left( {A}_{i} : Qi}\right) = P}\right\rbrack$ to hold,only one of the Qi -viz. Qj- needs to be the strongest solution of (6), while for the others it suffices to be a solution of (6). (End of Note.) (End of Proof.)

Perhaps a much simpler proof exists; if so, we were so far unable to construct it. The above proof leaves us with mixed feelings. That, suddenly, implications pop up all over the pages was only to be expected. But though its individual steps are simple, we take no offence when the last part is characterized as a piece of tricky shunting. It is really not nice; note, for instance, that on the one hand we use that $Qj$ is the strongest solution

of (6') - and we had to, since we could not prevent the implications from creeping in - while at the very end it is essential that the Q's are solutions of the "stranger" equation (6). In short: without the bit of theory devel- oped in EWD822, this proof would have been impossible.

We can somewhat simplify the proof of Lemma 0 by essentially concentrating the "sticky shunting" in the proof of Lemma 1. The (two-argument) predicate transformer $b$ is "doubly" conjunctive" means

[ b (X \wedge X ^ {\prime}) (R \wedge R ^ {\prime}) = b X R \wedge b X ^ {\prime} R ^ {\prime} ] f o r a n y X, X ^ {\prime}, R, R ^ {\prime}.

Lemma 1. Let $b$ be a doubly conjunctive predicate, trans-former. Let $P$ be the strongest solution of

$\left{ {1,2,3,4}\right} : \left{ {{1.3},{1.4},{1.5}}\right}$

let $Q$ be a solution of (7); let $H$ be the strongest solution of

(8) $X : \left\lbrack {b \times T = X}\right\rbrack$

Then $\left\lbrack {P = Q ∧ H}\right\rbrack$

Proof. We first show $[P ⇒ Q ∧ H]$ by demonstrating that $Q ∧ H$ is a solution of (7). We have for any $Z$

\begin{array}{l} [ Z = b (Q \wedge H) R ] \ = {b i s d o u t _ {y} c o n j u n c t i v e } [ Z = b Q R \wedge b H T ] \ = {Q a n d H a r e s o l u t i o n s o f (7) a n d (8) r e s p e c h i v e l y } [ Z = Q \wedge H ] \ \end{array}

We now show $[Q ∧ H ⇒ P]$ , i.e. $[H ⇒ P \lor Q]$ by showing that $P \lor Q$ is a solution of $X: [bX T ⇒ X]$ , of which $t$ is the strongest solution.

true

\begin{array}{l} = [ b (P \wedge Q) R = b (P \wedge Q) R ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ b ((p \vee ¬ Q) \wedge Q) R = b (p \wedge Q) R ] \ = {b \mathrm {i s d o u b l y c o n j u n c t i v e} } \ [ b (P v ¬ Q) T ∧ b Q R = b P R ∧ b Q R ] \ = {P a n d Q a r e s o l u t i o n s o f (7) } \ [ b (P \vee ¬ Q) T \wedge Q = P \wedge Q ] \ ⇒ {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ b ^ {\prime} (P _ {v ¬ Q}) T ⇒ P _ {v ¬ Q} ] \ \end{array}

(End of Proof)

Lemma 0 is now easily proved: straightforward substitution shows that the infinite conjunction of arbitrary solutions ${Q}^{\prime }$ of(6) is a solution ${P}^{\prime }$ of(5),i.e. $\left\lbrack {{P}^{\prime } = \left( {\underline{A}j : {Q}^{\prime }j}\right) }\right\rbrack$ . Taking at both sides the conjunction with $H$ then yields Lemma 0.

In this last version, the meaning of the adjective "strongest" is only used in the proof of Lemma 1. From then onwards we only use the equality expressed by Lemma 1. We expect this to be the case in very many proofs; it is very much like separating a proof of total correctness in a proof of partial correctness and a proof of termination:

9 May 1982

drs. C.S. Scholten

Scientific Adviser

Philips Research Laboratories

5600 MD EINDHOVEN

The Netherlands

prof. dr. Edsger W. Dgkstra

Burroughs Research Fellow

Plataansstraat 5

5671 AL NUENEN

The Netherlands