Lecture notes “Predicate transformers” (Draft)

Lecture notes "Predicate transformers" (Draft)

Introduction

The purpose of this course is manifold. A main target is the development of a number of theorems about predicate transformers, which have proved themselves to be a viable means for the definition of programming language semantics. It is our goal that this development be as self-contained as possible; as a consequence, we shall not hesitate to derive results for which no novelty is claimed. With the statement of our intention to give a "self-contained development" we mean that we intend to build on little more than the predicate calculus.

We have a secondary target, however. We have strong indications that the predicate calculus can serve as much more than just a basis to build upon and that, when properly used, it can be a very useful tool lending itself to intensive usage. Hence our secondary target: showing how the predicate calculus can be used at good advantage.

So we shall use the predicate calculus intensively. In doing so we hope to discover -and in this respect our development can be viewed as gathering experience- how to separate the many, many formulae from the predicate calculus into those to be known and those to be derived when needed. This (as yet absent) body of experience is needed when we wish to learn and then to teach how to use the predicate calculus sufficiently effectively, i.e. several orders of magnitude more effectively than its untrained user applies it. The inspiration for this last desire is very simple. On

the one hand -as some reflexion shows- the predicate calculus is the most promising carrier for convincing arguments about specific programs and for the derivation of programs meeting given specifications. On the other hand the viability of the predicate calculus as tool for programming methodology has been doubted on account of the experience that, in situations more ambitious than toy examples, formulae quickly tended to get unwieldy. We have reasons to believe that this disappointing experience is less due to some intrinsic inadequacy of the predicate calculus than to lack of knowledge how to use the predicate calculus well. Hence our desire to learn how to do the latter.

As said above, we intend to build on the predicate calculus. That means that we assume our readers able to convince themselves of the correctness of all its formulae we use and that we leave its definition and foundation gladly to the logicians, who are the experts in that field.

In contrast, we shall be fairly explicit about our notational conventions -conventions to which we intend to stick religiously-. We have to, not only because the world that agrees what the predicate calculus is about does not display a similar consensus on what notational conventions to adopt, but also because -after much hesitation and careful consid- deration. I have adopted a few conventions of my own that, to the best of my knowledge and foresight, made my formulae better suited to my manipula-tive needs. (Adoption of a notational convention of one's own is a very grave step; I found the courage to take it in the observation that it enabled me to ma

nipulate my formulae much more simply and sys- tematically than I could have done otherwise. I am perfectly willing to discuss the merits of my conven- tions with those of alternatives; the Freedom to shed the notational shackles with which others are trying to live and to work I consider, however, the scientist's inalienable right, notwithstanding the fact that I know full well the difficulty of making good use of it.)

General concepts and notational conventions

We consider predicates to be two-valued total functions defined on the Cartesian product of the spaces belonging to zero or more named coordinates, in this context also often referred to as variables. The spaces belonging to the individual coordinates are non-empty and well-understood -say, as well-understood as the integers or the natural numbers-.

Note that the trivial space of zero dimensions is deemed to consist of a single anonymous point. Hence, only two different predicates can be defined on the trivial space; they are denoted by true and false respectively.

A predicate in x and y is also a predicate in x, y, and z ; its value not depending on z, it enjoys in this three-dimensional space the special property of being constant along lines in the z-direction. In other words, a predicate on a given space is also a predicate on any space of more dimensions of which the given space is a "Cartesian factor". The trivial space being a factor of any space, aforementioned predicates are defined on any space.

As a result, two predicates, each with its own space, can always be regarded as predicates in the same space, viz. "the least common Cartesian multiple" of their individual spaces; when two predicates on possibly different spaces are connected to form a new predicate, the latter is a predicate on that "least common Cartesian multiple," e.g. if $P$ is a predicate in $x$ and $y$ , and $Q$ is a predicate in $y$ and $z$ , connecting $P$ and $Q$ yields a predicate in $x$ , $y$ , and $z$ .

Note that from a predicate in at least two variables we can always form without loss of information a predicate in one variable less: for a predicate in x and y we can construct a predicate in a new variable instead that ranges over all ordered pairs (x,y). We shall only consider predicates depending on a finite number of variables, and the moral of the previous remark is that their precise number is a bit arbitrary. (This need not disturb us too much: the system of two equations P and Q is also the system of the one equation PwQ.) Since a variable may be of a type with an infinite range -e.g. of type integer-the number of points of a predicate's space need not be finite.

Side remark Variables ranging over a class of predi-dicates will not be excluded. We shall - in order to avoid all sorts of difficulties - never introduce a predicate whose value depends on a variable of which the predicate itself is a possible value. As far as I can see this constraint will not prevent me from introducing all the recursive predicate definitions I need. (End of Side remark.)

From predicates we shall construct new predicates using the well-known operators -given in order of decreasing binding power

negation A conjunc tion V disj u n c t i o n $⇒$ implication 三 equivalence ≠ difference

Note. Since it does not matter whether we write

(P \equiv Q) ≠ R o r P \equiv (Q ≠ R)

the suggested greater binding power of $\equiv$ over $≠$ is spurious. I could have given them in the same line, or the other way round. (End of Note.)

Negation is a unary operator and is point-wise defined: $P$ and $?P$ are defined on the same space, in each point of which the one of them is true and the other is false.

The others are binary operators, and are pointwise defined on the smallest common Cartesian multiple of the spaces of their arguments.

Conjunction is symmetric and associative: if it is true where all its arguments are true, and false elsewhere.

Disjunction is symmetric and associative: it is false where all its arguments are false, and true elsewhere.

Implication is neither symmetric nor associative; the distinction between $P ⇒ Q$ and $¬ P \lor Q$ is only textual. We shall use implication only where its asym-

metry can be exploited to advantage.

Note. Together with universal quantification - see below- implication can be used for the definition of a partial order among predicates which enables us to link the predicate calculus to lattice theory. This fact is of fundamental significance; its lack of symmetry and of associativity, however, make it cumbersome to manipulate. Universal quantification often being left implicit, it has led to endless confusions -vide the rather scholastic flavour of the distinction between the "logical implication" and the "material implication". We shall not hesitate to use implication in the trivial space in which universal quan- hification - whether hidden or not- is the identity function. (End of Note.)

Equivalence is symmetric and associative: if it is true where an even number of its arguments are false, and is false elsewhere.

Difference is symmetric and associative: if is false where an even number of its arguments are true, and is true elsewhere.

Equivalence and difference usually occur with two arguments, and rarely with more than three (which is not amazing in view of the role of the notion "even").

There is one drastic way of deriving from a predicate P on some space a predicate on the trivial space: uni- versal quantification over all points of the space on which $\mathcal{P}$ is defined. Since in many of our manipula- tions that space will be left anonymous -we have already seen that its actual dimension is not of overwhelming relevance-and we need that universal quantification

quite frequently denoted, we introduce a special no- tation for it, viz. surrounding P by a pair of square brackets: [P] . Axioms, theorems, facts, definitions, etc. will frequently be expressed in terms of such universally quantified predicates, e.g. defining for given Q the predicate P by

[ P \equiv Q ]

means that the distinction between "P" and "Q" is only textual - as is the distinction between "[P=Q]" and "true". Thus we can express the following rewrite rules, applicable to any P, Q, and R. (For a start we give both the fully parenthesized form and the form in which parenthesis pairs that our binding conventions have made redundant have been omitted.)

[ (¬ (¬ P)) \equiv P ]

[ 7 7 P \equiv P ]

[ (G (P ∧ Q)) \equiv ((¬ P) \lor (¬ Q)) ]

[ ¬ (P ∧ Q) \equiv ¬ P \lor ¬ Q ]

[ (P ⇒ Q) \equiv (¬ P) \vee Q) ]

[ P ⇒ Q \equiv ¬ P \lor Q ]

Remarks. A comparison of the above two columns strongly suggests that the writing of the fully parenthesized form is a pain in the neck. So we had better appeal to the binding conventions to eliminate a number of parenthesis pairs.

In general I cannot recommend the exploitation of the convention that gives the conjunction a greater binding power than the disjunction, since this convention introduces the syntactic destruction of a semantic symmetry.

In the case of long formulae it is recommended to surround the connective with the lowest binding

power by some additional blank space.

Comment. This is a suggestion very similar to the well-known "rules of indentation" that have established themselves -almost by natural selection- for many a programming language. Impressed by indentation's "aid to readability", some language designers have gone a step further and have given indentation a role in the definition of the nesting structure of the text. In my experience the convention leads to consequences that are in conflict with other purposes of layout, and hence I cannot recommend it. (End of Comment.)

In order to avoid confusion with the Roman v and V and with the Greek A, I recommend striving for a right angle when writing V or A. (End of Remarks.)

With $P$ and $Q$ "of type Boolean" - i.e. predicates on the trivial space - many theorems are expressed in terms of $P \equiv Q$ or of $P ⇒ Q$ . When this is not an obvious instance of a known formula, we prove it in two or more steps by the introduction of one or more intermediate predicates.

So may the computation that $P \equiv Q$ has the value true take the form of establishing that for some pro- perly chosen $R$ , $P \equiv R$ and $R \equiv Q$ both have the value true.

So may the computation that $P ⇒ Q$ has the value true take the form of establishing that for some properly chosen $R$ , $P \equiv R$ and $R ⇒ Q$ both have the value true.

