The repetition (Draft Ch.6)

The repetition (Draft Ch.6)

This chapter deals with the statement called "the repetitive construct" or "the repetition for short. We shall use DO to denote statements of the form

\begin{array}{l} \underline {{d}} _ {0} \colon B O \rightarrow S O \underline {{o d}} \ d o B O \rightarrow S O J B 1 \rightarrow S 1 o d \ d o B 0 \rightarrow S 0 [ ] B 1 \rightarrow S 1 [ ] B 2 \rightarrow S 2 o d \ \end{array}

in general

\underline {{d o}} \left(\mathbb {I} i: 0 ≤ i < n: B. i \rightarrow S. i\right) \underline {{o d}}

Syntactically it is very similar to the corresp- ponding alternative statement IF:

i f (1 1 i: 0 ≤ i < n: B. i \rightarrow S. i) f _ {i}

Semantically, ${DO}$ and ${IF}$ are related by

\begin{array}{l} (0) D O = \underline {{d o}} B B \rightarrow I F \underline {{o d}} \ w h e r e B B i s a g a m g i v e n b y [ B B \equiv (E _ {i}: o s i < n: B. i) ]. \ \end{array}

Legenda The equality sign between two statements expresses that they are semantically equivalent, i.e. have the same predicate transformers:

S _ {0} = S _ {1} \equiv (¬ X:: [ w ] p (S _ {0}, X) \equiv w ] p (S _ {1}, X) ] \wedge

[ w p (S _ {0}, X) = w p (S _ {1}, X) ]

(End of Legend.)

Remark There are more such equivalences, such as

(1) $\mathrm{{IF}} = \mathrm{{if}}\mathrm{{BB}} \rightarrow \mathrm{{IF}}\mathrm{{fi}}$ ,

which can be proved using the definition of IF

(2) ${DO} = \underline{\operatorname{do}}{BB} \rightarrow {DO}\overset{.1}{0}$

which cannot be proved before we have defined DO . (End of Remark.)

Equality (0) is a postulate. It reduces the repetition with possibly many guards to a repetition with a single guard. It allows us to confine our further definition of the semantics of the repetition to the specially simple state- ment DO given by

(3) ${DO} = \underset{\sim }{do}B \rightarrow S \left( {0}\right)$

and for brevity's sake we shall do so in the sequel.

For DO, B, and S, as connected by (3) we insist on the semantic equivalence

(4) ${DO} =$ if $B \rightarrow S;{DO}∥ ¬ B \rightarrow \operatorname{skip}\frac{f\left( B\right) }{c}$

i.e. we insist that both sides have the same wlp and the same wp . Using the semantics of skip , the semicolon, and the alternative construct this leads to the requirements

(5) $\left\lbrack {{w\rbrack }{p}\left( {{D0},X}\right) \equiv \left( {{GB} \vee {w\rbrack }{p}\left( {S,{w\rbrack }_{p}\left( {{D0},X}\right) }\right) }\right) ∧ \left( {{B}^{ \vee }X}\right) }\right\rbrack$ (6) $\left\lbrack {{wp}\left( {{DO},X}\right) \equiv \left( {¬ B \vee {wp}\left( {S,{wp}\left( {{DO},X}\right) }\right) }\right) ∧ \left( {B \vee X}\right) }\right\rbrack$ .

We shall show that these two requirements are met by defining

(7) $\lbrack {wp}\left( {{DO},{true}}\right) \equiv$ the strongest solution of

Y: [ Y \equiv (¬ B \vee w p (S, Y)) ] ]

(8) [wlp $\left( {{DO},X}\right) \equiv$ the weakest solution of

Y: [ Y \equiv (¬ B \vee w l p (S, Y)) \wedge (¬ B \vee X) ],

From which we shall derive

(g) $\lbrack {wp}\left( {{DO},X}\right) \equiv$ the strongest solution of

Y: [ Y \equiv (¬ B \vee w p (S, Y)) \wedge (B \vee X) ] ].

That requirements (5) and (6) are met is a direct consequence of (8) and (9) respectively, so that is fine. We have to show, however

