A sequel to EWD874 (with C.S. Scholten)

Lemma 0 of EWD874 "A miscellany of results" can be strengthened and its proof can be simplified. Lemma 0 For monotonic $f$ and any natural $n$ , the equations

X: [ (\underline {{E}} _ {i}: 0 ≤ i: f ^ {i + 1} X) \equiv X ] \tag {0}

X: [ f ^ {m + 1} X \equiv X ] \tag {7}

X: [ (\underline {{A}} i: 0 ≤ i: f ^ {i + 1} X) \equiv X ] \tag {2}

have the same extreme solutions.

Proof Since the conjugate of $f$ is monotonic as well, it suffices to give the proof for the strongest solutions.

Let $P, Q,$ and $R$ be the strongest solutions of (0), (1), and (2) respectively. Since the left-hand sides of (0), (1), and (2) are strengthening in that order, we have - see Lemma 1, below -

[ R ⇒ Q ] ∧ [ Q ⇒ P ]

The proof is concluded by demonstrating $\left\lbrack {P ⇒ P}\right\rbrack$ as follows:

\begin{array}{l} λ r u e \ = {m o n o t o n i c i t y o f p 3 \ [ f (\underline {{A}} i: f ^ {i} R) ⇒ (\underline {{A}} i: f (p ^ {i} R)) ] \ = {\mathrm {p r e d . c a l c , d e f i n i t i o n o f p u n c h i o n a l i t e r a t i o n a n d} \ \end{array}

\begin{array}{l} [ f (R \wedge (\underline {{A}} _ {i}: f ^ {i + 1} R)) ⇒ (\underline {{A}} _ {i}: f ^ {i + 1} R) ] \ = {R \mathrm {i s a s o l u t i o n o f (2) a n d p r e d . c a l c .} } \ [ f R ⇒ R ] \ = {\mathrm {m o n o t o n i c i t y o f} p \mathrm {a n d i n d u c t i o n o v e r} i } \ (\underline {{A}} _ {i}: [ f ^ {i + 1} R ⇒ R ]) \ = {\mathrm {p r e d . c a l c .} } \ [ (\underline {{E}} _ {i}: f ^ {i + 1} R) ⇒ R ] \ ⇒ {P i s t h e s t r o n g e s t s o l u t i o n o f (0) a n d k n a s t e r - 1. 3 \ [ P ⇒ R ] \ \end{array}

(E n d o f P r o o f.)

Lemma 1 Let $f_0$ and $f_1$ be two monotonic predicate transformers such that

[ f _ {0} X ⇒ f _ {1} X ] \mathrm {f o r a l l} X. \tag {3}

Let the equations

X: [ f _ {0} X \equiv X ] \qquad a n d X: [ f _ {1} X \equiv X ]

have go and G1 as their strongest , and Ho and Hi as their weakest solutions. Then we have

[ G 0 ⇒ G 1 ] a n d [ H 0 ⇒ H 1 ]

\begin{array}{l} \mathbf {P r o o f} \ f r u e \ = {\mathrm {d e f i n i t i o n} G _ {1} } \ [ f _ {1} g _ {1} = g _ {1} ] \ ⇒ {(3) } \ [ \rho_ {0} G _ {1} ⇒ G _ {1} ] \ ⇒ {\mathrm {d e p . o f} G O \mathrm {a n d} K - T. } \ [ \mathfrak {G} 0 ⇒ \mathfrak {G} _ {1} ] \ \end{array}

\begin{array}{l} t r u e \ = {\mathrm {d e f . o f} H O } \ [ H _ {0} \equiv f _ {0} H _ {0} ] \ ⇒ {(3) } \ [ H O ⇒ f _ {1} H O ] \ ⇒ {\mathrm {d e f . o f} H 1 \mathrm {a n d} K - T. } \ [ H _ {0} ⇒ H _ {1} ] \ (E n d o f P r o o f.) \ \end{array}

Remark Consider for any nonempty bag $V$ of natural numbers the predicates

(\underline {{E}} i: i \ln V: \rho^ {i + 1} X) a n d (\underline {{A}} i: i \ln V: \rho^ {i + 1} X).

Bag V being nonempty, these predicates are at least as strong as the left-hand side of (0) and at least as weak as the left-hand side of (2). From Lemma 0 and Lemma 1 we now conclude that

X: [ (\underline {{E}} i: i \underline {{i n}} V; f ^ {i + 1} X) \equiv X ] \qquad a n d

X: [ (\underline {{A}} i: i \ln V: p ^ {i + 1} X) \equiv X ]

have the same extreme solutions as (0) and (2).

(End of Remark.)

12 April 1984

drs. C.S. Scholten prof. dr. Edsger W. Dgksstra Scientific Adviser Burroughs Research Fellow Philips Research Laboratories Plataansstraat 5 5600 JA EINDHOVEN 5671 AL NUENEN The Netherlands The Netherlands

*) EWD having accepted the Schlumberger Centennial Chair in Computer Sciences at the University of Texas at Austin, his mailing address is as of 1 Sep. 1984:

Department of Computer Sciences

The University of Texas at Austin

AUSTIN, Texas 78712-1188

United States of America