Remark. In view of the use made of $\mathsf{P}\equiv \mathsf{R}$ in the last example, it would have "sufficed" to compute that

$P ⇒ R$ has the value true. For the sake of clarity, we shall not use the implication where the equivalence applies. (End of Remark.)

For very fundamental reasons we need a notational convention that allows us to render the structure of such a proof in a way such that the intermediate pre-dicate R needs to be written down only once.

The above computation that $P \equiv Q$ has the value true will be represented as follows:

\begin{array}{l} = \begin{array}{l} P \ \hline \text {h i n t w h y} P \equiv R \text {h a s t h e v a l u e t r u e} \ R \end{array} \ = {\mathrm {h i n t} \mathrm {w h y} R \equiv Q \mathrm {h a s t h e v a l u e t r u e} } \ \end{array}

The above computation that $P ⇒ Q$ has the value true will be represented as follows:

\begin{array}{l} = \left{ \begin{array}{l l} P \ R \end{array} \right. \ ⇒ {\mathrm {h i n t} \mathrm {w h y} R ⇒ Q \mathrm {h a s t h e v a l u e t r u e} } \ \end{array}

Legenda. In the above "why" can be read (four times) as "how the reader can convince himself that".

Whether the hint suffices depends at least as much on the reader as on the writer: if the reader is to convince himself -whatever that may mean!- he is the one to do that. (End of Legend.)

The reasons for selecting a notation that mentions the intermediate predicate R only once are the following. In non-trivial proofs, such an R is often a formula of some length. Writing it out twice

EWD835-9

would not only be a burden on the writer (which would not matter if it helped the reader) but also a burden on the reader, who would have to perform a string comparison in order to establish the (for the argument essential) sameness of the two oc-currences. This, of course, could be circumvented by giving the formula a name, $R$ say.

But we should not burden our texts with names if we can avoid them. Naming something which is se- ferred to by name only once is obviously pointless; two references is therefore the most meagre justifica tion for the introduction of a new name. This justification is insufficient when the duplication can be avoided by placing the "something" in some sort of infix position, provided the notational convention thus introduced is used sufficiently frequently.

Note. Since the scaling up of discrete reasoning is one of the central challenges of computing science, seemingly minor details like the size of the nomenclature to be introduced need our attention. (End of Note.)

Syntactic remark. When thus representing demonstrations, we give the separators $= {$ hint $}$ " and $⇒ {$ hint $}$ " the lowest binding power of all. (End of Syntactic remark.)

Occasionally we shall compute that $P \equiv Q$ has the value true by computing that both $P ⇒ Q$ and $Q ⇒ P$ have the value true. Omitting intermediate steps, we can render the structure of that computation by

\begin{array}{l} p \ ⇒ {\mathrm {h i n t} 1 } \ Q \ ⇒ {\mathrm {h i n t} 2 } \ p \ \end{array}

Here the use of the $⇒$ could have been avoided: with the same hints we could have written

or

\begin{array}{l} = \left{ \begin{array}{l} P \ \mathrm {h i n t} + 1 \ P \wedge Q \end{array} \right} \ \begin{array}{l} P \ = \left{ \begin{array}{l} h i n + 2 \ P \vee Q \end{array} \right} \end{array} \ = \left{ \begin{array}{l} \mathrm {h i n t 2} \ Q \end{array} \right} \ = {h i n t: 1 } \ \end{array}

Our earlier version, however, is shorter.

For $\left\lbrack {P ⇒ Q}\right\rbrack$ we also read " $P$ is as strong as ${Q}^{\prime \prime }$ or " $Q$ is as weak as ${P}^{\prime \prime }$ ; for ${\left\lbrack P ⇒ Q\right\rbrack }^{ ∧ }$ ? [P=P] we also read " $P$ is stronger than " or "Q is weaker than $P$ ". The nature of our game is now clear: from one line to the next we shall massage predicate expressions either hinting why equivalence holds or why in the transi tion to the next line we have not strengthened the predicate.

As said before, this is not the moment to give an exhaustive catalogue which hints to admit. I expect to give the not very descriptive hint "predicate calculus" wherever it seems obvious to me which by then familiar rewriting rule has been applied. Some of them I shall take for granted right at the start, such as the following

\begin{array}{l} [ P ∧ (Q \lor R) \equiv (P ∧ Q) \lor (P ∧ R) ] \ [ P \vee (Q \wedge R) \equiv (P \vee Q) \wedge (P \vee R) ] \ \end{array}

expressing the mutual distributivity of conjunction and disjunction. Since also

(0) [ P \equiv Q ] ⇒ ([ P ] \equiv [ Q ])

has the value true for any $P$ and $Q$ ,we compute that also

[ P ∧ (Q \lor R) ] \equiv [ (P ∧ Q) \lor (P ∧ R) ]

has the value true for any $P,Q,$ and $R$ .

Reasonably well-known is the formula

[ P ⇒ Q ] \equiv [ P \equiv P ∧ Q ]

(and so is its companion $\left\lbrack {P \equiv Q}\right\rbrack \equiv \left\lbrack {Q \equiv P \vee Q}\right\rbrack$ ); the abominable Venn-diagrams have seen to that. It is, however, with the aid of (o) a direct consequence of the also valid

[ P ⇒ Q \equiv P \equiv P ∧ Q ]

• easily settled by the point- wise argument substitu

[ Q \equiv \mathrm {t r u e} \equiv Q ] a n d [ t r u e \equiv f a l s e \equiv f a l s e ]

have the value true - Remembering that $\equiv$ is symmetric and associative,we see two other ways of applying (o), yielding that both

\begin{array}{l} [ P ⇒ Q \equiv P ] \equiv [ P ∧ Q ] \qquad a n d \ [ P ⇒ Q \equiv P ∧ Q ] \equiv [ P ] \ \end{array}

have the value true. (Neither of the last two formulae seems worth remembering. They were derived by way of illustration.)

Formulae specially related to the fact that square brackets denote universal quantification (over a nonempty space) are

[ P ] \vee [ Q ] ⇒ [ P \vee Q ]

[ P ] \wedge [ Q ] \equiv [ P \wedge Q ]

[ P ] \vee [ Q ] \equiv [ P \vee [ Q ] ]

[ P ] \wedge [ Q ] \equiv [ P \wedge [ Q ] ]

• the last formula only being valid because the space is not empty. (Well, not really!)

Besides (universal) quantification over the points of the space of a predicate, we need quantification over predicates from a bag $B$ of predicates defined on the same space. Universal quantification is expressed by

(\underline {{A}} X: X \underline {{\mathrm {i n}}} B: X)

In the case of a finite bag B , this expression denotes the conjunction of the elements of $B$ . It then satisfies

(A) $\left( {\underline{A}X : X\text{ in }B : \left\lbrack X\right\rbrack }\right) \equiv \left\lbrack {\left( {\underline{A}X : X\text{ in }B : X}\right) }\right\rbrack$

-i.e. universal quantificatons commute

(2) $\left\lbrack {\left( {{\underline{\mathrm{A}}}\mathrm{X} : \mathrm{X}\text{ in }\mathrm{B} : Q\mathrm{v}\mathrm{X}}\right) \equiv Q\mathrm{v}\left( {{\underline{\mathrm{A}}}\mathrm{X} : \mathrm{X}\text{ in }\mathrm{B} : \mathrm{X}}\right) }\right\rbrack$

-i.e. disjunctiOn distributes over universal quantificaion

(3) $\left( {\underline{A}Y;Y\mathop{\in}\limits_{B} : \left\lbrack {\left( {A}^{X};X\mathop{\in}\limits_{B} : X\right) ⇒ Y}\right\rbrack }\right)$

Formula (1), (2), and (3) are postulated to apply as well in the case of an infinite bag B ; B need

not even be denumerable.

From (3) it follows that (A $X : X$ in $B : X$ ) is a solution of

$Z : \left( {{AY} : Y\text{ in }B : \left\lbrack {Z ⇒ Y}\right\rbrack }\right)$

Note on notation. For given $Z$ and $Y$ , $[Z ⇒ Y]$ is a predicate on the trivial space. For given $Z$ and $B$ , $(\underline{A}Y: Y \underline{\mathrm{in}} B: [Z ⇒ Y])$ is again a predicate on the trivial space. By prefixing it with "Z:" we form the equation whose roots are those predicates that, (when substituted for $Z$ ) make the prefixed predicate coincide with true. (End of Note on notation.)

Furthermore we have for any $P$

\begin{array}{l} (A Y: Y _ {i n} B: [ P ⇒ Y ]) \ = {\text {p r e d i c a t e c a l c u l u s , (1) i n p a r t i c u l a r} } \ [ (A Y: Y \underline {{\underline {{\mathrm {i n}}} B}}: P ⇒ Y) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (A Y: Y _ {i n} B: ¬ P \vee Y) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s , i . e . (2) w i t h} \mathcal {P} \mathrm {f o r} Q } \ [ Π P V (A Y: Y \underline {{\underline {{\mathrm {i n}}} B}}: Y) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s a n d r e n a m i n g} } \ [ P ⇒ (\underset {\mathrm {A X : X i n B : X}} {¬}) ] \ \end{array}