(i) that (7), (8), and (9) make sense in the sense that the postulated extreme solutions exist (ii) that (9) follows from (7) and (8) (iii) that wlp(D0,?) is universally conjunctive (i.e. Theorem 4.0) (iv) that $wp(D0,?)$ satisfies the law of the Excluded Miracle (i.e. Theorem 4.1)

To begin with, we rewrite (7) and (9) using $[wp(S,Y)\equiv wlp(S,Y)∧ wlp(S,\text{true})]$

(7') [wp (D0, true) = the strongest solution of

Y: [ Y \equiv (¬ B \vee w | p (S, Y)) \wedge (¬ B \vee w p (S, f r u e)) ]

$\left( {9}^{\prime }\right) \left\lbrack {\operatorname{lrp}\left( {{DO},X}\right) \equiv \text{the strongest solution of}f}\right\rbrack$

Y: [ Y \equiv (¬ B v w l p (S, Y)) ∧ (¬ B v w p (S, ¬ u e)) ∧ (B v X) ] ]

thus achieving that in all three defining equations - i.e. in $\left( {7}^{\prime }\right) ,\left( 8\right)$ ,and $\left( {9}^{\prime }\right)$ - the dependence of the right-hand side on $Y$ is confined to the term wlp(S,Y). In particular,all three equations are now of the form -each with its own Z -

\begin{array}{l} (1 0) Y: [ Y \equiv f. (Y, Z) ] \ w i t h F g i v e n b y \ (1 1) \qquad [ p. (Y, Z) \equiv (¬ B \vee w | _ {p} (S, Y)) \wedge Z ] \ \end{array}

From the universal conjunctivity of wlp (S,?) we conclude with Lemma 3.13 that $¬ B \vee wlp(S, ?)$ is universally conjunctive; with - lemma 3.11. The identity function being universally conjunctive as well, we conclude from Lemma 3.18 that $f$ is universally conjunctive (in its complete argument). Hence - lemma 3.19- $f$ is monotonic in its first component and - lemma 5.4: Knaster-Tarski - the extreme solutions of (10) exist. (This conclusion deals with (i).)

Let $g, z$ be (10)'s strongest solution, and

h.2 its weakest. Hence - (10), (11)

$\left( {7}^{1}\right) \equiv \left\lbrack {{wp}\left( {{DO},{true}}\right) \equiv g\left( {{1B} \vee {wp}\left( {S,{true}}\right) }\right) }\right\rbrack$

$\left( 8\right) \equiv \left\lbrack {w\rbrack p\left( {{DO}.X}\right) \equiv h\left( {B \vee X}\right) }\right\rbrack$

$\left( 9\right) \equiv \left\lbrack {{wp}\left( {DO,X}\right) \equiv g.\left( {\left( {{1B} \vee {wp}\left( {S,{true}}\right) }\right) ∧ \left( {{B \vee X}}\right) }\right) }\right\rbrack$

