More annotated proofs (a sequel to 1143)

More annotated proofs (a sequel to 1143)

From the collection of WF & Avg, we consider the theorem

$\left( 0\right) \;\left\lbrack {x \Rightarrow J}\right\rbrack \land \left\lbrack {y \Rightarrow J}\right\rbrack \Rightarrow \left\lbrack {x;y \equiv x \land y}\right\rbrack$

How do we prove this? Well, to the left we have "J", which does not occur to the right, where we have ";", which does not occur to the left. Hence we need a connection between "J" and ";", which is, of course, that "J" is the neutral element of ";". We can go further: because what the antecedent states about "J" is symmetric in x and y, which in the consequent occur as left- and right-hand argument of the ";", we can expect to need that "J" is, both, the left-neutral and the right-neutral element of the composition.

In view of the above it is tempting to start a weakening chain at the antecedent and head for the expression $x; y$ . Thus we observe

$$ [ x \Rightarrow J ] \wedge [ y \Rightarrow J ] $$

$\Rightarrow { ;\operatorname{monotonic in both arguments}}$

$$ [ x; y \Rightarrow ]; y ] \land [ x; y \Rightarrow x; ] $$

$= \left{ {\left{ J\text{ is left - and right - neutral element of }i}\right} \end{array} \Rightarrow }\right.$

$$ [ x; y \Rightarrow y ] \land [ x; y, \Rightarrow x ] $$

$= {$ predicate calculus

$$ [ x; y \Rightarrow x \land y ] $$

So ping has been proved; note that, in the mean time, we have used composition's monotonicity. We still have to show pong:

(1) $\left\lbrack {x \rightarrow J}\right\rbrack \land \left\lbrack {y \Rightarrow J}\right\rbrack \Rightarrow \left\lbrack {x \land y \Rightarrow x;y}\right\rbrack$

The antecedent -and we have used this in the proof of ping- implies that the prefix operators like "x;" and the postfix operators like ";y". If we wish to use that to strengthen $\left\lbrack {x \land y \Rightarrow x;y}\right\rbrack$ ,we have to strengthen a term in the consequent. Hence some shunting seems indicated:

$$ \begin{array}{l} [ x \wedge y \Rightarrow x; y ] \ = {\mathrm {s h u n t i n g} } \ [ x \Rightarrow x; y \lor \neg y ] \ = {j _ {n e u t r a l e l e m e n t} } \ [ x \Rightarrow x; y \lor ]; [ y ] \ \Leftrightarrow {[ x \Rightarrow ] } \ [ x \Rightarrow x; y \lor x; \neg y ] \ = {\overline {{\vdots o v e r}} v } \ [ x \Rightarrow x; (y \lor \neg y) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ x \Rightarrow x; t r u e ] \ = {\mathrm {r e l a t i o n a l c a l c u l u s} } \ t r u e \ \end{array} $$

The way in which the symmetry is destroyed in the shunting step is strange and surprising. (My first proof shunted to [x; y v 1x v 7y] and maintained the symmetry between x and y as

are

much as possible.) The surprise reflects that if we drop in the antecedent one of the conjuncts, it is still a theorem. In the mean time, we have also used composition's distribution over v ; in the sequence "monotonic", "distributing over v ", "universally disjunctive" was that the next stronger property of composition to be taken into account, thus presenting a further invitation to do some shunting.

The next theorem we owe to the WF&Avg is For $p$ a left- condition

(2) $\left\lbrack {p;p \equiv p}\right\rbrack$

where - see EWD1143- we characterize p's being

(3) $\left\lbrack {p;X \Rightarrow p}\right\rbrack$ for all $X$

Remark Note similarity and difference between

(3) and our consequences of $\left\lbrack {y \Rightarrow }}\right\rbrack$ in the previous example, such as

$$ [ x; y \Rightarrow x ] f o r a l l x $$

Not surprisingly, our current proof shows structural similarities with the previous one. (End of Remark.)

Again, ping is a walk-over:

true

$$ \begin{array}{l} = {(3) \mathrm {w i t h} x := p } \ [ p; p \Rightarrow p ] \ \end{array} $$

When we tackled pong in class -without all these preliminaries- and looked at our proof

obligation

