On the design of calculational proofs

On the design of calculational proofs

§ 0. By their brevity and unexpected turns, calcula- tional proofs often strike the reader as being very ingenious constructions. Far be it from us to be- little the ingenuity of their inventors, but that should not prevent us from studying a number of representative proofs in the hope of learning why those proofs have the structure they have. This paper reports on such a study.

Among the things that will emerge, I al- ready mention a few.

Firstly, many steps that may seem surprising at first sight, are, in fact, (almost) dictated, as they are the only (or by far the simplest) transformation that will enable us to exploit one of the givens that has to be taken into account. In this connection I recommend that we maintain as fine-grained a book-keeping as possible of what of the givens we have used: what has not been used yet often indicates the direction in which the proof should be completed

Secondly, when faced with an antisymmetric and reflexive relation, i.e. a relation $\leq$ (with transpose $\geq$ ) such that

$$ x = y \equiv x \leq y \land x \geq y \quad \mathrm {f o r a l l} x, y $$

we must be prepared for a proof with a possibly. subtle interplay between calculating with equal- ities and with inequalities: any hints we can extract as to when to stress which of the two approaches will obviously be most welcome.

$\S 1$ . Let me show you, as a first indication of the kind of considerations I would like to highlight, a calculational proof of which each step is forced (as a result of which the proof is very well known, not to say canonical).

given About predicate transformers

(0) $\left\lbrack {f \cdot x \Rightarrow y}\right\rbrack \equiv \left\lbrack {x \Rightarrow g \cdot y}\right\rbrack \quad \text{for all}x,y;$

we are asked to show that $g$ is universally conjunctive, i.e.

$\left\lbrack {g.1 < \forall y : y \in W : y}\right\rbrack \equiv \left\langle {\forall y : y \in W : g.y}\right\rangle$

for any bag $W$ of predicates.

Remark We indicate function application not impliciTY by juxtaposition but explicitly by an infix period of high syntactic binding power. With the square brackets we denote the "everywhere operator", a function from predicates" to the "boolean scalars" true and false . For further elaboration

we refer the reader for instance to [0]. (End of Remark.)

For brevity's sake, the range "yew" is omitted in the following calculation; we should remember that it is a scalar range. We shall first give the proof and then discuss it.

Proof We observe for any $x$

$$ \begin{array}{l} [ x \Rightarrow g. \langle \forall y: y \rangle ] \ = {(0) \mathrm {w i t h} y := \langle \forall y: y \rangle } \ [ f. x \Rightarrow \langle \forall y: y \rangle ] \ = {\mathrm {p r e d . c a l c .}: Q \Rightarrow \mathrm {o v e r} \forall } \ [ \langle \forall y: f. x \Rightarrow y \rangle ] \ = {\mathrm {p r e d . c a l c : i n t e r c h a n g e (N B . r a n g e i s s c a l a r)} } \ \langle \forall y: [ f. x \Rightarrow y ] \rangle \ = {0 } \ \langle \forall y: [ x \Rightarrow g \cdot y ] \rangle \ = {\text {p r e d . c a l c . : i n t e r c h a n g e (N B . r a n g e i s s c a l a r)} } \ \end{array} $$

$$ [ \langle \forall y: x \Rightarrow g. y \rangle ] $$

$$ \begin{array}{l} = {\mathrm {p r e d . c a l c .}: Q \Rightarrow \mathrm {o v e r} \forall } \ [ x \Rightarrow \langle \forall y: g. y \rangle ] \ \end{array} $$

$$ \begin{array}{l} h a v i n g t h u s e s t a b l i s h e d \ [ x \Rightarrow g. \langle \forall y: y \rangle ] = [ x \Rightarrow \langle \forall y: g. y \rangle ] \quad f o r a l l x, \ \end{array} $$

we conclude (1) on account of

(2) $\left\langle \forall x: \text { true: } [x \Rightarrow P] \equiv [x \Rightarrow Q] \right\rangle \equiv [P \equiv Q]$ ,

