A summary of formulae (and of some theory)

A summary of formulae (and of some theory).

The following contains nothing new and nothing deep. It is written in reaction to my exposure to recent work of C.A.R.Hoare and of C.S.Scholten, in which I needed all kinds of formulae of which I was, until recently, only vaguely aware. Some formulae I knew longer have been included for the sake of completeness. As we have done lately, universal quantification over all states will be denoted by enclosure within square brackets. The boolean operators are in the order of decreasing priority: $¬ ∧ V ⇒ =$ . Following a suggestion of Jan L.A. van de Sneepscheut's, I shall not rely on conjunction's priority over disjunction: the omission of brackets would destroy too much symmetry. The letters $B,P,Q,R,X,Y$ ,and $Z$ will only be used to denote predicates. Functional application has the highest priority of all.

(o) $\left\lbrack {P ⇒ Q = \left( {P ∧ Q = P}\right) }\right\rbrack$ For all $P,Q$ (1) $\left\lbrack {P ⇒ Q = \left( {{P}^{v}Q = Q}\right) }\right\rbrack$ for all $P,Q$ . (2) $\left\lbrack {\left( {{¬ B} \vee P}\right) ∧ \left( {{B}^{ ∧ }Q}\right) = \left( {{B}^{ ∧ }P}\right) \vee \left( {{¬ B} ∧ Q}\right) }\right\rbrack$ for all $P,Q,B$

A predicate transformer $f$ that distributes over conjunction, i.e. that satisfies

(3) $\left\lbrack {f\left( {{P}^{A}Q}\right) = f{P}^{A} ∧ {fQ}}\right\rbrack$ for all ${P}_{2}Q$

is called "conjunctive". Similarly, a predicate trans- from $f$ that distributes over disjunction,i.e. that satisfies

(4) $\left\lbrack {f\left( {{P}{v}Q}\right) = f{P}{v}fQ}\right\rbrack$ for all ${P}_{v}Q$ is called "disjunctive". A predicate transformer $f$ that is conjunctive or disjunctive is monotonic, i.e. satisfies (5) $\left\lbrack {P ⇒ Q}\right\rbrack ⇒ \left\lbrack {fP ⇒ fQ}\right\rbrack$ for all $P,Q$ .

For conjunctive $f,$ (5) follows from (0), for disjunctive $f,$ (5) follows from (1) more precisely from their consequences $[P ⇒ Q] = [P ∧ Q = P]$ and $[P ⇒ Q] = [P \lor Q = Q]$ respectively. Since being conjunctive or disjunctive is not uncommon, monotonic predicate transformers are not uncommon.

An infinite sequence of predicates Pi (i20) such that (Aic: i20: [Pi $⇒$ P(c+1)]) is called "weakening"; one such that (Aic: i20: [P(c+1) $⇒$ Pi]) is called "strengthening". A sequence that is weakening or strengthening is called monotonic, and monotonic sequences are not uncommon since for monotonic $f$ the sequence $p_i^c F$ is weakening and the sequence $p_i^c T$ is strengthening—as can be proved by mathematical induction.

A monotonic sequence of predicates Pi has a limit. for which we have the two alternative expressions

(\underline {{A}} i: i \ge 0: (\underline {{E}} j: j \ge i: P _ {j}))

and

(\underline {{E}}: i \ge 0: (\underline {{A}}: j \ge i: P: j))

For a weakening sequence of predicates Pi we have a third expression for the limit, viz. (Ei: i≥o: Pi); similarly for the limit of a strengthening sequence of

predicates ${P}_{i}$ ,viz. (A: i≥0; Pi).

A predicate transformer $f$ that satisfies for any sequence of predicates $P \in \left( {i ≥ 0}\right)$

(6) $\left\lbrack {f\left( {{A}{i} : i ≥ 0;P}\right) = \left( {{A}{i} : i ≥ 0;f\left( {P}_{i}\right) }\right) }\right\rbrack$

is called "infinitely conjunctive"; an infinitely conjunctive predicate transformer is conjunctive. A predicate transformer $f$ that satisfies (6) for any strengthening sequence of predicates $P_{i}$ ( $i ≥ 0$ ) is called "and-continuous". A predicate transformer may be and-continuous without being conjunctive.

