A summary for Turner’s class (An extract from EWD1107)

A summary for Turner's class (An extract from EWD1107)

Let $\varepsilon$ -read "below" be a punctual relation on structures of some type , i.e. for all $u,v,x,y$

$$ [ u = v \land x = y \Rightarrow (u \leq x \equiv v \leq y) ] $$

For $\varepsilon$ a preorder -i.e. a reflexive and transitive relation

$\left\lbrack {\;x \leq y}\right. \equiv \left\langle {\forall z : z \leq x \Rightarrow z \leq y}\right\rangle \rbrack$ and $\left\lbrack {\underset{\sim }{x} \leq \underset{\sim }{y}}\right. \equiv \left\langle {\forall z : x \leq z \Leftrightarrow y \leq z}\right\rangle \rbrack$

For a preorder $\varepsilon$ ,a value $k$ satisfying

(2) $\langle \forall x : \left\lbrack {x \leq k}\right. \equiv \langle \forall y : y \in W : x \leq {p}_{y}\rangle \rbrack$

is called "a highest lower bound" for the set $S$ given

$S = { z} \langle \exists y : y \in W : f.y\rangle }$

(Note that, for $f$ the identity function, $S = W$ .)

Moreover, a value $h$ satisfying

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

is called "a lowest higher bound for $S$ ". We remind the reader that these two names only make sense because we have chosen to read the symbol $\mathbf{S}$ as "below". For the rest of this note we restrict ourselves to a preorder $\mathbf{E}$ such that highest lower and lowest higher bounds exist for any set $S$ . Each of these bounds is unique if $\mathbf{E}$ is antisymmetric as well, i.e.

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

a preorder that is antisymmetric as well is called "a partial order" and in what follows, 5 is further restricted to a partial order. We now show the uniqueness of the highest lower bound.

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

$\left\langle {\forall x : \left\lbrack {x \leq {k}^{\prime }}\right. \equiv \left\langle {\forall y : y \in W : x \leq {p}_{y}}\right\rangle }\right\rbrack \rangle$

We then observe

true

$$ \begin{array}{l} = {(2) a n d (2 ^ {\prime}) } \ \langle \forall x: [ x \leq k \equiv x \leq k ^ {\prime} ] \rangle \ \Rightarrow \quad {x := k \mathrm {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} ] \ = {\xi \mathrm {i s r e f l e x i v e} } \ [ k \leq k ^ {\prime} ] \land [ k ^ {\prime} \leq k ] \ \Rightarrow {\mathrm {5 i s a n t h i s y m m e t r i c} } \ [ k = k ^ {\prime} ] \ \end{array} $$

(End of Proof.)

The highest lower bound of the empty set is traditionally denoted by $T$ and called "top"; the lowest higher bound of the empty set is traditionally denoted by $\bot$ and called "bottom". From (2) and (3) follow

$$ \langle \forall x: [ x \in T ] \rangle a n d \langle \forall x: [ \bot \in X ] \rangle . $$

The unique value for $k$ satisfying ${p}{y}$ mg(2) is denoted by $\langle {\pi }{y} : y \in W : f.y\rangle$ ,i.e.

(4) $\langle {\forall x : \left\lbrack {x \leq \langle {N}{y} : y \in W : {p}{y}}\right\rangle \equiv \langle {\forall y} : y \in W : x \leq {p}{y}\rangle }\right\rbrack \rangle$ . Similarly, the lowest higher bound is denoted using $U$ : (s) $\left\langle {\forall x : \left\lbrack {\langle {U}{y} : y \in W : f \cdot y}\right\rangle \leq x \equiv \langle {\forall y} : y \in W : f \cdot y \leq x}\right\rangle }\right\rangle$ .

Function $f$ is monotonic means here

(6) $\left\lbrack {x \leq y}\right\rbrack \Rightarrow \left\lbrack {f \cdot x \leq f \cdot y}\right\rbrack$ for all $x,y$ .

For monotonic $f$ we can prove (7) and (8):

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

of which we prove (7).

Proof In the following we leave the ranges $x \in W, y \in W$ understood and observe for any monotonic $f$

$$ \begin{array}{l} [ f. \langle \Pi x:: x \rangle \leq \langle \Pi y:: f. g \rangle ] \ = {4) w i t h x := f. \langle \prod x: x \rangle } \ [ \langle \forall y: f. \langle \pi x:: x \rangle \leq f. y \rangle ] \ = {\mathrm {i n t e r c h a n g e} } \ \langle \forall y: [ f. \langle \pi x:: x \rangle \leq f. y ] \rangle \ \Leftarrow {f \mathrm {i s m o n o t o n i c}; \mathrm {p r e d i c a t e c a l c u l u s} } \ \langle \forall y: [ \langle \Pi x:: x \rangle \equiv y ] \rangle \ = {(4) \mathrm {w i t h} x, f := \langle \cap x:: x \rangle , \mathrm {i d e n t i f y} } \ [ \langle \Pi x:: x \rangle \subseteq \langle \Pi y:: y \rangle ] \ \end{array} $$