which is a well-known lemma that follows from implication's reflexivity and antisymmetry.

(End of Proof.)

Let us now analyse the extent to which the structure of the above proof has been forced upon us.

Firstly, do we need (0) in order to show (1)? Yes, we do, because (with $W \coloneqq \varnothing$ ) a consequence of (1) is [g true = true ], and that definitely does not hold for any $g$ , for instance not for the predicate transformer defined by [g.x = false] for all x.

Next, being obliged to use (0), we ob- serve that our only way of exploiting that the $g$ in the left-hand side $g.\langle \forall y::y\rangle$ of (1) satisfies (0), is to instantiate the latter by $y := \langle \forall y::y \rangle$ ; this forces us to explore $[x \Rightarrow g.\langle \forall y::y \rangle]$ , this now being the smallest expression that contains the left-hand side of (1) and can be rewritten using (0). The first step then applies (0) with that instantiation.

In view of the right-hand side of (1), it is from here on our duty to eliminate $f$ and to reintroduce $g$ , which can only

be done by a second appeal to (o). Because there is no point in undoing the first step, we must apply (o) to a subexpression of the form $\left\lbrack {f \cdot x \Rightarrow ?}\right\rbrack$ with a consequent different from $\langle \forall y : y\rangle$ . The next two steps of the predicate calculus form such a subexpression, and then our second appeal to (o) reintroduces $g$ .

Our final task is to form $\langle \forall y : g.y \rangle$ , the right-hand side of (1), as subexpression; the next two steps of the predicate calculus form $\langle \forall y : g.y \rangle$ as consequent, and, on account of (2), we are done.

The moral of the story is that, apart from the choice of syntax for proof presentation, we had no choice.

$\S 2$ . The full-blown principle of Leibniz states (to the best of my knowledge) that for $x$ and $y$ of some type, and $f$ ranging over the functions on that type

$$ (3) \quad x = y \equiv \langle \forall f: f. x = f. y \rangle $$

Reading the above equivalence as a mutual implication, we observe that " $\Leftarrow$ " follows by instantiating the right-hand side with for $f$ the identity. function. For this con-

clusion, even the existence of other functions is irrelevant. For the general function it is the implication in the other direction that is relevant:

$$ (4) \qquad x = y \Rightarrow f _ {x} = f _ {y} $$

and this is what is usually referred to as "Leibniz's Principle".

Remark Appealing to

$$ q \Rightarrow \langle \forall x:: x \rangle \equiv \langle \forall x:: q \Rightarrow x \rangle $$

itself an immediate consequence of " $\vee$ dis- tributes over $\forall$ ",we have taken the universal quantificaton over f outside. The possiblity of thus removing a universal quantificaton from a consequent often provides the incentive to split up an equivalence involving a univer- sally quantified equivalent into a mutual implication.(End of Remark.)

The connection between function application and equality is very tight: function ap- plication preserves equality and, conversely, - besides the two constant relations true and false - equality is the only relation that is preserved by function application. In Section 0 , we referred to the interplay between calculating with equalities and with

inequalities; the above observation tells us that when we have to capture the essence of function application, i.e. when we have to apply Leibniz's Principle, we may be forced to introduce an equality so as to be able to do so. The next section gives two examples of this phenomenon.

§3. In a wider context, Jamey Leifer had to deal with two functions $f$ and $g$ whose domains and ranges are all the same, and whose applications commute, i.e.

(5) $f \cdot \left( {g \cdot x}\right) = g \cdot \left( {f \cdot x}\right)$ for "all" $x$ .

In order to appeal to (5), we have to apply -say- g to an f-value, say f.x. In order to appeal to Leibniz's Principle, that f-value has to equal something else, say y ,for the time being. So we observe for any x,y

