Extreme solutions of equations (Draft Ch.5)

Copyright Notice

The following manuscript

EWD 912: Extreme solutions of equations

is an early draft of Chapter 8 of

E.W. Dijkstra and C.S. Scholten, Predicate Calculus and Program Semantics, Springer-Verlag, 1990.

Permission to reproduce the manuscript here has been granted by Springer-Verlag New York.

Extreme solutions of equations (Draft Ch. 5)

In the previous chapter we have encountered a number of statements S for which the predicate transformers wlp(S,?) and wp(S,?) were given in closed form. In the next chapter we shall encounter a statement for which the predicates wlp(S,X) and wp(S,X) are given as solutions of equations of the form

(0) $Y \colon \left\lbrack {b.\left( {X,Y}\right) }\right\rbrack$

Here, $b$ is a predicate transformer operating on an argument that is a predicate pair, $b.(X,Y)$ is a predicate, $[b.(X,Y)]$ is a domain constant, i.e. for given $X$ and $Y$ either equivalent to true or equivalent to false: For given $X$ en $Y$ , either $[b.(X,Y)]$ or $¬ [b.(X,Y)]$ holds. For given $X$ , we can consider the predicates $Y$ for which $[b.(X,Y)]$ holds, i.e. we may consider the domain constant $[b.(X,Y)]$ as an equation in the "unknown" predicate $Y$ . We now introduce the notational convention that the transition from a domain constant to an equation in which a variable is regarded as the "unknown" made by prefixing the domain constant by a colon, preceded by the unknown.

Which predicates Y are solutions of (0) -if any- depends in general on what predicate we have chosen for X . A thing we would like to show -and we

shall do so - is that the b's we shall encounter when defining semantics are such that (0) is solvable for any predicate X . A minor complica- tion, however, is that -for a single X - (0) has often many solutions. Which do we want? Well, sometimes what is called "its strongest solution", i.e. a solution that implies all its other solutions, sometimes "its weakest solution", i.e. a solution that is implied by all its other solutions. An "extreme solution" is a strongest or a weakest solution. Again, we have to show that the b's we shall encounter when defining semantics are such that (o) has the extreme solution we are interested in. (Note that $[\ldots ⇒ \ldots ]$ defines only a partial order an that, as a result, an arbitrary set of predicates contains neither a strongest nor a weakest element.)

The formal definitions are

Def. (X is the strongest predicate in $\operatorname{bag} V$ ) $\equiv$

X \in V ∧ (\underline {{A}} Z: Z \in V: [ X ⇒ Z ])

$\left( {X\text{is the weakest predicate in}\log V}\right) \equiv$

X \in V ∧ (\underline {{A}} Z: Z \in V: [ Z ⇒ X ])

The use of the definite article in "the strongest/ weakest predicate" is justified by the following lemma 5.0 In a bag of predicates containing a strongest predicate, the strongest predicate is unique. And so for a weakest predicate.

Proof 5.0 We shall prove the theorem for strongest predicates, leaving the corresponding proof for weakest predicates to the reader.

$X$ is the strongest predicate in $V$ )

$r$ is the strongest predicate in $V$ )

$= {$ definition of stronggest $}$

$X \in V,\Lambda \left( {\underline{A}Z,Z \in V;[X ⇒ Z]}\right) ∧$

$Y \in V A\left( {2;Z \in V : { Y ⇒ Z} }\right)$

$= {$ rearranging terms and introducing (superficial) parentheses $}$

$\left( {Y \in V ∧ \left( {¬ Z : Z \in V : \left\lbrack {X ⇒ Z}\right\rbrack }\right) }\right) ∧$

(X∈V ∧ (A:Z∈V: [Y⇒Z]))

$⇒$ {instantiation:} Z := Y and $Z := X$ respectively

[ X ⇒ Y ] ∧ [ Y ⇒ X ]

$= {$ predicate calculus $}$

[ X \equiv Y ]

(End of Proof 5.0)

We return now to equation (0) Y: [b. (X, Y)]. Let b be such that for all X it has a strongest solution . Since , for all X , this strongest solution is unique , it is a function of X , which we can give a name , g say . Com- bining this with the formal definition of ' strongestwe arrive at

(Ax: $g.x$ is the strongest solution of $Y : \left\lbrack {b.\left( {X,Y}\right) }\right\rbrack ) \equiv$

