The derivation of a proof by J.C.S.P. van der Woude

Copyright Notice

The following manuscript, EWD 1020: The derivation of a proof by J.C.S.P. van der Woude was published as Chapter 16 of Edsger W. Dijkstra, ed., Formal Development of Programs and Proofs. Addison-Wesley, 1990. It was adapted, with permission, from Chapter 6, pp.90-95 of Edsger W. Dijkstra and Carel S. Scholten, Predicate Calculus and Program Semantics, Springer-Verlag, Berlin 1989 It is held in copyright by Springer-Verlag, and is reproduced here with permission of Springer-Verlag New York.

The derivation of a proof by J.C.S.P. van der Woude

In the following

• $P$ and $Q$ will be used to denote predicates on some space.
• X and Y will be used to denote functions from the natural numbers to predicates on that space; accordingly, X.i (0≤i) and Y.i (0≤i) denote predicate sequences. will be used to denote a predicate transformer, i.e. a function from predicates to predicates. square brackets will be used to denote universal quantification of the enclosed predicate over the space in question.

With the above notational conventions we give the following definitions

• "sequence $X.i$ ( $0 \leq i$ ) is monotonic" means

• "sequence $X.i$ ( $0 \leq i$ ) is weakening or strengthening".

• "sequence $X.i\left( {0 \leq i}\right)$ is weakening" means $\left( {\underline{A}{i,j} : 0 \leq i < j : \left\lbrack {X.i \Rightarrow {X.j}}\right\rbrack }\right)$ .

• "sequence $X.i\left( {0 \leq i}\right)$ is strengthening" means

• "predicate transformer $f$ is monotonic" means $\left\lbrack {P \Rightarrow Q}\right\rbrack \Rightarrow \left\lbrack {f.P \Rightarrow f.Q}\right\rbrack$ for all $P,Q$

• "predicate transformer $f$ is finitely conjunctive" means $\left\lbrack {f \cdot \left( {P \land Q}\right) \equiv f \cdot P \land f \cdot Q}\right\rbrack$ for all $P,Q$ "predicate transformer $f$ is or-continuous" means $[f.(\underline{E} i:0\leq i:X.i)\equiv (\underline{E} i:0\leq i:f.(X.i))]$ for any monotonic sequence X.i (oSi)
• "predicate transformer $f$ is and continuous" means $\left\lbrack {f\left( {\underline{A}i : 0 \leq i : X,i}\right) \equiv \left( {\underline{A}i : 0 \leq i : f\left( {X,i}\right) }\right) }\right\rbrack$ for any monotonic sequence ${X}_{i}\left( {0 \leq i}\right)$

We can now formulate the

Theorem For any predicate transformer $f$

(0) ( $f$ is finitely conjunctive) $\land \left( {f\text{is}\underline{\text{or}}\text{-continuous}}\right) \Rightarrow$ ( $f$ is and- continuous)

Here, we shall sketch the simple part of the proof and shall derive the exciting part (which we owe to J.C.S.P. van der Woude).

Proof Under the truth of the antecedent of (0) we have to show for monotonic $X_{i}$ $(0\leq i)$

$\left\lbrack {f.\left( {{A}{i} : 0 \leq i : X,i}\right) \equiv \left( {{A}{i} : 0 \leq i : f.\left( {X,i}\right) }\right) }\right\rbrack$

To begin with we recall that -not proved here- because $f$ is finitely conjunctive, $f$ is

monotonic. We now distinguish two cases.

$X_{i}(0\leq i)$ is weakening Because $f$ is monotonic, also the predicate sequence $f.(X.i)(0\leq i)$ is weakening; consequently - not shown here- both sides of (1) are equivalent to $f.(X.0)$ . This concludes the first case.

${X}_{i}\left( {0 \leq i}\right)$ is strengthening. Because $f$ is monotonic - not shown here - LHS(1) $\Rightarrow$ RHS(1) and we are left with the proof obligation

(2) $\left\lbrack {f.\left( {\underline{A}i : 0 \leq i : X,i}\right) \Leftrightarrow \left( {\underline{A}i : 0 \leq i : f\left( {X,i}\right) }\right) }\right\rbrack$

for strengthening $X.i\left( {0 \leq i}\right)$ and an $f$ that is finitely conjunctive and or-continuous.

