More on monotonic predicate transformers and the introduction of dummies (see EWD1117)

More on monotonic predicate transformers and the introduction of dummies (see EWD1117)

We are interested in predicate transformers $g$ such that for any monotonic predicate trans-

(0) $\left\lbrack {f.b \equiv \langle \exists x : \left\lbrack {g.b.} \times \right\rbrack : f.}\right\rbrack$

Thanks to the 1-point rule, the choice of $b \equiv x$ for $g.b.x$ would do the job, but this choice is too specific for our purposes, as it does the job for any $f$ , monotonic or not. We shall therefore follow the usual route of proving (0), on the way collecting the requirements on $g$ that make the proof work. The proof of (0) is a ping pong argument.

Proof For ping we observe

\langle \exists x: [ g. b. x ]: f. x \rangle

$\Leftarrow$ {instantiation with} x: = b?

\begin{array}{l} [ g, b, b ] ∧ f, b \ = {() } \ \end{array}

f \cdot b

where we appealed to

[\left\lbrack {g,b,b}\right\rbrack ]

note that $f_{s}^{\prime}$ monotonicity has not been used.

For pang we observe for any monotonic $f$

\begin{array}{l} [ f, b \Leftarrow \langle \exists x: [ g, b, x ]: f, x \rangle ] \ = {\text {p r e d . c a l c .} } \ [ \langle \forall x: [ g. b. x ]: f. b \Leftarrow f. x \rangle ] \ = {\mathrm {s c a l a r} r a n g e } \ \langle \forall x: [ g, b, x ]: [ f, b \Leftarrow f, x ] \rangle \ \Leftrightarrow {f _ {i s m o n o t o n i c} } ^ {*} \ \langle \forall x: [ g, b, x ]: [ b \Leftarrow x ] \rangle \ = {(2) } \ t r u e \ \end{array}

where we appealed to

(2) $\left\lbrack {g.b.x}\right\rbrack ⇒ \left\lbrack {x ⇒ b}\right\rbrack \text{for all}x$ ;

note that we did use the monotonicity of $f$ .

Remark The strengthening in the step marked *) is spurious in the sense that we could have quantified universally over all monotonic $f$ .Leaving that range understood ,the step in question would have been

\langle \forall f: \langle \forall x: [ g. b. x ]: [ f. b \Leftarrow f. x ] \rangle \rangle

\begin{array}{l} = {f \in f _ {i s m o n o t o n i c}, \ ⇒ \mathrm {i n s t a n t i a t i o n w i t h} f := \mathrm {i d e n t i t y f u n c t i o n} \ \langle \forall x: [ g, b, x ]: [ b \Leftarrow x ] \rangle \ \end{array}

(End of Remark.)

(End of Proof.)

collecting requirements (1) and (2) we see that (0) holds if $b$ is the weakest

solution of the equation $x : \left\lbrack {g,b,x}\right\rbrack$

The observation that ${f}^{\prime }$ s conjugate ${f}^{ * }$ is as monotonic as $f$ ,invites us to substi- hute ${f}^{ * }$ for $f$ . More precisely,(0) with ${f}_{2}g = {f}^{ * },n{h}^{ * }$ yields

[ f ^ {}. b \equiv \langle \exists x: [ ¬ h ^ {} b. x ]: f ^ {*} x \rangle ]

the definition of ${}^{ * }$ yields

[ \eta f. (1 b) \equiv \langle \exists x: [ h. (1 b). (1 x) ]: \eta f. (1 x) \rangle ]

which can be simplified by $b,x \mathrel{\text{:=}} {1b},{7x}$ to

[ ¬ f. b \equiv \langle \exists x: [ h. b. x ]: ¬ f. x \rangle ] ;

now de Morgan yields what we were heading for:

(3) $\left\lbrack {f,b \equiv \langle \forall x : \left\lbrack {h.b.x}\right\rbrack : f.x}\right\rbrack$

holds for monotonic $f$ if $b$ is the strongest solution of the equation $x : \left\lbrack {h.b.x}\right\rbrack$ ,the latter condition being captured by

(4) $\left\lbrack {h,b,b}\right\rbrack$ (5) $\left\lbrack {h.b.x}\right\rbrack ⇒ \left\lbrack {b ⇒ x}\right\rbrack $ for all $x$

(1) and (4) can be reformulated as

[\left\lbrack {x \equiv b}\right\rbrack ⇒ \left\lbrack {g.b.x}\right\rbrack \text{for all}x] $\left\lbrack {x \equiv b}\right\rbrack ⇒ \left\lbrack {h.b.x}\right\rbrack$ for all $x$

These formulae tell us that the strongest choices for the ranges in (0) and (3) are both $[x \equiv b]$ ; the 1-point rules result. More interesting are the weakest possible choices for $g$ and $h$ respectively: (2) and (5) give us those bounds, yielding

(6) $\left\lbrack {f,b \equiv \langle \exists x : \left\lbrack {x ⇒ b}\right\rbrack : f.x}\right\rbrack$ (7) $\left\lbrack {f.b \equiv \langle \forall x : \left\lbrack {b ⇒ x}\right\rbrack : f.x}\right\rbrack$

minor generalizations of the 2 formulae given in EWD1117 (where $f_{x}w$ as a boolean scalar).

This note has been written for the following reasons.

• In EWD1117, nothing was proved.
• I did not know that the one formula was the conjugate of the other.
• I did not know that the ranges in (6) and (7) could be derived as weakest solutions, nor was I aware of the relation with the 1-point rule. I would like to point out a special property of formulae (6) and (7) - when universally quantified over b - . We have derived them for monotonic f , but, conversely, their validity implies that is monotonic , for , independently of f , the right-hand sides are expressions

that monotonically depend on b . I don't know yet of an example where it comes in handy, but (6) and (7) give us the opportunity of incorporating in calculations the monotonicity of functions by the rewriting of subexpressions.

In view of the rising interest in mono-tonic predicate transformers, the above is definitely something to keep in mind.

Nuenen, 17 December 1992

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