Comparing the first line of the above deduction with (4) we see that any solution of (4) is as strong as $\left( {AX : X\ln B : X}\right)$ ,which is therefore the weakest solution of (4).

Conversely we could have defined $\left( {A \times : X\text{ in }B : X}\right)$ as the weakest solution of (4); in that case the existence of the weakest solution should have been postulated.

Defining (E X: X in B: X) - existental quantificatior -

which very much looks like a generalization of de Morgan's law-, this expression denotes in the case of a finite bag B the disjunction of its elements. Analogously to (2) and (3) we have

(5) $\left\lbrack {\left( {{E}{X} : X\text{ in }B : Q ∧ X}\right) \equiv Q ∧ \left( {{E}{X} : X\text{ in }B : X}\right) }\right\rbrack$

i.e. conjunction distributes over existential quanti- fication- and

(6) $\left( {{A}{Y} : {Y}{\text{in }}B : \left\lbrack {Y ⇒ \left( {{EX} : X\text{ in }B : X}\right) }\right\rbrack }\right)$

Conversely we could have defined (E X: X in B: X) as the strongest solution of

$Z : \left( {{AY} : {Y}_{\text{in}}B : \left\lbrack {Y ⇒ Z}\right\rbrack }\right)$

together with the postulate that that solution exists.

Between the colons we had " $x$ in $\mathcal{B}$ " or " $Y_{\underline{\mathrm{i}}}$ B"; this is referred to as the range of the dummy. The indication is omitted - what is indicated by placing the colons in immediate succession - when the range is understood, e.g. to be the set of all predicates on the space under consideration, as is the case in the formulation of

(8) $\left( {A{X}_{\because }\left\lbrack {{Xv}P}\right\rbrack \equiv \left\lbrack {{Xv}Q}\right\rbrack }\right) \equiv \left\lbrack {P \equiv Q}\right\rbrack$

To compute that the above coincides with true we use the elementary

[ (P \vee ¬ Q) \wedge (Q \vee ¬ P) \equiv P \equiv Q ]

and proceed as follows:

\begin{array}{l} [ P \equiv Q ] \ ⇒ {\text {p r e d . c a l c . , v i z . (0)} } \ (\underset {\sim} {A} X:: [ X \vee P ] \equiv [ X \vee Q ]) \ ⇒ {\mathrm {c h o o s e} ¬ P \mathrm {a n d} ¬ Q \mathrm {r e s p e c t i v e l y} } \ ([ ¬ P \vee P ] \equiv [ ¬ P \vee Q ]) \wedge ([ ¬ Q \vee P ] \equiv [ ¬ Q \vee Q ]) \ = {\mathrm {p r e d . c a l c .} } \ [ ¬ P \lor Q ] ∧ [ ¬ Q \lor P ] \ = {\mathrm {p r e d . c a l c .} } \ [ (¬ P \lor Q) ∧ (¬ Q \lor P) ] \ ⇒ {\mathrm {p r e d . c a l c . a n d} (0) } \ [ \vec {P} \equiv 0 ] \ \end{array}

Predicate transformers and programming languages.

Semantics of programming languages have been de- fined in terms of so-called "predicate transformers", in particular $\mathsf{wp}$ ("weakest precondition") and $\mathsf{wlp}$ ("weakest liberal precondition").

For a given program $s$ and a postcondition R the operational interpretation of wp(S,R) is the weakest condition on the initial state such that firing S is guaranteed to lead to a terminating computation ending in a final state where R coincides with true .

In the case of unbounded nondeterminacy - as we shall see later- two different notions of termination present themselves. They correspond to two different definitions for $\mathfrak{wp}$ that we shall denote differently. The distinction will be postponed until relevant.

The definition in terms of $wp$ has the practical advantage that it fully captures what we are usually in- terested in when designing a program: in that situation

we are usually not too interested in initial states for which termination is not guaranteed. For such initial states the concept of wp alone leaves the semantics of the program undefined. This is no longer the case when we define the weakest liberal precondition as well.

For a given program $S$ and a postcondition $\mathcal{R}$ the operational interpretation of wlp(S,R) is the weakest condition on the initial state such that firing $S$ is guaranteed to lead to a computation that either fails to terminate or ends in a final state where R coincides with true.

