A sequel to EWD912, i.e. to Draft Ch.5

A sequel to EWD912, i.e. to Draft Ch.5

[I had restricted the material in EWD912 to what I thought I would need in the next chapter. Writing the latter, I found I wanted to include some program transformations for the justification of which EWD was insufficient. Hence this extension.]

Solutions of an equation of the form

Y: [ f. Y \equiv Y ]

are known as "fixpoints of $f$ "; for fixpoints of $f$ , the application of $f$ is the identity operation. The Theorem of Knaster-Tarski tells us that for monotonic $f$ , the weakest and strongest fixpoints of $f$ exist. For monotonic functions, taking an extreme fixpoint is order-preserving in the sense expressed precisely in the following lemma.

Lemma 5.12 Let $\mathfrak{p}_0$ and $\mathfrak{p}_1$ be two monotonic predicate transformers, and let the strongest solutions - or the weakest solutions - of

Y: [ p _ {0}. Y \equiv Y ] \qquad a n d Y: [ p _ {1}. Y \equiv Y ]

be E0 and E1 respectively. Then, if

(23) $\left\lbrack {{f}{0}.Y ⇒ {f}{1}.Y}\right\rbrack$ for all $Y$ ,

we have $\left\lbrack {E0 ⇒ {E}_{1}}\right\rbrack$

Proof 5.12 We shall prove the lemma for strongest solutions, the conclusion for weakest solutions being the dual one.

\begin{array}{l} t r u e \ = {\mathrm {d e f i n i t i o n} o f E _ {1} } \ [ f _ {1}. E _ {1} \equiv E _ {1} ] \ ⇒ {(2 3) \mathrm {w i t h} Y := E 1 } \ [ \rho_ {0}. E _ {1} ⇒ E _ {1} ] \ ⇒ {\mathrm {d e f . o p E 0 a n d k n a s t e r - T a r s k i} } \ [ E _ {0} ⇒ E _ {1} ] \ \end{array}

(End of Proof 5.12)

As an aside we remark that the above proof is a perfect illustration of the discussion following Corollary 5.3 : when using that $E_1$ is a solution, we take the equation with the equivalence sign, when using that $E_0$ is an extreme solution, we take the corresponding equation with the implication.

Remark Lemma 5.12 and its proof illustrate another point. As a lemma captures the fruits of the (in- tellectual or formal) labour that has gone in its proof, it has been conjectured that, the more "la-borious" the proof, the more "valuable" the lemma. And as a result it would be hardly worthwhile to take the trouble of formulating a theorem when its proof is very short. But the conjecture is wrong: the "value" of a theorem depends on the ease with which it can be applied. We shall use Lemma 5.12 in

our next proof. (End of Remark.)

By way of introduction to our next lemma we consider for monotonic the equations

(i) $Y : \left\lbrack {p,Y \equiv Y}\right\rbrack \mathrm{{and}} \left( \mathrm{{ii}}\right) Y : \left\lbrack {{p}^{2},Y \equiv Y}\right\rbrack$

On account of Leibniz's Rule , each solution of (i) solves (ii); for this conclusion , $\beta$ ’s monotonicity is not needed. It raises the question, whether, conversely, each solution of (ii) solves (i). A counterexample - even with monotonic $f$ - suffices to show that the question deserves a negative answer. (Let $z$ be an integer coordinate of the underlying space and let $f$ be given by $[f,Y\equiv Y_{-2}^{z}]$ . In that case, ${f}^{2}$ is the identity function.) A more positive result, however, is that for monotonic $f$ (i) and (ii) have the same extreme solutions; this is a consequence of the next lemma.

Lemma 5.13 For monotonic $f$ and any natural

(i) $Y : \left\lbrack {\left( {\underline{A}i : 0 ≤ i : {p}^{i + 1}.Y}\right) \equiv Y}\right\rbrack$ (ii) $Y : \left\lbrack {{P}^{n + 1}Y \equiv Y}\right\rbrack$ (iii) $Y : \left\lbrack {\left( {{E}_{i} : {0 ≤ i : {f}^{i + 1}}Y}\right) \equiv Y}\right\rbrack$

have the same extreme solutions; in particular, the extreme solutions of (ii) are independent of $n$ (provided,of course, $n$ is natural).

Proof 5.13 Since the conjugate of $f$ is monotonic as well, it suffices to give the proof for the strongest solutions.

Since the left-hand sides of the equations are all three monotonic, the three strongest solutions exist; let them be ,in order, $P,Q$ ,and $R$ Since the left-hand sides of the three equations are weakening in the order given, we have on account of Lemma 5.12