To show that (9) follows from (7') and (8) we observe

w p (D O, X)

= {\mathrm {d e f . o p} w p (S, X)

w p (D O, t r u e) \wedge w l p (D O, X)

= {(7!) a n d (8) }

g. (B v w p (S, f r u e)) \wedge h. (B v X)

= {P _ {i} \mathrm {f i n i t e l y c o n j u n c t i v e}; C o r o l l a r y 5. 5 }

g. ((¬ B \vee w p (S, t r u e)) \wedge (B \vee X))

and thus we have dealt with (ii)

From $p$ 's universal conjunctivity we conclude - Theorem 5.0- that $h$ is universally conjunctive; so is - Lemma 3.13- (Bv??); (8) defines wlp(Do,?) as the functional composition of two universally conjunctive functions, and from Lemma 3.14 we conclude that wlp(Do,?) is universally conjunctive; thus we have dealt with (iii).

To establish $[wp(D0, false) \equiv false]$ we observe that for $[X \equiv false]$ and $[wp(S, false) \equiv false]$ , false is a solution of the defining equation in (9); and hence by definition its strongest; thus we have

deal with (iv).

And this concludes for the repetition our proof obligations as regards Theorem 4.0 and Theorem 4.1. For the repetition we want, however, to prove more, viz. the main theorem we use when reasoning about programs in which a repetition occurs. Before formulating the main theorem, however, some notational preliminaries first.

Let $x$ and $y$ range over some set $D$ of which $C$ is a subset; in that case $x \in D, y \in D, x \in C$ , and $y \in C$ are domain constants of which the first two are by definition true. Let $t$ be a $D$ -valued function on the state space; then $t = y$ is a predicate and so is

(Ey: yEc: t=y) for which we introduce the abbreviation tEc, i.e.

(12) $\left\lbrack {t \in C \equiv \left( {\underline{E}y : y \in C : t = y}\right) }\right\rbrack$

The fact that $t$ is a $D$ -valued function on the state space is expressed by

(13) $\left\lbrack {t \in D}\right\rbrack$

or, in view of (12) - with $C \mathrel{\text{:=}} D$ - equivalently by

$\left\lbrack {\left( {{E}_{y} : y \in D : t = y}\right) }\right\rbrack$

But for the fact that we have not explained yet what it means for a subset of a partially ordered set to be "well-founded" - which shall be explained after the theorem- we are now ready for the formulation of

Theorem 6.0 Let $\left( {D,k}\right)$ be a partially ordered set; let $C$ be a subset of $D$ ,such that $\left( {C,k}\right)$ is well-founded; let statement $S$ , predicates $B$ and $P$ ,and function $t$ on the state space satisfies:

predicate transformer $w p\left( {S,?}\right)$ is monotonic;

(13) $\left\lbrack {t \in D}\right\rbrack$ ; (14) $\left\lbrack {P ∧ B} ⇒ f \in C}\right\rbrack$ (15) $\left\lbrack {P ∧ B ∧ t = x ⇒ {wp}\left( {S,P ∧ t < x}\right) }\right\rbrack$ for all $x$ ; then (16) $\left\lbrack {P ⇒ {wp}\left( {{}^{\prime }{do}B \rightarrow S\underline{od}{,7B} ∧ P}\right) }\right\rbrack$

(The well-informed reader will recognize in the above P an "invariant" of the repetition and in $t$ a "variant function", which is the vehicle of the termination argument.)

from a strictly logical point of view, it would suffice to mention of well-founded sets only the property that is needed to prove Theorem 6.0, something that can be done in a single line. But in order to

apply Theorem 6.0, one has at least to recognize a well-founded set when encountering it (if one has not to construct a well-founded set oneself as part of the correctness argument about a program). For that reason, we now insert, in view of the very central position of Theorem 6.0, an intermezzo on well-founded sets.

Intermezzo on well-founded sets

The standard definition of $(D, \epsilon)$ as a partially ordered set is the combination of a set $D$ and a relation $≤$ (pronounced "at most") such that for all $x, y, z$ elements of $D$

(i) $x ≤ x$ (Reflexivity) (ii) $x ≤ y ∧ y ≤ x ⇒ x = y$ (Anhysymmetry) (iii) $x ≤ y ∧ y ≤ 2 ⇒ x ≤ 2$ (Transitivity).

Its most common model is a directed graph with the elements of $D$ as its nodes and an arrow from $y$ to $x$ as a coding for $x ≤ y$ . From the reflexivity it follows that each $x$ has a so-called "autoloop", i.e. an arrow leading From it to itself. From the antisymmetry it follows that the autoloops are the only directed cyclic paths. The transitivity means that we can inter-

Removing the autoloops -which don't carry any

with the non-reflexive relation $<$ (pronounced "less than")

given in terms of

x < y \equiv x ≤ y ∧ x ≠ y

Alternatively we have

x ≤ y \equiv x < y \vee x = y

Also relation $<$ is transitive. (It is not completely fair to call $(D, <)$ also a partially ordered set, $<$ not being reflexive; yet it is not uncommon. If $x < y$ , it makes, for instance, sense to state that all directed paths from $y$ to $x$ in $(D, <)$ are of finite length: if in $(D, <)$ there is a directed path from $y$ to $x$ , there are also such paths of infinite lengths.)

Next we have the definition of "minimal element":

$\left( {x\text{ is a minimal element of}p}\right) \equiv$

x \in C ∧ (¬ y: y < x: ¬ y \in C)

Note that a minimal element need not be unique.

Take for C the natural numbers; with the standard interpretation of $< ,0$ is the only minimal ele.

ment of $C$ ,but with $<$ defined as

x < y \equiv (\mathrm {E p}: p \mathrm {i s p o s i h v e m o d e g e r :} x + 2 \cdot p = y)

both 0 and 1 are minimal elements of C. Note also that a subset may have no minimal elements: take for $C$ the integers and for $<$ the usual interpretation.

For a partially ordered set to be well-founded is given by the definition

\begin{array}{l} {(C \mathrm {i s w e l l - f o u n d e d}) \equiv (\mathrm {e a c h n o n - e m p h y s u b s e t}} \ {\mathrm {o f} C \mathrm {c o n t a i n s a m i n i m a l e l e m e n t})} \end{array}

For a sequence of elements $x.i\left( {i ≥ 0}\right)$ of $C$ to be a descending chain is given by

\begin{array}{l} (s e q u e n c e x. i (i \ge 0) i s a d e s c e n d i n g c h a i n) \equiv \ (\underline {{A}} i, j: 0 ≤ i < j: x. j < x. i) \ \end{array}

the number of elements in the sequence is called its length.

For mathematical induction over $C$ to be valid, it should suffice to demonstrate

P _ {x} \vee (\exists y: y \in C ∧ y < x: ¬ P _ {y}) \mathrm {f o r a n y} x \in C

in order to prove (Ax: x E C: P.x)

After the above definitions we can formulate

Theorem 6.1 For a partially ordered set $(C, <)$ the following three statements are equivalent

(i) $C$ is well-founded (ii) mathematical induction over $C$ is valid (iii) all deferring chains in $C$ are of finite length.

Proof Th.6.1 In the following proof of the equivalence of (i) and (ii), $V$ ranges over the subsets of $C$ and $P$ over the predicates over the elements of $C$ .

Between the subsets $V$ and the predicates $P$ we establish a one-to-one correspondence by

(1 7) (¬ x: x \in C: P _ {x} \equiv ¬ x \in V)

with the special consequence

(1 8) (\underline {{A}} x: x \in C: P. x) \equiv V = \phi

We now observe

(i)

(ii)

\begin{array}{l} = {\mathrm {d e f i n i t i o n o f w e l l - f o u n d e d n e s s o p c} } \ (\underline {{A}} V: \vee ≠ \phi = (\underline {{E}} x: x \in C: x \in V \wedge (\underline {{A}} y: y \in C \wedge y < x: y \in V))) \ = {\mathrm {n e g a t i n g b o t h s i d e s}; \mathrm {d e M o r g a n} } \ (\underline {{A}} V: V = \phi \equiv (\underline {{A}} x: x \in C: ¬ x \in V \vee (E y: y \in C ∧ y < x: y \in V))) \ = {\mathrm {f r o m d u m m y} V \mathrm {t o d u m m y} P; (1 7) \mathrm {a n d} (1 8) } \ (\underline {{A P}}: (\underline {{A x}}: x \in C: P. x) = \ (\exists x: x \in C: P _ {x} v (\exists y: y \in C ∧ y < x: ¬ P _ {y})) \ = {\mathrm {d e f i n i t i o n o f m a t h e m a t h a t i c a l} \mathrm {i n d u c t i o n o v e r C 3} \ \end{array}

In order to prove $(i) \equiv (iii)$ , we shall show that either side implies the other.

(i) $⇒$ (ii) Defining the predicate DCF by

DCF. $x \equiv$ (all descending chains in $C$ with $x$ as leading element are of finite length)

we observe

D C F. x ≠ (E y: y \equiv c \wedge y < x: ¬ D C F. y)

and further

(i)

\begin{array}{l} ⇒ {\mathrm {m a t h e m a d i c a l} \mathrm {i n d u c t i o n o v e r C v a l i d} } \ (A x: x \in C: D C F. x) \equiv \ (A x: x \in C: D C F. x \vee (E y: y \text {i n} C \wedge y < x: ¬ D C F, y)) \ = {\mathrm {r i g h t - h a n d s i d e} \equiv \mathrm {t r u e} } \ (A x: x \in C: D C F. x) \ = {\mathrm {d e f . o f} D C F } \ (i i i) \ \end{array}

$\eta \left( i\right) ⇒ \eta \left( {iii}\right)$ Let $C$ be not well-founded,i.e. there exists a non-empty $V$ without minimal element, i.e. such that

(\underline {{A}} x: x \in V: (\underline {{E}} y: y < x: y \in V))

but this expresses that each $x$ in $V$ is the leading element of an infinite descending chain in $V$ , from which, $V$ being non-empty, $i(i)$ follows.

(End of Proof Th. 6.1.)

Needless to say, a theorem as beautiful as Theorem 6.1 is of profound significance. The equivalence of (i) and (ii) is nice when we are interested in the existence of minimal elements of subsets, the equivalence between (ii) and (iii) is of particular interest for computing: associating terminating computations with descending chains of finite length, we see some sort of link between finite computations on the one hand and the validity of an inductive argument on the other: computation and mathematical induction go somehow hand in hand.

A well-known example of a well-founded set is presented by the natural numbers with $<$ with its standard meaning; we appeal to its well-foundedness whenever we prove something by mathematical induction over the natural numbers.

Another well-known example is provided by the sentences of a programming language - or any formalism with a similar grammar-; here " $<$ " should be read as "occurs as subsentence in" - clearly a transitive relation! . It leads to "induction over the grammar" as we have encountered in Chapter 4, "Semantics of straight-line programs".

Well-founded sets being the indispensable in- gradient of all termination arguments, computing scientists are regularly invited to invent the proper well-founded set that will carry the ter- mination argument. In this connection, what is known as "The Lexical Ordering" is particularly relevant, as it allows us to construct new well- founded sets from given ones.

Consider two sequences $x.i\left( {osic}n\right)$ and $y.i\left( {osic}\right)$ - note that the sequences are of finite length! - , called x and y respectively; let for each $i$ the elements $x.i$ and $y.i$ belong to the same well-founded set,so that ${x}{i} < {y}{i}$ is defined (i.e. to refer to the ordering relation corresponding that well-founded set). We now define on the sequences $x$ and $y$

\begin{array}{l} a n o r d e r b y d e f i n i n g x < y b y \ x < y \equiv \ (E i: 0 ≤ i < n: (A j: 0 ≤ j < i: x. j = y. j) ∧ x. i < y. i) \ \end{array}

This is called "The Lexical Order"; it is well-founded if, for all i, xi and yi are taken from a well-founded set and vice versa; the proof is left to the reader. (Sometimes one finds the lexical order only defined for $n = 2$ ,i.e.as a - often barely visible - infx operator; this infx operator is as associative as juxtaposition. We leave the proof to the interested reader.)

Example Given a finite bag of natural numbers; a move consists of replacing an $x$ from the bag by a finite bag of natural numbers all $< x$ . Show that the game terminates (because the bag has become empty).

Let all numbers in the bag be $< n$ ; characterize the contents of the bag by listing for $n > j ≥ 0$ in the order of decreasing j the frequency with which $j$ occurs in the bag. Each frequency being a natural number, the lexical order induces well- foundedness on the frequency listings; furthermore the frequency listing is lexically decreased by each move. (End of Example.)

(End of Intermezzo on well-founded sets.)

After the above intermezzo we return to Theorem 6.0, which we still have to prove.

Proof Th.60 On account of (9) - the definition of ${wp}\left( {{DO},?}\right)$ - we can prove (16) by showing

[ P ⇒ Q ]

for any $Q$ that satisfies

[ Q \equiv (¬ B \vee w p (S, Q)) \wedge (B \vee P) ],

an equation, from which we derive by predicate calculus (because we shall need them in a moment) the implications

(19) $\left\lbrack {{¬ B} ∧ P ⇒ Q}\right\rbrack$ (20) $\left\lbrack {P ⇒ \left( {{7B} \vee {wp}\left( {S,Q}\right) \equiv Q}\right) }\right\rbrack$ .

We shall show $\left\lbrack {P ⇒ Q}\right\rbrack$ by showing separately

(i) $\left\lbrack {P ∧ P \Leftrightarrow C ⇒ Q}\right\rbrack$ and subsequently (ii) $\left\lbrack {P ∧ t \in C ⇒ Q}\right\rbrack$

\begin{array}{l} \mathrm {P r o o f} _ {-} = \mathrm {O F} _ {-} (i) \ f r u e \ = {(1 4) a n d p r e d i c a t e c a l c u l u s } \ [ P ∧ ¬ t e c ⇒ ¬ B ∧ P ] \ ⇒ {(1 9) } \ [ P ∧ ¬ ⇒ C ⇒ Q ] \ \end{array}

(E n d o f P r o o f (i).)

Proof. oF (ii).

This part of the proof relies on the fact that $C$ is well-founded. In order to exploit this fact, we first manipulate our demonstrandum so as to make it amenable to a proof by mathematical induction over $C$ .

\begin{array}{l} [ P ∧ t e c ⇒ Q ] \ = {(1 2) } \ [ P ∧ (E x: x \in C: + = x) ⇒ Q ] \ = {\mathrm {d i s t r i b u t i o n o f} \wedge \mathrm {o v e r e x i s t e n t i a l q u a n d i f i c a t i o n} } [ (\mathrm {E x : x \in C : P \wedge t = x}) ⇒ Q ] \ \begin{array}{r l} & {= {\mathrm {p r e d i c a t e c a l c u l u s}; \mathrm {i n t e r c h a n g e o f u n i v . q u a n t i f i c a t i o n} }} \ & { (\underline {{A}} x: x \in C: [ P ∧ t = x ⇒ Q ])} \end{array} \ \end{array}

In view of $C$ 's well-foundedness, the latter is proved by deriving -for any $x$ in $C$

$\left\lbrack {P ∧ t = x ⇒ Q}\right\rbrack$

from

(22) $\left( {A,y : y \in C ∧ y < x : \left\lbrack {P ∧ t = y ⇒ Q}\right\rbrack }\right)$

To this end we observe

(22)

$= {$ interchange of quantifications; predicate calculus

[ (\underline {{E}} y: y \in C ∧ y < x: P ∧ t = y) ⇒ Q ]

$= \left{ {\left\lbrack t = y ∧ y < x \equiv t = y ∧ t < x\right\rbrack ⇒ }\right}$

[ (\underline {{E}} y: y \in C: P \wedge t = y \wedge t < x) ⇒ Q ]

$= {$ distribution of $\Lambda$ over existential quanlification

\begin{array}{l} [ P \wedge (E y: y \in C: t = y) \wedge t < x ⇒ Q ] \ = {(1 2) } \ [ P ∧ t \in C ∧ t < x ⇒ Q ] \ = {[ P ∧ ¬ t \in C ∧ t < x ⇒ Q ] o n a c c o u n t o f (i) } \ [ P ∧ + < x ⇒ Q ] \ ⇒ {w p (S,?) i s m o n o t o n i c } \ [ w p (S, P ∧ f < x) ⇒ w p (S, Q) ] \ ⇒ {(1 5) } \ [ P \wedge B \wedge t = x ⇒ w p (S, Q) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ P \wedge f = x ⇒ ¬ B \vee w p (S, Q) ] \ = {(2 0) } \ [ P ∧ t = x ⇒ 0 ] \ = {\mathrm {d e f i n i t i o n} } \ \end{array}

(End of Proof of (ii).)

(End of Proof Th.6.0.)

We recall for our next discussion

${DO} =$ if $B \rightarrow S$ ; ${DO}∥ ¬ B \rightarrow$ skip ${fi}$

The intended equivalence of these two statements led us to considering extreme solutions of equations of the form

(23) $Y: [Y \equiv f_{\cdot}(X, Y)]$

with $f$ of the form

[ f (X, Y) \equiv (¬ B \vee k. Y) \wedge (B \vee X) ] \tag {24}

According to (8), $w$ lp $\left( {{D0},X}\right)$ is the weakest solution of (23) with wlp $\left( {S,?}\right)$ for $k ;{ac}$ - cording to (9), ${wp}\left( {D0,X}\right)$ is the strongest solution of (23) with ${wp}\left( {S,?}\right)$ for $k$ .

Since the semantics of a program should not be changed if we replace one of its constituent statements by a semantically equivalent one we derive from (4)

(25) $D O = \frac{1}{2} B \rightarrow S;$

i f B \rightarrow S; D O ∥ - B \rightarrow s k i p F _ {i}

\begin{array}{l} | ¬ B \rightarrow s k i p \ F \ \end{array}

Remark The right-hand side of (4) is sometimes referred to as "the first unfolding of $D0$ "; the right-hand side of (25) is similarly called "the second unfolding of $D0$ ". Unfolding -and the inverse transformation, called "folding" - are standard program transformations, which may be used to transform one program into another semantically equivalent one (for instance with the aim of proving their equivalence). (End of Remark.)

Equation (25) immediately raises the question what equation we would have got instead of (23),

had we started from (25) instead of from (4), and also: would we get the same extreme solutions?

of (25) yields instead of (23)

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

with for $k$ the same choices $w\mathbf{l}p\left( {S,?}\right)$ and

[ \tilde {f}. X. Y = f. (X, Y) ]

we could write the above equation

Y: [ Y \equiv (\tilde {P}. X) ^ {2}. Y ]

From Lemma 5.13 we learn that it has the same extreme solutions as (23), for the occasion -functional application being left-associative-- rewritten as

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

This is very comforting. (It were, in fact, considerations like the above that led us to Lemma 5.13. The following "obviously correct" Theorem led similarly to Lemma 5.14.)

\mathrm {T h e o r e m 6 . 2} D O = D O; D O

Proof Th.6.2 Since equivalence of programs means equality of their predicate transformers, we have to show that wlp(D0,?) and wp(D0,?) are idempotent. Since $¬ B \vee k.Y$ is monotonic in $Y$ for

both choices for $k$ ,and $B \vee X$ is monotonic,weakening, and idempotent in $X$ ,we conclude on account of (24) that equation (23) meets the requirements of Lemma 5.14 and, hence, has idempotent extreme solutions. (End of Proof Th.6.2)

Theorem 6.3 ${DO} = \underline{d}0 B \rightarrow {DO} \underline{OD}$

Proof Th.6.3 Let e.x be an extreme solution of (23) with the appropriate choice for k (i.e. wlp(S,?) if e.x is the weakest solution and wp(S,) if e.x is the strongest solution). From (23) and (24) we then deduce

(26) $[e.x\equiv (¬ B\lor k.(e.x))∧ (B\lor x)]$ The predicate transformers of $\mathrm{{do}}\mathrm{B} \rightarrow \mathrm{{DO}} \mathrm{{od}}$ are then the corresponding extreme solutions of (27) $Y \colon \left\lbrack {Y \equiv \left( {¬ B \vee e.Y}\right) ∧ \left( {B \vee X}\right) }\right\rbrack$

We observe

\begin{array}{l} \lnot B \lor e. Y \ = {(2 6) \mathrm {w i t h} X := Y } \ \lnot B \vee ((\lnot B \vee k. (e. Y)) ∧ (B \vee Y)) \ = {v d i s t r i b u t e s o v e r \wedge } \ (¬ B \vee ¬ B \vee k. (e. r)) \wedge (¬ B \vee B \vee Y) \ = {\text {p r e d i c a t e c a l c u l u s} } \ 7 B \vee k. (e. Y) \ \end{array}

Hence (27) is the same equation as

Y: [ Y \equiv (¬ B \vee k. (e. Y)) \wedge (B \vee X) ]

i.e. - see (24)

(2 7 ^ {\prime}) Y: [ Y \equiv f _ {0} (X, e. Y) ]

On account of (24) and Lemma 5.14, our f satisfies the requirement of Lemma 5.15 - even for any monotonic $ip$ , hence the corresponding extreme solution of (27') is again e. (End of Proof Th. 6.3)

Austin, 15 April 1985

prop. dr. Edsger W. Dgikstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1138 United States of America