(A X : [ b. (X, g. X) ] A (A Z : [ b. (X, Z) ] : [ g. X ⇒ Z ])

This enables us to relate the strongest solution of

one equation to the weakest solution of another equation, as expressed by

Lemma 5.1

(A $X :$ g. $X$ is the strongest solution of $Y : \left\lbrack {b.\left( {X,Y}\right) }\right\rbrack ) \equiv$

$\left( {\underline{A}X\because {g}^{ * }.X}\right.$ is the weakest solution of $Y : \left\lbrack {b.\left( {¬ X,¬ Y}\right) }\right\rbrack$ ).

Proof 5.1

(Ax: $g.x$ is the strongest solution of $Y : \left\lbrack {b.\left( {X,Y}\right) }\right\rbrack$ )

$= {$ definition of strongest,see above

(Ax: [b. (X, g. x) A (A Z: [b. (X, Z)): [g. X ⇒ Z)))

$= {$ transforming the dummies: $x : {7x},z : {7z}}$

$\left( {\underline{A}X : \left\lbrack {b.GX,g\left( I\right) }\right) ∧ \left( {\underline{A}Z : \left\lbrack {b.GX,IZ}\right\rbrack }\right) : \left\lbrack {g.GX ⇒ {12}}\right\rbrack }\right)$

$= {$ definition of conjugate,properly of $⇒ }$

$\left( {\underline{A}X : \left\lbrack {b.({}{1}{X}{1},{}{1}{g}^{ * }.X}\right) ∧ \left( {\underline{A}Z : \left\lbrack {b.({}{1}{X}{1},{}{1}Z}\right) }\right\rbrack ;\left\lbrack {Z ⇒ {g}^{ * }.X}\right\rbrack }\right)$

$= {$ definition of weakest $}$

(A) ${X}_{1} : {g}^{ * }X$ is the weakest solution of $Y : \left\lbrack {b\left( {¬ X,¬ Y}\right) }\right\rbrack$ ).

(End of Proof 5.1)

Remark In quite a few applications of Lemma 5.1,

b. $\left( {7X,7Y}\right)$ can be expressed in terms of the conjugates of the functions $b$ is expressed in. These applications look much nicer than Lemma 5.1 itself. (End of Remark.)

In case $b$ does not depend on $X$ , Lemma 5.1 has the

Corollary 5.0

$\left( {X\text{ is the strongest solution of}Y : \left\lbrack {b,Y}\right\rbrack }\right) \equiv$

(iX is the weakest solution of $Y$ : $\left\lbrack {b\left( {iY}\right) }\right\rbrack$ )

The previous lemmata are about extreme solutions provided they exist. Our following lemmata are about the existence of extreme solutions. In view of Lemma 5.1 we only need to define and prove them for strongest solutions; sometimes we shall formulate the dual lemma as well. Since in this context nothing is gained by dragging the parameter $X$ around all the time we would be universally quantifying over it- we leave it out.

Lemma 5.2 Consider equation (1) given by

(1) $Y : \left\lbrack {b,Y}\right\rbrack$

and predicate Q given by

[ Q \equiv (\underline {{A}} Y; [ b. Y ]; Y) ]

then the following three propositions are equivalent (i.e. either none or each of them holds):

(i) $Q$ is a solution of (1) (ii) $Q$ is the strongest solution of (1) (iii) (1) has a strongest solution

Proof 5.2 Formally expressed, the three assertions are

(i) [b.Q] (ii) $\left\lbrack {b,q}\right\rbrack ∧ \left( {\underline{A}Y : \left\lbrack {b,Y}\right\rbrack : \left\lbrack {Q ⇒ Y}\right\rbrack }\right)$ (iii) $\left( {E \times :\left\lbrack {b,X}\right\rbrack : \left( {A,Y : \left\lbrack {b,Y}\right\rbrack : \left\lbrack {X ⇒ Y}\right\rbrack }\right) }\right)$

To begin with, we observe for any $X$

true

= {\mathrm {d i s t r i b u t i o n o f d i s j u n c h i o n o v e r u n i v e r s a l q u a n t i f i c a t i o n} }

\begin{array}{l} [ (A Y: [ b. Y ]: ¬ X \vee Y) \equiv ¬ X \vee (A Y: [ b. Y ]: Y) ] \ = {\mathrm {i m p l i c a t i o n a n d d e f i n i t i o n o f} Q } \ [ (A Y: [ b. Y ]: X ⇒ Y) \equiv X ⇒ Q ] \ ⇒ {\mathrm {L e i b n i z ' s} \mathrm {R u l e} } \ [ (¬ Y: [ b. Y ]: X ⇒ Y) ] = [ X ⇒ Q ] \ = {\mathrm {i n t e r c h a n g e o f q u a n t i f i c a t i o n s} } \ \end{array}

(2) $\left\lbrack {A,Y : \left\lbrack {b,Y}\right\rbrack : \left\lbrack {X ⇒ Y}\right\rbrack }\right\rbrack \equiv \left\lbrack {X ⇒ Q}\right\rbrack$

And since (2) holds for any $X$ ,we conclude by instantiating $x = Q$ :

(3) $\left\lbrack {A,Y : \left\lbrack {b,Y}\right\rbrack : \left\lbrack {Q ⇒ Y}\right\rbrack }\right\rbrack$ ,

from which (i) $\equiv$ (ii) trivially follows. Further,

\begin{array}{l} (i i i) \ = {(2) } \ (E X: [ b. X ]: [ X ⇒ Q ]) \ = {(3), i n s t a n t i a t e d w i t h Y := X } \ (E X: [ b. x ]: [ X ⇒ Q ] ∧ [ Q ⇒ X ]) \ = {\text {p r e d i c a t e c a l c u l u s} } \ (E X: [ b. x ]: [ X \equiv Q ]) \ = {\mathrm {o n e - p o i n t r u l e} } [ b, Q ] \ = {\mathrm {d e p} o p (i) } _ {(i)} \ \end{array}

(E n d o f P r o o f 5. 2)

The above lemma is not "deep", but is useful because not a single assumption is made about the predicate transformer $b$ . Its proof is in-

Structive in that it nicely illustrates that a calculational proof requires a formal statement of what has to be proved.

Our next lemma deals with an equation of a slightly more specific form.

Lemma 5.3 Let equation (2) be given by

$\left{ {1,2,3,4}\right} : y = {10},y = {15},y = {10},y\left\lbrack {{10},{15}}\right\rbrack$

and let $p$ be monotonic and let $q$ be conjunctive over the set of solutions of (2); then equation (2) has a strongest solution. (The dual lemma states that, for monotonic $q$ and for $p$ disjoint over the set of solutions of (2), equation (2) has a weakest solution.)

Proof 5.3

\begin{array}{l} p. (\underline {{A}} Y: [ p. Y ⇒ q. Y ]: Y) \ ⇒ {p i s m o n o t o n i c } \ (\underline {{A}} ^ {\prime} Y: [ p. Y ⇒ q. Y ]: p. Y) \ ⇒ {\mathrm {p r e d . c a l c .} } \ (¬ A Y: [ p. Y ⇒ q. Y ]: q. Y) \ = {q \mathrm {i s a p p r o p r a t e l y c o n j u n c t i v e} } \ q. (¬ Y: [ p. Y ⇒ q. Y ]; Y) \ \end{array}

First and last line of the above derivation assert - mutatis mutandis - proposition (i) of Lemma 5.2, and with (iii) the lemma is proved.

(End of Proof 5.3)

Insertion bottom EWD912-3

For $b$ of the form of an implication, Lemma 5.1 has the nice

Corollary 5.1

(A X : g. X is the strongest solution of Y: [p. (X, Y) ⇒ q. (X, Y)] = (A X : g. X is the weakest solution of Y: [q. (X, Y) ⇒ p. (X, Y)]

(End of Insertion bottom EWD912-3)

Better known than Lemma 5.3 is its corollary obtained by choosing for the predicate transformer on which a junctivity condition is imposed the identity function, which - Lemma 3.11 - is universally junctive.

Corollary 5.2 For monotonic $f$ ,equation

(2) $Y: \left\lbrack {P,Y ⇒ Y}\right\rbrack$

has a strongest solution and equation

(3) $Y \colon \left\lbrack {Y ⇒ f,Y}\right\rbrack$

has a weakest solution.

Remark Equation(2)has a weakest solution as well, since true, the weakest predicate of all, is a solution of (2); similarly, (3) has false as its strongest solution. (End of Remark.)

Lemma 5.4 (Known in the oral tradition as the "Theorem of Knaster-Tarski.) For monotonic $f$ , equation

(4) Y: [ P, Y \equiv Y ] \mathrm {o r} Y: [ Y \equiv P, Y ]

has the same strongest solution as

(2) Y: [ f. Y ⇒ Y ]

and has the same weakest solution as

(3) Y: [ Y ⇒ P, Y ]

Proof 5.4 It suffices to show that (2) and (4) have the same strongest solution: that (3) and (4) have the same weakest solution is merely the dual.

From Corollary 5.2, we know that (2) has a strongest solution; calling that strongest solution $X$ we have

(5) \qquad [ p. X ⇒ X ] \qquad a n d

(6) (\underline {{A}} Y: [ f. Y ⇒ Y ]: [ X ⇒ Y ])

\begin{array}{l} w e o b s e r v e, p r i s t f l y, \ (5) \ = {f _ {1} \mathrm {i s m o n o t o n i c} } [ f _ {1}. X ⇒ X ] ∧ [ f _ {1}. (f _ {1}. X) ⇒ f _ {1}. X ] \ ⇒ {\mathrm {i n s t a n t i a t e} (6) \mathrm {w i t h} Y _ {i} = f \cdot X } \ [ p, X ⇒ X ] ∧ [ X ⇒ p, Y ] \ = \left{ \begin{array}{l} \text {p r e d i c a t e c a l c u l u s} \ [ f. X \equiv X ] \end{array} \right. \ \end{array}

i.e. $X$ solves (4),and,secondly

(6)

\begin{array}{l} ⇒ {[ p. Y \equiv Y ] ⇒ [ p. Y ⇒ Y ] } \ (A Y: [ f. Y \equiv Y ]: [ X ⇒ Y ]) \ \end{array}

i.e. $X$ implies all solutions of (4).

(E n d o f P r o o f 5. 4)

The Theorem of Knaster-Tarski is extremely useful, when dealing with predicates defined as strongest solutions. A consequence of Lemma 5.4 is

Corollary 5.3 For monotonic $f$

\begin{array}{l} [ p, X \equiv X ] ∧ (A Y: [ p, Y ⇒ Y ]; [ X ⇒ Y ]) \equiv \ [ p. X ⇒ X ] ∧ (\underline {{A}} Y: [ p. Y \equiv Y ]: [ X ⇒ Y ]) \ \end{array}

as both sides of the above equivalence are equivalent to the proposition that $X$ is the strongest solution of

(2) and (4). But notice that, taken in isolation, the conjuncts of the left-hand side are stronger than the conjuncts of the right-hand side. Hence, in a proof in which it has been given that $X$ is such a strongest solution, we tend to use the conjuncts of the left-hand side; in an argument that has to show that some $X$ is such a strongest solution, we tend to establish the conjuncts of the right-hand side. The usefulness of the above device is enhanced by the fact that $P$ only needs to be monotonic, i.e. only needs to satisfy the weakest junctivity property we have introduced.

Lemma 5.5 For monotonic

[ X ⇒ Y ] ∧ [ \beta . Y ⇒ Y ] ⇒ [ \beta . X ⇒ Y ]

Proof 5.5

\begin{array}{l} [ X ⇒ Y ] ∧ [ P: Y ⇒ Y ] \ ⇒ {{f i s m o n o t o n i c } \ [ p. x ⇒ p. y ] ∧ [ p. y ⇒ y ] \ ⇒ {\dots ⇒ \dots } i s t r a n s i l v e } \ [ f. X ⇒ Y ] \ \end{array}

(End of Proof 5.5)

Lemma 5.6 For monotonic $f$

[ p, Y ⇒ Y ] ⇒ [ (\exists i: i \ge 0: p ^ {i}, p a s e) ⇒ Y ]

Proof 5.6 To begin with, we massage the consequent:

\begin{array}{l} [ (\exists i: i \ge 0: f ^ {i} \cdot f a l s e) ⇒ Y ] \ = {“ d i s t r i b u t i o n ” o f ⇒ } \ [ (¬ i: i \ge 0: p ^ {i}. P a l s e ⇒ Y) ] \ = {\mathrm {i n t e r c h a n g e o f q u a n t i f i c a t i o n s} } \ (\underline {{A}} i: i \ge 0: [ p ^ {c}. f a l s e ⇒ Y ]) \ \end{array}

which we shall prove by mathematical induction over i under the assumptions that $\phi$ is monotonic and that $Y$ is a solution of (2).

\begin{array}{l} \begin{array}{l l} \mathrm {B a s e} & [ f ^ {0}. \mathrm {f a l s e} ⇒ Y ] \end{array} \ = {\mathrm {d e f . o p f u n c t i o n a l i t e r a t i o n} } \ [ \mathrm {P a l s e} ⇒ Y ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ t r u e \ \end{array}

\begin{array}{l} \begin{array}{r l} {\mathrm {S t e p}} & {[ f ^ {i}. \mathrm {f a l s e} ⇒ Y ]} \end{array} \ ⇒ {\mathrm {L e m m a} 5. 5, f _ {\mathrm {m o n o t o n i c}} \mathrm {a n d} [ f. Y ⇒ Y ] } \ [ f. (f ^ {i} \cdot f ^ {j}) ] ⇒ Y ] \ = {\mathrm {d e f i n i t i o n o f f u n c t h r o m a l i t e r a t i o n} } \ [ p ^ {i + 1}, \mathrm {f a l s e} ⇒ Y ] \ \end{array}

(E n d o f P r o o f 5. 6)

One third of the above proof has been caused by the way in which we have formulated Lemma 5.6, but we have formulated it in the way we did because we wished to express clearly that, for monotonic $f$ , (Ei: izo: Pi false) implies any solution of (2), just like (2)'s strongest solution then does. And this raises the question of whether (Ei: izo: Pi false) could itself be the strongest solution of (2).

Lemma 5.7 For or-continuous $f$

(E i: i \ge 0: p ^ {i}. f a s e)

is the strongest solution of

(2) Y: [ p, Y ⇒ Y ]

(It's dual) is that, for and - continuous $f$ ,the weakest solution of $Y : \left\lbrack {Y ⇒ f \cdot Y}\right\rbrack$ is(Ai: i≥0: p'true).)

Proof 5.7 Since an or-continuous $f$ is monotonic, (2) has a strongest solution. In view of Lemma 5.6, it suffices to show that (Ei: i≥0: fi false) is a

solution of (2) We observe to begin with

\begin{array}{l} [ f ^ {0}. f ^ {\mathrm {a l s e}} ⇒ f ^ {1}. f ^ {\mathrm {a l s e}} ] \ = {\mathrm {d e f i n i t i o n o f p u n c t i o n a l i t e r a t i o n} } \ [ \mathrm {f a l s e} ⇒ f. \mathrm {f a l s e} ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ f r u e \ \end{array}

and

\begin{array}{l} [ p ^ {i}. f a s e ⇒ p ^ {i + 1}. f a s e ] \ ⇒ {f i s m o n o t o n i c } \ [ f. (p ^ {i}. p a l s e) ⇒ f. (p ^ {i + 1}. p a l s e) ] \ = {\mathrm {d e f i n i t i o n o f p u n c t i o n a l i t e r a t i o n} } \ [ p ^ {i + 1}; \mathrm {f a l s e} ⇒ p ^ {i + 2}; \mathrm {f a l s e} ] , \ \end{array}

observations, which serve as base and step for a proof by mathematical induction that the Pifalse form a weakening sequence.

Next we observe

\begin{array}{l} p _ {i} (\mathrm {E i}; i \ge 0: p _ {j} ^ {i}. P a l s e) \ = {p \text {i s o r - c o n t i n u o u s , s e q u e n c e w e a k e n i n g} } \ (E _ {i}: i + 1 ≥ 1: P ^ {i + 1}. P a l s e) \ = {\text {r e n a m i n g t h e d u m m y} i + 1 := i; [ p ^ {0}. \text {p a l s e} \equiv \text {p a l s e} ] } \ (E i: i ≥ 1: p ^ {i}. f a l s e) \vee p ^ {0}. f a l s e \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (E _ {i}: i \ge 0: p ^ {i}. p a s e) \ \end{array}

(End of Proof 5.7)

E W D 9 / 2 - 1 3

Continuity derives a lot of its significance from the above lemma, being the condition under which we have a closed form for an extreme solution of $Y$ : $\left\lbrack {P,Y \equiv Y}\right\rbrack$ ; it is,however,possible that the importance of the exis-istance of such a closed form has been overrated.

*

We now turn our attention to the equation

$Y : \left\lbrack {P\left( {X,Y}\right) \equiv Y}\right\rbrack$

with monotonic $f$ - i.e. with an $f$ that is mono- tonic in its complete argument - . Lemma 3.19 states that $f$ is monotonic in both components, in particular in the second one. Hence, on account of Lemma 5.4 (Knaster-Tarski), equation (7) has both extreme solutions. In the rest of this section we shall denote the strongest solution of (7) by $g.X$ and the weakest solution of (7) by $h.X$ , i.e. they satisfy - with in (9) and (11) again an appeal to Knaster-Tarski - (8) $\left\lbrack {f.}\left( {X,g \cdot X}\right) \equiv g \cdot X\right\rbrack$ (9) $\left( {A \vee : \left\lbrack {f\left( {X,Y}\right) ⇒ Y}\right\rbrack : \left\lbrack {g \cdot X ⇒ Y}\right\rbrack }\right)$ (10) $\left\lbrack {h.X \equiv f\left( {X,h.X}\right) }\right\rbrack$ (11) $\left{ {\underline{A}Y : \left\lbrack {Y ⇒ f.\left( {X,Y}\right) }\right\rbrack : \left\lbrack {Y ⇒ h.X}\right\rbrack }\right.$

The ultimate goal of this section is to establish junctivity properties of $g$ and $h$ , given the

junchivity properties of $f$ . As a starter we establish Lemma 5.8 . (It will be subsumed in Theorems 5.0 and 5.2 ; it is proved separately as we wish to use it in the proofs of those theorems.)

Lemma 5.8 If $f$ is monotonic, $g$ and $h$ are monotonic as well.

Proof 5.8

\begin{array}{l} [ X _ {0} ⇒ X _ {1} ] \ ⇒ {f \mathrm {i s m o n o t o n i c i n i t s f i r s c o m p o n e n t} (\mathrm {L e m m a 3 . 1 9}) } \ [ f. (X _ {0}, g. X _ {1}) ⇒ f. (X _ {1}, g. X _ {1}) ] \ = {(8) } \ [ p. (X _ {0}, g. X _ {1}) ⇒ g. X _ {1} ] \ ⇒ {\mathrm {i n s t a n t i f a t i o n} (9) \mathrm {w i t h} X, Y := X _ {0}, g. X _ {1} } \ [ g \cdot X _ {0} ⇒ g \cdot X _ {1} ] \ \end{array}

Having proved the monotonicity of the strongest solution, we are done as -see Corollary 5.1 - $h^ X$ is the strongest solution of $Y: [P^(X, Y) \equiv Y]$ and - see Lemma 3.4 - (h is monotonic) $\equiv (h^*$ is monotonic).

(End of Proof 5.8)

In the rest of this section, $W$ stands for a bag of ordered pairs - denoted as $(X, Y)$ - of predicates, and we define the predicates $Xw$ and $Yw$ by

\begin{array}{l} (1 2) [ X _ {W} \equiv (\underline {{A}} X, Y: (X, Y) \in W: X) ] \ (1 3) [ Y _ {W} \equiv (\underline {{A}} X, Y: (X, Y) \in W: Y) ] \ \end{array}

In the sequel, the abbreviations $Xw$ and $Yw$ come in handy when we shall relate the conjunctivities of $g$ and $h$ to the conjunctivity of $f$ .

Our next preliminary is Lemma 5.9. (It is so simple that one could question whether it is worth the trouble of explicit formulation; we think we use it frequently enough to justify its inclusion.)

Lemma 5.9 With $f$ conjunctive over $W$ and $W$ such that

(1 4) (\underline {{A}} X, Y: (X, Y) \in W: [ f. (X, Y) = Y ])

we have

(1 5) [ f. (X _ {w}, Y _ {w}) = Y _ {w} ]

\begin{array}{l} \mathrm {P r o o f} 5. 9 \ f. (X _ {w}, Y _ {w}) \ = {f \mathrm {c o n j u n c t i v e} W; (1 2) \mathrm {a n d} (1 3) } \ (\underline {{A}} X, Y: (X, Y) \in W: f _ {1} (X, Y)) \ = {(1 4) } \ (A X, Y: (X, Y) \in W: Y) \ = {(1 3) } \ Y _ {W} \ \end{array}

(End of Proof 5.9)

Our last preliminary is

Lemma 5.10 With $V$ and $W$ for some $k$ satisfying

(1 6) (X, Y) \in W \equiv X \in V \wedge [ Y \equiv k. X ]

we have for any predicate transformer q with a pair

(17) $\left\lbrack {\left( {\underline{A}X,Y : \left( {X,Y}\right) \in W : q\left( {X,Y}\right) }\right) \equiv \left( {\underline{A}X : X \in V : q\left( {X,k \cdot X}\right) }\right) }\right\rbrack$

with the special cases $- \left\lbrack {q.\left( {X,Y}\right) \equiv X}\right\rbrack -$

(18) $[X_w \equiv (\underline{A} X: X \in V: X)]$

and $- \left\lbrack {q.\left( {X,Y}\right) \equiv Y}\right\rbrack -$

(19) $\left\lbrack {{Y}_{W} \equiv \left( {\underline{A}X : X \in V : k \cdot X}\right) }\right\rbrack$

Proof 5.10 We have to establish (17); in order to do so we observe

\begin{array}{l} (\underline {{A}} X, Y: (X, Y) \in W: q. (X, Y)) \ = {(1 6) } \ (A X, Y: X \in V ∧ [ Y \equiv k. X ]: q. (X, Y)) \ = {\mathrm {n e s t r i n g o f q u a n t i f i c a t i o n s} } \ (\underline {{A}} X: X \in V: (\underline {{A}} Y: [ Y \equiv k. X ]: q. (X, Y))) \ = {\mathrm {c o n e - p o i n t r u l e} } \ (\underline {{A}} X: X \in V: q. (X, k. X)) \ \end{array}

(End of Proof 5.10)

We are now ready to demonstrate

Theorem 5.0 Any type of conjunctivity enjoyed

Proof th 5.0 With f enjoying some type of con. junctivity, $f$ is monotonic; hence - Lemma 5.8-

$h$ is monotonic.

In order to show that $h$ is conjunctive over some $V$ , i.e.

[ h. (\underline {{A}} X: X \in V: X) \equiv (\underline {{A}} X: X \in V: h. X) ]

we show that either side implies the other.

(i) Because $h$ is monotonic,we have

[ h. (\underset {\sim} {A X}: X \in V: X) ⇒ (\underset {\sim} {A X}: X \in V: h. X) ]

(ii) To show the implication in the other direction, we construct a bag $W$ according to (16), with $h$ for $k$ . Since $h$ is monotonic, to a $V$ ordered as a monotonic sequence of predicates corresponds a $W$ ordered as a monotonic sequence of predicate pairs; since, furthermore, $W$ is as non-empty/denumerable/finite as $V$ , $V$ and $W$ are of the same type.

Because $[Y \equiv h.X]$ implies on account of (10) $[Y \equiv f.(X,Y)]$ , a second consequence of our choice of $h$ for $k$ is that $W$ satisfies condition (14) of Lemma 5.9; hence (15) holds if, as we assume, $f$ is conjunctive over $W$ .

And now we observe

\begin{array}{l} (A X: X \in V: h. X) \ = {(1 9) } \ Y _ {W} \ ⇒ {(1 5) a n d (1 1) } \ \end{array}

\begin{array}{l} h, X _ {w} \ = {(1 8) } \ h. (A X: X \in V: X) \ \end{array}

(End of Proof Th. 5.0)

Whereas Theorem 5.0 dealt with the conjunctivity properties of the weakest solution of

(7) $Y \colon \left\lbrack {P\left( {X,Y}\right) \equiv Y}\right\rbrack$

Theorem 5.2 will do so for the strongest solution of (7). But first we state and prove Theorem 5.1 - $g$ and $h$ denoting,as before,the strongest and weakest solution of (7)

Theorem 5.1 For finitely conjunctive $f$ and predicates

[ p. (X, Y) \equiv Y ]

we have

[ g. X \equiv g. t r u e ∧ Y ]

Remark. Note that, since $[P(X,Y) \equiv Y]$ , we may regard $Y$ as an arbitrary solution of (7) for that $X$ . Theorem 5.1 states that the strongest solution of (7) is the conjunction of the predicate $g$ .true and an arbitrary solution of (7). (End of Remark.)

Proof Th.5.1

We shall prove the equivalence by showing that

either side implies the other

(i) Firstly, since a finitely conjunctive $f$ is monotonic, $g$ is -see Lemma 5.8 - also monotonic; hence we have $[g.x ⇒ g.x]$

Secondly, since $[f(X,Y) \equiv Y]$ means that $Y$ is some solution of (7), of which $g.X$ is the strongest solution - see (9) - we have $[g.X ⇒ Y]$ .

Combining these two results we establish $\left\lbrack {g \cdot X ⇒ g \cdot \text{true} ∧ Y}\right\rbrack$ .

(ii) The crux of the proof of $\left\lbrack {g.\text{true} ∧ Y ⇒ g.X}\right\rbrack$ is to rewrite that implication as $\left\lbrack {g.\text{true} ⇒ g.X \vee ¬ Y}\right\rbrack$ and to prove the latter by showing that $g \times v \upharpoonright Y$ is the solution of an equation of which $g$ .true is the strongest solution. There we go!

true

= {(8) }

[ f. (X, g. X) \equiv g. X ]

$⇒$ {monotonic} $f$ -see Lemma 3.19- is monotonic in its second component $}$ or ${$ conjunctive $f$ is monotonic $}$

[ f. (X, g \cdot X \wedge Y) ⇒ g \cdot X ]

$= {$ predicate calculus,complement rule in particular $}$

[ f. (X, (g \cdot X \vee ¬ Y) \wedge Y) ⇒ g \cdot X ]

$= { f\left( p\right) \mid p \in I$

[ f. (t r u e, g. X \vee ¬ Y) \wedge f. (X, Y) ⇒ g. X ]

$= \left{ {\left\lbrack {P\left( {X,Y}\right) \equiv Y}\right\rbrack }\right}$

\begin{array}{l} [ f. (\mathrm {t r u e}, g \cdot X \vee ¬ Y) \wedge Y ⇒ g \cdot X ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ \end{array}

\begin{array}{l} [ f. (f r u e, g. X v ¬ Y) ⇒ g. X v ¬ Y ] \ ⇒ {\mathrm {i n s t a n h i a t i o n} o f (q) \mathrm {w i t h} X, Y := \mathrm {t r u e}, g. X \vee ¬ Y } \ [ g. t r u e ⇒ g. X \vee ¬ Y ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ g. t r u e ∧ Y ⇒ g. X ] \ \end{array}

(End of Proof Th. 5.1)

Since - see (10) - $[f_{\cdot}(X,Y)\equiv Y]$ is satisfied with h.x for Y, Theorem 5.1 has as corollary

Corollary 5.4 For finitely conjunctive $f$

[ g. x \equiv g. t r u e ∧ h. x ]

from this and Theorem 5.0 one derives

Corollary 5.5 For finitely conjunctive $p$

[ g. (X \wedge Y) \equiv g. X \wedge h. Y ]

And now we are ready for

Theorem 5.2 With the exception of universal conjunctivity and and- continuity, the conjunctivity enjoyed by $f$ is enjoyed by $g$ as well.

Proof Th.5.2 For monotonic $f$ , the monotonicity of $g$ is asserted in Lemma 5.8. For the remainders of conjunctivity (i.e. unbounded, denumerable or finite) of $f$ , $f$ is finitely conjunctive and, hence,

we can use Corollary 5.4 and write $[g.X\equiv g.$ true X]. Theorem 5.0 states that h inherits the conjunctivity of $f$ , and Lemma 3.13 -as described on EwD910-24!states that g inherits the conjunctivity of h , universal conjunctivity excepted.

(End of Proof Th.5.2)

With $g \times$ the strongest solution of $Y: [f(X, Y) \equiv Y]$ and of $Y: [f(X, Y) ⇒ Y]$ , $g^ X$ is - see Lemma 5.1- the weakest solution of $Y: [Y \equiv f^(X, Y)]$ and of $Y: [Y ⇒ f^(X, Y)]$ . Since - see Lemma 3.3 - $f^$ is as disjunctive as $f$ is conjunctive (and similarly for $g$ and $g^$ and for $h$ and $h^)$ all these theorems have their dual:

Theorem 5.0 Any type of disjunctivity enjoyed

Theorem 5.1* For finitely disjunctive $f$ and predicates

[ Y \equiv f _ {\cdot} (X, Y) ]

we have

[ h. X \equiv h. f a s e \vee Y ]

Corollary 5.4* For finitely disjunctive $f$

[ h. X \equiv h. f a l s e \vee g. X ]

Corollary 5.5* For finitely disjunctive $f$

[ h. (X \vee Y) \equiv h. X \vee g. Y ]

Theorem 5.2* With the exception of universal disjunctivity and or-monotonicity, the disjunctivity enjoyed by $f$ is enjoyed by $h$ as well.

Remark Of the predicate transformers introduced in Chapter 4 "The semantics of straight-line programs", wlp (IF,?) and wp (IF,?) are in general not disjunctive; as a result conjunctivity properties of predicate transformers corresponding to straight-line programs are in general stronger than their disjunctivity properties. This makes us keenly interested in the inheritance of conjunctivity properties; comparing Theorem 5.0 with Theorem 5.2 we may expect weakest solutions to play a more central role than strongest ones. (End of Remark.)

To close this chapter we shall show a relation between extreme solutions of related equations. We shall formulate the lemma for strongest solutions, but as its premiss is only monotonicity, it holds for weakest solutions as well.

Lemma 5.11 Let for monotonic ${f}{x}$ and ${F}{y}$ predicate transformer

[ f _ {X, Y} ] \equiv (f _ {X, (X, Y)}, f _ {Y, (X, Y)}) ]

let $g$ . $X$ be the strongest solution of

(2 0) Y: [ f _ {Y}. (X, Y) \equiv Y ] ;

let $\left( {{X}{s},{Y}{s}}\right)$ be the strongest solution of

(x, Y): [ f. (X, Y) \equiv (X, Y) ] ;

\mathrm {t h e n} [ g. X _ {s} = Y _ {s} ]

Proof 5.11 From the monotonicity of $f_{x}$ and $f_{y}$ we conclude the monotonicity of $f$ and hence - knaster.Tarski- the existence of the strongest solutions; moreover, $(X_{s}, Y_{s})$ is also the strongest solution of

(2 2) (X, Y): [ f. (X, Y) ⇒ (X, Y) ]

To prove the required equivalence we shall show that either side implies the other.

(i) true

\begin{array}{l} = {(X s, Y s) \text {s o l v e s} (2 1) } \ [ p _ {y} (X s, Y s) \equiv Y s ] \ ⇒ {\mathrm {d e f i n i t i o n} o p g } \ [ g. X _ {s} ⇒ Y _ {s} ] \ \end{array}

(ii) true

= {(X s, Y s) \text {s o l v e s} (2 1) }

[ \rho_ {x}. (X _ {s}, Y _ {s}) \equiv X _ {s} ]

$⇒ \left{ {P \times \text{monotonic and (i); definition of }g}\right}$

[ p _ {x.} (X s, g. X s) ⇒ X s ] \wedge [ p _ {y.} (X s, g. X s) \equiv g. X s ]

(End of Proof 5.11)

\begin{array}{l} ⇒ {(X s, g. X s) \mathrm {s o l v e s} (2 2); \mathrm {d e p i n i t i o n o f} (X s, Y s) } \ [ (X _ {s}, Y _ {s}) ⇒ (X _ {s}, g. X _ {s}) ] \ = {\mathrm {p r o p e r t i e s o f p r e d i c a t e p a i r s} } \ [ Y s ⇒ g \cdot X s ] \ \end{array}

Comments on Draft Ch.5

From Lemma 5.9 this draft shows the traces of EwD849a in which we made heavier use of Xw and Yw. I am now wondering whether we cannot kick them out, together with Lemmata 5.9 and 5.10 . Certainly the k of 5.10 is now a bit heavy-going! And so is its g ! We could formulate 5.10 :

With V and W satisfying

(X, Y) \in W \equiv X \in V ∧ [ Y = h. X ]

we have

[ (\underline {{A}} X, Y: (X, Y) \in W: (X, Y)) \equiv (\underline {{A}} X: X \in V: (X, h X)) ] ^ {\prime}

which would capture all we need from it. (EWD849a

Note that, with predicate pairs we can write

${P}{1}\left( {{A}{X,Y} : \left( {X,Y}\right) \in W : \left( {X,Y}\right) }\right)$ (for what was denoted as " $f \in {Xw}{Yw}^{\prime }$ in EWD849a.

I was pleased when I needed the new 3.13 again.

I have spent a lot of time on an alternative

proof for Theorem 5.1, particularly (ii), following a suggestion of CSS. I could even isolate "the shunting trick" - EWD912, bottom half- still further. But in my final version, the text was longer, and used more identifiers and numbered formulae. So that effort went into the waste-paper basket.

In chapter 3 , we should, I think, include that for monotonic h , replacing each $X \in V$ by $h.x$ - poor formulation!- yields a bag of the same type (also when maintaining the order of the predicates if ordered). We need it there for a correct proof of 3.14 , we need it here in Proof Th.5.0 when constructing $W$ .

Austin. 20 March 1985

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