The proof of the pudding

The proof of the pudding

(This note is not self-contained, but a sequel of EWD945; formulae are numbered here starting at (5). The lower numbers referring to EWD945.)

Let $S$ be the strongest solution of

$X : \left\lbrack {X \cdot x.y \equiv p \cdot x.y \vee \left( {\underline{E}w : X \cdot x.w \land X \cdot w.y}\right) }\right\rbrack$ (5)

As before we have

$$ \begin{array}{l} [ S ^ {\prime}. x. y \Leftarrow p. x. y \vee (\underline {{E}} w: S ^ {\prime}. x. w \wedge S ^ {\prime}. w. y) ] \ \Rightarrow [ S. x. y \Rightarrow S ^ {\prime}. x. y ] \quad (6) \ \end{array} $$

We then have $\left\lbrack {Q.x.y \equiv S.x.y}\right\rbrack$ (7)

Note A proof of (7) is, for reasons of symmetry, also a proof of

$$ [ R. x. y \equiv S. x. y ] \quad (8) $$

and, hence an alternative proof of the theorem of EWD945. (End of Note).

Let us proceed as before.

$$ [ Q. x. y \Rightarrow S. x. y ] $$

$$ \begin{array}{l} \Leftrightarrow {Q ^ {\prime} := S i n (3) } \ [ S. x. y \Leftarrow p. x. y \vee (E z: p. x. z \wedge S. z. y) ] \ \Leftrightarrow {\mathrm {s i n c e} S \mathrm {s o l v e s}. (5): [ S. x. 2 \leq p. x. 2 ] \ [ S. x. y \Leftrightarrow p. x. y \vee (\underline {{E}} z: S. x. z \wedge S. z. y) ] \ = {\mathrm {s i n c e} S \mathrm {s o l v e s} (5) } \ \end{array} $$

Here, a little theorem is trying to get out; see below.

$$ \begin{array}{l} \begin{array}{r l} & {[ Q. x. y \Leftarrow S. x. y ]} \ & {\Leftarrow {S ^ {\prime} := Q i n (6) }} \end{array} \ [ Q. x. y \Leftarrow p. x. y \vee (E w: Q. x. w \wedge Q. w. y) ] \ = {\mathrm {s i n c e} Q \mathrm {s o l v e s} (0): [ Q. x. y \leqslant p. x. y ] } [ Q. x. y \leqslant (\mathrm {E w}: Q. x. w \wedge Q. w. y) ] \ = {p r e d i c a t e c a l c u l u s } [ Q. x. y \Leftarrow Q. x. w \land \ = {p r e d i c a t e {c a l c u l u s} [ Q. x. w \Rightarrow Q. x. y \vee \neg Q. w. y ] \ = {r e n a m i n g t h e d u m m i e s: w, y := y, w } [ Q. x. y \Rightarrow Q. x. w \lor \neg Q. y. w ] \ \Leftrightarrow {Q ^ {\prime} x, y := Q. x. w \vee \neg Q. y. w \mathrm {i n} (3) } \ [ Q. x. w \vee \neg Q. y. w \Leftarrow \ p. x. y \vee (\frac {1}{2} z: p. x. z \wedge (Q. z. w \vee 7 Q. y. w)) ] \ \Leftrightarrow {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ Q ^ {\prime}. x. w \Leftarrow p. x. y \land Q. y. w \lor (E z: p. x. z \land Q. z. w) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ Q. x. w \Leftarrow (E z: p. x. z \land Q. z. w) ] \ = {Q \mathrm {s o l v e s} (0) } \ f r u e \ \end{array} $$

(End of Proof.)

The moral of the above is that, instead of proving

The title of this note was chosen as soon as I had decided to write it without any prior explora- tion, just to check whether my heuristics would work again. They did! (In the first proof, on EWD946-0, I had introduced the superfluous step of

removing the conjunct p.x.y from the right-hand side, mechanically copying what I had done in EWD945. This superfluous step has been removed with the aid of glue and scissors.)

The step, marked *) contains a choice. Why not $\left\lbrack {Q.w.y \Rightarrow Q.x.y \vee ?Q.x.w}\right\rbrack$ ?

Well, that is because we are heading far an appli-. cation of (3). In the case of $\mathcal{R}$ ,the other choice should have been made.

Equation (0) can be obtained by replacing in the right-hand side of (5) one of the occurrences of the unknown by a lower bound of the right-hand side -viz. $X$ by $p$ . This transformation can only strengthen the strongest solution, as shown below.

The little theorem Let $k$ and $f$ be monotonic functions of their arguments and such that

$$ (\mathrm {A X}: [ k. x \Rightarrow f. x. x ]) \quad ; \quad (9) $$

let $S$ be the strongest solution of

$$ X: [ p. X. X \equiv X ] \quad ; \quad (1 0) $$

let $Q$ be the strongest solution of

$$ X: [ f. X. (k. X) \equiv X ] \quad . \quad (1 1) $$

Then

Little proof.

$$ \begin{array}{l} [ Q \Rightarrow S ] \ \Leftrightarrow {\mathrm {d e f . o f} Q \mathrm {b y (1 1)} } \ [ p, S, (k, S) \Rightarrow S ] \ = {\dot {S} \mathrm {s o l v e s} (1 0) } \ [ f. s. (k. s) \Rightarrow f. s. s ] \ \Leftrightarrow {f \mathrm {i s m o n o t o n i c i n} 2 ^ {n d} a r g u m e n t } \ [ k. S \Rightarrow S ] \ = {S \text {s o l v e s} (1 0) } \ [ k. s \Rightarrow f. s. s ] \ \Leftarrow {\mathrm {i n s t a n t i o n} o f (9): x := S } \ t r u e \ \end{array} $$

(End of Little proof.)

Remark for the sake of the above proof I could have defined $s$ as any solution of

$$ x: [ p. x. x \Rightarrow x ] $$

but this I did not know beforehand, hence (10). (End of Remark.)

Deriving proofs like in this note gets more and more the flavour of "turning the handle": an appropriate choice of identifier becomes one of the major decisions.

Austin, 4 November 1985

prof. dr. Edsger W. Dgkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712 - 1188

USA