On extreme solutions

Introductory Remark Following Misra, I shall use the dedicated parenthesis pair $\langle \rangle$ to define lineate the scope of dummies. Following J.L.A. van de Sneepscheut, I shall write the quantifier to the left of the opening parenthesis. Finally, I shall use $\forall$ and $\exists$ , but not for very good reason: it can be argued that $\Delta$ and $\underline{\vee}$ are to be preferred. (End of Introductory Remark.)

Let $E$ - read "below" be a punctual relation on structures of some type, i.e.

$$ \begin{array}{l} [ u = v \land x = y \Rightarrow (u \leq x \equiv v \leq y) ] f o r a l l \ u, v, x, y \ \end{array} $$

In EWD1102, we have shown that for $\varepsilon$ a preorder -i.e. a reflexive and transitive relation

(0) $\left\lbrack {x \leq y \equiv \forall \langle z : z \leq x \Rightarrow z \leq y\rangle }\right\rbrack$ and (1) $\left\lbrack {x \leq y \leq x}\right\rbrack \Rightarrow \forall \left\langle {z : x \leq z \Leftrightarrow y \leq z}\right\rangle \Rightarrow$

Furthermore, for a preorder $\varepsilon$ , a value $k$ satisfying $\forall 1 < x\left\lbrack {x \leq k \equiv \forall 1 < y : y \in W : x \leq f,y}\right\rbrack >$

is called a highest lower bound for the set ${ z \mid \exists \langle y : y \in W : \left\lbrack {z = f \cdot y}\right\rbrack } .$ (Note that,for equal

to the identity function, i.e. $\forall \left\langle {y : \left\lbrack {f.y = y}\right\rbrack }\right\rangle$ ,the $k$ satisfying (2) is a highest lower bound of the set $W$ .) A lowest higher bound of that set is,similarly,a value $h$ satisfying

(3) $\forall \langle x : \left\lbrack {h \leq x \equiv \forall y : y \in W : f \cdot y \leq x}\right\rbrack \rangle$

We remind the reader that the names "highest lower bound" and "lowest higher bound" only make sense because we have chosen to pronounce the character as below.

*

Let us now investigate, how we can ensure that (2), viewed as equation in k , does not have more than 1 solution. Let $k^{\prime}$ satisfy

$\forall 1 < x \leq {k}^{\prime } \leq \forall \langle y : y \in W : x \leq f,y\rangle \rbrack$

demonstrating uniqueness of the highest lower bound then amounts to demonstrating. [k=k'] We observe

true

$$ \begin{array}{l} = \left{ \begin{array}{l l} (2) \mathrm {w i t h} x := k \end{array} \right} \ [ k \leq k \equiv \forall \langle y: y _ {i} \in W: k \in f \cdot y \rangle ] \ = {\leq i s r e f l e x i v e } \ [ \forall \langle y: y \in W: k \leq f. y \rangle ] \ = {2 ^ {1} \mathrm {w i t h} x := k } \ [ k \in k ^ {\prime} ] \ \end{array} $$

The transpose $\left\lbrack {{k}^{\prime } \leq k}\right\rbrack$ can be derived similarly.

In order to conclude now $[k = k^{\prime}]$ , we assume 5 to be antisymmetric as well, i.e.

$$ [ x \leq y \land y \leq x \Rightarrow x = y ] $$

A relation that is reflexive, transitive, & antisymmetric is called a partial order. For the rest of this note, $\equiv$ denotes a partial order.

By restricting ourselves for $\varepsilon$ to a partial order, we ensure that at most 1 value $k$ satisfies (2) and at most 1 value $h$ satisfies (3). But there may be none! From now onwards we restrict ourselves for $\varepsilon$ to such partial orders that a $k$ and $h$ , satisfying (2) and (3) respectively, always exist, i.e. for the rest of this note, each set has a unique lowest higher bound and a unique highest lower bound.

The lowest higher bound of the universe - i.e. $y \in W \equiv$ true and $\left\lbrack {f,y = y}\right\rbrack -$ is tradi- tionally called "top" and denoted by "T"; it is also the highest lower bound of the empty set -i.e. $y \in W \equiv$ false. In order to demonstrate this dual role of $T$ we observe

$= { \left( 3\right)$ with $h : = T,y \in W \equiv$ true, ${f}_{y} = y}$

(T is the highest lower bound of the empty set).

$$ \begin{array}{l} \forall \langle x: [ T \leq x \equiv \forall \langle y: y \leq x \rangle ] \rangle \ \Rightarrow \quad {\mathrm {i n s t a n t i a t e w i t h} x := T } \ [ T \in T = \forall (y: y \in T) ] \ = {\leq i s r e f l e x i v e; r e n a m i n g d u m m y } \ [ \forall \langle x:: x \leq T \rangle ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ \forall \langle x: [ x \leq T \equiv \forall \langle y: f a s e: x \leq y \rangle ] \rangle \ = {(2) \mathrm {w i t h} k = T, y \in W \equiv \mathrm {f a l s e}, f y = y } \ \end{array} $$

Since (2) and (3) determine the bounds

uniquely, we don't need to demonstrate the

inverse implication (which is much harder).

Similarly, the highest lower bound of the universe is also the lowest higher bound of the empty set; it is traditionally called "bottom" and denoted by "⊥".

The extreme bounds now being unique, we are going to experiment with a functional notation. We denote the value $k$ satisfying

(2) by $\pi \left\langle {y : y \in W : f.y}\right\rangle$ ,and the value $h$

satisfying (3) ${by}\;L\langle y : y \in W : f.y\rangle$ , i.e.

the highest lower bound $\pi$ is defined by

(4) $\forall \langle x : \left\lbrack {x \subseteq \pi \langle y : y \in W : f.g.}\right\rbrack \equiv$

$$ \forall \langle y: y \in W: x \leq f. y \rangle ] \rangle $$

and the lowest higher bound is defined by

(5) $\forall 1 < x : \left\lbrack {L \mid l,y : y \in W : f.y}\right\rbrack \leq x \equiv$

$$ \forall \langle y: y \in W: f. y \leq x \rangle ] \rangle $$