$$ \begin{array}{l} \Rightarrow \begin{array}{r l} & {f. x = y} \ & {{\mathrm {L e i b n i z ' s P r i n c i p l e} }} \end{array} \ = g \cdot \left{ \begin{array}{l} f \cdot x \ (5) \end{array} \right} = g \cdot y \ f. (g \cdot x) = g \cdot y \ \end{array} $$

The last line tells us that a nice choice for $y$ is $x$ ,and thus we have proved

$$ f _ {.} x = x \Rightarrow f _ {.} (g. x) = g. x $$

or, in words: if $x$ is a fixed point of $f$ , so is $g.x$ . After the above observation, Jamey Leifer conducted all the rest of his (beautiful) argument in terms of fixed points, a concept that did not occur at all in the theorem he had set out to prove.

§ 4. The other example I would like to show is the proof of Perry Moerland's lemma. (Also this came up in a wider context.) About predicate transformer f we are given that it is monotonic and has a left-inverse g , i.e.

(6) $\left\lbrack {x \Rightarrow y}\right\rbrack \Rightarrow \left\lbrack {f.x \Rightarrow f.y}\right\rbrack$ for all $x,y$ (7) $\left\lbrack {g.p.}\right\rbrack \equiv x\rbrack$ for all $x$ ;

we have to show that as a consequence

(8) $\left\lbrack x\right\rbrack \Leftarrow \left\lbrack {f \cdot x}\right\rbrack$ for all $x$ .

We are looking for a strengthening chain of booleans, starting at [x] and ending with [f.x]. Along the way we have to introduce $f$ ; for doing so, (6) is not a good candidate, but (7) is. The advantage of introducing $f$ with the aid of (7) is that then $g$ is introduced as

well. (Note that (6) by itself does not suffice for the demonstration of (8), i.e. that (7) has to be exploited, but that exploitation obviously requires that $g$ enters the picture.)

Having introduced $g$ and still aiming for $[f.x]$ , we have to get rid of $g$ again. Since the only other thing known about $g$ is that it is a function, the proper candidate for the removal of $g$ is Leibniz's Principle. Since an appeal to the latter requires equalities, the introduction of an equality was Perry Moerland's first concern; one observes for any $x$

$$ \begin{array}{l} [ x ] \ = \begin{array}{l} {{\mathrm {p r e d i c a t e c a l c u l u s} }} \ {[ x \equiv \mathrm {t r u e} ]} \end{array} \ = \left{ \begin{array}{l l} (7); (7) \mathrm {w i t h} x := \mathrm {t r u e} \end{array} \right} [ g. (f. x) \equiv g. (f. + \mathrm {t r u e}) ] \ \Leftrightarrow {L e i b n i z ^ {\prime} s P r i n c i p l e } [ f. x \equiv f. t r u e ] \ = \begin{array}{l} {{\mathrm {p r e d i c a t e c a l c u l u s} }} \ {[ f. x \Leftarrow f. t r u e ] \land [ f. x \Rightarrow f. t r u e ]} \end{array} \ = {[ x \Rightarrow \mathrm {t r u e} ] \mathrm {a n d (6) w i t h} y := \mathrm {t r u e} } [ f. x \Leftarrow f. \mathrm {t r u e} ] \ \Leftrightarrow \begin{array}{l} {{\mathrm {p r e d i c a t e c a l c u l u s} }} \ {[ p. x ]} \end{array} \ \end{array} $$

§5. With a relation like $\geq$ (and its trans-pose $\leq$ ) comes the notion of monotonicity with respect to it, i.e. "preserving it": "f is monotonic with respect to $\geq$ " means

$x \geq y \Rightarrow f \cdot x \geq f \cdot y$ for all $x,y$

(Note that in this terminology, Leibniz's Principle states that each function is "monotonic with respect to $=$ ".)

We now restrict ourselves to such domains and relations $\geq$ such that for any set of values the lowest higher bound "up" -and similarly the highest lower bound " $\downarrow$ " - exists, i.e. we assume that for any range of the dummy x and any function t of the appropriate type we can define (↑x:: t.x) by

(10) $w \geq \left\langle {4x\left( {{t}^{2} - x}\right) }\right\rangle \equiv \left\langle {\forall x\left( {{t}^{2} - x}\right) }\right\rangle$ for all $w$ .

The important theorem is that, for any $f$ that is monotonic with respect to $\geq$ ,

(11) $f \cdot \left\langle {4 \times \cdots t.x}\right\rangle \geq \left\langle {4 \times \cdots f.}\right\rangle \left( {6.x}\right)$

its proof is another example of "there is only one thing you can do".

Proof We observe for any monotonic $f$ , et.

$$ \begin{array}{l} f: \langle 4 x:: t. x \rangle \geqslant \langle 4 x:: f (t. x) \rangle \ = {1 0) w i t h w, t := f. \langle 4 x: t. x \rangle , f o t } \ \langle \forall x: f. \langle 4 x: t. x \rangle \geq f. (t. x) \rangle \ \Leftarrow {f m o n o t o n i c w i t h r e s p e c t t o \geq , \ \forall \mathrm {m o n o t o n i c w i t h r e s p e c t} \Rightarrow } \ \langle \forall x:: \langle 4 x:: t. x \rangle \geqslant t. x \rangle \ = {1 0) w i t h w := \langle 4 x: t. x \rangle } \ \langle \hat {4} x:: t. x \rangle \geqslant \langle \hat {4} x:: t. x \rangle \ = {\geq i s r e f l e x i v e } \ t r u e \ \end{array} $$

Note that (10), when viewed as mutual implication, is used in either direction.

(End of Proof.)

The above proof is so simple, and so completely forced by the definitions, that the usefulness of the theorem may come as a surprise. Predicate transformers that are monotonie with respect to implication are very common, and for such an $f$ ,which satisfies (6),we have

$$ \begin{array}{l} (1 2) [ f. \langle \forall x:: x \rangle \Rightarrow \langle \forall x:: f. x \rangle ] \qquad \mathrm {f o r a l l r a n g e s} \ (1 3) [ f. \langle \exists x:: x \rangle \Leftarrow \langle \exists x:: f. x \rangle ] \ \end{array} $$

with the special cases

$$ \begin{array}{l} (1 4) [ f. (x \wedge y) \Rightarrow f. x \wedge f. y ] \qquad \mathrm {f o r a l l} x, y \ (1 5) [ f. (x \vee y) \Leftarrow f. x \vee f. y ] \ \end{array} $$

In fact, (12) through (15) are more than useful consequences of $f$ ’s monotonicity, they are restatements of it.

[\text{5.6. In section 1 we proved -in our appeal to}]

(2) $- \left\lbrack {P \equiv Q}\right\rbrack \;{by}\;{showing}\;{for}\;{any}\;x$

$$ [ x \Rightarrow P ] \equiv [ x \Rightarrow Q ] $$

We may well ask what has been gained by the introduction of the dummy $x$ . A possi- sible answer is given by the observation that, in order to derive $\left\lbrack {P \equiv Q}\right\rbrack$ from the above,the latter has to be instantiated twice, viz. with $x \mathrel{\text{:=}} P$ and with $x \mathrel{\text{:=}} Q$ . This double instantiation strongly suggests that the the introduction of dummy $x$ has enabled us to avoid a ping-pong argument (i.e. a twofold case analysis).

But this is not the whole story, for, analogously to (2), we have, for instance,

(16) $\left\langle {\forall x : \left\lbrack {P \Rightarrow x}\right\rbrack \Leftarrow \left\lbrack {Q \Rightarrow x}\right\rbrack }\right\rangle \equiv \left\lbrack {P \Rightarrow Q}\right\rbrack$

This authorizes us to conclude $\left\lbrack {P \Rightarrow Q}\right\rbrack$ by showing for any

(17) $\left\lbrack {P \Rightarrow X}\right\rbrack \Leftarrow \left\lbrack {Q \Rightarrow X}\right\rbrack$

the conclusion, however, requires a single in-

tion of dummy x as in (17) is justifiable in more than one way. We can (i) prove (17) for arbitrary x, and then instantiate (17) with $x:= Q$ , or (ii) carry out the argument not for arbitrary x, but right from the start for $Q$ , thus deriving, instead of (17).

(18) $\left\lbrack {P \Rightarrow Q}\right\rbrack \Leftarrow \left\lbrack {Q \Leftarrow Q}\right\rbrack$

Here (i) is to be preferred above (ii) for more than one reason:

• the dummy x is shorter than the ex- pression Q , hence (i) saves ink and paper; - argument (ii) obscures the existence of demonstrandum (17), obscures the fact that the internal structure of the first Q and of the last Q in (18) is totally irrelevant for the latter's demonstration; argument (i) is clearer than (ii) in that it heads for (17), which clearly states that the first and the last Q's in (18) could be "any thing", provided they are the same. In the jargon: argument (i) is better disentangled than argument (ii). the full force of this disentanglement mani-fests itself when, besides the proof, we des-sign the theorem as well and Q emerges as the result of our calculations.

We shall illustrate the findings of the last two sections (and a little bit more) in the next section.

§7. In this section, we are looking, by way of example, for a nontrivial theorem about relational composition. Composition will be denoted by an infix “;” with a syntactic binding power higher than that of the logical infix operators but lower than that of the unary operators “!” and “~”.

We shall use that the transposition “~”dis- tributes over the logical operators, that com- position is monotonic in both its arguments, and that composition and transposition are coupled by the “right-exchange”, for which we choose here the formulation that for all $x,y,z$

$$ (1 9) [ x; y \wedge z \Rightarrow \mathrm {f a l s e} ] \equiv [ \sim x; z \wedge y \Rightarrow \mathrm {f a l s e} ]. $$

The exchange rules enable us to manipulate a composition that occurs as antecedent, but there are no analogous manipulative opportunities for a composition that occurs as a consequence, and we may therefore expect a problem when trying to prove a theorem of the form

$$ (2 0) \quad [ a \Rightarrow b; c ] $$

This problem, however, can be overcome with the aid of (16), which states that we can demonstrate (20) by proving -in a variation

on (17) - for arbitrary $z$ (21) $\left\lbrack {b;c \land z \Rightarrow \text{false}}\right\rbrack \Rightarrow \left\lbrack {a \land z \Rightarrow \text{false}}\right\rbrack ,$ and in this formulation of our proof obligation, the composition " $b;c$ " occurs as (conjunct in an) antecedent, and is thus amenable to manipulation via an exchange rule!

We shall now first give our calculation that transforms $[b;c \wedge z \Rightarrow \text{false}]$ without strengthening into $[a \wedge z \Rightarrow \text{false}]$ , and shall discuss the proof later. In the course of the calculation, suitable values for $c$ and $a$ will be chosen. We observe for any $z$

$$ \begin{array}{l} [ b; c \land z \Rightarrow f a l s e ] \ = {\text {r i g h t - e x c h a n g e} } \ [ \sim b; z \land c \Rightarrow f a l s e ] \ = {\text {c h o o s e} c: [ c \equiv \sim d; e \wedge f ] } (B) \ [ \sim b; z \land \sim d; e \land f \Rightarrow f a l s e ] \ \Rightarrow {\text {m o n o t o n i c i t i e s} } (C) \ [ (\sim b \wedge \sim d); (z \wedge e) \wedge f \Rightarrow f a l s e ] \ = {\sim d i s t r i b u t e s o v e r \wedge } (D) \ [ \sim (b \wedge d); (z \wedge e) \wedge f \Rightarrow f a l s e ] \ = {\text {r i g h t - e x c h a n g e} } (E) \ [ (b \wedge d); f \wedge e \wedge z \Rightarrow f a l s e ] \ = {\mathrm {c h o o s e} a: [ a \equiv (b \wedge d); f \wedge e ] } \quad (\mathrm {F}) \ [ a \wedge z \Rightarrow f a l s e ] \quad , \ \end{array} $$

and thus we have proved (20) with the choices made in steps (B) and (F), i.e.

(22) $\left\lbrack {\left( {b \land d}\right) ;f \land e \Rightarrow b;\left( {\sim d;e \land f}\right) }\right\rbrack$

a theorem, even uglier than "the first ugly theorem" of [1].

Remark We have used (19) instead of the formulation of the right-exchange from [2]

(23) $\left\lbrack {x;y \Rightarrow z}\right\rbrack = \left\lbrack {\sim x;\neg z \Rightarrow \neg y}\right\rbrack$

and (21) instead of what (17) would have given, viz.

$$ [ b; c \Rightarrow z ] \Rightarrow [ a \Rightarrow z ] \quad , $$

thus avoiding the need of introducing nega-tions and moving terms back and forth with the shunting rule

$$ [ x \Rightarrow y \lor z \equiv x \land y \Rightarrow z ]. $$

In [1], this economy is achieved by the introduction of the "somewhere" operator. (End of Remark.)

Step A is not surprising because (21) was intentionally chosen so as to make the right-exchange applicable to its ante- cedent.

The purpose of step B is to apply the most general substitution for $b$ or $c$

that makes continued manipulation pos-

sible. For $b$ ,I could not find a pro

distributive subqutution: after ${b}_{i} = d{ve}^{i}$ ,

we can use composition's monotonicity

as in (15) but that creates 2 occur

rences of dummy $z$ ,and after $b \mathrel{\text{:=}} d \land e$ ,

we are stuck because then composition's

monotonicity as in (14) works in the

wrong direction. If, however, we sub-

stifute a composition like ~dje for

C ,then monotonicity as in (14) works

in the right direction. The inclusion of

the additional " $\land {f}^{\prime \prime }$ is ,in a sense,

obligatory if we wish to keep our

options: open: since c occurs as

conjunct and conjunction is associative,

the ${}^{ \circ }$ additional " ${}^{ \circ }f$ " does not hamper

the combination of the two composites

tions, and, furthermore, omission of

the conjunct $\land f$ " can be interpreted

as a possibly premature instantiation

$f \mathrel{\text{:=}}$ true. (The choice of "or" instead)

of "d;e" is an irrelevant matter of

elegance; it allows us to ignore that

$\therefore {b}^{\prime }\left( x\right) = - \frac{1}{x} + \frac{2}{x} + 1 = - \frac{1}{x} + \frac{1}{\left( {1 - x}\right) x} + 1 = - \frac{1}{x} + \left( {-1}\right) x$

Step C' exploits the monotonicity

of $\left( {6,1}\right)$ (plus the usual ones from

predicate calculus), and, in view of our

target, our remaining duty is to extric- cate dummy $z$ from the composition.

Step E performs this extraction by - what else?- a second appeal to right-exchange after step D has prepared the ground. ( Step D could have been postponed, but then later simplicati on would have needed that "~" is its own inverse.)

Our final step F embodies the re- cognition of what to choose for "a" and thus we have designed and proved theorem (22).

[\text{8. In [2] , left- and right-conditions are}]

(2) $\left( {p\text{is a left-condition}}\right) \equiv \left\lbrack {p;\text{true} \equiv p}\right\rbrack$ (24b) ( $q$ is a right-condition) $\equiv \left\lbrack {\text{true};q \equiv q}\right\rbrack$ ;

we now focus our attention on the right- condition.

In [2], Feijen & van Gasteren point out that - because $\left\lbrack {\text{true};x \Leftrightarrow x}\right\rbrack$ for all $x$ - definition (24b) is equivalent to (25) ( $q$ is a right-condition) $\equiv \left\lbrack {\text{true};q \Rightarrow q}\right\rbrack$ ,

the right-hand side of which is formally weaker than that of (24b). Lincoln A. Wallen has taught us a greater awareness of monotonicity arguments and has urged us to notice when we used only one direction of a mutual implication. To prove that a relation is a right-condition, (25) is more convenient for the formulation of the demonstrandum than (24b).

When trying to use that a relation is a right-condition, formally stronger characteriza- tions are, in general, to be preferred. The stronger (24b) captures [true; $x \leq x$ ] -which follows from the existence of a neutral element of the composition and the latter's monotonicity-. . Here I propose another strengthening of (25), one that captures composition's monotonicity (in its left argument):

(26) ( $q$ is a right-condition) $\equiv \left\langle {\forall x : \left\lbrack {x;q \Rightarrow q}\right\rbrack \cdot }\right\rangle$ .

We shall use this definition (twice) to prove the following theorem:

(q is a right-condition) $\Rightarrow$ (7q is a right-condition)

Proof We observe for arbitrary relation $g$

$$ \begin{array}{l} (7 9 i s a r i g h t - c o n d i t i o n) \ = {(2 6) \mathrm {w i t h} q := 7 g } \ \langle \forall x: [ x; 7 q \Rightarrow 7 q ] \rangle \ = {(2 3), i. e. r i g h t - e x c h a n g e } \ \langle \forall x: [ \sim x; q \Rightarrow q ] \rangle \ \Leftrightarrow \quad {i n s t a n t i a t i o n x := \sim x } \ \langle \forall x: [ x; q \Rightarrow q ] \rangle \ = {(2 6) } \ (q i s a r i g h t - c o n d i t i o n) \ \end{array} $$

(End of Proof.)

In both [1] and [2], the proof of this theorem appeals to [vtrue = true], where as the above proof does not use any properties of $\sim$ or true. The manipulative disadvantage of (25) is that it contains a constant whose properties we have to use.

The heuristic significance of formulation (26) is that it almost dictates monotonicity arguments because the fact that prefixing $q$ by an arbitrary " $x;$ " weakens it, fully captures that $q$ is a right-condition. In other words, if, for instance, we set ourselves to prove that for a right-condition $q$

$$ (2 7) \qquad [ q; \mathrm {t r u e}; \sim q \equiv q; \sim q ] \qquad , $$

the implication sign in (26) tells us that a ping-pong argument is appropriate.

Remark When faced with a demonstrum of the form $[A\equiv B]$ we have a demonstrum that does not depend (anti)monotonically on either A or B . Hence, proving this directly can only be done by appealing to Leibniz's Principle, i.e. by value-preserving transformations. (We have seen an example of this in section 1.) Rewriting the demonstrum as mutual implication $[A\Rightarrow B]\land [A\Leftarrow B]$ yields two conjuncts that do depend (anti) monotonically on both A and B ! Because we like to avoid avoidable ping-pong arguments, it is nice to recognize circumstances under which they are indicated. (End of Remark.)

In proving (27) we observe for ping:

$$ \begin{array}{l} [ q; \mathrm {t r u e}; \sim q \Leftrightarrow q; \sim q ] \ \Leftrightarrow {m o n o t o n i c i t y o f ; } \ [ q; t r u e \Leftarrow q ] \ = {[ x; t r u e \Leftarrow x ] } \ f r u e, \ \end{array} $$

a demonstration in which we did not use that $q$ is a right-condition. For pang we observe that we can strengthen the right-hand side:

$$ [ q; \mathrm {t r u e}; \sim q \Rightarrow q; \sim q ] $$

$$ \begin{array}{l} \Leftarrow {2 6) w i t h x := q; t r u e; \sim q } \ [ q; \mathrm {t r u e}; \sim q \Rightarrow q; \mathrm {t r u e}; \sim q; q; \sim q ] \ \Leftrightarrow {\mathrm {m o n o t o n i c i t y} _ {\mathrm {o f}}; } \ {\mathrm {m o n o t o n i c i t y} \in f; } [ \sim q \Rightarrow \sim q; q; \sim q ] \ = {2 8) \mathrm {w i t h} b := \sim q } \ t r u e \ \end{array} $$