[ P ⇒ Q ] ∧ [ Q ⇒ R ]

The proof is completed by showing $\left\lbrack {R ⇒ P}\right\rbrack$ as follows, the range "0s i" uniformly having been omitted for brevity's sake.

true

\begin{array}{l} = {\rho_ {i s m o n o t o n i c} } \ [ p. (A _ {i}: f ^ {i}. P) ⇒ (A _ {i}: p. (P ^ {i}. P)) ] \ = {\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 a n d r e n a m i n g} _ {\mathrm {t h e l e f t d u m m y}} } \ [ P. (P \wedge (\underline {{A}} i: f ^ {i + 1}. P)) ⇒ (\underline {{A}} i: f ^ {i + 1}. P) ] \ = {P s o l v e s (i); i d e m p o t e n c y o f \Lambda } \ [ P, P ⇒ P ] \ = {\mathrm {m o n o t o n i c i t y} o f f \mathrm {a n d i n d u c t i o n o v e r i} } \ (A _ {i}: [ P ^ {i + 1}, P ⇒ P ]) \ = {\mathrm {i n t e r c h a n g e o f q u a n i t i f i c a t i o n s a n d} ⇒ " d i s t r i b u t i o n" } [ (\underline {{E}} _ {i}: P ^ {i + 1} P) ⇒ P ] \ \begin{array}{l} {= {\mathcal {R} \mathrm {i s s l o r n e s t s o l u t i o n o f (i i i) a n d k n a s t e r - T a r s k i} }} \ {\left[ \mathcal {R} ⇒ P \right]} \end{array} \ \end{array}

Remark Consider the equation

Y: [ (\underline {{Q}} i: i \in V; f ^ {i + 1}. Y) \equiv Y ]

with Q either A or E and V a non-empty bag of natural numbers. The predicate on its left is weaker than that of than that of (i) and stronger than that of (iii). With Lemmata 5.12 and 5.13 we conclude that the above equation has the same extreme solutions as (i) and (iii). (End of Remark.)

Are the preceding lemmata rather general, the next one is very specific. It is, in fact, too special to our taste; the reason that we include it never- theless is that we need it in the next chapter in which the semantics of the repetition will be defined in terms of extreme solutions of an indeed rather specific equation.

Lemma 5.14 Consider for monotonic $p$ and

(2 4) Y: [ p. X \wedge q. Y \equiv Y ]

in which $p$ is, furthermore, weakening and idem.

[ X ⇒ p. X ] \qquad {\mathrm {a n d}} [ p ^ {2}. X \equiv p. X ] {\mathrm {f o r a l l}} X;

then the extreme solutions $g.X$ and $h.X$ of (24) are idempotent.

Proof 5.14 To begin with, we remark, on account of $[g^{2}.X\equiv g.(g.X)]$ and $g.x$ being the strongest solution of (24), that

${g}^{2}X$ is the strongest solution of

${Y}{1} : \left\lbrack {{p}{1}\left( {g,X}\right) ∧ q,{Y}^{ * }}\right\rbrack \equiv Y\rbrack$

and, similarly,

${h}^{2}X$ is the weakest solution of

$\gamma : \left\lbrack {p,h,x ∧ q,y \equiv r}\right\rbrack$

Our proof proceeds in three parts: the first part shows $\lbrack {g}^{2}X ⇒ g.X\rbrack$ and $\left\lbrack {{h}^{2}X ⇒ h.X}\right\rbrack$ , the two remaining parts will each demonstrate one of the inverse implications.

(i) $\left\lbrack {{g}^{2}X ⇒ g.X}\right\rbrack$ and $\left\lbrack {{h}^{2}X ⇒ h.X}\right\rbrack$

This part of the proof does not rely on the assumption that $p$ is weakening. To begin with we observe for any predicates $X, Y$ , and $Z$

\begin{array}{l} [ p. X ∧ q. Z \equiv Z ] \ ⇒ {\mathrm {p r e d i c a t e c a l c u l u s} } [ Z ⇒ p. X ] \ ⇒ {p \mathrm {i s m o n o t o n i c} } [ p. 2 ⇒ p ^ {2}. X ] \ = {p _ {i s i d e m p o t e n t} } [ p. z ⇒ p. x ] \ ⇒ {p r e d i c a t e c a l c u l u s } [ p. Z ∧ q. Y ⇒ p. X ∧ q. Y ] \ \end{array}

