On two equations that have the same extreme solution

On two equations that have the same extreme solution

In [DS90], we have shown that for monotonic $f$ and sufficiently conjunctive $g$ ,equation

$$ x: [ f. x \Rightarrow g. x ] $$

has a unique strongest solution. Also, if $f_{x.y}$ is monotonic in $x$ and in $y$ , $f_{x.x}$ is monotonic in $x$ . (In the following theorem, however, the existence of the strongest solutions is part of the premiss.)

Theorem Let the strongest solution of $x: [f.x.x \Rightarrow g.x]$ (exist and) be $t$ ; let the strongest solution of $x: [f.x.t \Rightarrow g.x]$ (exist and) be $s$ ; then $[t \equiv s]$ if $f.x.y$ is monotonic in $y$ .

Proof We are given

[\left\lbrack {f.t.t \Rightarrow g.t}\right\rbrack ] (1) $\left\lbrack {f \cdot x \cdot x \Rightarrow g \cdot x}\right\rbrack \Rightarrow \left\lbrack {t \Rightarrow x}\right\rbrack \;\left. \text{ for all }x\right\rbrack$ (2) $\left\lbrack {f \cdot s \cdot t \Rightarrow g \cdot s}\right\rbrack$ (3) $\left\lbrack {f \cdot x.t \Rightarrow g \cdot x}\right\rbrack \Rightarrow \left\lbrack {s \Rightarrow x}\right\rbrack \;$ for all $x$ $\left\lbrack {p,q \Rightarrow p \Rightarrow q}\right\rbrack$ for all $p,q,x$ .

We now observe

[ \Leftrightarrow \left\lbrack {t \Rightarrow s}\right\rbrack ] $\Leftrightarrow \;\left{ \begin{array}{l} \text{ (1 ) with } \ x \end{array}\right. = 5$

$$ [ f. s. s \Rightarrow g. s ] $$

$\Leftrightarrow \;\left{ \begin{array}{l} \text{ (2 ) and monotonicties } \ \end{array}\right}$

$$ [ f. s. s \Rightarrow f. s. t ] $$

$\Leftrightarrow { \left( 4\right)$ with $p,q,x = s,t,s}$

[\left\lbrack {s \Rightarrow t}\right\rbrack ]

$\Leftrightarrow \;\left{ \begin{array}{l} \text{ (3 ) with }x \mathrel{\text{:=}} t \ \end{array}\right}$

$$ \begin{array}{l} [ f. t. t \Rightarrow g. t ] \ = {0 } \ \begin{array}{l} \mathrm {t r u e} \ \end{array} , \ \end{array} $$

which observation proves, in view of the two lines marked $t$ , $\left\lbrack {t \equiv s}\right\rbrack$ by mutual implicac- tion.

(End of Proof.)

The proof is very short, as befits such a small theorem. In fact, the theorem is so small that one may wonder why this EWD has been written at all. Here are my reasons.

• I did not really know the theorem.
• I did not know the proof, which with 1 step pen given is a very nice example of a shortest pos-sible proof.
• It makes clear that this theorem has nothing to do with fixpoints.
• It is always nice to start the new year with a theorem.

Nuenen, 1 January 1994 Prof. Dr. Edsger W. Dgkstra, Department of Computer Sciences, The University of Texas at Austin, Austin TX 78712-1188, USA