where the "seesaw lemma" - see [1] -

$$ (2 8) \quad [ b \Rightarrow b; \sim b; b ] $$

follows from (22) with $d,e,f \mathrel{\text{:=}} b,b,$ true

(Knowledge of the seesaw lemma admittedly helps in the choice of how to instantiate

[\frac{9.1}{by}\text{In [1] "middle-conditions" are introduced.}]

(29) ( $c$ is a middle-condition) $\equiv \left\lbrack {c \Rightarrow j}\right\rbrack$

where " $J$ " is the neutral element of ${}^{\prime \prime }$ ,

Also here the constant can be eliminated

from the definition: we could have defined

(30) (c is a middle-condition) $\equiv \langle \forall x::[c;x\Rightarrow x]\rangle$ or (31) (c is a middle-condition) $\equiv \left\langle {\forall x : \left\lbrack {x;c \Rightarrow x}\right\rbrack \cdot }\right\rangle$ .

In other words, $c$ being a middle-condition

is captured by the fact that the prefix

operator "c; and the postfix operator "c"

are strengthening operators. The implication signs in these definitions tell us that, for instance,

(32) $\left\lbrack {c \equiv \sim c}\right\rbrack \quad$ for middle-condition

has to be proved by mutual implication.

Since ${\left\lbrack \sim x \Rightarrow x\right\rbrack }^{3} = \left\lbrack {x \Rightarrow \sim x}\right\rbrack$ ,it suffices

to prove $\left\lbrack {c \Rightarrow \sim c}\right\rbrack .\;\left{ {\begin{array}{ll} \text{ We observe to this end } \ \end{array} }\right.$

$$ \sim c $$

$$ \begin{array}{l} \Leftrightarrow \quad \left{ \begin{array}{l} (3 0) \text {w i t h} x := \sim c \end{array} \right} \ c; \sim c \ \Leftrightarrow \quad {(3 1) \mathrm {w i t h} x := c; \sim c } \ c; \sim c; c \ \Leftrightarrow \quad \left{ \begin{array}{l} (2 8) \text {w i t h} b := c \end{array} \right} \ \mathbf {C} \ \end{array} $$

Our wish to apply strengthening operators suggested to start at the consequent and the first two steps then followed. (And we were just lucky that we did not try to prove $[w c \Rightarrow c]$ according to the above scheme.)

$\S 10$ . Let me conclude. We set out to ex- plore for antisymmetric and reflexive rela- tions the interplay between calculating with equalities and inequalities, the latter drawing our attention to monotonicity arguments. In passing we encountered a number of instances - (2), (3), (16), (26), (30), (31) -

where, sometimes to clear advantage, a formula or definition could be rewritten as a universally quantified expression.

A closely related topic is the design of calculational proofs of theorems about extreme solutions. Since this topic has been dealt with in [0] we shall not pursue it here. To close I shall borrow an example from [1] to show that also here universal quantification can be used to eliminate a constant. Instead of defining the reflexive transitive closure by $\left( {s}^{ * }\right.$ is the reflexive transitive closure of $s) \equiv$ $\left( {s}^{ * }\right.$ is the strongest solution of $x : \left\lbrack \;\right\rbrack v\;s;x \Rightarrow x\rbrack$ )

we can define ${s}^{ * }$ equivalently by

$\left\langle {\forall t : {s}^{ * };t\text{ is the strongest solution of }{x}^{ * }}\right\rangle$

We shall not repeat the standard proof here (which is, as is to be expected, a ping-pong argument). We do wish to point out that the instantiation $t \mathrel{\text{:=}} J$ returns the original definition.

Acknowledgements Anyone familiar with their writings will realize that I am greatly indebted to Rutger M. Dgkstra,

W.H.J.Feijen, and A.J.M.van Gasteren.

[0] Predicate Calculus and Program Semantics, Edsger W. Dijkstra & Carel S. Scholten, Springer-Verlag, 1990 [1] Relational Calculus and Relational Program Semantics, Rutger M. Dijkstra 1992 [2] An Introduction to the Relational Calculus, W.H.J. Feijen & A.J.M. van Gasteren Appeared in: C.S. Scholten Dedicata: Van oude machines en neue rekenwijzen, W.H.J. Feijen & A.J.M. van Gasteren (Eds.) Schoonhoven, Academic Service, 1991

Austin, 11 April 1993

Prof. dr. Edsger W. Dgksira Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 USA