We shall give one further consequence of this operational interpretation: $¬ \operatorname{wlp}\left( {S,¬ R}\right)$ characterizes those initial states for which firing $S$ may lead to a computation ending in a final state where $R$ coincides with true . (It expresses the possiblity of $R$ being finally valid. If pairs each final state to those initial states "from which it can be reached via ${S}^{\prime }$ ; it thus opens the way of dealing with program semantics in terms of the relational calculus.)

These predicate transformers will be defined in the usual way, i.e. inductively over the syntax of the little programming language fragment. At the same time we would like to prove a number theorems, such as

Theorem 0. [7 w p (S, f a s e) ] for any program S.

Theorem 1. [wlp(S, true)] for any program $S$ .

Theorem 2. [wp(S,R) ≡ wlp(S,R) ∧ wp(S,false)] For any program S and any R.

Theorem 3. [wp(S,(AP:PinB:P))](For any program S and any non-empty bag B of pre-dicates.

Theorem 4. [wlp(S, (AP: Pin B: P)) ≡ (AP: Pin B: wlp(S, P))] for any program S and any bag $B$ of predicates.

Theorem 3 Follows from Theorems 2 and 4.

Proof For any $X$ and any non-empty bag $B$ of predicates

\begin{array}{l} [ X \equiv w _ {p} (S, (\underline {{A}} P: P _ {\underline {{i n}}} B: P)) ] \ = {\mathrm {T h e o r e m} 2 } [ X \equiv w p (S, (\underline {{A P}}: P _ {\mathrm {i n}} B: P)) \wedge w p (S, \mathrm {t r u e}) ] \ = {\mathrm {T h e o r e m} 4 } [ X \equiv (\underline {{A}} P: P _ {\mathrm {i n}} B: w p (S, P)) \wedge w p (S, t r u e) ] \ = {\mathcal {B} \mathrm {i s n o n - e m p h y} } [ X \equiv (\overline {{A}} P: P _ {\mathrm {i n}} \mathcal {B}: w l p (S, P) \wedge w p (S, t r u e)) ] \ = \left{T h e o r e m 2 \right} [ X \equiv (\underline {{A}} P: P _ {\ln B}: w p (S, P)) ] \ \end{array}

(End of Proof.)

Remark. At the very end we have omitted explicit reference (AX: [X=P] [X=Q]) = [P=Q]

We shall also do so in the sequel. (End of Remark.)

By now we have had two hints that of wp and wlp, the latter one has the nicer properties. The one is that $¬ \mathsf{wp}(\mathsf{S},¬ \mathsf{R})$ -try to interpret it! - is not half as useful as $¬ \mathsf{wlp}(\mathsf{S},¬ \mathsf{R})$ ; the other one is that, as a result of the added constraint "non-empty", Theorem 3 is not as beautiful as Theorem 4. (The added constraint "non-empty" is essential; without it, Theorem 3 would be wrong.)

In order to prove such theorems smoothly, we can make good use of a number of concepts and theorems about predicate transformers in general.

Let $f$ be a predicate transformer, i.e. some func tion from predicates to predicates. Functional ap- plication will be denoted by juxtaposition, eg "f P", and will be given the highest binding power of all, i.e.

f P ∧ Q i s s h o r t f o r (f P) ∧ Q

Note. For the time being we can postpone the decision whether functional application will be regarded as left-associative or right-associative. When the time comes I expect us to prefer left-associativity. (End of Note.)

Until further notice we shall confine ourselves to predicate transformers for which argu-ment and value are predicates on the same space.

For a predicate transformer $f$ and a bag $B$ of predicates on the same space we define - in- spired by the formulae in Theorems 3 and 4 - the notion of conjunctivity by

(f i s c o n j u n c t i v e o v e r B) \equiv

[ f (\underline {{A}} P: \overline {{P _ {\mathrm {i n} B : P}}}) \equiv (\underline {{A}} P: P _ {\mathrm {i n} B}: f P) ]

and different degrees of conjunctivity by specifying over bags of which type $f$ is conjunctive, in particular:

\begin{array}{l} {(f i s u n i v e r s a l l y c o n j u n c t i v e) \equiv} \ {(f i s c o n j u n c t i v e o v e r a n y b a g)} \end{array}

\begin{array}{l} \begin{array}{l} {(f i s \mathrm {u n b o u n d e d l y c o n j u n c t i v e}) \equiv} \ {(f i s \mathrm {c o n j u n c t i v e o v e r a n y n o n - e m p l y b a g})} \end{array} \ \begin{array}{l} {(f i s \mathrm {i n f i n i t e l y c o n j u n c t i v e}) \equiv} \ {(f i s \mathrm {c o n j u n c t i v e o v e r a n y n o n - e m p l y d e n u m e r a b l e b a g})} \end{array} \ \begin{array}{l} {(f \mathrm {i s c o n j u n c t i v e}) \equiv} \ {(f \mathrm {i s c o n j u n c t i v e o v e r a n y n o n - e m p l y f i n i t e b a g}).} \end{array} \ \end{array}

Note that as the class of bags over which conjunctiv is required gets smaller, the type of conjunctiv becomes a weaker property: a universally conjunctive $f$ is unboundedly conjunctive; an unboundedly conjunctive $f$ is infinitely conjunctive; an finitely conjunctive $f$ is conjunctive (sec).

In our new jargon, we can summarize Theorems 3 and 4 by stating that wlp is universally conjunctive, whereas wp is only unboundedly conjunctive.

Note that, since universal quantification $\gamma$ by definition coincides with true , for any $f$

\begin{array}{l} (f \mathrm {i s u n b o u n d e d l y c o n j u n c t i v e}) \wedge [ f \mathrm {t r u e} ] \ \equiv (\dot {f} i s u n i v e r s a l l y c o n j u n c t i v e) \ \end{array}

The importance of the various degrees of conjunctivvity is probably to be found in the circumstante that the functional composition of two predicate transformers of the same degree of conjunctivity enjoys that same degree of conjunctivity. Let us define functional composition of predicate transformers first.

For any two predicate transformers $f$ and $g$

the functional composition fog is defined by

[ \operatorname {p o g} X \equiv f (g X) ] \mathrm {f o r a n y} X.

Note. Here the binding power of $\phi$ is deemed to be even higher than functional application. At the same time we have placed the parenthesis in $\phi (gX)$ as if we have already decided that functional application is left-associative. Were functional application chosen to be right-associative $\phi gX$ would be interpreted "automatically" as $\phi (gX)$ , what we denote as $\phi gX$ . Right-associativity would make the character o therefore rather superfluous. But Curry would not like its omission. We wish to be able to denote the functional composition e.g. by $\phi g$ ; omission of the o would then lead to $\phi g$ , but this justa-position would then not be functional application. The decision to choose functional application to be left-associative -at least: not right-associative -came sooner than expected! (End of Note.)

Remark on notation. We have defined universal quantifici- cation for any bag $B$ of predicates: (AX: X in B: X) We have, however, already used (AX: X in B: QvX) which is a special case of (AX: X in B: Px).

For any bag $B$ of predicates and any predicate transformer $f$ we can define a new bag, denoted

i.e. the bag B in which each element is replaced by fX . (This is standard usage of the bag for mator B).

The more general universal quantification com then be defined by

EWD835-21

[ (\underline {{A}} X: X \underline {{\ln}} B: f X) \equiv (\underline {{A}} Y: Y \underline {{\ln}} (\underline {{B}} X: X \underline {{\ln}} B: f X): Y) ].

The same can be done for existential quantification.

The construction of (Bx: X in B: fX) implies that (Bx: X in B: fX) has "as many elements" as B : they are both empty or both non-empty, they are both finite or both infinite, they are both denumerable or both nondenumerable. (End of Remark on notation.)

We now return to the conservation of degree of conjunctivity. Reading for BAG "bag", "non-empty bag", "non-empty denumerable bag" or "non-empty finite bag", we have the four theorems

$\left( {fandg}\right.$ are both conjunctive over any ${BAG}) ⇒$ (fog is conjunctive over any BAG)

Four proofs. Let $f$ and $g$ be both conjunctive over any BAG and let $B$ be a BAG. Then, for any

\begin{array}{l} [ z \equiv f \circ g (\underline {{A}} X: X _ {\mathrm {i n}} B: X) ] \ = {d e f i n i t i o n o f p u n c t i o n a l c o m p o s i t i o n } [ 2 \equiv f (g (\underline {{A}} X: X \underline {{i n}} B: X)) ] \ = {g \mathrm {i s c o n j u n c t i v e o v e r a n y B A G} } \ = {f \mathrm {i s c o n j u n c t i v e o v e r a n y} B A G } \ = {\mathrm {d e f i n i t i o n o f p u n c t i o n a l c o m p o s i t i o n} } [ Z \equiv (\underset {\sim} {A} X: X \underline {{\operatorname {i n}}} \mathcal {B}: \log X) ] \ \end{array}

hence $\left\lbrack {\operatorname{Pog}\left( {\underline{A}X : X\text{ in }B : X}\right) \equiv \left( {\underline{A}X : X\text{ in }B : \operatorname{Pog}X}\right) }\right\rbrack$

i.e. fog is conjunctive over any BAG.

(End of Four proofs.)

A predicate transformer is said to be monotonic if it preserves the partial order of universally quan- tified implication, more precisely

\begin{array}{l} (f _ {i s m o n o t o n i c}) \equiv \ (\mathrm {f o r a n y} X \mathrm {a n d} Y [ X ⇒ Y ] ⇒ [ f X ⇒ f Y ]) \ \end{array}

Theorem. A conjunctive predicate transformer is monotonic.

Proof. For any conjunctive predicate transformer $f$ and any two predicates $X$ and $Y$

\begin{array}{l} [ X ⇒ Y ] \ = {\mathrm {p r e d . c a l c} } [ X ∧ Y \equiv X ] \ ⇒ {\mathrm {f u n c t i o n a l} \mathrm {a p p l i c a t i o n} } \ [ f (X \wedge Y) = f X ] \ = {f ^ {p} \mathrm {i s c o n j u n c t i v e} } \ = \left{ \begin{array}{l l} p r e d. c a l c \ [ f X ⇒ p Y ] \end{array} \right. \ \end{array}

(End of Proof)

Intermezzo. While lecturing last week I realized that I should probably have used the "bagiFier": given a bag B containing X's on which a function $f$ is defined, we can form a new bag

C = (\underline {{B}} x: x \mathrm {i n} B: f x)

where $B$ and $C$ are both empty or not,etc. The one essential property of bagification is that with $f$ the identity function. $C = B$ ,i.e.

C = (\underline {{B}} y: y \mathrm {i n} C: y)

The other essential property of bagification is

\begin{array}{l} (\underline {{B}} x: x \underline {{i n}} (\underline {{B}} y: y \underline {{i n}} C: g y): f x) = \ (\underline {{B}} y: y \mathrm {i n} C: f (g y)) \ \end{array}

(End of Intermezzo.)

With " $P$ is a fixed point of $f$ " meaning $\left\lbrack {P \cap P \equiv P}\right\rbrack$ we can formulate the theorem:

A common fixed point of $f$ and $g$ is also a fixed point of $\log ,\mathrm{i.e.}$ "Functional composition is fixed-point preserving".

Proof. Let $P$ be a fixed point of both $f$ and $g$ . Then for any $z$

\begin{array}{l} [ Z \equiv f o g P ] \ = {\mathrm {d e f i n i t i o n o f} \mathrm {f u n c t i o n a l c o m p o s i t i o n} } \ = {P \mathrm {i s a} [ z \equiv f P ] ^ {\mathrm {f i x e d p o i n t o f}} g } \ = {P i s a f i x e d p o i n t o f P } [ Z \equiv P ] \ \end{array}

(End of Proof.)

The simple fact that fixed points are preserved by functional composition is our first indication that the notion of a fixed point might be an important concept.

We now proceed to define our little program- ming language, proving the Theorems 0,1,2, and 4 as we go along. Note that theorems 0 and 1 could have been formulated as

$\left\lbrack {{wp}\left( {S,\text{false}}\right) \equiv \text{false}}\right\rbrack$ and $\left\lbrack {{wlp}\left( {S,\text{true}}\right) \equiv \text{true}}\right\rbrack$ , in other words: false is a fixed point of ${wp}$ , and true is a fixed point of wlp.

The semantics of skip are defined by

[ w p (s k i p, R) \equiv R ] a n d [ w l p (s k i p, R) \equiv R ]

for any $R$ . Since any predicate is a fixed point of both ${wp}$ and ${Wp}$ ,all five (or four) theorems are trivially correct.

Let $x$ be one of the coordinates of the state space; let defE be the predicate that coincides with true wherever the expression E is defined, and false everywhere else.

Remark. The predicate defE is assumed to be a total function. Evaluation of E where defE is assumed to lead to a unique value of E, where i defE , however, it is assumed to lead to a non-terminating computation. (End of Remark.)

The semantics of the assignment statement $x \mathrel{\text{:=}} E$ is given by

[ w p (x := E, R) \equiv d e f E \underline {{c a n d}} R (E / x) ] \mathrm {f o r a n y} R

[ w l p (x := E, R) \equiv ¬ d e p E c o r R (E / x) ] f o r a n y R

Here and and cor are the so called conditional

[true cox = true] without assumptions that X is a total predicate. Note that cand and cor are not symmetric, but satisfy together de Morgans law [7(P cand Q) ≡ (7P) cor(7Q)]. These con- nectives have been used to make the right-hand sides also total predicates iP 7[def E]

The expression $R\left( {E/x}\right)$ is usually described as "the predicate $R$ in which each occurrence of the variable $x$ is replaced by $E$ ". We shall define it by

[ R (E / x) \equiv R (x ^ {\prime} / x) (E / x ^ {\prime}) ]

where $R\left( {{x}^{\prime }/x}\right)$ is a predicate defined on the same space as $R$ ,except that the coordinate $x$ has been renamed ${x}^{\prime }$ - the name of a "fresh variable".

R (x ^ {\prime} / x) = (A x: x ≠ x ^ {\prime} \vee R)

and $Q\left( {E/{x}^{\prime }}\right) = \left( {\underline{A}{x}^{\prime } : {x}^{\prime } ≠ E \vee G}\right)$

Combining all this, we find

[ R (E / x) \equiv (\underline {{A}} x ^ {\prime}: x ^ {\prime} ≠ E \vee (\underline {{A}} x: x ≠ x ^ {\prime} \vee R)) ]

Remark. The temporary shift to a predicate in which $x$ has been renamed $x'$ is necessary because $E$ might depend on $x$ . (End of Remark.)

Since in our usage of $R\left( {E/x}\right)$ -also denoted by ${R}_{E}^{x}$ - it is either preFixed by "def E cand" or by "def E cor" the value of ${x}^{\prime } ≠ E$ is irrelevant where def E coincides with false.

Since $\left\lbrack {\text{true}\left( {E/x}\right) \equiv \text{true}}\right\rbrack$ and $\left\lbrack {\text{false}\left( {E/x}\right) \equiv \text{false}}\right\rbrack$ , Theorems 0 and 1 are also valid for the assignment

statement. In order to prove Theorem 2 , we observe for any Z and R

\begin{array}{l} [ Z \equiv w l p (x := E, R) ∧ w p (x := E, f r u e) ] \ = {\mathrm {d e f i n i t i o n o f s e m a n t h i c s o f} x := E } \ [ 2 \equiv (¬ d e f E c o r R (E / x)) \wedge (d e f E c a n d t r u e (E / x)) ] \ = {\mathrm {s i n c e} [ \mathrm {t r u e} (\overline {{E}} / x) \equiv \mathrm {t r u e} ] \mathrm {a n d p r e d . c a l c .} } \ [ Z \equiv (¬ d e f E \equiv R (E / x)) ∧ d e f E) \ = {\mathrm {p r e d . c a l c} } \ [ Z ^ {\prime} \equiv d e p E c a n d R (E / x) ] \ \end{array}

In order to prove Theorem 4, we have to show that for any $E$ and any bag of predicates $B$

\begin{array}{l} [ ¬ d e f E \underline {{c o r}} (\underline {{A P}}; P _ {\underline {{i n}}} B; P) (E / x) \equiv \ (\underline {{A P}}; \overline {{P}} _ {\ln} \overline {{B}}; 7 d e f E \underline {{c o r}} P (E / x)) ] \ \end{array}

Omitting the range $B$ ,we observe for any $Z$

\begin{array}{l} [ Z \equiv (\mathrm {A P}:: ¬ def E \mathrm {c o r} P (E / x)) ] \ = {\mathrm {p r e d . c a l c} } \ [ Z \equiv ¬ d e f E c o r (A P: P (E X)) ] \ = {\mathrm {d e p i n i t i o n o f} P (E / x) } \ [ Z \equiv - 7 def E \underline {{\mathrm {c o r}}} (\underline {{A}} P: ((\underline {{A}} x ^ {\prime}: x ^ {\prime} ≠ E) (E x: x ≠ x ^ {\prime} \vee P))) ] \ = {\mathrm {p r e d . c a l c . , v i z i n t e r c h a n g i n g o p u n i v e r s a l q u a n t i f i c a t i o n s} } \ = {\mathrm {p r e d . c a l c . , s i n c e} x ^ {\prime} ≠ E \mathrm {d o e s n o t d e p e n d o n d u m m y P} } \ [ 2 \equiv - def E \underline {{\operatorname {c o r}}} (\underline {{A}} x ^ {\prime}:: x ^ {\prime} ≠ E \vee (\underline {{A}} P: (\underline {{A}} x: x ≠ x ^ {\prime} \vee P)) ] \ = {\mathrm {t w o s i m i l a r s t e p s c o m b i n e d i n t o} \mathrm {c m e} } \ [ 2 \equiv - def E \underline {{\underline {{c o r}}}} (\underline {{A}} x ^ {\prime}: x ^ {\prime} ≠ E v (\underline {{A}} x: x ≠ x ^ {\prime} v (\underline {{A}} P: P))) ] \ = {\mathrm {d e f i n i t i o n} \overline {{P}} (A P: P) (E / x) } \ [ Z \equiv ¬ \operatorname {d e f} E \underline {{\operatorname {c o r}}} (A P: P) (E / x) ] \ \end{array}

This ends the proof of Theorem 4. (In including

Concatenation is simple. The semantics of So; St is defined in terms of that of So and St by

\begin{array}{l} [ w p (^ {\prime \prime} S _ {0}; S _ {1}, R) \equiv w p (S _ {0}, w p (S _ {1}, R)) ] f o r a n y R \ [ w l p (S _ {0}, S _ {1}, R) \equiv w l p (S _ {0}, w l p (S _ {1}, R)) ] f o r a n y R \ \end{array}

The right-hand sides have the form of functional composition, say foof R and goog1 R respectively. From the validity of Theorems 0 through 4 for the f's and the g's we have to derive the validity for their functional compositions. Since - see EWD835-23 - Functional composition is fixed point preserving, Theorems O and 1 are valid for the concatenation; since functional composition preserves the common degree of conjunctivity of the components, also Theorems 3 and 4 are valid for the concatenation. For Theorem 2 we have to do some work: for any Z and any R we observe

\begin{array}{l} [ Z \equiv p _ {0} \circ p _ {1} R ] \ = {\mathrm {d e f i n i t i o n o f f u n c t i o n a l c o m p o s i t i o n} } [ z \equiv p _ {0} (p _ {1} R) ] \ = {\mathrm {T h e o r e m 2 v a l i d f o r} p _ {1}, g _ {1} } [ Z \equiv f _ {0} (g _ {1} R \wedge f _ {1} ^ {\prime} t r u e) ] \ = {f _ {0} \mathrm {i s c o n j u n c t i v e} } [ 2 \equiv f _ {0} (g _ {1} R) \wedge f _ {0} (f _ {1} \mathrm {t r u e}) ] \ = {\mathrm {T h e o r e m 2 v a l i d f o r} p _ {0}, g _ {0} } [ z \equiv g _ {0} (g _ {1} R) \wedge f _ {0} \mathrm {t r u e} \wedge f _ {0} \ = {\rho_ {0} \mathrm {i s c o n j u n c t i v e} } [ 2 \equiv g _ {0} (g _ {1} R) \wedge f _ {0} (f _ {1} \mathrm {t r u e}) ] \ = {\mathrm {d e f i n i t i o n} \mathrm {f o r n c t i o n a l c o m p o s i t i o n} } [ 2 \equiv g 0 \cdot g 1 \Rsh \wedge {0 \cdot f 1 \mathrm {t r u e} } \ \end{array}

Next the alternative statement. For brevily's sake we use the "as guarded command set former". Let, as usual, IF denote if (i: Bi → Si) and let BB be given by [BB = (Ei:: Bi)].

The semantics of IF is given by

\begin{array}{l} [ w p (I F, R) \equiv B B \wedge (\underline {{A}} i: ¬ B i \vee w p (S i, R)) ] \ [ w l p (I F, R) \equiv (\underline {{A}} i: ¬ B i \vee w l p (S i, R)) ] \ \end{array}

Again we have to prove Theorems 0 through 4 for IF, assuming they hold for all the Si.

To prove Theorem 0, we observe for any $Z$

\begin{array}{l} [ Z \equiv w p (I F, f a l s e) ] \ = {d e f i n i t i o n o f s e m a n t i c s } \ [ 2 \equiv B B \wedge (A i: ¬ B i \vee w p (S i, f a l s e)) ] \ = {\mathrm {T h e o r e m} 0 \mathrm {h o l d s f o r a l l S i} } \ [ 2 \equiv B B \wedge (A C: ¬ B C) ] \ = {\mathrm {d e f i n i t i o n} B B \mathrm {a n d} \mathrm {d e M o r g a n} } \ [ 2 \equiv f a l s e ]. \ \end{array}

We don't need to prove Theorem 1 , since it follows from Theorem 4 . the universal conjunctivity. To prove Theorem 4 , we formulate two little lemmata.

Lemma For any universally conjunctive $f$ and predicate $Q$ ,predicate $g$ ,defined by $\left\lbrack {gX \equiv Q \vee {f}^{\prime }X}\right\rbrack$ for any $X$ ,is universally conjunctive.

This is proved by observing for any bag C

\begin{array}{l} [ Z \equiv g (\underline {{A}} P: P _ {\underline {{i n}}} C: P) ] \ = {\mathrm {d e f i n i t i o n} o f g _ {3} \ [ Z \equiv Q \vee f (\underline {{A P}}: P _ {\ln C}: P) ] \ = {f \mathrm {i s u n i v e r s a l l y c o n j u n c t i v e} } \ \end{array}

\begin{array}{l} [ Z \equiv Q \vee (\underline {{A P}}: P _ {\mathrm {i n}} C: f P) ] \ = {\mathrm {p r e d . c a l c} } [ 2 \equiv (\mathrm {A P}: P _ {\mathrm {i n}} C: Q \vee f P) ] \ = {\mathrm {d e f i n i t i o n o f} g } [ Z \equiv (\underline {{A P}}: P _ {\mathrm {i n}} C: g P) ] \ \end{array}

Lemma For a bag of universally conjunctive $f_i$ , is universally conjunctive.

This is proved by observing for any bag C

\begin{array}{l} [ 2 \equiv g (\underline {{A}} P: P _ {\underline {{i n}}} C: P) ] \ = \left{ \begin{array}{l} \text {d e f i n i t i o n o f g} \ [ 2 ] Z \equiv (A _ {i}: f _ {i} (\underline {{A P}}; P _ {\mathrm {i n}} C; P)) ] \end{array} \right. \ = {\underline {{F _ {i}}} \mathrm {a r e u n i v e r s a l l y c o n j u n c h i v e} } [ Z \equiv (\underline {{A}} _ {i}: (\underline {{A}} _ {P}: \underline {{P}} _ {\mathrm {i n}} C: F _ {i} P)) ] \ = {\mathrm {i n t e r c h a n g e o f u n i v e r s a l q u a n t i f i c a t i o n s} } [ 2 \equiv (\underline {{A P}}: \underline {{P}} _ {\mathrm {i n}} C: (\underline {{A C}}: \underline {{f c}} P)) ] \ = {d e f i n i t i o n o f g } [ 2 \equiv (\underline {{A P}}: \underline {{P i n C}}: g P) ] \ \end{array}

From these two lemmata it follows immediately that IF is universally conjunctive.

To prove Theorem 2, we observe for any $R$ and $Z$

\begin{array}{l} [ 2 \equiv w p (I F, R) \wedge w p (I F, t r u e) ] \ \begin{array}{r l} & {= {\mathrm {d e f i n i t i o n o f s e m a n t i c s} }} \ & {[ 2 \equiv (\underset {\sim} {A} \mathrm {c : :} ¬ \underset {\sim} {B} \mathrm {c : :} \vee w p (\underset {\sim} {S} \mathrm {c}, R)) \wedge} \ & { B \overline {{B}} \wedge (\underset {\sim} {A} \mathrm {c : :} ¬ \underset {\sim} {B} \mathrm {c : :} \vee w p (\underset {\sim} {S} \mathrm {c}, \mathrm {t r u e})) ]} \end{array} \ = {\mathrm {p r e d . c a l c} } \ = {\mathrm {T h e o r e m 2 v a l i d f o r a l l} S i: } [ Z \equiv B B ∧ (\underline {{A}} c: ¬ B i \lor w p (S i, R)) \ \end{array}

= {\mathrm {d e f i n i t i o n o f s e m a n t i c s} } [ Z \equiv w p (I F, R) ].

So far our proofs have mostly been very boring. They were also effective. But the element of surprise was usually lacking.

To prepare the road for our treatment of repetition we shall first prove our version of the

Theorem of Knaster-Tarshi. For monotonic f the equations $X : \left\lbrack {pX ⇒ X}\right\rbrack$ and $X : \left\lbrack {pX \equiv X}\right\rbrack$ have the same strongest solution Q given by $\left\lbrack {Q \equiv \left( {\underline{A}X : \left\lbrack {pX \equiv X}\right\rbrack : X}\right) }\right\rbrack$

Corollary. For monotonic $f,x : \left\lbrack {f\left( x \right) ⇒ X}\right\rbrack$ and

Proof of Theorem of Knaster-Tarski.

\begin{array}{l} f r u e \ = {\mathrm {d e f i n i t i o n} Q } \ [ Q \equiv (\underline {{A}} X: [ f X ⇒ X ]: X) ] \ ⇒ {\mathrm {p r e d . c a l c} } \ [ Q ⇒ (¬ X; [ P X ⇒ X ]; X) ] \ = {\mathrm {p r e d . c a l c .} } \ [ (\theta X: [ \phi X ⇒ X ]: Q ⇒ X) ] \ = {p r e d, c a l c. } \ (\underset {\sim} {A} X: [ f X ⇒ X ]: [ Q ⇒ X ]) \ ⇒ {f i s m o n o t o n i c } \ (\exists x: [ f x ⇒ x ]: [ f q ⇒ f x ]) \ = {\mathrm {p r e d . c a l c .} } \ [ f ^ {\prime} Q ⇒ (A X: [ P X ⇒ X ]: f X) ] \ ⇒ {\mathrm {p r e d . c a l c .} } \ \end{array}

\begin{array}{l} [ P Q ⇒ (A X: [ F X ⇒ X ]: X) ] \ = {\mathrm {d e f i n i t i o n} _ {f}, Q } \ [ p Q ⇒ Q ] \ \end{array}

Now it has been established that $Q$ is a solution of $X: [fX ⇒ X]$ , whereas the line * states that it is as strong as any solution; hence $Q$ is the strongest solution of $X: [fX ⇒ X]$ .

We confrinue

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

Hence $[fQ\equiv Q]$

(End of Proof of Theorem of Knaster-Tarski)

Though the steps in the above proof are as simple as those in our earlier proofs, this one is not boring; on the contrary, it is surprising to see what we can prove about $f^{\circ}$ when, firstly, we remember how $Q$ has been defined and, secondly, we realize that for $f$ no conjunctivity of any form has been assumed. The Theorem of Knaster-Tarski clearly captures something nontrivial. It is also worth noting that, again, we see fixed points emerging.

Another theorem that only requires monotonicity of $f$ is the

Limb Theorem. For monotonic $f$ and $P$ any solution of $X: [fX \equiv X]$ or of $X: [fX \equiv X]$ ,

Here the exponent indicates iterated functional composition, more precisely

[ p ^ {\circ} X \equiv X ] f o r a n y X

[ f ^ {i + 1} X \equiv f _ {0} f ^ {i} X ] \mathrm {f o r a n y} X

\mathrm {C o r} [ f ^ {i + 1} X \equiv f (f ^ {i} X) ] \mathrm {F o r a n g l y} X).

Proof of the limit Theorem. Since any solution X: [fX ≡ X] is also a solution of X: [fX ≡ X], it suffices to prove the theorem for a solution P of the latter equation.

We observe firstly

true

\begin{array}{l} = {\text {p r e d i c a t e c a l c u l u s} } \ = \left{ \begin{array}{l l} d e f i n i t i o n o f l i t e r a t e d f u n c t h i o n a l c o m p o s i t i o n \ [ 7 ] f ^ {0} f a l s e v P ] \end{array} \right} \ \end{array}

a n d s e c o n d l y

\begin{array}{l} [ ¬ f ^ {i} \mathrm {f a l s e} v P ] \ ⇒ {f ^ {i} \mathrm {i s m o n o t o n i c} } \ = {\mathrm {d e f i n i t i o n o f i t e r a t e d f u n c h o n a l c o m p o s i t i o n} } \ ⇒ \left{ \begin{array}{l} P ^ {\prime} i s a s o l u t i o n ^ {\prime} o f X: [ f X ⇒ X ] \end{array} \right} \ \end{array}

Hence

true

\begin{array}{l} = {\mathrm {m a t h e m a t h i c a l} \mathrm {i n d u c t i o n} } (A: i: i \ge 0: [ - P ^ {i} \mathrm {f a l s e} v P ]) \ = {\text {p r e d . c a l c .} } [ (\underline {{A}}: \dot {c}: \dot {c} ≥ 0: ¬ P ^ {c} \mathrm {p a i s e} V P) ] \ = {\text {p r e d , c a l c} } [ (¬ A: C ≥ 0: ? P ^ {c} F ^ {\prime} s e) v P ] \ = {\mathrm {p r e d . c a l c} } [ (\mathrm {E} i: i \ge 0: f ^ {(p a s s)} ⇒ P ]. \ \end{array}

(E n d o f P r o o f o f l i m i t T h e o r e m.)

For the sake of brevity we observe that we can write the statement IF with a number of alternatives if (i): Bi→ Si) ii also as

i f B B \rightarrow I F f _ {i}

i.e. an alternative construct with in the first instance only 1 guarded command. Similarly, the repetitive construct do (I c:: Bi→ Si) od can be written as

\underline {{d o}} \colon B B \to I F \underline {{o d}}

The above observation is exploited to study the repetition

D O: \underline {{d o}} B \rightarrow S \underline {{o d}}

in relation to the corresponding

I F: I F B \rightarrow S P C

The generalization to the general repetition with more guarded commands is left to the reader.

We take the position that the semantics of DO is not changed by unfolding it once, i.e. is equivalent to that of

D O ^ {\prime}: i f B \rightarrow S; D O ∥ ¬ B \rightarrow s h i p F i

In other words, we require

[ w p (D O, R) \equiv w p (D O ^ {\prime}, R) ] f o r a l l R, a n d

[ w l p (D O, R) \equiv w l p (D O ^ {\prime}, R) ] f o r a l l R

i.e. ${wp}\left( {{DO},R}\right)$ is a solution of $X : \left\lbrack {X = fX}\right\rbrack$ with

[ f X \equiv (¬ B \vee w p (S, X)) \wedge (B \vee R) ]

and $\operatorname{wlp}\left( {{DO},R}\right)$ is a solution of $X : \left\lbrack {X \equiv hX}\right\rbrack$ with

[ n X \equiv (¬ B \vee w p (S, X)) \wedge (B \vee R) ]

Since we have for any $B, P,$ and $Q$

[ (¬ B \lor P) ∧ (B \lor Q) \equiv (B ∧ P) \lor (¬ B ∧ Q) ] ,

we could also have defined

\begin{array}{l} [ f X \equiv (B \wedge w p (S, X)) \vee (¬ B \wedge R) ] f o r a l l X \ [ h X \equiv (B \wedge w l p (S, X)) \vee (¬ B \wedge R) ] f o r a l l X. \ \end{array}

We now define $w p(D O, R)$ as the strongest solution of $X: [X \equiv f X]$ and $w p(D O, R)$ as the weakest solution of $X: [X \equiv h X]$ .

Remembering that Theorem 2 states in this case

[ w p (D O, R) \equiv w l p (D O, R) \wedge w p (D O, t r u e) ],

we see that we also need to consider the strongest solution of $X : \left\lbrack {X \equiv gX}\right\rbrack$ with $g$ defined by

[ g X \equiv (B \wedge w p (S, X)) \vee ¬ B ]

in short, we have to establish a relation between extreme solutions of three different equations.

In order to cope with that problem we devise a notation in which we strictly separate what these equations have in common from where they differ. Since we study the equations with an S satisfying Theorem 2, we may replace $wp(S,X)$ in $f$ and $g$ by $wlp(S,X) ∧ wlp(S,\text{true})$ , or, since the last term is a constant predicate for fixed $S$ , by $wlp(S,X) ∧ K$ . Our notation introduces a predicate transformer $c$ which operates on three arguments instead of the usual one; it is defined by

\begin{array}{l} [ c X Y Z \equiv (B \wedge w l p (S, X) \wedge Y) \vee (T B \wedge Z) ] \ f o r a l l X, Y, a n d Z \ \end{array}

In terms of $c$ ,the equations $X : \left\lbrack {X \equiv fX}\right\rbrack$ ,

\begin{array}{l} X: [ X \equiv c X K R ] \ X: [ X \equiv c X K t r u e ] \ X: [ X \equiv c X \mathrm {f r u e} R ] \ \end{array}

There is hope because $c$ is multiply conjunctive,

i.e. $\left\lbrack {c\left( {X ∧ {X}^{\prime }}\right) \left( {Y ∧ {Y}^{\prime }}\right) \left( {Z ∧ {Z}^{\prime }}\right) \equiv }\right\rbrack$

(c \times Y Z) \wedge (c X ^ {\prime} Y ^ {\prime} Z ^ {\prime}) ]

for any predicates $X,{X}^{\prime },Y,{Y}^{\prime },Z$ ,and ${Z}^{\prime }$ .

Proof. The proof depends primarily on the special structure of $c$ and the general formula from predicate calculus

\begin{array}{l} [ (B ∧ P ∧ P ^ {\prime}) \lor (¬ B ∧ Q ∧ Q ^ {\prime}) ] = \ ((B ∧ P) \lor (¬ B ∧ Q)) ∧ ((B ∧ P ^ {\prime}) \lor (¬ B ∧ Q ^ {\prime})) ] \ \end{array}

which is most readily proved by substituting for $B$ ,true and false reprechtively (the latter substitution being superfluous on account of symmetry considerations)

Foreachany $H$ ,etc.

\begin{array}{l} [ H \equiv (c X Y Z) \wedge (c X ^ {\prime} Y ^ {\prime} Z ^ {\prime}) ] \ = {\mathrm {d e f i n i t i o n o f} c } \ [ H \equiv ((B ∧ w) | _ {p} (S, X) ∧ Y) \lor (¬ B ∧ Z)) ∧ \ ((B ∧ w l p (S, X ^ {\prime}) ∧ Y ^ {\prime}) v _ {2} (¬ B ∧ Z ^ {\prime})) ] \ = {p r e d i c a t e c a l c u l u s, s e e a b o v e } \ [ H \equiv (B \wedge w l p (S, X) \wedge w l p (S, X ^ {\prime}) \wedge Y \wedge Y ^ {\prime}) V \ (¬ B ∧ Z ^ {\prime} ∧ Z ^ {\prime}) ] \ = {\mathrm {c o n j u n c t i v i t y} \mathrm {o f} w | p } \ {H \equiv (\mathcal {B} \wedge w l p (S, X \wedge X ^ {\prime}) \wedge (Y \wedge Y ^ {\prime})) v \ (¬ B ∧ (¬ Z ∧ Z ^ {\prime})) ] \ = {\mathrm {d e f i n i t i o n} o f _ {1}, c } \ [ H \equiv c (X \wedge X ^ {\prime}) (Y \wedge Y ^ {\prime}) (Z \wedge Z ^ {\prime}) ] \ \end{array}

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

A pleasant consequence of c's multiple conjunctivty is the. Multiple Conjunctivty Lemma 0. With $P$ a solution of $X: \left\lbrack {X \equiv c \times Y{Y}^{\prime }Z}\right\rbrack$ and ${P}^{\prime }$ one of $X : {\left\lbrack X \equiv c \times {Y}^{\prime }{Z}^{\prime }\right\rbrack }^{2}$ ${P}^{\Lambda }{P}^{\prime }$ is a solution of $X : {\left\lbrack X \equiv c \times {\left( Y ∧ {Y}^{\prime }\right) }^{2}\left( Z ∧ {Z}^{\prime }\right) \right\rbrack }$ .

Proof. true ( = { \text{definitions of } P and P' } \left[ P \equiv cP'YZ \right] ∧ \left[ P' \equiv cP'Y'Z' \right] ) ( ⇒ ) {predicate calculus} [ P ∧ P' \equiv cP'YZ ∧ cP'Y'Z' ] ( = { c ) is multiply conjunctive ( } \left[ P ∧ P' \equiv c(P ∧ P')(Y ∧ Y')(Z ∧ Z') \right] ] (End of Proof)

Before proceeding it is correct to establish that our definitions of $\mathfrak{wp}$ and $\mathfrak{wlp}$ make sense, i.e. that weakest and strongest solutions of $X: [X \equiv cX Y Z]$ exist for any $Y$ and $Z$ . Because $c$ is multiply conjunctive, it is conjunctive, and hence monotonic, in its first argument. The strongest solution exists on account of Knaster-Tarski as formulated, the weakest solution exists on account of its equivalent formulation

Theorem of Knaster-Tarshi. For monotonic ${f}^{ * }$ the equations $Y : \left\lbrack {Y ⇒ {f}^{ * }Y}\right\rbrack$ and $Y : \left\lbrack {Y \equiv {f}^{ * }Y}\right\rbrack$ have the same weakest solution $R$ given by $\left\lbrack {R \equiv \left( {{EY} : \left\lbrack {Y \equiv {f}^{ * }Y}\right\rbrack : Y}\right\rbrack }\right.$

Sketch of Proof. Relating firstly $f$ and ${f}^{ * }$ by

-i.e. $f$ and $f^x$ are each other's so-called conjugate-one establishes first

(f _ {i s m o n o t o n i c}) \equiv (f ^ {*} _ {i s m o n o t o n i c})

Relating furthermore $\left\lbrack {¬ X \equiv Y}\right\rbrack$ and $\left\lbrack {¬ Q \equiv R}\right\rbrack$ , one can transform the one formulation into the other. (End of Sketch of Proof)

Having established the existence of the extreme solutions, we show two further lemmata about them (since we shall need them in the near future).

Multiple Conjunctivity Lemma 1

For multiply conjunctive C P the weakest solution of X: [X ≡ cXYZ], P' the weakest solution of X: [X ≡ cXY'Z'] H the weakest solution of X: [X ≡ cX (Y ∧ Y') (Z ∧ Z')] we have [H ≡ P ∧ P']

Proof. Multiple Conjunctivity Lemma 0 tells us that $\overline{P ∧ P'}$ is a solution of the equation of which $H$ is the weakest solution, hence $[P ∧ P' ⇒ H]$ .

In order to show $\left\lbrack {H ⇒ P ∧ {P}^{\prime }}\right\rbrack$ ,we show $\left\lbrack {H ⇒ P}\right\rbrack ∧ \left\lbrack {H ⇒ {P}^{\prime }}\right\rbrack$ . To show $\left\lbrack {H ⇒ P}\right\rbrack$ ,we show that $H$ is a solution of $X : \left\lbrack {X ⇒ c \times YZ}\right\rbrack$ ,of which $P$ is the weakest solution.

\begin{array}{l} \mathrm {t r u e} \ = {\mathrm {d e f i n i t i o n o f} H } \ [ H \equiv c H (Y \wedge Y ^ {\prime}) (Z \wedge Z ^ {\prime}) ] \end{array}

$⇒ {$ being multiply conjunctive, $c$ is a monotonic function $}$ $\left\lbrack {H ⇒ c \mid Y \mid Z}\right\rbrack$ , whence $\left\lbrack {H ⇒ P}\right\rbrack ;\left\lbrack {H ⇒ P}\right\rbrack$ similarly. (End of Proof)

Remark The above Lemma 1 also holds for multiply conjunctive C with 2 or more than 3 arguments. (End of Remark.)

Multiple Conjunctivity Lemma 2 For doubly conjunct

P the strongest solution of $X : \left\lbrack {X \equiv b \times R}\right\rbrack$ , Q any solution of $X : \left\lbrack {X \equiv b \times R}\right\rbrack ,$ and H the strongest solution of $X : \left\lbrack {X \equiv b \times \text{true}}\right\rbrack$ ,

we have $\left\lbrack {\widetilde{P} \equiv Q ∧ H}\right\rbrack$ .

Proof. We first show $[P ⇒ Q ∧ H]$ by demonstrating that $Q ∧ H$ satisfies the equation of which $P$ is the strongest solution. We have for

\begin{array}{l} a n y z \ [ Z \equiv b (Q \wedge H) R ] \ = {b i s m u l t i p l y c o n j u n c t i v e } [ 2 \equiv b Q R \wedge b H t r u e ] \ = {\mathrm {d e f i n i t i o n s o f} Q \mathrm {a n d} H } [ Z \equiv Q ∧ H ] \ \end{array}

Hence $\left\lbrack {P ⇒ Q ∧ H}\right\rbrack$ . We now show $\left\lbrack {Q ∧ H ⇒ P}\right\rbrack$ ,

i.e. $\left\lbrack {H ⇒ {7Q} \vee P}\right\rbrack$ by demonstrating that ${7Q} \vee P$

satisfies $X$ : $\left\lbrack {b \times \text{true} ⇒ X}\right\rbrack$ of which-knaster-Tarski-

H is the strongest solution: true

\begin{array}{l} = \left{ \begin{array}{l} \mathrm {t r i v i a l l y} \ b (P ∧ Q) R \equiv b (P ∧ Q) R \end{array} \right. \ = {p r e d i c a t e c a l c u l u s } [ b ((P v ¬ Q) ∧ Q) R \equiv b (P ∧ Q) R ] \ ⇒ {b \mathrm {i s d o u b l y c o n j u n c h i v e a n d m o n o t o n i c} } [ b (P v 7 Q) \mathrm {t r u e} ∧ b Q R ⇒ b P R ] \ = {\mathrm {d e f i n i t i o n s} \mathrm {o f} P \mathrm {a n d} Q } [ b (P v ¬ Q) \mathrm {t r u e} ∧ Q ⇒ P ] \ = {p r e d i c a t e c a l c u l u s } [ b (P v ¬ Q) \mathrm {t r u e} ⇒ P v ¬ Q ] \ \end{array}

(End of Proof.)

And now we are ready to prove that, provided Theorem 2 holds for $S$ , it holds for $DO$ . For any $Z$ , etc.

[ Z \equiv w p (D O, R) ]

= {\mathrm {d e f i n i t i o n o f} w p }

[ Z \equiv (\mathrm {s t r o n g e s t} \mathrm {s o l u t i o n o f} X: [ X \equiv c X K R ]) ]

= {\mathrm {L e m m a} 2 \mathrm {a p p l i e d w i t h}" \mathrm {w e a k e s t}" f o r " a n y " };

c \mathrm {i s d o u b l y} ^ {\prime} \mathrm {c o n j u n c t i v e} \mathrm {i n t h e p a i r} ^ {\prime} X R }

[ Z \equiv (\mathrm {w e a k e s t} ^ {\prime} \mathrm {s o l u t i o n o f} X: [ X \equiv c X K R ]) ∧

(s t r o n g e s t s o l u t i o n o f x: [ x \equiv c \times k \mathrm {t r u e} ]) ]

= {\mathrm {L e m m a} 1 }

[ Z \equiv (\mathrm {w e a k e s t} \mathrm {s o l u t i o n o f} X: [ X \equiv c X \mathrm {t r u e} R ]) ∧

(\mathrm {w e a k e s t} \mathrm {s o l u t i o n o f} X: [ X \equiv c X K \mathrm {t r u e} ]) ∧

(\mathrm {s t r o n g e s t} \mathrm {s o l u t i o n o p X: [ X \equiv c X K t r u e ]}) ]

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

[ Z \equiv (\mathrm {w e a k e s t} \mathrm {s o l u t i o n o f} X: [ X \equiv c X \mathrm {t r u e} R ]) ∧

(\mathrm {s t r o n g e s t} \mathrm {s o l u t i o n} \mathrm {o f} X: [ X \equiv c \times K \mathrm {t r u e} ]) ]

= {\mathrm {d e f i n i t i o n s} \mathrm {o f} w p \mathrm {a n d} w l p }

[ z \equiv w p (D O, R) \wedge w p (D O, t r u e) ]

Thus Theorem 2 has been proved for DO

Theorem 0 follows for DO from the fact that if Theorem 0 holds for $s$ [false $\equiv$ c false K false] i.e. false is the strongest solution of X: [X=cXX false].

Finally we have to show the validity of Theorem 4, i.e. that wlp (D0,?) is universally conjunctive if wlp (S,?) is. We shall not prove that here. We should have observed 4 pages ago that c is multiply universally conjunctive and lemmata 0 and 1 should have been generalized from 2 (primed and unprimed) to any bag. The generalization is straightforward.

Concluding Remarks.

These draft lecture notes are now concluded, not because all theory developed in the preceding eight months has been presented, but because the semester draws to a close and - together with, say, EWD830 and EWD844- I think we have collected enough material for our secondary target, viz. the discovery how to use the predicate calculus effectively.

After I had lectured for a few weeks, J.T. Udding suggested a generalization of one of my notational conventions which I have not adopted since one of my purposes was to experiment with the conventions I had chosen. The result of the experiment is that Udding's suggestion is, indeed, an improvement, and that I shall adopt it.

On p. EWD835-8 I have proposed to render the computation via an intermediate predicate $R$ that $P \equiv Q$ has the value true - coincides with true - as follows

\begin{array}{l} = \left{ \begin{array}{l l} P \ R \end{array} \right. \mathrm {h i n t w h y} P \equiv R \mathrm {h a s t h e v a l u e t r u e} \ = {\mathrm {h i n t w h y} R \equiv Q \mathrm {h a s t h e v a l u e t r u e} } \ \end{array}

and I have religiously adhered to the constraint that in such proofs $P, Q$ and $R$ were predicates on the trivial space. In that case $P \equiv 0, P \equiv 1,$ and $R \equiv 0, R \equiv 1$ are predicates on the trivial space as well, and without change of meaning we could have written:

\begin{array}{l} = \left{ \begin{array}{l} P \ R \end{array} \right. \ = {h i n t w h y [ R \equiv Q ] } \ \end{array}

as structure of a computation of the truth of $\left\lbrack {P \equiv Q}\right\rbrack$ . But in the latter interpretation there is no need anymore for $P,Q$ ,and $R$ to be elementary predicates. Removing that constraint does away with the need for the "dummy" as in

\begin{array}{l} [ Z \equiv P ] \ = \left{ \begin{array}{l l} h i n t w h y & [ P \equiv R ] \ [ Z \equiv R ] \end{array} \right} \ = \left{ \begin{array}{l l} h i n t w h y & [ R \equiv 0 ] \rbrace \ [ 2 \equiv 0 ] \end{array} \right. \ \end{array}

for any $z$ .

We had lots of such proofs in which we observed such equivalences "for any $z$ ". Udding's sugesis tion eliminates the need for such a dummy. In the case of a proof of $\left\lbrack {P ⇒ Q}\right\rbrack$ the improvement is even more marked.

EWD844 is a definite improvement compared to this draft's introduction of universal quanti-

Nomenclature. In (AX: X in B; FX) I need a name for "fX"; I propose "the term". I also need a name for B ; I propose to call it "the range" over which the term is quantified. (End of Nomenclature.)

In connection with EWD842 I have replaced

during a number of lectures the phrasing "has the value true" by "coincides with black". The intro. duction of the verb "to coincide" and of the identi- fier "black" were both experienced as an improve- ment. The verb "to coincide" can be introduced noise- lessly, just by using it; abolishing "true" by re- placing it by "black" will cause a greater shock . In my current estimation the latter change of terminology is the more essential one.

Re EWD842 and EWD843 the following remarks. In EWD842 I have omitted to state that when P.Q. and R stand for predicate variables they may be systematically replaced by any predicate expression.

Furthermore, EwD843 has to be rewritten or to be made superfluous by rewriting EWD842 - The remark is the following. In the presence of a formula of the form

(P \equiv Q) \vee R

we may generate from $F$ the formula $F^{\prime}vR$ in which $F^{\prime}$ is obtained from $F$ by replacing in $F$ some (but not necessarily all) occurrences of $P$ by $\Theta$ . Unless I am profoundly mistaken, this does away with all the magic and philosophy associated with the turnstile. Dis-junction -and probably also equivalence- has in any case to be defined as well on a bag contain- ing a single argument.)

Finally one observation, the full significance of which I have not fathomed yet. Nowhere in EWD 835 have I used the fact that the space consists of points!

We can introduce them by postulating the existence of "elementary predicates" - denoted

Axiom 0: $\left\lbrack {\left( {E}_{P} : P\right) }\right\rbrack$

Axiom 1: $[p ⇒ Q] \equiv 7\left\lbrack {p ⇒ 7Q}\right\rbrack$ for any $Q$ .

In the theory developed so far we did not need those two axioms. For the time being I regard this as another indication that set theory does not deserve the primacy usually given to it.

The remark that "a space without points" is a bit hard to imagine is beside the point since "imagining" could very well be a habit not to be universally encouraged.

The elementary predicates -be it,by mistake,their complements- have been introduced in EwD830 that deals with termination in the light of unbounded non-determinacy (as announced op p. EwD835-15). The contents of EwD830 belong to this lecture course as well.

Plataansstaat 5

5671 AL NUENEN

The Netherlands

22 November 1982

prof. d. Edsger W. Dgksha

Burroughs Research Fellow