A predicate transformer $p$ that satisfies for any sequence of predicates $P \in \left( {i ≥ 0}\right)$

$\left\lbrack {f\left( {{E}{i} : i ≥ 0 : {P}{i}}\right) = \left( {{E}{i} : i ≥ 0 : f\left( {P}{i}\right) }\right) }\right\rbrack$

is called "infinitely disjunctive"; an infinitely disjunctive predicate transformer is disjunctive. A predicate trans- former $P$ that satisfies (7) for any weakening sequence of predicates Pi (i>0) is called "or- continuous". A predicate transformer may be or-continuous with. out being disjunctive.

For the language fragment from "A Discipline of Programming" the predicate transformer $w p(S,?)$ is infinitely conjunctive, hence conjunctive and and- continuous. As a result of its nondeterminacy it is not disjunctive, hence not infinitely disjunctive; as a result of its nondeterminacy being bounded, $w p(S,?)$ is, however, or- continuous.

For predicate transformer $f$ its "conjugate" ${f}^{ * }$ is defined

Relevant properties are

(8) $\left\lbrack {{f}^{ * }P = fP}\right\rbrack$ for all $P$ ,i.e. the conjugate of (g) ( $f$ is monotonic $) = \left( {f * }\right)$ is monotonic (10) $\left( {f\text{ is }\left( {\text{infinitely}}\right) \text{conjunctive}}\right)$ $= \left( {{f}^{ * }\operatorname{is}\left( {\operatorname{infinitely}}\right) \operatorname{disjunctive}}\right)$ (11) $\left( {f\text{ is }and - \text{ continuous }}\right) = \left( {{f}^{ * }\text{ is }or - \text{ continuous }}\right)$ (12) $[(f\circ g)^{}P = (P^{}\circ g^{*})P]$ for all $P$ , i.e. the conjugate of a functional composition is the functional composition of the conjugates.

As a corollary we mention $\left\lbrack {{p}^{i * }P = {p}^{n * }P}\right\rbrack$ .

(13) For a predicate transformer $f$ defined by

we have

[ f P = (\underline {{A}} i: i \ge 0: f _ {i} P) ] \mathrm {f o r a l l} P

[ f ^ {} P = (\exists i: i \ge 0: f _ {i} ^ {} P) ] f o r a l l P.

For monotonic $f$ the equations

(14) $X : \left\lbrack {pX = X}\right\rbrack$ and $X : \left\lbrack {{pX} ⇒ X}\right\rbrack$ have strongest solutions

that are equal, and

(15) $X \colon \left\lbrack {X = f{X}^{\prime }}\right\rbrack$ and $X \colon \left\lbrack {X ⇒ f{X}^{\prime }}\right\rbrack$ have weakest solutions that are equal.

Property (15) follows from (14) with $f$ replaced by $f^*$ - see g-. For (14) I include C.S. Scholten's proof.

Proof With $Q$ defined by $[Q = (\underline{A} X: [fX ⇒ X]: X)]$ we shall first show that $Q$ is the strongest solution of $X: [fX ⇒ X]$ .

\begin{array}{l} \begin{array}{l} \mathrm {t r u e} \end{array} \ = {\mathrm {d e f i n i t i o n} Q } \ [ Q = (¬ X: [ f X ⇒ X ]: X) ] \ ⇒ {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ Q ⇒ (¬ X: [ f X ⇒ X ]; X) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (A X: [ f X ⇒ X ]: Q ⇒ X) ] \ = {p r e d i c a t e c a l c u l u s } \ (\underline {{A}} X: [ f X ⇒ X ]: [ Q ⇒ X ]) \ ⇒ {f i s m o n o t o n i c } \ (A X: [ f X ⇒ X ]: [ f Q ⇒ f X ]) \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (\underline {{A}} X: [ f X ⇒ X ]; f Q ⇒ f X) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ f Q ⇒ (\underline {{A}} X: [ f X ⇒ X ]: f X) ] \ ⇒ {\text {p r e d i c a t e c a l c u l u s} } \ [ f Q ⇒ (¬ X: [ f X ⇒ X ]: X) ] \ = {\mathrm {d e f i n i t i o n} _ {Q} } \ [ \beta Q ⇒ Q ] \ \end{array}