The equivalent expressions are in both formulae so similar that doubts about the usefulness of $\Pi$ and $U$ could be voiced .

The extreme bounds are monotonic in the following sense - we formulate and prove for $\pi$

$$ \begin{array}{l} [ \forall \langle y: y \in W: f. y \in g. y \rangle \Rightarrow \ \pi \langle y: y \in W: f \cdot y \rangle = \pi \langle y: y \in W: g \cdot y \rangle ] \ \end{array} $$

Proof We observe

$$ \begin{array}{l} \pi \langle y: y \in W: f. y \rangle \leq \pi \langle y: y \in W: g. y \rangle \ = {() } \ \end{array} $$

$$ \begin{array}{l} \forall \langle z: z \leq \Pi \langle y: y \in W: f _ {y} \rangle \Rightarrow z \leq \Pi \langle y: y \in W: g _ {y} \rangle \rangle \ = {(4) \mathrm {t w i c e} } \ \forall \langle z:: \forall \langle y: y \in W: z \leq f _ {.} y \rangle \Rightarrow \forall \langle y: y \in W: z \leq g _ {.} y \rangle) \ \Leftrightarrow {\mathrm {m o n o t o n i c i t y} o f \forall } \ \forall \langle z: \forall \langle y: y \in W: z \notin f. y \Rightarrow z \in g. y \rangle \ = {\mathrm {i n t e r c h a n g e o f u n i v e r s a l q u a n t i f i c a t i o n s} } \ \forall \langle y: y \in W: \forall z: z \leq f. y \Rightarrow z \leq g. y \rangle \ = {(\bar {0}) } \ \forall \langle y: y \in W: f \cdot y \leq g \cdot y \rangle \ \end{array} $$

Note how (0) is used "in both directions": to introduce and to eliminate again the universal quantification over $z$ . (End of Proof.)

In the above the symbol $\Pi$ is primarily used to formulate the theorem; in the proof, the symbol $\Pi$ is eliminated as soon as possible.

We leave to the reader the proofs of

$$ \begin{array}{l} V \subseteq W \Rightarrow [ \Pi \langle y: y \in W: f. g \rangle \subseteq \Pi \langle y: y \in V: f. g \rangle ] \land \ [ U \langle y: y \in V: f _ {y} \rangle \subseteq U \langle y: y \in W: f _ {y} \rangle ] \ \end{array} $$

The proofs are very similar to what we just saw.

Function $f$ is monotonic means here

$\left\lbrack {x \leq y}\right\rbrack \Rightarrow \left\lbrack {f \cdot x \leq f \cdot y}\right\rbrack$

For monotonic $f$ we can prove (7) & (8)

