Generators of extreme values

Generators of extreme values

"s generates the strongest value of p" means

(0) $\left\langle {\forall x : \left\lbrack {p \cdot s \Rightarrow p \cdot x}\right\rbrack }\right\rangle$

" $W$ generates the weakest value of $p$ " means

(1) $\left\langle {\forall x : \left\lbrack {p.x \Rightarrow p.w}\right\rbrack }\right\rangle$

For arbitrary $p$ , these extreme-value generators need not exist, and if they exist, they need not be unique. Notice that $p$ need not have any monotonicity property. From (0) and (1) follow (by predicate calculus)

$$ [ p. s \Rightarrow \langle \forall x:: p. x \rangle ] a n d [ \langle \exists x:: p. x \rangle \Rightarrow p. w ] $$

respectively, which imply by instantiation

(2) $\left\lbrack {p.s \equiv \left\langle {\forall x : p.x}\right\rangle \rbrack }\right.$ (3) $\left\lbrack {\langle \exists x : p \cdot x\rangle \equiv p \cdot w}\right\rbrack$

These formulae are of potential interest because they equate a quantified expression to a non-quantified one.

Remark Note (0) $\equiv \left( 2\right)$ and $\left( 1\right) \equiv \left( 3\right)$ . (End of Remark.)

In the case of monotonic $m$ ,(0) implies

(4) $\left\langle {\forall x\therefore \left\lbrack {m \cdot \left( {p \cdot s}\right) \Rightarrow m \cdot \left( {p \cdot x}\right) }\right\rbrack }\right\rangle$

i.e. s generates the strongest value of mOp. In the case of anti-monotonic am , however,

(1) implies (5) $\left\langle {\forall x : \left\lbrack {{am}.\left( {p \cdot w}\right) \Rightarrow {am}.\left( {p \cdot x}\right) }\right\rbrack ,\right.$

i.e. $w$ generates the strongest value of $a$ omp .

Example 0 In the case

$$ [ p. x \equiv \mathrm {c o n s t a n t} ] \qquad (\mathrm {f o r a l l} x), $$

both s and w exist and arbitrary values can be chosen for them. For instance, in EWD1195 we saw an example with

$$ [ p. x \equiv x \lor \neg x ], $$

$$ [ s \equiv j ] $$

$$ m. y \equiv [ p; y ] $$

J generates the strongest value of $\mathrm{{mop}}$ , that is (2) with $p \mathrel{\text{:=}} \mathrm{{mop}}\;.\;$ Since

$$ (m o p). x \equiv [ 7 (f; x) \Rightarrow f; 7 x ] $$

• see EWD 1195 or prove it yourself - this

$$ [ \neg (f; J) \Rightarrow f; \neg J ] \equiv \langle \forall x: [ \neg (f; x) \Rightarrow f; \neg x ] \rangle $$

which is EWD 1195 (2).

Example 1 In the case of the identity

function

$$ [ p. x \equiv x ] (\mathrm {f o r a l l} x) $$

both and $\omega$ exist and are unique:

$$ [ s \equiv f a l s e ] a n d [ w \equiv t r u e ]. $$

For example, (see EWD 1191), with

$$ [ p. x \equiv x ] $$

$$ [ w \equiv t r u e ] $$

$$ a m. y \equiv [ y; r \Rightarrow r ], $$

$w$ generates the strongest value of ${amop}$ , i.e. (2) with $p,s \mathrel{\text{:=}} {amop}$ ,true

$$ [ t r u e; r \Rightarrow r ] \equiv \langle \forall x: [ x; r \Rightarrow r ] \rangle , $$

i.e. the two ways of expressing that r is a "right condition".

Example 2 We begin by observing

$$ t r u e $$

$$ = {\neg \mathrm {n e u t r a l e l e m e n t o f c o m p o s i t i o n} } $$

$$ \langle \forall x: [ ]; x \Rightarrow x ] \rangle $$

$$ = {\text {l e f t} x \text {e x c h a n g e} } $$

$$ \langle \forall x: [ 7 x; \sim x \Rightarrow 7 ] \rangle $$

$$ = {n J a l s o n e u t r a l e l e m e n t o f c o m p o s i t i o n } $$

(6) $\left\langle {\forall x : \left\lbrack {1,2; \sim x \Rightarrow 7}\right\rbrack \sim 7}\right\rbrack \rangle$

that is:

with

$$ [ p. x \equiv 7 x; \sim x ] (f o r a l l x) $$

we have

$$ [ \omega \equiv J ] $$

Now, with

$$ a m. y \equiv [ y \Rightarrow 7 c ] $$

J generates the strongest value of amop.

$$ s i n c e $$

$$ (a m \cdot p). x \equiv [ c; x \Rightarrow x ] $$

we conclude

$$ [ c; J \Rightarrow J ] \equiv \langle \forall x: [ c; x \Rightarrow x ] \rangle , $$

i.e. the equivalence of two ways of $f$ -

Remark

With the specific choice

$$ [ c \equiv r f; f ] $$

we get

$$ (a m o p). x \equiv [ f; 7 x \Rightarrow 7 (f; x) ] $$

and our last conclusion becomes

$$ [ f; \tau J \Rightarrow \tau (f; J) ] \equiv \langle \forall x: [ f; \tau x \Rightarrow \tau (f; x) ] \rangle , $$

which is EWD1195 (3). (End of Remark.)

With thanks to Caryl S. Scholten!

Austin, 16 January 1995

pror. dr Edsger W. Dgksta

Department of Computer Sciences The University of Texas at Austin

Austin, TX 78712- 1188 USA