Meeting the obligation of showing (2) is the exciting part of the proof. Reduced to its bare essentials, it consists of one definition and about a dozen simple steps. But in present- ing just that irrefutable formal argument, we would pull several rabbits out of the magical hat. The proof is exciting because of the existence of heuristic considerations that quite effectively buffer these shocks of in- vention. For that reason, we shall develop this proof instead of just presenting it. To aid the reader in parsing the interleaved presentation of heuristic considerations and proof fragments, the latter will be indented. Here we go!

For the sake of brevity we shall omit from here on the ranges osi and osj, which are to be understood. We begin with a general remark about the exploitation of or-continuity. The or-continuity of $f$ states

(3) $\left\lbrack {f.\left( {{E}{i} : {Y}{i}}\right) \equiv \left( {{E}{i} : f\left( {Y}{i}\right) }\right) }\right\rbrack$

for any monotonic sequence Y.i . For a strenghtening sequence Yi , just monotonicity of f suffices for (3) to hold, and for constant sequences Yi , (3) holds for any f. The relevant conclusion from these observations is that, if f's or-continuity is going to be exploited -and it is a safe assumption that it has to- a truly weakening sequence has to enter the picture.

Armed with this insight, we return to our demonstrandum (2). The simplest way of demonstrating an implication is to start at one side and then to repeatedly manipulate the expression (while either weakening or strengthening is allowed) until the other side is reached. So, let us try that. That decision being taken, at which side should we start?

Both sides are built from the "familiar" universal quantification and the "unfamiliar" application of $f$ , about which our knowledge

is limited, the only difference being that, at the two sides, they occur in opposite order. In such a situation, the side with the "unfamiliar" operation as the outer one counts as the more complicated one and is therefore the preferred starting point. In our case, it is the consequence

(4) $f.\left( {A,i : X,i}\right)$

so let us start from there. The formal chal- lenge of manipulating (4) while exploiting what we know about f should provide the heuristic guidance as to in which direction to proceed.

Rewriting (4) so as to exploit $f$ 's or- continuity would require rewriting its argument (Aii: Xii) as an existential quantifica-tion over a truly weakening sequence, but how to do that - I tried in vain- is not clear at all. So, let us try to exploit at this stage $f$ 's finite conjunctivity, i.e. let us introduce a $P$ and $Q$ such that

$$ [ (\underline {{A}} _ {i}: X _ {i}) \equiv P \wedge Q ] $$

For one of the conjuncts, say P, we may choose any predicate implied by (A i: X. i); the law of instantiation tells us that any Xj would do. (Note that this choice is

less restrictive than it might seem: because X. i is a strengthening sequence, any finite conjunction of some X. i 's yields some X. j .) We could therefore consider for some $j$ the introduction of a predicate $Q$ constrained by

$$ [ (\underline {{\mathrm {日}}} i: X. i) \equiv X. j \land Q ] $$

But the introduction of one predicate Q for one specific j is unlikely to do the job: for one thing, the universal quantifications in the demonstrandum don't change their value if the range 0s i is replaced by jki . This observation suggests, instead of the introduction of a single predicate Q , a predicate sequence Yj , constrained by

(5) $\left\lbrack {\left( {\underline{\mathrm{A}}}{i} : {X}{i}}\right) \equiv {X}{j} \land {Y}{j}}\right\rbrack$ )

The introduction of the sequence Yj will turn out to be the major invention of the proof under design. For the time being, we don't define Y - as would be done immediately in a "bottom-up" proof- but only collect constraints on Y, of which (5) is the first one. We do so in the hope that, eventually, we can construct a Y that meets all the constraints.

A minor problem with the use of (5) as a rewrite rule is that it equates an ex

pression not depending on j with one that formally does depend on j . The formal de- pendency on j that would thus be introduced can be eliminated by quantifying over j ; because we are rewriting a consequent, we use existential quantification because that yields a formally weaker expression -the range being non-empty!- than universal quanti- fication (and the weaker the consequent, the lighter the task ahead of us). In short, we propose to start our proof under design with

$$ f: (\underline {{A}} _ {i}: X _ {i}) $$

$$ = {(5) a n d r a n g e o f j n o n - e m p l y } $$