\begin{array}{l} ⇒ {\mathrm {L e m m a} 5. 1 2, \mathrm {a n d} (2 4) } \ \begin{array}{l} {[ a n e x t r e m e s o l u t i o n o f Y: [ p. 2 ∧ q. Y \equiv Y ] ⇒} \ {\mathrm {t h e c o r r e s p o n d i n g e x t r e m e s o l u t i o n o f (2 4) ]}} \end{array} . \ \end{array}

The first line of the above holds for $Z$ any solution of (24), in particular for $[Z \equiv g \cdot X]$ and for $[Z \equiv h \cdot X]$ . The conclusion of the above is then about extreme solutions of (25) and (26) respectively, in particular $[g^2 \cdot X ⇒ g \cdot X]$ and $[h^2 \cdot X ⇒ h \cdot X]$ . (The other possible conclusions $[g \cdot (h \cdot X) ⇒ g \cdot X]$ and $[h \cdot (g \cdot X) ⇒ h \cdot X]$ are now less interesting.)

(ii) $\left\lbrack {g \cdot X ⇒ {g}^{2} \cdot X}\right\rbrack$

This part of the proof relies directly on $p$ being weakening and indirectly -by an appeal to (i)- on $p$ being idempotent. The proof is by showing that ${g}^{2}x$ solves an equation of which

true

\begin{array}{l} = {g ^ {2} X \text {s o l v e s (2 5)} } \ [ p. (g. X) \wedge q. (g ^ {2}. X) \equiv g ^ {2}. X ] \ ⇒ {p i s w e a k e n i n g } \ [ g. X \wedge q. (g ^ {2}. X) ⇒ g ^ {2}. X ] \ = {g. x \mathrm {s o l v e s} (2 4) \mathrm {a n d L e i b n i z s R u l e} } \ [ p. X \wedge q. (g. X) \wedge q. (g ^ {2}. X) ⇒ g ^ {2}. X ] \ = {[ g ^ {2} X ⇒ g. X ] - \mathrm {s e e} (i) - \mathrm {a n d} q \mathrm {i s m o n o t o n i c} } \ [ p. X \wedge q. (g ^ {2}. X) ⇒ g ^ {2}. X ] \ ⇒ {g. X \mathrm {s t r o n g e s t} \mathrm {s o l u t i o n o f (2 4) a n d h i n a s t e r - T a r s k i} } \ [ g. X ⇒ g ^ {2}. X ] \ \end{array}

(iii) $\left\lbrack {h.X ⇒ {h}^{2}.X}\right\rbrack$

This part of the proof does not rely on $p$ being idempotent. The proof is by showing that $hX$ solves an equation of which $h^2 X$ is the weakest solution.

true

\begin{array}{l} = {p \text {i s w e a k e n i n g}; h. X \text {s o l v e s (2 4)} } \ [ h. x ⇒ p. (h. x) ] ∧ [ h. x ⇒ q. (h. x) ] \ ⇒ {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ h. x ⇒ p. (h. x) ∧ q. (h. x) ] \ ⇒ {h ^ {2} X \mathrm {w e a k e s} \mathrm {s o l u t i o n o f (2 6)}; \mathrm {k i n a s t e r T a r s k i} } [ h. X ⇒ h ^ {2} X ] \ \end{array}

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

The previous lemma gives circumstances under which we can conclude that extreme solutions are idempotent. The next lemma gives us a conclusion we may draw if extreme solutions are idempotent.

Lemma 5.15 Let monotonic $f$ be such that for each monotonic, idempotent predicate transformip , the extreme solutions of

Y: [ f. (X, i p. Y) \equiv Y ]

are idempotent. Let

(2 7) Y: [ f. (X, Y) \equiv Y ]

have $g.X$ and $h.X$ as its strongest and weakest solutions respectively. Then $g.X$ is the strongest

solution of

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

and $h.x$ is the weakest solution of

$\left( {2g}\right)$ $Y : \left\lbrack {f.\left( {X,h,Y}\right) \equiv Y}\right\rbrack$

Proof 5.15. Let $e.x$ be a monotonic, idempotent solution of (27); then we have

(30) $\left\lbrack {f.}\left( {X,e.X}\right) \equiv e.X}\right\rbrack$

let $k.x$ be an idempotent solution of

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

so that we have

(32) $\left\lbrack {P.\left( {X,e.\left( {k.X}\right) }\right) \equiv k.X}\right\rbrack$

We observe firstly

true

\begin{array}{l} = {(3 0) a n d i d e m p o t e n c y o f e } \ [ f. (X, e. (e. X)) \equiv e. X ] \ = {(3 1) } \ \end{array}

