A more disentangled characterization of extreme solutions

A more disentangled characterization of

extreme solutions

Let E - read "below" - be a punctual partial order. Let equation X: [B.x] have a lowest solution k . The traditional characterization of k has been that it satisfies

(0) $\left\lbrack {B,k}\right\rbrack$

(1) $\left\langle {\forall x : \left\lbrack {B.x}\right\rbrack : \left\lbrack {k \leq x}\right\rbrack }\right\rangle$

where (0) expresses that k is a solution, and (1) states that k is everywhere below any solution.

Here I propose to characterize $k$ by

(2) $\langle \exists x : \lbrack 8.x\rbrack : \left\lbrack {x \leq k}\right\rbrack \rangle$ (3) $\langle \forall x : \left\lbrack {\mathcal{B}.x}\right\rbrack : \left\lbrack {k \leq x}\right\rbrack \rangle$

(Here, (3) is a copy of (1): I have repeated the formula so as to ease its comparison with (2).) We have to prove the

Theorem (0) $\land \left( 1\right) \equiv \left( 2\right) \land \left( 3\right)$

Proof For pinging it suffices to show $(0) \Rightarrow (2)$ :

$$ \begin{array}{l} \langle \exists x: [ B, x ]: [ x \leq k ] \rangle \ \Leftarrow \quad {i n s t a n t i a t i o n x := k } \ \end{array} $$

$$ \begin{array}{l} [ B, k ] \wedge [ k \leq k ] \ = {\underline {{\underline {{E}}}} i s a p a r t i a l o r d e r, h e n c e r f l e x i v e } \ \end{array} $$

For pong it suffices to show $\left( 0\right) \Leftarrow \left( 2\right) \land \left( 3\right)$ :

$$ \langle \exists x: [ B. x ]: [ x \leq k ] \rangle \land \langle \forall x: [ B. x ]: [ k \leq x ] \rangle $$

$$ \begin{array}{l} \Rightarrow \quad {\text {p r e d . c a l c .} } \ \langle \exists x: [ B, x ]: [ x \leq k ] \land [ k \leq x ] \rangle \ \Rightarrow {\leq i s a p a r t i a l o r d e r, h e n c e a n t i s y m m e t r i c } \ \langle \exists x: [ B, x ]: [ x = k ] \rangle \ = {\mathrm {t r a d i n g} } \ \langle \exists x: [ x = k ]: [ B, x ] \rangle \ = {\text {1 - p o i n t r u l e} } \ [ B, k ] \ \end{array} $$

(End of Proof)

The reason why (2)2(3) is such a nice pair is that (2) -monotonic in k - only bounds k from below, while (3) - antimonotonic in k- bounds k only from above. In the pair (0)&(1), (1) is obviously as nice as (3), but (0) - being in general not monotonic in k - is not a one-sided constraint. (It is not amazing that in the above pong argument we needed in the antecedent (3) as well.)

As an example of the heuristic guidance provided by this disentanglement we shall prove the following, now trivial, theorem.

Theorem x: [B.x] ; let h be the lowest solution of

$x : \left\lbrack {c.x}\right\rbrack$ . Then

$$ \langle \forall x: [ C. x ] \Rightarrow [ B. x ] \rangle \Rightarrow [ k \leq h ] $$

Proof Analogously to (2) & (3), $h$ is defined

(4) $\langle \exists x : \left\lbrack {C.x}\right\rbrack : \left\lbrack {x \leq h}\right\rbrack \rangle$ $\left\langle {\forall x : \lbrack 0.5\rbrack : \lbrack h \leq x}\right\rangle$

In view of the demonstrandum, (3) gives all we need to know about $k$ and (4) gives all we need to know about $h$ .

$$ \langle \forall x: [ C. x ] \Rightarrow [ B. x ] \rangle $$

$\Rightarrow \left{ \begin{array}{l} \left( 3\right) ;\forall \text{antimonotric with respect to range}} \ \left\langle {\forall x : \lbrack C.x\rbrack : \lbrack k \leq x\rbrack }\right\rangle \end{array}\right.$ $\Rightarrow \;{ (4),\operatorname{predicate calculus}}$

$$ \langle \exists x: [ C. x ]: [ k \leq x ] \land [ x \leq h ] \rangle $$

$$ \langle \exists x: [ C, x ]: [ k \leq h ] \rangle $$

$$ [ k \le h ] $$

$\Rightarrow$ ${ 5$ is a partial order,hence transitive [\left{ \begin{array}{l} \text{predicate calculus}\ \text{ } \end{array}\right} ]

(End of Proof.)

The above heuristics are tighter than those for the proof that for monotonic $f$ , $g$ is monotonic when $g.x$ is given as the strongest solution of $y: [f.x.y \Rightarrow y]$ - see Dyksbra, Scholten, 90, p.153 -

is given by

(6) $\langle \exists x : \left\lbrack {B,x}\right\rbrack : \left\lbrack {h \leq x}\right\rbrack \rangle$ $\left\langle {\forall x : \left\lbrack {B,x}\right\rbrack : \left\lbrack {x \leq h}\right\rbrack }\right\rangle$

Remark In the classical notation, which does not have a range, these formulae would not be half as nice. (End of Remark.)

I am utterly amazed that it took me more than a decade to come up with the above characterization of extreme solutions.

Nuenen, 17 December 1992

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