(7) $\left\lbrack {f.\pi \left\langle {y : y \in W : y}\right\rangle \leq \pi \left\langle {y : y \in W : f.y}\right\rangle }\right\rbrack$ (8) $\left\lbrack {U\left\langle {y : y \in W : f \cdot y}\right\rangle \leq f.} \cup \left\langle {y : y \in W : y}\right\rangle }\right\rbrack$

we shall prove (7).

Proof In the following we leave the range "yew" understood and observe for any monotonic

$$ \begin{array}{l} [ f. \pi \langle y: y \rangle \leq \pi \langle y: f \cdot y \rangle ] \ = {(\lambda_ {1}) \mathrm {w i t h} x := f \cap \langle y; y \rangle } \ [ \forall \langle y: f. \pi \langle y: y \rangle \leq f. y ] \ = {\mathrm {i n t e r c h a n g e} } \ \forall \langle y: [ f. \cap \langle y: y \rangle , = f. y ] \rangle \ \Leftarrow {f m o n o t o n i c } \ \end{array} $$

$$ \begin{array}{l} \forall \langle y: [ \pi \langle y: y \rangle \leq y ] \rangle \ = {(0), \mathrm {s e e N o t e b e l o w} } \ \forall \langle y: [ \forall \langle z: z \in \pi \langle y: y \rangle \Rightarrow z \in y ] \rangle \ = {(4) \mathrm {w i t h} x, f := z, \mathrm {i d e n t i t y} } \ \forall \langle y: [ \forall \langle z: \forall \langle y: z \leq y \rangle \Rightarrow z \leq y ] \rangle \ = {\text {p r e d i c a t e c a l c u l u s} } \ t r u e \ \end{array} $$

(End of Proof.)

Note The appeal to (0), rather than to (1), is to get $\pi < y\because y >$ as right-hand operand of $E$ ,as -see (4)- we need $\pi$ there in order to be able to eliminate it. (End of Note.)

Now we are ready for the theorem of Knaster-Tarshi:

For monotonic $f$ ,the equations

(9) $x : \left\lbrack {f.x \leq x}\right\rbrack$

and

(10) $x : \left\lbrack {f.x = x}\right\rbrack$

both have a lowest solution, and the two lowest solutions are the same.

Proof We define $g\;{by}$

$$ [ q = \pi \langle y: [ f. y \leq y ]: y \rangle ] $$

and observe, in order to prove that $q$ solves (9):

$$ \begin{array}{l} f. q \ = {\mathrm {d e p . o f} q } \ p. \pi \langle y: [ f \cdot y \leq y ]: y \rangle \ \equiv {f \mathrm {i s m o n o t u n i c}, (7) } \ \pi \langle y: [ f. y \leq y ]: f. y \rangle \ E \quad {N i s m o n o t o n i c } \ \pi \langle y: [ f. y \leq y ]: y \rangle \ = {\mathrm {d e f . o f} q } \ \end{array} $$

$$ q \quad , $$

which observation establishes $\left\lbrack {p,q \leq q}\right\rbrack$ thanks

to the transitivity of $5;{S}_{0}q$ is a

solution of (9), and it is its lowest

solution, for we observe

$\forall < y : \left\lbrack {p,y \leq y}\right\rbrack : q \leq y$

$$ \begin{array}{l} = {\mathrm {d e p} o f n } \ 9 \leq \pi \langle y: [ p, y \leq y ]: y \rangle \ = {\mathrm {d e f . o f} q, E \mathrm {i s r e f l e x i v e} } \ t r u e \ \end{array} $$

Next we observe