$$ [ p \Rightarrow p; p ] f o r l e f t - c o n d i t i o n p, $$

we took the standard approach of listing the "direct consequences" or "simple properties" of the ingredients

• logical expressions built from left-conditions are left-conditions ; having only left-condition p this leads to $\neg p$ being a left-condition:

(4) $\left\lbrack {{7p};x \Rightarrow {7p}}\right\rbrack$ for all $x$

$\Rightarrow$ can be expressed with $\left( {\land \equiv }\right) ,\left( {v \equiv }\right)$ , or $\left( {\neg v}\right)$ ; further shunting and contra- positive ; $\Rightarrow$ is transitive - is monotonic , distributes over $v$ , is universally disjunctive ; has an identity element is associative

Looking at these properties we concluded that they suggested to use the implication in the proof obligation for the introduction of $\neg$ and $v$ , and (after some polishing) we came up with

$$ \begin{array}{l} [ p \Rightarrow p; p ] \ = {s o r t o f s h u n t i n g } \ [ p \Rightarrow p; p \lor \neg p ] \ \Leftarrow {4 } \mathrm {w i t h} x := p } \ [ p \Rightarrow p; p v, v p; p ] \ = {; o v e r v } \ [ p \Rightarrow (p \lor \neg p); p ] \ = {\mathrm {p r e d . c a l c .} } \ [ p \Rightarrow t r u e; p ] \ = {\mathrm {r e l . c a l c .} } \ t r u e. \ \end{array} $$

Remark The "sort of shunting" - instead of eliminating the $\Rightarrow$ by rewriting the demonstrandum as $\left\lbrack {{7p} \vee {p}_{;}p}\right\rbrack -$ was introduced in the polishing phase ; it is purely cosmetic. (End of Remark.)

Remark In the context in which this problem was posed,

(5) $\left\lbrack {\left( {p \land x}\right) ;y \equiv p \land x;y}\right\rbrack$ for left-condition $p$

had been established. Rutger M. Dýksha used it to establish (2) without ping-pong argument :

$$ t r u e $$

$$ \begin{array}{l} = {(5) \mathrm {w i t h} x, y := \mathrm {t r u e}, p } \ [ (p \wedge t r u e); p \equiv p \wedge t r u e; p ] \ = {\mathrm {p r e d . c a l c .}; \mathrm {r e l . c a l c .} } \ [ p; p \equiv p ] \ \end{array} $$

(End of Remark.)

It is customary to denote the strongest solution

[{x}_{1} : \left\lbrack {a,b,x \Rightarrow x}\right\rbrack ]

by $a^*$ - read "a star" and called "the reflexive transitive closure of $a$ ". In EwD1136 we compared proofs for the theorem that, in our new terminology, the strongest solution of

$$ x: [ b \vee a; x \Rightarrow x ] $$

is $a^*$ ; b. Knowing the theorem of Knaster-Tarski, we see that all this is expressed by

(6) $\left\lbrack J \vee a;{a}^{ * } \equiv {a}^{ * }\right\rbrack$ $\left\lbrack {b \vee a;x \Rightarrow x}\right\rbrack \Rightarrow \left\lbrack {{a}^{ * };b \Rightarrow x}\right\rbrack$

(Formula (6) expresses that $a^$ solves the first equation; (7) with $b := J$ expresses that $a^$ implies all its solutions. Applying the postfix operator " $j$ b" to both sides of (6) tells us that $a^$ ;b solves the second equation, while (7) expresses that $a^$ ;b implies all its solutions.)

Following the traditions, we shall give the postfix operator * in its exponential position a higher binding power than all other (relational and logical) operators. (In a note about notation, I should probably argue in favour of a prefix operator, but this note is about proof design.)

We are now going to show that \~ and * commute - distribute over each other-, i.e.

$$ [ (\sim s) ^ {} \equiv \sim s ^ {} ] \tag {8} $$

Because of the structure of (7), proofs of theorems about extreme solutions are often ping-pong arguments. We shall first demonstrate ping: it is a proof largely constructed on the principle "there is only one thing you can do". [It is therefore not a tribute to RMD, who produced the following proof almost verbatim.]

