Extreme solutions of equations

Copyright Notice

The following manuscript

EWD 969: Extreme solutions of equations

is a 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

In the previous chapter we have encountered a number of statements , 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: [b.(X,Y)]

Here, $b$ is a function from predicate pairs to predicates, i.e. $b(X, Y)$ is a boolean structure, $[b(X, Y)]$ is a boolean expression in $X$ and $Y$ , which for given $X$ and $Y$ is either true or false.

In (a) we have followed our convention of notationally distinguishing between boolean expressions and equations: by prefixing the boolean expression $\left\lbrack {b.\left( {X,Y}\right) }\right\rbrack$ by "Y: " we indicate that the boolean expression should be viewed as equation in the unknown $Y$ .

Remark We found the convention of explicitly identifying the unknown(s) preferable to the convention of using reserved letters for the unknowns. It enables us to distinguish between the quadratic equation $x:(x^{2} + a\cdot x + b = 0)$ and the linear equation $b:(x^{2} + a\cdot x + b = 0)$ . (End of Remark.)

which predicates $Y$ are solutions of (0)

-if any- depends in general on which 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 problem is that - for a single $x$ - (0) has often many solutions. Fortunately, we can strengthen (0) into equations that have at most one solution, viz.

(1) $Y : \left( {\left\lbrack {b.\left( {X,Y}\right) }\right\rbrack \land \left( {\underline{A}Z.\left\lbrack {b.\left( {X,Z}\right) }\right\rbrack .\left\lbrack {Y \Rightarrow Z}\right\rbrack }\right) }\right)$ (2) $Y : \left\lbrack {b.\left( {X,Y}\right) }\right\rbrack \land \left( {\underline{A}Z : \left\lbrack {b.\left( {X,Z}\right) }\right\rbrack : \left\lbrack {Z \Rightarrow Y}\right\rbrack }\right)$ .

The solution of (1) is called "the strongest solution of (0)" since it implies all solutions of (0); the solution of (2) is called "the weakest solution of (0)" since it follows from all solutions of (0). Together they are referred to as "the extreme solutions of (0)". In due time we shall show that the b's we shall encounter in the definition of semantics are such that for any predicate X equations (1) and (2) are solvable, i.e. that the extreme solutions of (0) exist for any predicate X.

Before proceeding to do so, however, we shall demonstrate that extreme solutions are unique, i.e. that (1) and (2) each have at most one solution.

Proof. We prove the uniqueness of the solution of (1); for (2), the proof is very similar.

To this end we observe - for fixed $x$ -

(P and Q solve (1))

$= { {d\phi }_{i}f\left( i\right)$ and rearrangement of terms

$$ [ b. (X, P) ] \wedge (\neg Z: [ b. (X, Z) ]: [ Q \Rightarrow Z ]) \wedge $$

$$ [ b. (X, Q) ] \wedge (\neg Z: [ b. (X, Z) ]: [ P \Rightarrow Z ]) $$

( \Rightarrow ) { instantiated}{2}^{. = }P ) and ( Z\because Q ) respectively

$$ [ Q \Rightarrow P ] \land [ P \Rightarrow Q ] $$

$= {$ predicate calculus $}$

$$ [ P \equiv 0 ] $$

(End of Proof.)

Thus we have established that the extreme solutions are each unique, provided that they exist. Instead of showing the existence of strongest solutions separately from the existence of weakest solutions, we shall first establish a duality theorem by means of which we can halve the length of the existence proof.

Two introductory remarks first. Let $b$ be such that (1) has a solution for any $X$ , or - equivalently - that (0) has a strongest solution for any $X$ . Since that strongest solution depends in general on the predicate $X$ , which occurs as parameter in the equation, it is a function of $X$ ; accordingly we denote it by $g.X$ , thus indicating explicitly its dependence on $X$ . Furthermore we shall formulate and prove the duality theorem only for a special form of the function $b$ , viz. the form that allows the most elegant formula-