$$ \begin{array}{l} \begin{array}{r l} {[ p. q = q ]} & \ {\Leftrightarrow \quad {\mathrm {5 i s a n t i s y m m e t r i c} }} \end{array} \ [ f \cdot q \leq q ] \land [ q \leq f \cdot q ] \ \Leftrightarrow {1 1) w i t h y := f \cdot g } \ [ f. q \leq q ] \land [ f. (f. q) ^ {\prime} \leq f. q ] \ \Leftrightarrow \quad \left{ \begin{array}{l l} p _ {i s m o n o t o n i c} \ [ f, q ] \end{array} \right. \ = {q \mathrm {s o l v e s} (9) } \ \end{array} $$

true

so $q$ solves (10) as well. Moreover, $q$ is the lowest solution of (10), as follows from the observation

$$ \begin{array}{l} \begin{array}{r l} & {\forall \langle y: [ f. y = y ]: q \leq y \rangle} \ {\iff} & {{[ f. y = y ] \Rightarrow [ f. y \leq y ], a s \equiv r e f p e x i v e }} \ & {\forall \langle y: [ f. y \leq y ]: q \leq y \rangle} \end{array} \ = \begin{array}{l} {{\mathrm {1 1} }} \ {\mathrm {t r u e .}} \end{array} \ \end{array} $$

We now consider the equation

$$ (1 2) \quad x: [ f. x. y \leq x ] $$

We assume $f$ .x.y to be a monotonic function of both arguments. We have just seen that $f$ 's monotonicity in its 1st argument guarantees the existence of a lowest solution of (12). We denote it by g.y , its being a solution expressed by

$$ (1 3) \qquad [ f. (g \cdot y). y \equiv g \cdot y ] \qquad \mathrm {f o r a l l} y $$

$$ \begin{array}{l} a n d i t s b e i n g a s l o w a s a n y s o l u t i o n e x p r e s s e d b y \ (1 4) \qquad [ f. x. y \leq x ] \Rightarrow [ g. y \leq x ] \quad \mathrm {f o r a l l} x, y \ \end{array} $$

(Here we mention (13) and (14) as properties of $g$ ; they do, in fact, determine $g$ .)

It is well-known that $g$ is monotonic if $f$ is monotonic in its 2nd argument. I used to demonstrate that by observing

$$ [ g, p ] = [ g, q ] $$

$\Leftrightarrow \;{f}^{\prime }\left( x\right) = {h}^{\prime }\left( x\right)$

$$ [ f. (g \cdot q). p \leq g \cdot q ] $$

$\Leftrightarrow { \left( {13}\right)$ with $y = 9$ ,transitivity $p \in }$

$$ [ f. (g. q). p \leq f. (g. q). q ] $$

$\Leftrightarrow$ {f monotonic in 2nd argument}

$$ [ p \equiv q ] $$

QED

But because

$$ [ g, y \equiv \Pi \langle x: [ f. x, y \leq x ]: x \rangle ] $$

we can write alternatively

$\left( *\right) \;\left\lbrack {\neg \langle x : \left\lbrack {f.x.p \leq x}\right\rbrack : x\rangle \leq \neg \langle x : \left\lbrack {f.x.q \leq x}\right\rbrack : x\rangle }\right\rbrack$ $\Leftrightarrow$ ${ {r}_{\text{range monotonicity }}} \cap \pi$ ,see EWD1107-5 $\Leftrightarrow \left{ {\text{transitivity of }\rho }\right. \equiv }$ $\Leftrightarrow { f}$ monotonic in $2\mathrm{{nd}}$ argument

Comparing the two proofs, we see that, in the latter proof, there was no need to formulate (13) and (14); we could even have done without the function name $g$ , as we could have taken (*) as the consequent of our proof obligation. The latter proof has the

disadvantage -if it is one- of needing the theorem about the range monotonicity of $\Pi$ , but the charm that after the first step, all traces of extreme solutions have disappeared. Notice, in contrast, that in the former proof the intermediate result after the second step $[f.(g,q).p \equiv f.(g,q).q]$

still mentions the no longer relevant function $g$ .

In the writing of this note, there was a sizeable intermission, and in the mean time the quantifiers like $\forall$ and $\Pi$ moved back inside the angular brackets. I owe to David A. Naumann the observation that

$$ \langle \forall x: r. x: t. x \rangle $$

can be viewed as an abbreviation for

$$ (\forall \langle x: r. x: f. x \rangle) $$

This abbreviation is most welcome because a parenthesis pair around the quantifier is needed as soon as a function is applied to a quantified expression.

I owe to J.R. Rao the theorem that for $f$ monotonic in both arguments

$$ [ \langle N x: [ f. x. x \leq x ]: x \rangle = \langle N x: [ \langle N y: [ f. x. y \leq y ]: y \rangle \leq x ]: x \rangle ]. $$

With a specific notation for the lowest fixpoint - applicable thanks to Knaster-Tarski - we can abbreviate the statement of the theorem to

$$ [ \langle \mu x: f. x. x \rangle = \langle \mu x: \langle \mu y: f. x. y \rangle ] $$

which looks a lot nicer, but is not nice enough. To show that the right-hand side is a fixpoint of $\langle \lambda x: f.x.x \rangle$ , one has to show

$$ \begin{array}{l} [ f. \langle \mu x: \langle \mu y: f. x. y \rangle ]. \langle \mu x: \langle \mu y: f. x. y \rangle \rangle = \ \langle \mu x: \langle \mu y: f. x. y \rangle \rangle ] \ \end{array} $$