(i) (e.x solves (31))

We observe secondly

true

\begin{array}{l} = {(3 2) \mathrm {w i t h} X := k \cdot X } \ [ p. (k. X, e. (k ^ {2}. X)) \equiv k ^ {2}. X ] \ = {\mathrm {i d e m p o t e n c y} f k } \ \end{array}

\begin{array}{l} [ f. (k. X, e. (k. X)) \equiv k. X ] \ = {(3 0) \mathrm {w i t h} X := k. X } \ [ e. (k. X) \equiv k. X ] \ ⇒ {\mathrm {L e i b n i z} } \ [ f. (X, e. (k. X)) \equiv f. (X, k. X) ] \ = {(3 2) } \ [ k, X \equiv P (X, k, X) ] \ = {(2 7) } \ \end{array}

(ii) (k. X solves (27))

Now the hard work has been done. Function $f$ being monotonic, it is - Lemma 3.19- monotonic in its second component as well and - Lemma 5.4 - its extreme solutions exist and - Lemma 5.8 - are monotonic. Choosing for $i$ the identity function, we conclude that $g$ and $h$ are furthermore idempotent.

Choosing for e either g or h - e.g. Lemmata 3.14 and 3.20 - the left-hand side of (31) is mono- tonic as well, the extreme solutions of (31) exist, and - choose monotonic, idempotent e for ip - are idempotent as well. So we may choose for k.x either the strongest or the weakest solu tion of (31)

Choose $g$ for $e$ ; equation (31) becomes (28), and let $k.x$ be its strongest solution. From (i) $[k.x ⇒ g.x]$ , from (ii) $[g.x ⇒ k.x]$ , hence (27) and (28) have the same strongest solution $g.x$ .

Choose $h$ for $e$ ; equation (31) becomes (29), and let $k.X$ be its weakest solution. From (i) $[h.X ⇒ k.X]$ , from (ii) $[k.X ⇒ h.X]$ , hence (27) and (29) have the same weakest solution $h.X$ .

(End of Proof 5.15)

Remarks. Since $h^X$ is the strongest solution of the conjugate equation of (27), and the weakest solution of (29) is the conjugate of the strongest solution of (29)'s conjugate $Y: [f^(X, h^*Y) \equiv Y]$ , the introduction of $e$ could have been avoided: the second half of the conclusion is the dual of the first half.

It should be noted, however, that the above proof does not depend on the Theorem of Knaster. Tarski in the sense that in equations (27) and (31) the equivalence is not replaced by an implication. This circumstance seduced us not to destroy the symmetry and to carry out the formal work in terms of $e$

As last remark , we would like to add a word of reassurance for those readers who , at first reading of our latter proofs, have been left with somewhat uneasy or disturbed feelings. They might, for instance wonder what made us conjecture the lemmata in the first place; the answer to this question may be found in the next chapter. They

also might wonder how one ever finds such a proof. Well, the answer is of course: rarely immediately and never immediately in the form in which it sees the light of day.

When you come to think of it, the overall struc- ture of the proofs - i.e. the choice of the subgoals- is not too surprising. The detailed formal calculations are another matter, because the formulae we may use always contain free variables for which you are free to substitute whatever suits your argument. In recognition of the fact that theorem proving is a goal-directed activity one often begins by working backwards; the search of which formulae to use in one's substitutions is often narrowed down by the knowledge of a counterexample from which one can conclude that such and such condition in the antecedent is essential and, hence, has to be used somewhere. And, once a proof has been found, there comes the long process of polishing and editing. One tries to reduce the calculation to its bare essentials, one has to decide whether to capture a pattern of argument into an explicit sublemma, one has to choose one's free variables very carefully, so as to minimize the amount of renaming, one has to decide upon the order and which formulae to give a number for future reference, etc. (A de- tailed example of such considerations: should you write down -and give a number to - (30) and (32)?

After all, we all know what it means to be a solution to (27) or to (31), don't we? But then you consider, firstly, that in your preliminary explorations you wrote them down yourself - so as not to get confused - and, secondly, that it had been a good thing that you had done so because in some of their usages you substituted something for X. And as it is a good principle never to demand of your reader what you could not do yourself - in this case: substituting in a formula that is nowhere shown - you decide to display the "redundant" (30) and (32) explicitly.) And only when all such decisions have been taken, one can start to write (and even then one sometimes discovers having started to early). (End of Remarks.)

Austin, 5 April 1985

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