From the truth of the last line we conclude that $Q$ is a solution of $X: \left\lbrack {pX ⇒ X}\right\rbrack$ ; the line marked with an asterisk

then shows that $\mathbb{Q}$ is its strongest solution.

Continuing the above we have

\begin{array}{l} [ f Q ⇒ Q ] \ ⇒ {f i s m o n o t o n i c } \ [ f (p Q) ⇒ p Q ] \ ⇒ {Q \mathrm {i s t h e s t r u n g e s} \mathrm {s o l u t i o n o f} X: [ P X ⇒ X ] } \ [ Q ⇒ f Q ] \ \end{array}

From the truths of first and last lines we see $\left\lbrack {{fQ} = Q}\right\rbrack$ , showing Q to be a solution of X: [Px=X]. The line marked with an asterisk implies (A X: [P X = X]: [Q ⇒ X]), showing Q to be the strongest solution. (End of Proof.)

For a while we continue our study of the equation $X: \left\lbrack {X = f{X}^{\prime }}\right\rbrack$ with monotonic $f$ . Let $Y$ be a solution. Then we have

(1 6) [ (\exists i: i ≥ 0: f ^ {i} F) ⇒ Y ]

(1 7) [ Y ⇒ (¬ i: i ≥ 0: f ^ {i} T) ]

We shall give the proof of (16).

Proof. Having untrained my usage of the implication, I have to observe first