and these formulae become unwieldy. Naming

(a) $\left\lbrack {f.x.\left( {g.x}\right) = g.x}\right\rbrack$ (b) $\left\lbrack {f{x}{1}y \leq y}\right\rbrack \Rightarrow \left\lbrack {g{x}{2} \leq y}\right\rbrack$ (c) $\left\lbrack {G \cdot K = K \cdot }\right\rbrack$ [\left\lbrack {G \times \leq x}\right\rbrack \Rightarrow \left\lbrack {K \leq x}\right\rbrack ]

and shall prove about them

(e) $\left\lbrack {f.K.K = K}\right\rbrack$ $\left( p\right) \left\lbrack {p.x. \leq x}\right\rbrack \Rightarrow \left\lbrack {k \leq x}\right\rbrack$

Note that in the above we have exploited Knaster-Tarshi by choosing (a) through (d) formally as strong as possible; it turns out that for the demonstrandum we can do the same.

The appeal to Knaster-Tarski is our only use of the monotonicity of $f$ . To fulfill our proof obligations,we observe for any

to prove (e):

$$ [ p, k, k = k ] $$

$$ = {(c) \mathrm {t w i c e} } $$

$$ [ f. k. (g. k) = g. k ] $$

$$ = {(a) w i t h x := k } $$

true

to prove (f)

$$ \begin{array}{l} [ K \leq x ] \ \Leftrightarrow \quad {(d) } \ [ G. x \equiv x ] \ \Leftrightarrow {(\mathcal {B}) \mathrm {w i t h} y := x } \ [ f. x. x \in x ] \ \end{array} $$

Note that the left column is entirely formulated in terms of the "tolerant equations" whereas the right-hand column uses the "tolerant equations". The whole left-hand calculation is independent of the partial order $\varepsilon$ , it only deals with the fixpoint issue. It is unclear to me to what extent the possibility of the above rigorous separation of concerns could have been predicted on general principles. (Such principles would be of great heuristic value.)

When comparing notational alternatives using $\Pi$ or $\mu$ , lines (a) through (f) should be included in counting the number of lines of the above proof, for they record what otherwise would be standard properties of $\Pi$ or $\mu$ . The reader is invited to reformulate the above, say, in terms of $\mu$ ; it will make him appreciate the conciseness of the above.

We now consider a new type of equation, viz

$$ x: [ f. x \leq y ] $$

and define $h.y$ to be the lowest higher bound of its solution set, i.e.

$$ (1 5) \quad [ h, y = \langle U x: [ f. x \in y ]: x \rangle ] \quad , $$

from which, using (5) and the reflexivity, one can derive in a few steps that for any $x,y$

$$ (1 6) \qquad [ f. x \leq y ] \Rightarrow [ x \leq h. y ] \qquad . $$

Our next theorem states now the equivalence of the following three assertions

$$ \begin{array}{l} (1 7) f d i s t r i b u t e s o v e r U \ (1 8) f i s m o n o t o n i c a n d [ f. (h. y) \equiv y ] \ (1 9) \mathrm {t h e r e} \mathrm {e x i s t s a f u n c t i o n g , u n i q u e l y} \ [ f. x \leq y ] = [ x \leq g. y ] \tag {20} \ \end{array} $$

and it equals $h$ ,as defined by (15).

Before proceeding with the proof we first draw two general conclusions we should have drawn earlier. By instantiating (s) with $x \mathrel{\text{:=}} \langle {Uy} : y \in W : P.y\rangle$ we derive, because $E$ is reflexive

$$ \begin{array}{l} \langle \forall y: y \in W: [ f. y \leq \langle U y: y \in W: f. y \rangle ] \rangle , \ i. e. U i s i n d e e d a h i g h e r b o u n d. \ \end{array} $$

Investigating about the simplest example in which we can use this, we observe for any $p,q,p$