$$ (E _ {j} = f (X _ {j} \wedge Y _ {j})) $$

$$ = {f ^ {\prime} \mathrm {i s f i n i t e l y c o n j u n c h i v e} } $$

(6)

$$ (E _ {j}: f (X _ {j}) \wedge f (Y _ {j})) $$

So far, so good! We have not yet exploited $f_{s}^{\prime}$ or-continuity and we cannot do so be- fore we have an existential quantificaton over a truly weakening sequence. In (6) we do have an existential quantificaton (albeit, as yet, over a constant sequence) and, with X.i a (truly) strengthening sequence, there is a fair chance that (5) permits a (truly) weakening sequence Yj . So let us introduce the second constraint on Y

(7) sequence ${Y}_{j}\left( {0 \leq j}\right)$ is weakening

as a next step towards the use of $f$ 's or- continuity , i.e. the use of (3) as a rewrite rule.

Comparison of the right-hand side of (3) with (6) shows that we can use (3) as rewrite rule only after we have succeeded in removing in (6) the first conjunct $f_{\cdot}(x, j)$ from the term. We cannot just omit it, as that would weaken the expression and, heading for an antecedent, we are not allowed to do that. We may strengthen it; in particular, strengthening it to something independent of $j$ would allow us to take the constant conjunct outside the existential quantification of (6). In order to strengthen $f_{\cdot}(x, j)$ to something that is independent of $j$ , we propose to quantify universally over $j$ . That is, at (6) we propose to continue our proof under design with

$$ \begin{array}{r l} & {\quad (\underline {{E}} _ {j}: f. (X _ {j}) \wedge f. (Y _ {j}))} \ & {\Leftrightarrow {\mathrm {i n s t a n t i a t i o n , m o n o t o n i c i t y o f} \wedge , \underline {{E}} }} \ & {\quad (\underline {{E}} _ {j}: (\underline {{A}} _ {i}: f. (X _ {i})) \wedge f. (Y _ {j}))} \ & {= {\wedge \mathrm {d i s t r i b u t e s o v e r} \underline {{E}} }} \ & {\quad (\underline {{A}} _ {i}: f. (X _ {i})) \wedge (\underline {{E}} _ {j}: f. (Y _ {j}))} \ & {= {(3) \mathrm {a n d} (7), \mathrm {i . e . t h e u s e o f o r - c o n t i n u i t y} }} \ & {\quad (\underline {{A}} _ {i}: f. (X _ {i})) \wedge f. (\underline {{E}} _ {j}: Y _ {j})} \end{array} $$

So far, so very good! Note that the left con-

junct of (8) is the antecedent of (2) we are heading for! Again, we cannot just omit the second conjunct in (8) as that would weaken the expression; the second conjunct has to be subsumed - i.e. implied- by the first one. By the looks of it we can equate (8) with its first conjunct on just the monotonicity of $\mathcal{P}$ and some implicative relation between $X$ and $Y$ - which will emerge as our third and last constraint on $Y-$ . But be careful! If the range of $i$ were empty, the first conjunct of (8) would yield true, whereas (8) would yield $\mathcal{P}$ . (Ej:Y.) and there is no reason to assume these equivalent. Some-where along the completion of our formal argument, we have to exploit the non-emptiness of $i$ 's range. As we can do it immediately, let us do it immediately. In short, we propose to continue our proof under design at (8) with

$$ \begin{array}{l} (\underline {{A}} _ {i}: f. (X, i)) \wedge f. (\underline {{E}} _ {j}: Y, j) \ = {\text {r a n g e o f i n o n - e m p t y} } \ (\underline {{A}} _ {i}: f. (X, i) \wedge f. (E _ {j}: Y _ {j})) \ = {m o n o t o n i c i t y o f p a n d (9) } \ \end{array} $$

with, as our third and last constraint on $Y$

$$ (9) \quad (\underline {{A}} _ {i}: [ X, i \Rightarrow (E _ {j}: Y, j) ]) $$

But for the demonstration of the existence of $Y$ ,we have completed the proof in seven steps (six of which are equivalences). Now for the existence of a $Y$ satisfying (5),(7),and (9).

In order to ease satisfaction of (9), we define $Y$ as the weakest solution of (5), i.e. we define $Y_{j}$ for any $j$ by