$$ \begin{array}{l} [ (\sim s) ^ {} \Rightarrow \sim s ^ {} ] \ \Leftrightarrow {(\mathbf {7}) \mathrm {w i t h} a, b, x := \sim s, J, \sim s ^ {} } \ [ ] \vee \sim s; \sim s ^ {} \Rightarrow \sim s ^ {} ] \ = {\mathrm {r e l a t i o n a l c a l c u l u s}, \mathrm {a p p l y i n g} \sim \mathrm {t o b o t h s i d e s} } \ [ ] \vee s ^ {}; s \Rightarrow s ^ {*} ] \ \end{array} $$

The first step is dictated, because (7) is our only tool for concluding that a closure implies something. The "intuitive" calculator will justify the next step as "cleaning up", as a way of removing a large number of tildes. The conscious calculator will realize, that we can deal - see (7)- with a demonstrandum where the closure is the left argument of a composition; hence the decision to apply $\sim$ to both sides. Next, heading for a re-application of (7), we had better find a way of removing "jv" from the antecedent.

The only other place where J occurs is (6), so that is what we appeal to - in the hint I have recorded the direction of the appeal

$$ [ J \vee S ^ {}; S \Rightarrow S ^ {} ] $$

$$ \begin{array}{l} \Leftrightarrow {6 } \Rightarrow w i t h a := s } \ [ ] \vee s ^ {}; s \Rightarrow ] \vee s; s ^ {} ] \ \Leftarrow {m o n o t h o n i a i l y o p v } \ [ s ^ {}; s \Rightarrow s; s ^ {} ] \ \end{array} $$

and now we have again a demonstrum

with an antecedent to which (7) is applicable.

so full of faith we coninue:

$$ [ s ^ {}; s \Rightarrow s; s ^ {} ] $$

$$ \begin{array}{l} \Leftrightarrow {(\mathbf {7}) \mathrm {w i t h} a, b, x := s, s, s; s ^ {} } \ [ s \vee s; s; s ^ {} \Rightarrow s; s ^ {} ] \ = {\quad ; \quad w e r v } \ [ s; () \vee s; s ^ {}) \Rightarrow s; s ^ {} ] \ \Leftrightarrow {\quad ; \mathrm {m o n o t o n i c i n 2 n d a r g u m e n t} } \ [ ] \vee s; s ^ {} \Rightarrow s ^ {*} ] \ = {\left(6\right) \Rightarrow \mathrm {w i t h} a := s } \ f r u e _ {n} \ \end{array} $$

In passing we note that we did not need the theorem of Knaster-Tarski : the proof could as well have been carried out , had (6) been replaced by the - formally much! - weaker

$$ (6!) \quad [ ] \vee a; a ^ {} \Rightarrow a ^ {} ] $$

I interpret this observation as a further confirmation of my suspicion that it is misleading

to call a* the strongest Fixpoint of

$\left\langle {\lambda x;\operatorname{Jv}a;x}\right\rangle :$ there are too many arguments

Having proved $\left\lbrack {{\left( \sim s\right) }^{ * } \Rightarrow \sim {s}^{ * }}\right\rbrack$ for all $s$ ,pong is now easy: the calculation below

$$ t r u e $$

$$ \begin{array}{l} = \begin{array}{l} {\text {p i n g w i t h} s := \sim s } \ [ (\sim s) ^ {} \Rightarrow \sim (\sim s) ^ {} ] \end{array} \ = \begin{array}{l} {{\sim i s a n i n v o l u t i o n }} \ {[ s ^ {} \Rightarrow \sim (\sim s) ^ {} ]} \end{array} \ = {\mathrm {t r a n s p o s i t i o n} } [ \sim s ^ {} \Rightarrow (\sim s) ^ {} ] \ \end{array} $$

establishes pong, and hence (8) has been proved.

Reading the proof on the previous page, line $\neq$ shows that we have proved a next ping: $[s^{};s\Rightarrow s;s^{}]$ for all s. The calculation below

$$ \begin{array}{l} t r u e \ = \left{ \begin{array}{l} \text {p i n g w i t h} s := \sim s \ [ (\sim s) ^ {} ]; \sim s \Rightarrow \sim s; (\sim s) ^ {} ] \end{array} \right} \ = \left{ \begin{array}{l} (8) \end{array} \right} \ = {r e l. c a l c. } [ \sim (s; s ^ {4}) \Rightarrow \sim (s ^ {4}; s) ] \ = {\mathrm {t r a n s p o s i t i o n} } \ \end{array} $$