$$ \begin{array}{l} \langle U z: z \in {p, q }: f. z \rangle = f. q \ = {\xi \mathrm {i s a n t i s y m m e t r i c} } \ \langle U z: z \in {p, q }: f. z \rangle \leq f. q \wedge f. q \leq \langle U z: z \in {p, q }: f. z \rangle \ = {2 1) w i t h y, W := q, {p, q } } \ \langle U _ {2}: z \in {p, q }: f. z \rangle \leq f. q \ = {(5) \text {w i t h} W, x := {p, q }, f, g } \ \langle \forall z: z \in {p, q }: f. z \leq f. q \rangle \ = {\mathrm {r a n g e} \mathrm {s p i t} \mathrm {a n d o n e - p o i n t r u l e} } \ f \cdot p \leq f \cdot q \land f \cdot q \leq f \cdot q \ = {\mathrm {E} i s r e f l e x i v e } \ f \cdot p \equiv f \cdot q \qquad , \qquad h e n c e \ \end{array} $$

And now we proceed with the proof of the equivalence of (17), (18), and (19).

Proof The proof is by cyclic implication.

To demonstrate the monotonicity of $f$ we observe for any $p,q$

$$ \begin{array}{l} (2 2) \quad [ \langle U z: z \in {p, q }: f. z \rangle = f. q \equiv f. p \equiv f. q ] \ (1 7) \Rightarrow (1 8) \ [ f, p \leq f, q ] \ = {\left(2 2\right) } \ [ \langle U _ {2}: z \in {p, q }: f. z \rangle = f. q ] \ = {(1 7), i. e. f d i s t r i b u t e s o v e r U } \ [ f. \langle U z: z \in {p, q }: z \rangle = f. q ] \ \Leftrightarrow \quad {L e i b n i z } \ \end{array} $$

$$ \begin{array}{l} [ \langle U z: z \in {p, q }: z \rangle = q ] \ = {(2 2) \mathrm {w i t h} f \mathrm {t h e i d e n t i t y f u n c h o n} } \ [ p \leq q ] \ \end{array} $$

and furthermore we observe

$$ \begin{array}{l} [ f. (h. y) \leq y ] \ = {(1 5), i. e. d e p. o f h, y } \ [ f. \langle U x: [ f. x \leq y ]: x \rangle \leq y ] \ = {(1 7): f d i s t r i b u t e s o v e r L } \ [ \langle U x: [ f. x \leq y ]: f. x \rangle \leq y ] \ = {(5), i. e. d e p. o p U } \ [ \langle \forall x: [ f. x \leq y ]: f. x \leq y \rangle ] \ = \quad {p r e d, c a l c. } \ t r u e \ \end{array} $$

(End of Proof of $\left( {17}\right) \Rightarrow \left( {18}\right) .$ )

$$ (1 8) \Rightarrow (1 9) $$

We show the existence of a $g$ satisfying

(20) by showing that $h$ is a suitable without any assumptions about $f$ ,

(16) gives $\mathrm{{LHS}} \Rightarrow \mathrm{{RHS}}\;$ . To show $\mathrm{{LHS}} \Leftarrow \mathrm{{RHS}}$

we observe for any $x,y$

$$ [ f. x \leq y ] $$