[\left\lbrack {Y,j \equiv \left( {\underline{A}i : X,i}\right) \vee \neg X,j}\right\rbrack ]

In order to verify that this Y indeed satisfies (5), we observe for any $j$

$$ \begin{array}{l} = \begin{array}{l} X _ {j} \wedge Y _ {j} \ {(1 0) } \end{array} \ x _ {j} \wedge ((\underline {{A}} _ {i}: X _ {i}) \vee \neg X _ {j}) \ = {\wedge d i s t r i b u t e s o v e r v } \ \end{array} $$

$$ (X _ {j} \land (\underline {{A}} i: X _ {i})) \lor (X _ {j} \land \neg X _ {j}) $$

$$ \begin{array}{l} = {j \mathrm {i n} i s \mathrm {r a n g e}; \mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} _ {i}: X _ {i}) \ \end{array} $$

In order to verify that condition (7) is met, i.e. that $Y_{j}(0 \leq j)$ is indeed weakening, we observe for any $j$ and $k$

$$ = \begin{array}{r l} {[ Y, j \Rightarrow Y, k ]} & \ {{\mathrm {(1 0)} }} & \end{array} $$

$\left\lbrack {\left( {{A}{i} : {X}{i}}\right) \vee i \times j} \Rightarrow \left( {{A}{i} : {X}{i}}\right) \vee i \times k}\right\rbrack$

$$ \begin{array}{l} [ \neg X, j \Rightarrow \neg X, k ] \ = {\mathrm {c o u n t e r p o s i t i v e} } \ [ X, j \Leftarrow X, k ] \ \Leftrightarrow {X _ {i} (0 \leq i) \mathrm {i s s t r e n g t h e n i n g} } \ [ j < k ] \ \end{array} $$

Finally, in order to verify that $Y$ satisfies (9), we observe

$$ \begin{array}{l} (E _ {j}: Y _ {j}) \ = {(\mathbf {1 0}) } \ (E _ {j}: (A _ {i}: X _ {i}) \vee \neg X _ {j}) \ = {j s r a n g e i s n o t e m p t y } \ (\underline {{A}} i: X. i) \vee (\underline {{E}} j: X. j) \ = {d e M o r g a n } \ (\underline {{A}} _ {i}: X. i) \sim \neg (\underline {{A}} _ {j}: X. j) \ = {\text {E x c l u d e d M i d d l e} } \ t r u e \ \end{array} $$

And this concludes the exciting part.

(End of Proof.)

Van der Woude's proof is very beautiful and I think it worthwhile to ponder over the question why this is so. It is beautiful in the way in which the proof has been divided into two parts, with Y and its three properties forming the interface between them. It is a meaning-

ful division in the sense that our dealing with f is entirely confined to the first part. Also, the interface between the two parts is the right one, void of any overspecification: it only mentions the existence of a Y with the properties relevant for the first part. Finally, the second part, which no longer deals with f but is concerned with the existence of a Y, is pleasingly constructive. It is really a beautifully structured argument.

I think also our derivation of the proof very beautiful. The development of the first part, which deals with $f$ , is fully driven by the need to exploit that $f$ is given to be finitely conjunctive and or-continuous, and the interface was constructed as we went along. Furthermore, the second part, which constructs a Y meeting the three requirements, does so in the most straightforward manner without pulling a single rabbit out of a hat; finally it contains three mutually independent verifications that the Y constructed meets the three requirements indeed. A very nice disentanglement!

Remark I would like to draw attention to the second step of the final calculation, which establishes $[(Ej:Yj)\equiv true]$ . Because this

cannot be established if the range for j is empty - existential quantification over an empty range yields false -, the calculation has to exploit that j's range is not empty. The knowledge that disjunction distributes over existential quantification only in the case of a non-empty range -and this belongs to the general knowledge the predicate calculator should have at his disposal- all but dictates that second step. (End of Remark.)

Finally, I would like to point out that, though carried out in great detail, the whole formal proof consists of fewer than twenty steps: the whole calculation is really quite short. I beg the reader to remember this whenever he is faced with a defence of informality on the supposed grounds that formal proofs are too lengthy and too tedious to be of any practical value. This supposition is wrong.

Austin, 27 January 1988

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