$$ = {\underline {{\underline {{\mathbf {E}}}}} i s r e f l e x i v e } $$

true.

(End of Proof)

We are now ready for the theorem of Knaster. Tarski: for monotonic $f$ , the equations

$$ \begin{array}{l} (9) \quad x: [ f. x \leq x ] \quad a n d \ (1 0) \quad x: [ f. x = x ] \ \end{array} $$

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

$$ \begin{array}{l} \mathrm {P r o o f} \quad \mathrm {W e d e f i n e} \quad q \quad b y \ [ q = \langle \cap y: [ f \cdot y = y ]: y \rangle ] \ \end{array} $$

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

$$ \begin{array}{l} = \begin{array}{l} f \cdot q \ {\mathrm {d e p i n i t i o n o f} q } \end{array} \ f: \langle \cap y: [ f, y \leq y ]: y \rangle \ 5 \quad {f \mathrm {i s m o n o t o n i c}, (7) } \ \langle n _ {y}: [ f. y \leq y ]: f. y \rangle \ \equiv {\Pi \mathrm {i s m o n o t o n i c}, \mathrm {s e e (1 2) b e l o w} } \ \langle \Pi y: [ p _ {y} \leq y ]: y \rangle \ = {\mathrm {d e f i n i t i o n} o p = 9 } \ \end{array} $$

$$ q \quad , $$

which observation establishes $[p,q\leq q]$ thanks to the transitivity of E; so q solves (9), and it is its lowest solution by construction, for we observe

$\left( {11}\right) \;\left\langle {\forall y : \left\lbrack {{f}_{y} \leq y}\right\rbrack : q \leq y}\right\rangle$

$$ \begin{array}{l} = {(\lambda), d e f. o f \Pi } \ q \in \langle \pi y: [ p, y \leq y ]: y \rangle \ = {d e f. o p q, \equiv i s r e p l e x i v e } \ \end{array} $$

Next we observe

$$ [ f, g = q ] $$

[\left{ \begin{array}{ll} 5 & \text{ is antisymmetric.} \end{array}\right. ]

$$ [ p, q \leq q ] \land [ q \leq f, q ] $$

$\Leftrightarrow \;{ {111}}$ with $y \mathrel{\text{:=}} {f.9}}$

$$ [ f. q \equiv q ] \land [ p. (p. q) \equiv p. q ] $$

$\Leftrightarrow { f}$ is monotonic

$$ [ f, g \leq q ] \land [ f, g \leq q ] $$

$= \left{ {q\text{solves}\left( 9\right) }\right}$

$$ t r u e $$

so q solves (10) as well. Moreover, q

is (10)'s lowest solution , as follows from

the observation

$$ \langle \forall y: [ f. y = y ]: q \equiv y \rangle $$

$\Leftrightarrow { \left\lbrack {{p}{y} = y}\right\rbrack \Rightarrow \left\lbrack {{p}{y} \leq y}\right\rbrack$ since $\leq$ is reflexive

$$ \begin{array}{l} \langle \forall y: [ f. y \leq y ]: q \leq y \rangle \ = {(\pi) } \ t r u e. \ \end{array} $$

The monotonicity of $\Pi$ is expressed by

(12) $\left\lbrack {\langle {y}{1} : y \leq h,y\rangle \Rightarrow \langle {y}{1} : y \leq h,y\rangle \leq \langle {y}_{1} : y \leq h,y\rangle }\right\rbrack$

where we left the range of $y$ understood.

Proof We observe for any $g,h$ ,and range of $y$

$$ \langle \pi_ {y}: g \cdot y \rangle \equiv \langle \pi_ {y}: h \cdot y \rangle $$

$$ = {0 } $$

$$ \langle \forall z: z \leq \langle \Pi y: g \cdot y \rangle \Rightarrow z \leq \langle \Pi y: h \cdot y \rangle \rangle $$

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

$$ \langle \forall z: \langle \forall y: z \leq g. y \rangle \Rightarrow \langle \forall y: z \leq h. y \rangle \rangle $$

$\Leftrightarrow {$ monotonicity of $\forall }$

$$ \langle \forall z: \langle \forall y: z \leq g. y \Rightarrow z \leq h. y \rangle \rangle $$

$$ = {\text {i n t e r c h a n g e} } $$

$$ \langle \forall y: \langle \forall z: z \leq g. y \Rightarrow z \leq h. y \rangle \rangle $$

$$ = {0 } $$

$$ \langle \forall y: g. y \subseteq h. y \rangle $$

(End of Proof)

Notice how, in the above proof, we started using (0) and not (1), which would have into. deduced to the left of $\leq$ ,whereas (4) enables us to eliminate $\pi$ to the right of $\leq$

Austin, 12 February 1992

proff. dr. Edsger W. Dgiksha

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712-1188

USA