\begin{array}{l} [ (E i: i \ge 0: f ^ {i} F) ⇒ Y ] \ = {\mathrm {d e f i n i t i o n o f} \mathrm {i m p l i c a t i o n a n d d e M o r g a n s} [ (\mathrm {A c}: i \ge 0: ¬ \rho^ {i} F) \vee Y ] \ = {\text {p r e d i c a t e} \mathrm {c a l u l u s} } \ \end{array}

\begin{array}{l} [ (\underset {i: i \ge 0} {\bigcap} {F V Y }) ] \ = {\mathrm {d e f i n i t i o n o f} \mathrm {i m p l i c a t i o n} } \ [ (\underline {{A}} i: i ≥ 0: {F ⇒ Y) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} i: i ≥ 0: [ f ^ {i} F ⇒ Y ]) \ \end{array}

We proceed by mathematical induction over $i$ .

[{f}^{ \circ }F ⇒ Y]

\begin{array}{l} = {\mathrm {d e f i n i t i o n o f i t e r a t e d f u n c t h o n a l c o m p o s i t i o n} } [ F ⇒ Y ] \ = {p r e d i c a t e c a l c u l u s } \ \end{array}

Step. $\left\lbrack {{f}^{i}F ⇒ Y}\right\rbrack$

\begin{array}{l} ⇒ {f _ {i} \mathrm {i s m o n o t o n i c} } [ f (p ^ {i} F) ⇒ p Y ] \ = {\mathrm {d e f i n i t i o n o f i t e r a t e d f u n c t i o n a l c o m p o s i t i o n} } [ \zeta^ {i + 1} F ⇒ \rho Y ] \ = {Y i s a s o l u t i o n o f X: [ X = f X ] } [ f ^ {i + 1} F ⇒ Y ]. \ \end{array}

(End of Proof.)

If, besides being monotonic, $p$ is or-continuous. (Ei: i.e.: ${p}^{i}T$ ) is the strongest solution of $x : {\left\lbrack x = pX\right\rbrack }^{2}$ . If, besides being monotonic, $p$ is and-continuous, (A i: i.e.: ${p}^{i}T$ ) is the weakest solution of $p : {\left\lbrack x = pX\right\rbrack }^{2}$

We shall prove the first of the two above statements.

Proof. In view of (16) it suffices to show that $\left( {{E}_{C} : c : c : f}\right)$ is a solution of $X : \left\lbrack {X = f/X}\right\rbrack$ . We observe for any $Z$ :

\begin{array}{l} [ Z = f (E i: i \ge 0: f ^ {i} F) ] \ = {f _ {i} \mathrm {i s o r - c o n t i n u o u s a n d} f _ {i} ^ {\prime} F \mathrm {i s a w e a k e n i n g s e q u e n c e} } \ [ Z = (\varepsilon_ {i}: i ≥ 0: f (p ^ {i} F)) ] \ = {\mathrm {d e f i n i t i o n o f i t e r a t e d f u n c t i o n a l c o m p o s i t i o n} } \ [ Z = (\underline {{E}} i: i \ge 0: f ^ {i + 1} F) \vee f ^ {o} F ] \ = {\text {p r e d i c a t e c a l e u l u s} } \ [ \dot {Z} = (\mathrm {E} _ {i}: i \ge 0: f ^ {i} F) ] \ (E n d o f P r o o f.) \ \end{array}

Our interest in the equation $X: [X = fX]$ is derived from our intention that the program segments

(18) $\underset{\partial }{d}o\mathcal{B} \rightarrow S$ od (called "DO") and (19) $\operatorname{if} B \rightarrow S;\underline{\operatorname{do}} B \rightarrow S\underline{\operatorname{od}}\llbracket ¬ B \rightarrow {skip}\frac{P}{2}$

be equivalent. Constructing the ${wp}\left( s\right)$ and the ${wlp}\left( s\right)$ ,res- pectively,for (18) and (19),we conclude that ${wp}\left( {{DO},R}\right)$ be a solution of

(20) $X : \left\lbrack {X = \left( {{7B} \vee {wp}\left( {S,X}\right) }\right) ∧ \left( {{B \vee R}}\right) }\right\rbrack$ and that $\operatorname{wlp}\left( {{DO},R}\right)$ be a solution of $\left( {21}\right) X : \left\lbrack {X = \left( {{7B} \vee {wlp}\left( {S,X}\right) }\right) ∧ \left( {{B \vee R}}\right) }\right\rbrack$

Note. We observe that (20) and (21) are the same equation if [7B v (w p(S, X) = w l p(S, X))] for all X. (End of Note.)

We can rewrite these two equations as

X: [ X = h X ] \mathrm {a n d} X: [ X = k X ] \mathrm {w i t h}

[ h X = (¬ B \vee w p (S, X)) \wedge (B \vee R) ] f o r a l l X, a n d

[ k X = (¬ B \vee w l p (S, X)) \wedge (B \vee R) ] f o r a l l X.

With "IF" equal to "if $B \rightarrow S$ ",we have

[ w p (1 F, X) = B ∧ w p (S, X) ] a n d [ w l p (1 F, X) = ¬ B \lor w l p (S, X) ],

and,thanks to (2),we can redefine $h$ and $k :$

\begin{array}{l} (2 2) [ h X = w p (I F, X) \vee (¬ B \wedge R) ] \mathrm {f o r a l l} X, \mathrm {a n d} \ (2 3) [ k X = w | _ {P} (I F, X) \wedge (B \vee R) ] f o r a l l X. \ \end{array}

Predicate transformers h and k are infinitely con- junctive, hence monotonic and and-continuous. As a result wlp (DO,R) defined by

[ w l p (D O, R) = (\underline {{A}} i: i \ge 0: k ^ {i} T) ]

is the weakest solution of (21).

In the absence of unbounded nondeterminacy, predicate transformer $h$ is also or-continuous, and as a result $w p\left( {D,O,R}\right)$ defined by

[ w p (D O, R) = (E c: c \ge 0: h ^ {i} F) ]

is the strongest solution of (20). We remind the reader that, with the above definition of ${w}_{p}$ ,(18) and (19)

are, indeed, to be regarded as not equivalent as soon as. unbounded nondeterminacy, which destroys or- continuity, has been included.

At the beginning of this note I announced that it would contain nothing new and nothing deep. I wrote it because its contents seems insufficiently known. "Fundamental Structures of Computer Science" by William A. Wulf, Mary Shaw, Paul N. Hilfinger, and Lawrence Flon (Addison-Wesley Publishing Company, Inc. 1981), for instance, in spite of its ambitious title, its four authors, and its more than 600 pages, contains nothing of the above. (Some might consider the book's dedication embarrassing: "To the CMU Computer Science community: this couldn't have happened elsewhere.")

Plataanstraat 5 5671 AL NUENEN The Netherlands

2 May 1982 prof. dr. Edsger W. Dýksta Burroughs Research Fellow