$$ [ s; s ^ {} \Rightarrow s ^ {}; s ] $$

establishes the corresponding pong, hence

(9) $[s^{}; s \equiv s; s^{}]$

As a final example of the use of (6) and (7) we shall show that $*$ is a closure, i.e. monotonic, weakening, and idempotent.

• is monotonic. We have to show for arbitrary s and t that

$$ [ s \Rightarrow t ] \Rightarrow [ s ^ {} \Rightarrow t ^ {} ] $$

The proof is standard:

$$ [ s ^ {} \Rightarrow t ^ {} ] $$

$\Leftrightarrow \;\left{ \begin{array}{l} \text{ (7 ) with } a,b,x \mathrel{\text{:=}} s,} ,{t}^{x}} \ \end{array}\right.$

$\Leftrightarrow \;\left{ {\left( 6\right) \Rightarrow \text{with}a : = t}\right}$

[\left. \left{ \begin{array}{l} \text{monotonicities} \ \end{array}\right. \right} ]

$$ \begin{array}{l} [ ] \vee s; t ^ {} \Rightarrow t ^ {} ] \ [ J \vee s; t ^ {} \Rightarrow J \vee t; t ^ {} ] \ [ s \Rightarrow t ] \ \end{array} $$

Note that we did not need Knaster-Tarski. Remark The fact that we first appealed to (7) and then to (6) is not essential, but in this order it works better; in the other order we would need a second appeal to (6). (End of Remark.)

• is weakening We have to show for arbitrary s

that

$$ [ s \Rightarrow s ^ {*} ] $$

Since this is a demonstrandum with $s^*$ as consequent, (7) is in this context irrelevant, and we shall only appeal to (6). This is perhaps the place to remark that (when we are not interested in Knaster-Tarski) we can draw to separate conclusions from (6)

(10) $\left\lbrack J \Rightarrow {a}^{ * }\right\rbrack$ [\left\lbrack {a;a}^{ * } \Rightarrow {a}^{ * }\right\rbrack ]

We now observe

$$ s ^ {*} $$

$$ \begin{array}{l} \Leftrightarrow \quad {(1 1) \mathrm {w i t h} a := s } \ s; s ^ {*} \ \end{array} $$

$\Leftrightarrow { {10}}$ with $a \mathrel{\text{:=}} s$ ,monotonicity of

$$ \begin{array}{l} s; J \ = {\mathrm {r e l a t i o n a l c a l c u l u s} } \ \mathfrak {s} \ \end{array} $$

* is idempotent We have to show for arbitrary s that $[s^{**} \equiv s^{\star}]$ , but since we have just shown that * is weakening, it suffices to show that for any $s$

$$ [ s ^ {} \Rightarrow s ^ {} ] $$

To this end we observe for any $s$

$$ [ s ^ {} \Rightarrow s ^ {*} ] $$

$$ \begin{array}{l} \Leftrightarrow {(\mathbf {7}) \mathrm {w i t h} a, b, x := s ^ {}, J, s ^ {} } \ [ ] \vee s ^ {}; s ^ {} \Rightarrow s ^ {} ] \ = {1 0 \mathrm {w i t h} a := s } \ [ s ^ {}; s ^ {} \Rightarrow s ^ {} ] \ \Leftrightarrow {(7) \mathrm {w i t h} a, b, x := s, s ^ {}, s ^ {} } \ [ s ^ {} \vee s; s ^ {} \Rightarrow s ^ {} ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ s; s ^ {} \Rightarrow s ^ {*} ] \ = {(1 1) \mathrm {w i t h} a _ {i} = s } \ t r u e. \ \end{array} $$

In the above proof I can think of only one place where we could have gone wrong:

$$ [ s ^ {}; s ^ {} \Rightarrow s ^ {*} ] $$

$$ \begin{array}{l} \Leftrightarrow {\mathrm {m o n o t o n i c i h y} } \ [ s ^ {*} \Rightarrow ] \ \end{array} $$

With the amount of annotation decreasing so rapidly, this EWD had better be concluded.

Austin, 13 November 1992

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin

Austin, TX 78712 - 1188

USA