$$ \begin{array}{l} \Leftrightarrow {\leq s t a n s i t h e v e r s \ [ f _ {x} \leq f _ {y} (h, y) ] \land [ f _ {0} (h, y) \leq y ] \ = {1 8 } \ [ f. x \leq f. (h, y) ] \ \end{array} $$

$$ \begin{array}{l} \Leftrightarrow {(\mathrm {1 8}) }, f i s m o n o t o n i c \ [ x \le h, y ] \ \end{array} $$

To show that (20) determines $g$ uniquely,

we observe for any $x,y$

$$ \begin{array}{l} [ x \leq h, y ] \ = {\text {p r e v i o u s} \quad \text {r e s u l t} } \ [ f, x \leq y ] \ = {2 0 } \ [ x \in g \cdot y ] \ \end{array} $$

and now $\leq$ being reflexive and antisymmetric

does the rest; instantiating the above twice

with $x \mathrel{\text{:=}} h.y$ and $x \mathrel{\text{:=}} g.y\;$ we observe for any $y$

$$ f r u e $$

$$ \begin{array}{l} = {\mathrm {a b o v e r e s u l t} } \ ([ h. y \leq h. y ] = [ h. y \leq g. y ]) \land ([ g. y \leq h. y ] = [ g. y \leq g. y ]) \ = {\leq i s r e f l e x i v e } \ [ h. y \leq g. y ] \land [ g. y \leq h. y ] \ = {5 \mathrm {i s a n t h i s y m m e t r i c} } \ [ g, y = h, y ] \quad (\mathrm {E n d o f P r o o f o f} (1 8) \Rightarrow (1 9).) \ \end{array} $$

$$ (1 9) \Rightarrow (1 7) $$

We observe for any $y =$ leaving the $x$ -range out-

$$ \begin{array}{l} [ p. \langle U x:: x \rangle \leq y ] \ = \left{\left(2 0\right) \text {w i t h} x := \langle U x: x \rangle \right} \ [ \langle U x: x \rangle \subseteq g. y ] \ = {\mathrm {d e f . o f} U } \ [ \langle \forall x: x \leq g \cdot y \rangle ] \ = {\mathrm {i n t e r c h a n g e : r a n g e o f} x \mathrm {i s s c a l a r} } \ \langle \forall x: [ x \leq g, y ] \rangle \ = {(\mathbf {2 0}) } \ \end{array} $$

$$ \begin{array}{l} \langle \forall x: [ f. x \leq y ] \rangle \ {\text {i n t e r c h a n g e} } \ [ \langle \forall x: f _ {x} \leq y \rangle ] \ {\mathrm {d e f . o f} U } \ [ \langle U x: \cdot : P x \rangle \subseteq y ] \ \end{array} $$

and first and last terms being equivalent for

$$ \mathrm {a n y} y, \quad [ f. \langle U x:: x \rangle = \langle U x:: f. x \rangle ] \quad \mathrm {f o l l o w s} $$

as before. Notice that the above proof establishes the stronger $\left( {20}\right) \Rightarrow \left( {17}\right)$ .

$$ \begin{array}{l} (\mathrm {E n d o f P r o o f o f} (1 9) \Rightarrow (1 7).) \ (E n d o f P r o o f.) \ \end{array} $$

The following section deals with (2). Mutatis mutandis, the same remark can be made about (3), (4), and (5).

Because of the Principle of Leibniz, $\left\lbrack {A \equiv B}\right\rbrack \Rightarrow \left( {\left\lbrack A\right\rbrack \equiv \left\lbrack B\right\rbrack }\right)$ ,and therefore, $a$ k satisfying (2) also satisfies the weaker

(23) $\langle {\forall x\therefore [x \leq k]} \equiv \langle \forall y : y \in W : \left\lbrack {x \leq f,y}\right\rbrack \rangle$

Though weaker, (23) still determines

Proof Let ${k}^{\prime }$ satisfy

$\left( {23}^{\prime }\right) \;\left\langle {\forall x : \lbrack x \leq {k}^{\prime }}\right\rbrack \equiv \left\langle {\forall y : y \in W : \lbrack x \leq {f}^{ \cdot }y\rbrack }\right\rangle$

We now have to show $\left\lbrack {k = {k}^{\prime }}\right\rbrack$ . We observe

true

$$ \begin{array}{l} = {(2 3) } \ \langle \forall x: [ x \leq k ] \equiv \langle \forall y: y \in W: [ x \leq f _ {y} ] \rangle \rangle \ = {2 3 ^ {\prime} } \ \langle \forall x: [ x \le k ] \equiv [ x \le k ^ {\prime} ] \rangle \ \Rightarrow \quad {i n s t a n t i a t e w i t h x := k a n d x := k ^ {\prime} } \ ([ k \leq k ] \equiv [ k \leq k ^ {\prime} ]) \wedge ([ k ^ {\prime} \leq k ] \equiv [ k ^ {\prime} \leq k ^ {\prime} ]) \ = {\underline {{\underline {{5}}}} \mathrm {r e f l e x i v e} } \ [ k \leq k ^ {\prime} ] \land [ k ^ {\prime} \leq k ] \ = {\left[ \right] i s c o n j u n c t i v e } \ [ k \leq k ^ {\prime} \land k ^ {\prime} \equiv k ] \ \Rightarrow {\in s i n t i s y m m e t r i c } \ [ k = k ^ {\prime} ] \ \end{array} $$

(End of Proof.)

To gather an indication of how much we lost or gained by the introduction of $U$ , we now reformulate (17) "f distributes over $U$ ", and then redo the proofs with (17) as antecedent or consequent.

Analogous to (3) and (5) we can refer. mulate "f distributes over $W$ " by stating that for all $h$

$\left\langle {\forall y : \left\lbrack {{h}{E}y}\right. \equiv \left\langle {{v}{X} : x \in W : x \leq y}\right\rangle }\right\rbrack \Rightarrow$

$$ \langle \forall y: [ f. h \leq y \equiv \langle \forall x: x \in W: f. x \leq y ] \rangle $$

or, in the style of (23)

(25) $\left\langle {\forall y : \lbrack h \leq y}\right\rbrack \equiv \left\langle {\forall x : x \in W : \lbrack x \leq y\rbrack }\right\rangle \Rightarrow$

$$ \langle \forall y: [ f. h \leq y ] \equiv \langle \forall x: x \in W: [ f. x \leq y ] \rangle $$

We now show: (24) $\Rightarrow$ ( $f$ is monotonic). To

this end we observe for any $p,q$

true

$$ \begin{array}{l} = {(2 4) \mathrm {w i t h} h, W := q, {p, q } } \ \langle \forall y: [ q \leq y \equiv \langle \forall x: x \in {p, q }: x \leq y \rangle ] \rangle \Rightarrow \ \langle \forall y: [ p, q \leq y \equiv \langle \forall x: x \in {p, q }: p \times \leq y \rangle ] \rangle \ = {\text {r a n g e - s p l i t a n d o n e - p o i n t r u l e} } \ \langle \forall y: [ q \leq y \equiv p \leq y ^ {\prime} \land q \leq y ] \rangle \Rightarrow \ \langle \forall y: [ f. q \leq y \equiv f. p \leq y \land f. q \leq y ] \rangle \ = {\text {p r e d . c a l c u l u s} } \ [ \langle \forall y: p \leq y \Leftrightarrow q \leq y \rangle ] \Rightarrow \ [ \langle \forall y: f. p \leq y \Leftarrow f. q \leq y ] \ = {(1) } \ [ p \leq q ] \Rightarrow [ f _ {p} \leq f _ {q} ] \ \end{array} $$

The above is mathematically the same as EWD1107-14, but it is notationally simpler. So much for the first part of the proof of $\left( {17}\right) \Rightarrow \left( {18}\right)$ .

Our second obligation was to show

true

$$ = \begin{array}{l} {{\mathrm {d e f o f} h. y }} \ {\langle \forall z: [ h. y \leq z ] = \langle \forall x: [ f. x \leq y ]: [ x \leq z ] \rangle} \end{array} $$

$$ \begin{array}{l} \Rightarrow \quad {(2 5) } \ \langle \forall z: [ f. (h, y) \leq z ] \equiv \langle \forall x: [ f. x \leq y ]: [ f. x \leq z ] \rangle \ \Rightarrow \begin{array}{l} {{\mathrm {i n s t a n t i a t i o n}, z := y; \mathrm {p r e d i c a t e c a l c u l u s} }} \ {[ f. (h. y) \leq y ]} \end{array} \ \end{array} $$

This proof is not shorter than the corresponding one on p. EWD1107-15; it is not much longer either; the individual lines are.

Now we shall prove $\left( {20}\right) \Rightarrow \left( {25}\right)$ ,to be compared with the proof of (19) $\Rightarrow$ (17) on p.p. EWD1107-16/17

We observe for any $h$

$$ \langle \forall y: [ h \leq y ] \equiv \langle \forall x: x \in W: [ x \leq y ] \rangle \rangle $$

$$ \begin{array}{l} \Rightarrow \quad \left{i n s t a n t i a t i o n: y := g \cdot y \right} \ \langle \forall y: [ h \leq g, y ] = \langle \forall x: x \in W: [ x \leq g, y ] \rangle \ = {2 0) t w i c e } \ \langle \forall y: [ f. h \leq y ] \equiv \langle \forall x: x \in W: [ f. x \leq y ] \rangle \ \end{array} $$

I think this proof at least as nice as the former proof.

*

Epilogue I apologize for my ill-considered choice of identifiers: I have used f,g,h, k,x,y,z over and over again in such a way that it sometimes almost confused myself. It is partly the consequence of the fact that when I started on this, I was not sure

where it would lead me. This is more a "working

I started with a dual goal. Together with C.S. Scholten I had derived most of the above for the special case that the above is the implication, and my first purpose was writing a summary of the theory for general . After that summary had been written I found a lot of it -for those who can read enough Category Theory- in David A. Naumann's thesis.)

My second purpose was to investigate the utility of special purpose notations like $\pi$ and $U$ for tightest bounds and $\mu \& \nu$ for extreme fixpoints. I felt obliged to this investigation because I have seen these notations used but have never used them myself. I feel that this investigation has so far failed to establish their utility. If they can easily be eliminated, they are probably an example of how general mathematical reluctance to manipulate boolean expressions has led to spurious notational diversification.

Austin, 11 October 1991

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