tion of the duality (and, not surprisingly, is the only

Theorem 5.0 (Duality Theorem.)

$\left( {g \times }\right)$ is the strongest solution of

$$ Y: [ p. (X, Y) \Rightarrow q. (X, Y) ] = $$

$\left( {g * x}\right)$ is the weakest solution of

$$ Y: [ p ^ {} (X, Y) \Leftarrow q ^ {} (X, Y) ] $$

Proof 5.0

${C}_{g}X$ is the strongest solution of

$$ Y: [ p. (X, Y) \Rightarrow q. (X, Y) ] $$

$= {$ definition of strongest solution,see (1) $}$

(A) [P. (X, g. X) ⇒ Q. (X, g. X)] A

$$ (\underline {{A}} Z: [ p. (X, Z) \Rightarrow q. (X, Z) ]: [ g. X \Rightarrow Z ]) $$

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

(Ax: [p. (iX, g. (jX)) ⇒ q. (iX, g. (jX))) ]

$$ (\underline {{A}} Z: [ p. (7 x, 7 z) \Rightarrow q. (7 x, 7 z) ]: [ g. (7 x) \Rightarrow 7 z ]) $$

$= {$ definition of conjugate,properly of $\Rightarrow$ and $\Leftarrow }$

(A) [P. (X, g. X) ⇌ g. (X, g. X)] ∧

$$ (\underline {{A}} Z: [ p ^ {}. (X, Z) \Leftarrow q ^ {}. (\tilde {X}, Z) ]: [ g ^ {*}. X \Leftarrow Z ]) $$

$= {$ definition of weakest solution,see (2) $}$

${C}^{ * }.X$ is the weakest solution of

$$ Y: [ p ^ {}. (X, Y) \Leftarrow q ^ {}. (X, Y) ] $$

(End of Proof 5.0)

The previous theorem is about extreme solutions provided that they exist. We now turn to existence of extreme solutions; in view of Theorem 5.0, we only need to define and prove them for strongest solutions; sometimes we shall formulate the dual theorem as well. Since in this context nothing is gained by dragging the parameter $X$ around all the time we would be quantifying universally over it - we leave it out.

The first (general) step of coming to grips with the existence of a strongest solution is the consideration that the only candidate for a strongest solution is the conjunction of all solutions. Indeed we have

Theorem 5.1 Consider equation

(3) $Y \colon \left\lbrack {b,Y}\right\rbrack$ ; then

$$ (e q u a t i o n (3) h a s a s t r e n g e s t s o l u t i o n) \equiv $$

$$ ((\underline {{a}} z: [ b. z ]: z) \mathrm {s o l v e s} (3)) $$

Proof 5.1

$$ \begin{array}{l} (e q u a t i o n (3) h a s a s t r o n g e s t s o l u t i o n) \ = {\mathrm {s e e} (1) } \ (E Y: [ b. Y ] \wedge (A Z: [ b. Z ]: [ Y \Rightarrow Z ])) \ = \begin{array}{l} {\mathrm {f i n o r d e r t o g e t Y a u s i d e t h e u n i v e r s a l}} \ {\mathrm {q u a n t i f i c a t i o n w e f i r s t i n t e r c h a n g e q u a n t i f i c a t i o n s}} \end{array} \ (E Y: [ b. Y ] \land [ (A Z: [ b. Z ]: Y \Rightarrow Z) ]) \ = {\mathrm {a n d u s e t h a t t h e a n t e c e d e n t d i s t r i b u t e s} \ (E Y: [ b. Y ] \wedge [ Y \Rightarrow (A Z: [ b. Z ]: Z) ]) \ \end{array} $$

$$ \begin{array}{l} = {\mathrm {n o w w e h a v e} (\underline {{A}} Z: [ b. Z ]; Z) \mathrm {a s s u b e x p r e s s i o n}; \quad \mathrm {b u t n o t e t h a t t h e i n v e r s e i m p l i c a t i o n f o l l o w s f r o m} [ b. Y ] } \ (E Y: [ b. Y ] \land [ Y \Leftarrow (A Z: [ b. Z ]: Z) ] \ \land [ Y \Rightarrow (\neg A Z: [ b. z ]: z) ]) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (E \dot {Y}: [ b. Y ] \land [ Y \equiv (\underline {{a}} Z: [ b. Z ]; Z) ]) \ = {\mathrm {c n e - p o i n t r u l e} } \ [ b. (A Z: [ b. Z ]: Z) ] \ = {(\mathbf {3}) } \ (\underline {{A}} Z: [ b. Z ]; Z) \mathrm {s o l v e s} (3). \ \end{array} $$

(End of Proof 5.1)

Note that in the above proof, until the application of the one-point rule, we have only massaged the existentially quantified term, which is nothing else but the body of the equation for the strongest solution of (3). Consequently, if $(\underline{A} Z: [b. z]: 2)$ solves (3), it is also (3)'s strongest solution.

Remark The dual of Theorem 5.1 is

(equation (3) has a weakest solution) $\equiv$

(E2: [b.2]: 2) solves (3)

(End of Remark.)

Our next theorem states the existence of the strongest solution for a special $b$ , viz. such that we can show that the equation is solved by the conjunction of its solutions.

Theorem 5.2 Let equation (4) be given by

(4) $Y \colon \left\lbrack {p,Y \Rightarrow q,Y}\right\rbrack$ ,

let $p$ be monotonic, and let $q$ be conjunctive over the set of solutions of (4). Then equation (4) has a strongest solution. (The dual theorem states that for monotonic $q$ , and for $p$ disjunctive over the set of solutions of (4), equation (4) has a weakest solution.)

Proof 5.2 Thanks to Theorem 5.1, it suffices to show that the conjunction of (4)'s solutions solves (4). The calculation is straightforward

$$ \begin{array}{l} p. (\underline {{A}} Z: [ p. Z \Rightarrow q. Z ]: Z) \ \Rightarrow {p i s m o n o t o n i c } \ (\underline {{A}} Z: [ p. 2 \Rightarrow q. 2 ]: p. 2) \ \Rightarrow {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} Z: [ p. z \Rightarrow q. z ]: q. z) \ = {g \mathrm {i s c o n j u n c t i v e o v e r t h e s o l u t i o n s e t o f (4)} } \ q. (\underline {{A}} Z: [ p. \tilde {Z} \Rightarrow q. Z ]; Z) \ \end{array} $$

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

And now we are ready for the famous

Theorem 5.3 (In the oral tradition known as the "Theorem of Knaster-Tarski.") For monotonic $f$

(5) $Y : \left\lbrack {{f}^{0}Y \equiv Y}\right\rbrack$

has the same strongest solution as

(6) $Y \colon \left\lbrack {P,Y \Rightarrow Y}\right\rbrack$

and has the same weakest solution as

$Y : \left\lbrack {P,Y \Leftrightarrow Y}\right\rbrack$

Proof 5.3 We can confine ourselves to demonstrating the existence and equality of the strongest solutions of (5) and (6), as existence and equality of the weakest solutions of (5) and (7) is merely the dual.

Choosing in Theorem 5.2 $f$ for $p$ , and for $q$ the identity function (which is universally conjunctive), we conclude that (6) has a strongest solution, i.e. calling it $Q$ , we have

(8) $\left\lbrack {f \cdot Q \Rightarrow Q}\right\rbrack$ (g) $\left( {\underline{a}z : \left\lbrack {f.2 \Rightarrow z}\right\rbrack .\left\lbrack {Q \Rightarrow z}\right\rbrack }\right)$

In order to show that $Q$ solves (5) we observe

$$ [ P, Q \equiv 0 ] $$

$= {$ predicate calculus; rewriting the equivalence as mutual implication is suggested by (8) $}$

$$ [ p. q \Rightarrow Q ] \land [ Q \Rightarrow p. q ] $$

$= \left{ {\left( 8\right) }\right}$

$\Leftrightarrow \quad {(9) \text { tells us what } Q \text { implies, hence instantiate (9) }$ with $Z := f \cdot Q}$

$$ [ f. (f. Q) \Rightarrow f. Q ] $$

$\Leftrightarrow {$ now we can use ${f}^{\prime }s$ monotonicity $}$ $= { \left( 8\right)$ again

In order to show that $Q$ implies all solutions of

(5) we observe

$$ (A Z: [ P, Z \equiv Z ]: [ Q \Rightarrow Z ]) $$

$$ \begin{array}{l} \Leftrightarrow \quad \left{f. z \Rightarrow 2 \right} \Rightarrow \left[ f. z \Rightarrow 2 \right], i.e. (5) i s \mathrm {t h e l e a s t t o l e r a n t e q u a t i o n} \rbrace \ (A Z: [ P, Z \Rightarrow Z ]: [ Q \Rightarrow Z ]) \ = \begin{array}{l} {(g) } \ \text {t r u e} \end{array} \ \end{array} $$

$$ (E n d o f P r o o p 5. 3) $$

The Theorem of Knaster. Tarski is of profound methodological significance. It allows us to characterize for monotonic $f$ as the unique solution of

(10) $Y : \left\lbrack {p,Y \equiv Y}\right\rbrack \land \left( {\underline{A}Z : \left\lbrack {p,Z \Rightarrow Z}\right\rbrack : \left\lbrack {Y \Rightarrow Z}\right\rbrack }\right)$ or as the unique solution of (11) $Y : \left\lbrack {P,Y \Rightarrow Y}\right\rbrack \land \left( {\underline{A}Z : \left\lbrack {P,Z \equiv Z}\right\rbrack : \left\lbrack {Y \Rightarrow Z}\right\rbrack }\right)$

Note that both conjuncts in the body of (11) are weaker than the corresponding conjuncts in the body of (10). Yet, for monotonic $p$ , these two equations have the same unique solution!

Hence, in a proof in which a predicate has been given to be such a strongest solution, we tend to use that it solves (10); in an argument in which we have to show that a predicate is such a strongest solution, it suffices to show that it solves (11).

The usefulness of the above device is enhanced by the fact that only needs to be monotonic, i.e. only needs to enjoy the weakest junctivity property.

EWD 969-9

We have seen that if $Y: [\rho, Y \Rightarrow Y]$ has a strongest solution, $(\underline{A}Z: [\rho, Z \Rightarrow Z]: Z)$ gives that solution in closed form. This closed form, however, is not one with which we can do very much. It is therefore good to know that for or-continuous $\rho$ there exists a closed expression for the strongest solution which is more easily manipulated. The next two theorems deal with that; the first one is a steppingstone.

Theorem 5.4 For monotonic $f$ and any $Y$

$$ [ p, Y \Rightarrow Y ] \Rightarrow [ (\exists i: i \ge 0: p ^ {i}. f a l s e) \Rightarrow Y) ] $$

Proof 5.4 The dummy i ranging over the natural numbers and functional iteration being defined recursively, a proof by mathematical induction over the natural numbers seems indicated. Hence we try to massage the consequent so as to make it amenable to an inductive proof:

$$ \begin{array}{l} [ (\exists i: i \ge 0: p ^ {i}. f a l s e) \Rightarrow Y ] \ = {\mathrm {q u a s i - d i s t r i b u t i o n o f t h e c o n s e q u e n t} } \ [ (\underline {{A}} i: i \ge 0: f ^ {i}. f a l s e \Rightarrow Y) ] \ = {\text {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 } \ (\underset {\sim} {A i}: i \ge 0: [ p ^ {\prime} \cdot p a l s e ^ {\prime} \Rightarrow Y ]) \ \end{array} $$

This we shall demonstrate by mathematical induction over i under the assumptions that $f$ is monotonic and $[f. Y \Rightarrow Y]$ . The base is easy; neither assumption is needed.

${Base}\;\left\lbrack {{p}^{0},{false} \Rightarrow Y}\right\rbrack$

$$ \begin{array}{l} = {\mathrm {d e f i n i t i o n o f f u n c t i o n a l i t e r a t i o n} } \ [ \mathrm {f a l s e} ^ {\prime} \Rightarrow Y ] \ = \left{ \begin{array}{l} \text {p r e d i c a t e c a l c u l u s} \ \text {t r u e} \end{array} \right. \ \end{array} $$

Step [P i+1 false ⇒ Y]

$$ \begin{array}{l} = {\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} } \ [ f. (f ^ {i}. f a l s e) \Rightarrow Y ] \ \Leftarrow {l e t u s u s e [ P. Y \Rightarrow Y ] t o g e t P i n t h e c o n s e q u e n t) } \ [ f. (p ^ {i}. p a s e) \Rightarrow f. r ] \ \Leftrightarrow {f \mathrm {i s m o n o t o n i c} } \ [ p ^ {i}. p ^ {a} s e \Rightarrow Y ] \ \end{array} $$

(End of Proof 5.4)

Theorem 5.4 states that, for monotonic $f$

$\left( {{E}_{i} : i \geq 0 : {p}^{i}\text{. false}}\right)$ implies any solution of

$Y$ : $\left\lbrack {P,Y \Rightarrow Y}\right\rbrack$ ,just as its strongest solution does.

And this raises the question whether (Ei: i20: p' false) could itself be that strongest solution. This

question is answered in

Theorem 5.5 For or-continuous $f$

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

is the strongest solution of

(6) $Y : \left\lbrack {P,Y \Rightarrow Y}\right\rbrack$

(The dual is that, for and-continuous $f$ ,the weakest solution of $Y : \left\lbrack {f,Y \Leftrightarrow Y}\right\rbrack$ is(Ai: i≥0: Pi. true).)

Proof 5.5 Since an or-continuous $f$ is monotonic,

(6) has a strongest solution. In view of Theorem 5.4 it suffices to show that (El: i>0: P'. false)

solves (6). To this end we shall first show that

its terms form a weakening sequence, i.e.

$$ (\underline {{A}} i: i \ge 0: [ f ^ {i}. f a l s e \Rightarrow f ^ {i + 1}. f a l s e ]) $$

This is done by mathematical induction:

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

Step [P+i+1 false] {definition} P functional iteration} [P. (P' false) ]

$$ \begin{array}{r l} & {\Leftrightarrow \quad {\mathrm {f a s m o n o t o n i c} }} \ & {[ \mathrm {f i . f a l s e} \Rightarrow \mathrm {f i + 1 . f a l s e} ]} \end{array} $$

Finally we observe

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

Continuity derives a lot of its significance from the above theorem; it enables us to prove properties of an extreme solution by means of mathematical induction over the natural numbers. It is, however, possible that the importance of this possibility has been overrated

We now reintroduce our parameter $X$ in the equation and turn our attention to equation

$$ Y: [ P (X, Y) \equiv Y ] \tag {12} $$

for monotonic $f$ . Such an $p$ being also monotonic in the individual components of its argument , in particular in the second component, Theorem 5.3 (Knaster-Tarski) asserts that its extreme solutions exist.

In what follows, g.x denotes the strongest solution of (12) and h.x denotes the weakest solution of (12). In analogy with (10), we cap-ture our knowledge about $g$ and $h$ in the formally strongest way: we have for all $X$ and $Z$

$$ \begin{array}{l} (1 3) [ f. (X, g. X) \equiv g. X ] \ (1 4) \quad [ f. (X, Z) \Rightarrow Z ] \Rightarrow [ g. X \Rightarrow Z ] \ (1 5) [ f. (X, h. X) \equiv h. X ] \ (1 6) \quad [ f. (X, Z) \Leftarrow Z ] \Rightarrow [ h. X \Leftarrow Z ] \ \end{array} $$

The ultimate goal of this section is to prove junctivily properties of $g$ and $h$ , given the junctivity properties. As we go along, we shall see that the proofs can be smoothly derived with a minimum of invention or trial and error by each time realizing which of the formulae (13) through (16) is the appropriate one to appeal to.

Let in the demonstrandum an application of $g$ occur in the consequent. For that $g$ , an appeal to (14) is of no interest: (14) allows us

to conclude that an application of $g$ implies something and not what it is implied by. Therefore, for such an application, only (13) can be of interest (and in all probability has to be used).

Conversely, if the demonstrandum has an ap- plication of $g$ as its antecedent, an appeal to (14) is almost certainly required as (13), all by itself, fails to express how strong $g$ really is.

For the choice between (15) and (16), similar considerations apply.

A major decision is often whether to start massaging the antecedent so as to show that it implies the consequent, or to start massaging the consequent so as to show that it follows from the antecedent. If may surprise the reader that we call this decision "major", since the two proofs are each other's reverse and, hence, logically identical. The point is that steps that in the one direction are almost dictated by what has been written down, may in the other direction require clairvoyance for their justification. The general advice is to start at the most complicated side (if there is one): usually the more complicated expression shows more explicitly which transformation is appropriate.

We have also minor decisions to take, such as the order in which to apply different transformations. We call them minor because as a rule they do not influence our ability to prove the theorem; they may influence the length of our proofs and are therefore preferably taken wisely.

Just to show how well these heuristics work, let us prove

Theorem 5.6 Let $p$ and $q$ be monotonic functions from predicate pairs to predicates; let $(P, Q)$ be the strongest solution of

$$ (X, Y): [ (p. (X, Y), q. (X, Y)) \equiv (X, Y) ] $$

let $g.x$ be the strongest solution of

$$ Y: [ q. (X, Y) \equiv Y ] $$

Then we have $\left\lbrack {g.P \equiv Q}\right\rbrack$

Proof 5.6 For the sake of completeness we observe that both strongest solutions exist - $(p.(X,Y),q.(X,Y))$ being a monotonic function of $(X,Y)$ for monodontic $p$ and $q$ .

Our formal knowledge about $p$ and $q$ is -expressed in the separate components- (analogously to (13) or the first conjunct of (10)):

(17) $\left\lbrack {p.\left( {P,Q}\right) \equiv P}\right\rbrack$ (18) $\left\lbrack {q.\left( {P,Q}\right) \equiv Q}\right\rbrack$

and analogously to (14) or the second conjunct of (10):

(19) $\left\lbrack {p,\left( {X,Y}\right) \Rightarrow X}\right\rbrack \land \left\lbrack {q,\left( {X,Y}\right) \Rightarrow Y}\right\rbrack \Rightarrow \left\lbrack {\left( {P,Q}\right) \Rightarrow \left( {X,Y}\right) }\right\rbrack$

Our formal knowledge about $g$ is similarly captured by

(20) $\left\lbrack {q.\left( {X,g.}X\right) \equiv g.}\right\rbrack$ $\left\lbrack {g.1}\right. \left( {X,Y) \Rightarrow Y}\right\rbrack \Rightarrow \left\lbrack {g.1}\right. \left( {X \Rightarrow Y}\right\rbrack$

So much for what has been given. Not surprisingly in this context, we shall prove the equivalence by mutual implication. Let us tackle $\left\lbrack {Q \Rightarrow g.P}\right\rbrack$ first. (That is one of those "minor decisions".)

$$ [ Q \Rightarrow g. P ] $$

$= {$ we can tackle $g_P$ via (20) or try to tackle Q via (19); let us take the minor decision to do the latter; in view of (19) we rewrite

$$ [ (P, Q) \Rightarrow (P, g, P) ] $$

$\Leftrightarrow { {19}}$ with $X,Y = P,g.P}$

$$ [ p. (p, g. p) \Rightarrow p ] \wedge [ q. (p, g. p) \Rightarrow g. p ] $$

$= \left{ {\begin{array}{l} \text{ for the consequent }g.p \ \text{ only }\left( {20}\right) \text{ can be of interest,so }\left( {20}\right) \text{ with } \end{array}\mathrm{x} \mathrel{\text{:=}} \mathrm{P}\right}$

$$ [ p. (p, g. P) \Rightarrow P ] \land [ q. (P, g. P) \Rightarrow q. (P, g. P) ] $$

$\left{ \begin{array}{l} \text{predicate calculus } \ \end{array}\right}$ $= {$ for the consequent $P$ ,only (17) can be of interest

$$ [ p. (P, g. P) \Rightarrow p. (P, Q) ] $$

$\Leftrightarrow \left{ {{for}\;{nate}\;y,\;p\;i{s}\;{monotonic}}\right}$ $\Leftarrow$ {we can tackle the consequent Q via (18) or the antecedent $g.P$ via(21); let us take the minor decision to do the latter; (21) with ${X}_{3}Y = P,Q}$

$$ [ q. (P, Q) \Rightarrow Q ] $$

$= { 1\text{ now we have a cicle consequent }Q$ with (18) $}$

$$ = {p r e d i c a t e c a l c u l u s } $$

Notice that in the mean time we have proved the other implication as well and that , hence, our proof obligation has been met. Notice also that we have

appeared to each of the given formulae (17) through (21) precisely once, and since we need all of them, our proof is in that sense the shortest possible one.

Remark Trusting that the reader has read the above proof very carefully and has absorbed the heuristics, we shall in future abbreviate the heuristics. We shall also combine steps, such as omitting the two intermediate results preceding "predicate calculus". (End of Remark.)

(End of Proof 5.6)

After this interlude we return to the junctivity properties of $g$ and $h$ , given the junctivity properties of $f$ . As a starter we establish Theorem 5.7. (It will be subsumed in later theorems, for whose proofs it will be used.)

Theorem 5.7 For monotonic $P, g$ and $h$ are monotonic.

Proof 5.7 To prove the monotonicity of $g$ , we have to show for arbitrary predicates $P$ and $Q$

$$ [ P \Rightarrow Q ] \Rightarrow [ g. P \Rightarrow g. Q ] \quad , $$

using that $g$ is given by

(13) $\left\lbrack {f\left( {X,g,X}\right) \equiv g \cdot X}\right\rbrack$ and $\left\lbrack {\rho \left( {X,Z}\right) \Rightarrow Z}\right\rbrack \Rightarrow \left\lbrack {g \cdot X \Rightarrow Z}\right\rbrack$

To this end we observe

EWD 969-17

$$ [ g, P \Rightarrow , g, Q ] $$

$$ \begin{array}{l} \Leftrightarrow {t a c k l e g. p v i a (1 4) w i t h x, z := p, g. q } \ [ f: (P, g. Q) \Rightarrow g. Q ] \ {t a c k l e g. Q v i a (1 3) w i t h X := Q } \ [ f. (P, g. Q) \Rightarrow f. (Q, g. Q) ] \ \Leftarrow {p \text {i s m o n o t o n i c , h e n c e m o n o t o n i c i n 1 ^ {s} c o m p .} } \ [ P \Rightarrow Q ] \ \end{array} $$

The monotonicity of $h$ is merely the dual of

(End of Proof 5.7)

And now we are ready to demonstrate the beautiful

Theorem 5.8 Any type of conjunctivity enjoyed

(It's dual is: Any type of disjunctivity enjoyed

Proof 5.8 With $f$ enjoying some type of conjunctivity, $f$ is monotonic; hence -Theorem 5.7- 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) \Rightarrow (\underset {\sim} {A X}: X \in V: h. X) ] $$

(Here we see what good use we can make of Theorem 5.7 when showing a junctivity property of extreme solutions; the latter being monotonic, we get the implication in the one direction for free.)

(ii) To show the implication in the other direction we begin by observing

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

$\Leftrightarrow \left{ \begin{array}{l} \text{the h. in the consequent is to be tackled via (16)} \ \text{with}X,Z = {\left( AX;X \in V;X\right) }_{3}\text{（}AX;{X \in V};h.X\text{）} \end{array}\right.$

$$ [ f. ((A X: X \in V: X), (A X: X \in V: h. X)) \Leftarrow (A X: X \in V: h. X) ] $$

$= \left{ \begin{array}{l} \text{ simplification of }{f}_{s}\text{ argument } : \text{ quantification } \ \text{ distributes over pair formincs } \end{array}\right.$

$$ [ P. (\underline {{A}} X: X \in V: (X, h. X ^ {\prime}) \Leftarrow (\underline {{A}} X: X \in V: h. X) ] $$

$= \left{ \begin{array}{l} \text{ the h. in the antecedent is to be tackled } \ \text{ via (15) }\end{array}\right.$

$$ [ f. (\underline {{A}} X: X \in V: (X, h. X)) \Leftarrow (\underline {{A}} X: X \in V: f. (X, h. X)) ] $$

Now the -minor- complication is that whereas h's conjunctivity is related to a bag of predicates, ${f}_{s}^{\prime }$ conjunctivity is related to a bag of predicate pairs. To be formally precise, we construct a bag $W$ of predicate pairs by

$\left( {X,Y}\right) \in W \equiv X \in V \land \left\lbrack {Y \equiv h \cdot X}\right\rbrack$

and observe that, thanks to the monotonicity of $h$ , $V$ and $W$ are of the same junctivity type. Hence it suffices to show the above implication under the assumption that $f$ is conjunctive over $W$ . The formal demonstration proceeds as follows

$$ f. (\underline {{A}} X: X \in V: (X, h. X)) $$

$= {$ one-point rule to introduce $Y}$

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

$= { {attesting} + { 2} + { 3} + { 4}$

$$ p. (\underline {{A}} X, Y: (X, Y) \in W: (X, Y)) $$

$= { {$ conjunctive over $W}$

$$ (A ^ {2} X, Y: (X, Y) \in W: f: (X, Y)) $$

$= {$ elimination of $W$ with(22)andnesting $}$

$$ (\underset {\sim} {A X}: X \in V: (\underset {\sim} {A Y}: [ Y \equiv h. X ]: f. (X, Y))) $$

$= {$ one-point rule to eliminate $Y}$

$$ (\underset {\sim} {A} X: X ^ {\prime} \in V: f. (X, h, X)) $$

Remark The last 5 steps of the above proof are not very exciting. Note that a number of them were needed to introduce Y and to get rid of it again, obligations caused by the way in which we defined W. Had we used the "bagifier" B, we could have defined W by

$$ W = (\underline {{B}} X: X \in V: (X, h. X)) $$

and with rules how to manipulate expressions for such bags, there would have been no need to refer explicitly to the one-point rule. (End of Remark.)

(End of Proof 5.8)

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

$$ Y: [ f. (X, Y) \equiv Y ], \tag {12} $$

Theorem 5.10 will do so for its strongest solution.

But first we state and prove Theorem 5.9.

$- g \cdot X$ and $h \cdot X$ denoting ,as before,the strongest

Theorem 5.9 For finitely conjunctive $f$ and

$$ [ f. (X, Y) \equiv Y ] $$

we have

$$ [ g, X \equiv g. t r u e \land Y ] $$

(The dual states that for finitely disjunctive $p$ and such $X$ and $Y$ we have

$$ [ h, X \equiv h. f a l s e \vee Y ].) $$

In other words: the strongest solution of (12) is for finitely conjunctive $f^{\vee}$ the conjunction of an arbitrary solution of (12) and the constant predicate -i.e. independent of $X$ - g true.

Proof 5.9 Given are

$\left\lbrack {P\left( {X,Y}\right) \equiv Y}\right\rbrack$ (13) $\left\lbrack {f.\left( {{X}^{\prime },{g}^{\prime }{X}^{\prime }}\right) \equiv g.{X}^{\prime }}\right\rbrack$ $\left\lbrack {f\left( {{X}^{\prime }Z}\right) \Rightarrow Z}\right\rbrack \Rightarrow \left\lbrack {g \cdot {X}^{\prime } \Rightarrow Z}\right\rbrack$

We shall prove the equivalence by proving that either side implies the other.

$\left\lbrack {g \cdot X \Rightarrow g \cdot \text{true} \land Y}\right\rbrack$

$$ \begin{array}{l} = {\text {p r e d i c a t e c a l c u l u s} } \ [ g. X \Rightarrow g. t r u e ] \land [ g. X \Rightarrow Y ] \ \Leftrightarrow {g \mathrm {i s m o n o t o n i c}; (1 4) \mathrm {w i t h} Z := Y } \ [ X \Rightarrow \mathrm {t r u e} ] \wedge [ f (X, Y) \Rightarrow Y ] \ = \left{ \begin{array}{l} \text {p r e d i c a t e c a l c u l u s}; (2 3) \end{array} \right} \ \end{array} $$

(ii) [g.true A Y $\Rightarrow$ g.x]

$$ \begin{array}{l} = {\mathrm {p r e d i c a t e} \mathrm {c a l c u l u s , s o a s t o t a c k l e g . t r u e v i a (1 4)} } \ [ q, t r u e \Rightarrow g. X \vee \neg Y ] \ \Leftrightarrow {1 4) \mathrm {w i t h} X, Z := \mathrm {f r u e}, g. X \vee \neg Y } \ [ f. (t r u e, g \cdot X \vee \neg Y) \Rightarrow g \cdot X \vee \neg Y ] \ = {\mathrm {p r e d i c a t e c a l c u l u s , p r e p a r i n g f o r} P _ {s} \mathrm {c o n j u n c t i v i t y} } \ [ f. (f r u e, g. X \vee \neg Y) \wedge Y \Rightarrow g. X ] \ = {(2 3), \mathrm {t h e o n l y t h i n g g i v e n a b o u t} Y! } \ [ \rho (\mathrm {t r u e}, g. X \vee \tilde {\gamma}) \tilde {\wedge} \rho (X, Y) \Rightarrow g. X ] \ = {f \text {i s} \mathrm {f i n i t e l y c o n j u n o t i v e ; p r e d i c a t e c a l c u l u s} } \ [ p. (X, g \cdot X \wedge Y) \Rightarrow g \cdot X ] \ = {2 3 \mathrm {a n d} (1 4) \mathrm {w i t h} X ^ {\prime}, Z := X, Y } \ [ f _ {1} (x, g x) \Rightarrow g _ {2} x ] \ = {1 3) w i t h X := X } \ t r u e \ \end{array} $$

(End of Proof 5.9)

Theorem 5.9 is most interesting for the weakest possible choice for $Y$ , viz. h.x. And so we get as first corollary

Theorem 5.9.0 For finitely conjunctive $P$

$$ [ g. X \equiv g. t r u e \land h. X ] $$

The second corollary is

Theorem 5.9.1 For finitely conjunctive $f$

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

Proof 5.9.1

$$ \begin{array}{l} g. (X, Y) \ = \int^ {1} {\mathrm {T h e o r e m} 5, 9. 0 \mathrm {w i t h} X := X \land Y } \ g. t r u e \wedge h. (X \wedge Y) \ = {f \mathrm {c o n j u n c t i v e}, \mathrm {h e n c e} h \mathrm {c o n j u n c t i v e}, \mathrm {T h e o r e m 5 . 8} } \ \end{array} $$

$$ \begin{array}{l} g. t r u e \land h. X \land h. Y \ = {\mathrm {T h e o r e m} 5. 9. 0 } \ g. X \wedge h. Y \ \end{array} $$

(End of Proof 5.9.1)

Remark. The last two corollaries capture the important outcome of Theorem 5.9. We could have proved Theorem 5.9.1 directly - Theorem 5.9.0 then follows - instead of Theorem 5.9. We have not done so, firstly because Theorem 5.9.1 is more specific (in its mentioning of $h$ ) and, secondly, because the formulae of the proof would have been quite a bit longer. (End of Remark.)

Having expressed -Theorem 5.9.0- g.x in terms of (a constant predicate and) h.x , and having established -Theorem 5.8- that h inherits the conjunctivity of f , we are ready for

Theorem 5.10 With the exception of universal conjunctivity and continuity, the conjunctivity

(It's dual states that with the exception of universal disjunctivity and or-continuity, the disjunctivity of $f$ is enjoyed by $h$ as well.)

Proof 5.10 For monotonic $f$ , the monotonicity of $g$ is asserted in Theorem 5.7. For the remain- ing types of conjunctivity (i.e. unbounded, denominator- able or finite), $f$ is finitely conjunctive and hence - Theorem 5.9.0 - we have

$$ [ g. X \equiv g. t r u e \land h. X ] $$

Theorem 5.8 states that h enjoys the conjunctivty of f , and states that g inherits the conjunctivity of h , universal conjunctivity excepted. (End of Proof 5.10)

Theorems 5.9 and 5.10 are less beautiful than Theorem 5.8 , which states that h inherits without constraint or exception the conjunctivity enjoyed by f . To show that these constraints and exceptions are not void - i.e. have not entered the picture merely as a result of our weakness as theorem provers- we shall construct counter-examples.

Theorem 5.9 is restricted to finitely conjunctive $p$ . All other forms of conjunctivity imply monotonicity, and, for a really convincing counter-example, it therefore suffices to come up with a monotonic - but not finitely conjunctive! - such that the conclusion of 5.9 or 5.9.0 or 5.9.1 does not hold.

Let us look for the simplest example we can come up with that is monotonic but not finitely conjunctive; $[f. (X, Y) \equiv X]$ , $[P. (X, Y) \equiv Y]$ , and $[P. (X, Y) \equiv X \land Y]$ won't do, because they are finitely conjunctive, but

$$ [ f (X, Y) \equiv X \vee Y ] $$

is monotonic and passes the test of non-conjunctivity. (In general we have $\eta \left\lbrack {\left( {{X}{\Lambda }{X}^{\prime }}\right) v\left( {{Y}{\Lambda }{Y}^{\prime }}\right) \equiv {\left( {X}{V}{Y}^{\prime }\right) }{\Lambda }{\left( {X}{V}^{\prime }{Y}^{\prime }\right) }{\Lambda }$ .) With this choice for $p$ ,equation

$$ \begin{array}{l} (1 2) \quad Y: [ f. (X, Y) \equiv Y ] \ b e c o m e s Y: [ X \Rightarrow Y ] \ \end{array} $$

with the obvious extreme solutions $[g.X\equiv X]$ and [h.x= true]. Substituting these in the conclusion of Theorem 5.9.0, viz. $[g.X\equiv g.$ true $\land$ h.x] would yield [X] which does not hold for any X. We have been fortunate: the simplest proposal for f that we could think of provided the counterexample. So much for the constraint of Theorem 5.9 to conjunctive f.

In order to show that Theorem 5.10's exception of universal conjunctivity is justified, we should look for a universally conjunctive such that $\neg [g.\text{true}]$ . Here the simple choice $[\rho(X,Y) \equiv Y]$ does the job. With this choice, (12) becomes

$$ Y: [ Y \equiv Y ] $$

with the obvious extreme solutions [g.x = false] and $\left\lbrack {h.X \equiv \text{true}}\right\rbrack ;g$ is not universally conjunctive.

In order to show, finally, that also Theorem 5.10's exception of and-continuity is justified, we look for an $f$ that is and-continuous, but is not finitely conjunctive. In our first counter-example we found the simple $f$ , given by $[f(X,Y) \equiv X \vee Y]$ , that was not finitely conjunctive, but we cannot use that because the corresponding strongest solution is the identity function, which is and-continuous. But we can use that $f$ by using it as a source of inspiration, and by complicating it a little: replacing $Y$ by $p.Y$ for a carefully chosen $p$ .

We look for a $p$ that is and-continuous, so

We look for a $p$ that is also 'or-continuous so that -Theorem 5.5- we have a closed form

for g.x . And we would like p so simple that there is hope of tackling that closed form analytically. In a state space that has z as one of its integer coordinates, we suggest wp $(z: = z + 1, Y)$ for p.y , i.e. we consider given by

$$ [ f (X, Y) = X \vee Y _ {2 + 1} ^ {2} ] $$

According to Theorem 5.5 and the fact that $p$ is or-continuous in its second argument, $g.x$

is given by

$$ [ g, X \equiv (\underline {{E}} i: i \ge 0: k ^ {i}. f a l s e) ] $$

where $k$ is given by $\left\lbrack {k.U \equiv X \vee {U}_{z + 1}^{2}}\right\rbrack$ ,which -via induction over $i$ - leads to

$$ [ g, X \equiv (\exists i: i \ge 0: X _ {z + i} ^ {2}) ] $$

Consider now the strengthening sequence of predicates $C_j$ given by $[C_j = 2 \geq j]$ for $j \geq 0$ .

$\neg \left\lbrack {g.\left( {\underline{A}j : j \geq 0 : C,j}\right) \equiv \left( {\underline{A}j : j \geq 0 : g.\left( {C,j}\right) }\right) }\right\rbrack$

for:

$g.\left( {\underline{A}j;j \geq 0,C.}\right)$

$$ \begin{array}{l} = {\mathrm {d e f . o f} C } \ g. (A j: j \ge 0: z \ge j) \ = {\text {p r e d i c a t e a n d i n t e g e r c a l c u l u s} } \ g. \mathbf {f} a s e \ = \begin{array}{l} {\mathrm {l a s t e x p r e s s i o n f o r g. x} } \ \mathrm {p a l s e} \end{array} \ \end{array} $$

and

$$ \begin{array}{l} (A j: j \geqslant 0: g (C j)) \ = {\mathrm {d e f .} c ^ {\prime} C } \ (\mathrm {即} j: j \geq 0: g. (z \geq j)) \ = {l a s t e x p r e s s i o n f o r g. X } \ (\underline {{A}} j: j \ge 0: (\underline {{E}} i: i \ge 0: z + i \ge j)) \ = {p r e d i c a t e a n d i n t e g e r c a l c u l u s } \ (\underline {{A}} j: j \ge 0: \mathrm {f r u e}) \ = \begin{array}{l} \frac {1}{2} \end{array} \mathrm {p r e d i c a t e c a l c u l u s} \ \end{array} $$

And this concludes the construction of the third and last counter-example. We would like to add that the sequence C.j used above is a standard ingredient for showing non-and-monotonicity. (Similarly, the weakening sequence $z \leq j$ is used to show that or-continuity has been lost.) This knowledge makes the choice of our last f less surprising.

8 September 1986

pror. dr. Edsger W. Dgksta

Department of Computer Science

The University of Texas at Austin

Austin, TX 78712 - 1188

USA