Total-order junctivity

Total-order junctivit y

Continuity -see [0],p.87- is a special case of total-order junctivity. A set $S^{\prime}$ of predicate transformers is totally ordered iff

$$ \langle \forall x, y: x \in S \land y \in S: [ x \Rightarrow y ] \lor [ x \Leftarrow y ] \rangle $$

and a predicate transformer is called "total-order junctive" iff it is junctive over totally ordered sets of predicates. We leave to the reader the proof of -see [0], p.84 -

$S$ is totally ordered $\equiv {S}^{ * }$ is totally ordered

and also of "any total-order junctive predicate transformer is monotonic". We now generalize Theorem (6.43) of [0] - see p.99- to

Theorem DisjunctiOn preserves total-order conjunctivity, i.e. let predicate transformer $f$ be given in terms of the total-order conjunctive predicate transformers $g$ and $h$ by

$$ [ f. x \equiv g. x \vee h. x ] \quad f o r a l l x; $$

then $p$ is total-order conjunctive.

Proof In this proof, $x$ and $y$ range over an arbitrary totally ordered set. Our proof obligation is then to show

$$ [ f. \langle \forall x:: x \rangle \equiv \langle \forall x:: f. x \rangle ] $$

To this end we observe

$$ \begin{array}{l} f. \langle \forall x: x \rangle \ = {\mathrm {d e f . o f} f \mathrm {a n d r e n a m i n g a d u m m y} } \ g. \langle \forall x: x \rangle \sim h. \langle \forall y: y \rangle \ = {g a n d h t o t a l - o r d e r c o n j u n c t i v e } \ \langle \forall x: g. x \rangle \vee \langle \forall y: h. y \rangle \ = {\text {d i s t r i b u t e} \vee \text {o v e r} \forall ; \text {u n n e s t i n g} } \ \langle \forall x, y: g. x \vee h. y \rangle \ = {\mathrm {r a n g e i s t o t a l l y o r d e r e d} } \ \langle \forall x, y: [ x \Rightarrow y ]: g. x \vee h. y \rangle . \ \langle \forall x, y: [ x \Leftarrow y ]: g. x \vee h. y \rangle \ = {\mathrm {n e s t i n g} } \ \langle \forall x: \langle \forall y: [ x \Rightarrow y ]: g. x \vee h. y \rangle \rangle \land \ \langle \forall y: \langle \forall x: [ x \Leftarrow y ]: g. x \vee h. y \rangle \rangle \ = {h m o n o t o n i c; g m o n o t o n i c } \ \langle \forall x: g. x \vee h. x \rangle \wedge \langle \forall y: g. y \vee h. y \rangle \ = {\mathrm {d e f} _ {p} o f f } \ \langle \forall x: f. x \rangle \ \end{array} $$

(End of Proof.)

The analog of Theorem (5.116) of [0] -see

With $f$ monotonic in both arguments and

$$ [ \langle \forall x, y: f. x. y \rangle \equiv \langle \forall x: f. x. x \rangle ] \quad , $$

which we could have appealed to in the above proof. All this is more general, cleaner

and simpler than in [0]. For the sake of com- pleteness (and having just started a new page) we prove the last theorem by observing

$$ \begin{array}{l} \langle \forall x, y: f. x. y \rangle \ = {\mathrm {r a n g e} _ {n} ^ {1} \mathrm {t o t a l l y o r d e r e d} } \ \langle \forall x, y: [ x \Rightarrow y ]: f. x. y \rangle \land \langle \forall x, y: [ x \Leftarrow y ]: f. x. y \rangle \ = {\mathrm {n e s t i n g} } \ \langle \forall x: \langle \forall y: [ x \Rightarrow y ]: f. x. y \rangle \rangle \land \langle \forall y: \langle \forall x: [ x \Leftarrow y ]: f. x. y \rangle \rangle \ = {f _ {\mathrm {m o n o t o n i c}} \mathrm {i n} \mathrm {b o t h a r g u m e n t s} } \ \langle \forall x: p. x. x \rangle , \land \langle \forall y: p. y. y \rangle \ = {\mathrm {p r e d . c a l c .} } \ \langle \forall x: f. x. x \rangle \ \end{array} $$

All this has been triggered by a theorem in the thesis of Ernie Cohen.

Austin, 16 October 1992

prof. dr. Edsger W. Dijkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712 - 1188

USA

[0] Edsger W. Dýkstra and Carel S. Scholten, Predicate Calculus and Program Semantics, Springer-Verlag, New York - Berlin-Heidelberg, 1990