A miscellany of results (with C.S.Scholten)

A miscellany of results

Lemma 0. For monotonic $f$ and natural $n$ ,the extreme solutions of

X: [ f ^ {n + 1} X \equiv X ] (0)

are independent of $n$ .

Proof. Since $f^{n+1}$ is monotonic for all natural $n$ , the extreme solutions exist for all natural $n$ . Since the conjugate of $f$ is monotonic, it suffices to prove the lemma for the strongest solutions only.

We denote the strongest solution of (0) by $Q \cap N$ .

Hence, for any natural $n$ ,

true

\begin{array}{l} = {\mathrm {d e f i n i t i o n} o f Q O } \ [ f (Q o) \equiv Q o ] \ ⇒ {i n d u c t i o n } \ [ {f ^ {n + 1} (Q o) \equiv Q o } \ ⇒ {Q n b e i n g a s t r o n g e s t s o l u t i o n } \ [ Q n ⇒ \tilde {Q} 0 ] \ \end{array}

Also, for any natural $n$ ,true

\begin{array}{l} = \left{ \begin{array}{l} d e f i n i t i o n o f Q n \end{array} \right} \ \begin{array}{r l} & {⇒ {\mathrm {p r e d i c a t e c a l c u l u s} }} \ & { [ (\underline {{A}} i: 0 ≤ i < n: f ^ {i + 1} (Q n)) \wedge f ^ {n + 1} (Q n) =} \ & { Q n \wedge (\underline {{A}} i: 0 ≤ i < n: f ^ {i + 1} (Q n)) ]} \end{array} \ \end{array}

\begin{array}{l} = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ (\underline {{A}} i: 0 ≤ i ≤ n: f ^ {1 + i} (Q _ {n})) \equiv (\underline {{A}} i: 0 ≤ i ≤ n: f ^ {i} (Q _ {n})) ] \ ⇒ {\mathrm {m o n o t h o n i c i t y} o f \rho } \ [ f (\underline {{A}} i: 0 ≤ i ≤ n: f ^ {i} (Q n)) ⇒ (\underline {{A}} i: 0 ≤ i ≤ n: f ^ {i} (Q n)) ] \ ⇒ {Q O b e i n g a s t r a m g e s t s o l u t i o n; K n a s t e r T a r s k i } \ [ Q o ⇒ (\underline {{\mathrm {H}}} i: 0 ≤ i ≤ n: f ^ {i} (Q n)) ] \ ⇒ {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ Q _ {0} ⇒ f ^ {0} (Q _ {n}) ] \ = {\mathrm {f u n c t i o n a l} \mathrm {i t e r a t i o n} } \ [ Q o ⇒ Q n ] \ \end{array}

(End of Proof.)

In EWD849a-2, we introduced different types of conjunctivity for predicate transformers. The following lemma connects three of them.

Lemma 1. For any predicate transformer $F$ we have

$\left( {f\text{ is denumerably }\text{conjunctive }}\right) \equiv$

$\left( {f\text{ is }\text{ conjunctive }}\right) ∧ \left( {f\text{ is }\text{ and-continuous }}\right)$

Proof. The fact that the left-hand side implies both terms of the right-hand side has already been shown in EWD84ga to follow immediately from the definitions. In order to prove the implication in the other direction, we derive, under the assumption of the right-hand side, that $f$ is denumerably conjunctive, i.e. for any sequence of predicates Pi (osi)

[ f (\underline {{A}} i: \mathcal {P} _ {i}) \equiv (\underline {{A}} i: f (\mathcal {P} _ {i})) ]

We observe for all $z$

\begin{array}{l} [ 2 \equiv f (\underline {{A}} _ {i}: P _ {i}) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ Z \equiv f (\underline {{A}} j: (\underline {{A}} i: 0 ≤ i ≤ j: P _ {i})) ] \ = {f \mathrm {i s a n d - c o n t i n u o u s}; (\underline {{A}} _ {i}: o s i s j: P _ {i}) \mathrm {i s s t r e n g t h e n i n g} } \ [ Z \equiv (\underline {{A}} j: f (\underline {{A}} i: o s i ≤ j: P _ {i})) ] \ = {f \mathrm {c o n j u n c t i v e a n d r a n g e n o n - e m p l y} } \ [ Z \equiv (\underline {{A}} j: (\underline {{A}} i: 0 ≤ i ≤ j: f (P _ {i}))) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ Z \equiv (\underline {{A}} i: P (P _ {i})) ] \ \end{array}

(End of Proof.)

Lemma 2. For conjunctive $f$ and monotonic $g$ and predicate $B$ such that

[ f X \equiv B \wedge g X ] f o r a l l X

we have $\left\lbrack {\left( {{A}{i} : i ≥ 0 : {P}^{i}\text{ true }}\right) \equiv \left( {{A}{i} : i ≥ 0 : {g}^{i}B}\right) }\right\rbrack$

Proof. To begin with, we prove, using the conjunctivity of $f$ , via mathematical induction for all natural $i$

[ f ^ {i} \mathrm {t r u e} \equiv (\underset {-} {A} j: 0 ≤ j < i: g ^ {j} B) \wedge g ^ {i} \mathrm {t r u e} ] . (1)

This holds for $i = 0$ . Furthermore we observe

\begin{array}{l} [ f ^ {i} \mathrm {t r u e} \equiv (\underline {{A}} j: 0 < j < i: g ^ {j} B) \wedge g ^ {i} \mathrm {t r u e} ] \ ⇒ {f _ {i} s i a f u n c t i o n } \ [ f ^ {i + 1} \mathrm {t r u e} ] = f ((A _ {j}: 0 ≤ j < i: g ^ {j} B) ∧ g ^ {i} \mathrm {t r u e}) ] \ = {f \mathrm {i s c o n j u n c t i v e , a p p l i e d t o f i n i t e , n o n e m p l y c o n j u n c t i o n} } \ \end{array}

\begin{array}{l} [ \rho^ {i + 1} t r u e \equiv (\underline {{A}} _ {j}: 0 ≤ j < i: \rho (g ^ {j} B)) \wedge \rho (g ^ {i} t r u e) ] \ = {[ f X \equiv B ∧ g X ] f o r a l l X } \ [ p ^ {i + 1} \mathrm {t r u e} \equiv B \wedge (\underline {{A}} _ {j}: 0 ≤ j < i: g ^ {j + 1} B) \wedge g ^ {i + 1} \mathrm {t r u e} ] \ = {[ B \equiv g ^ {0} B ] } \ [ p ^ {i + 1} \mathrm {t r u e} \equiv (\underline {{n}} j: 0 ≤ j < i + 1: g ^ {j} B) \wedge g ^ {i + 1} \mathrm {t r u e} ] \ \end{array}

which completes the proof of (1) for all natural $i$ .

Hence

\begin{array}{l} \mathbf {f r u e} \ = {(1) \mathrm {a n d} \mathrm {p r e d i c a t e c a l c u l u s} } \ [ (\underline {{A}} i: f ^ {i} t r u e) \equiv (\underline {{A}} i: g ^ {i} B) \wedge (\underline {{A}} i: g ^ {i} t r u e) ] \ = {g, a n d h e n c e g ^ {i}, i s m o n o t o n i c } \ [ (\underline {{A}} i:: f ^ {i} t r u e) \equiv (\underline {{A}} i:: g ^ {i} B) ] \ \end{array}

(End of Proof.)

Peccavirus In the proof of the similar formula (5)

{w l p (1 F,?) i s c o n j u n c t i v e }

is insufficient: we should have written "is universally conjunctive". (End of Peccavimus.)

Lemma 3 For denumerably conjunctive $f$ ,monotonic $g$ ,and predicate $B$ such that

[ p x \equiv B \wedge g X ] f o r a l l X

$\left( {A,i : {g}^{i}B}\right)$ is the weakest solution of $X : \left\lbrack {X = f{X}^{2}}\right\rbrack$ .

Proof. Since $f$ is denumerably conjunctive, $f$ is and-continuous, and hence the weakest solution of

junctive, and $g$ is monohotic,Lemma 2 is applica- able,which concludes the proof.(End of Proof.)

Note that, on account of Lemma 1, the require- ment on $f$ in Lemma 3 is not stronger than ne- cessary.

Lemma 4 For a predicate transformer $f$ satisfying

[ f X \wedge f (¬ X) \equiv f \mathrm {f a l s e} ] \wedge [ f X \vee f (¬ X) \equiv f \mathrm {t r u e} ]

for all $x$ ,

$\left( {p \mid s\text{type of conjunctionly}}\right) = \left( {{f}_{s} \upharpoonright s\text{ type of disjunctivity}}\right)$

Proof. We observe for any $X$

[ f X ∧ f (G X) \equiv f \mathrm {f a l s e} ] ∧ [ f X \lor f (G X) \equiv f \mathrm {f u r e} ]

$⇒$ {termwise conjunction with $\left\lbrack {{7f}\left( {7X}\right) \equiv {P}^{ * }X}\right\rbrack$ in ${2}^{\text{nd }}$ term

[ f X ∧ f (¬ X) \equiv f \mathrm {f a l s e} ] ∧ [ f X ∧ ¬ f (¬ X) \equiv f ^ {*} X ∧ f \mathrm {t r u e} ]

[\text{⇒}{ \text{termwise disjuncton}} ]

[ f X \equiv f \mathrm {f a l s e} v (p ^ {*} X ∧ f \mathrm {t r u e}) ]

Since f false and f true are predicates independ- ent of X, any junctivity of $\mathbb{P}^{\ast}$ ,except universal, is inherited by the right-hand side,and hence by 5 . Since a con (dis) junctivity property of $\mathbb{P}^{\ast}$ is the same dis(con) junctivity property of $\mathbb{P}$ , the Lemma follows. (End of Proof.)

为

Lemma 5. Let monotonic $f$ and predicate $Y$ be such that

has a strongest solution; this is then also the strongest solution of

X: [ P Y \equiv P X ] . (3)

Proof. Let $Z$ be the strongest solution of (2). We observe

\begin{array}{l} \begin{array}{l} {\mathrm {t r u e}} \ {= {Y \mathrm {i s a s o l u t i o n a n d} Z \mathrm {i s t h e s t r u n g e s t s o l u t i o n o f (2)} }} \ {[ Z ⇒ Y ]} \end{array} \ ⇒ {f _ {i s m o n o t o n i c} } [ f Z ⇒ f Y ] \ = \left{ \begin{array}{l l} Z & i s a s o l u t i o n o f (2) \ [ f Z ⇒ f Y ] & \wedge [ f Y ⇒ f Z ] \end{array} \right. \ = {p r e d i c a t e c a l c u l u s } [ f Y = f Z ] \ \end{array}

hence $Z$ is a solution of (3). Since the solutions of (3) constitute a subset of those of (2), of which $Z$ is the strongest, $Z$ is the strongest solution of (3). (End of Proof.)

Lemma 6. For any predicate transformers $h$ and $k$ ,the equation -in predicate transformers!-

f: (\underline {{A}} X:: [ f X \equiv h X \vee f (k X) ]) (4)

has a strongest solution $g$ ,defined by

[ g X \equiv (\underline {{E}} i: o s i: h (k ^ {i} X)) ] f o r a l l X.

Proof. We observe for any $X$

\begin{array}{l} t r u e \ = {\mathrm {d e f i n i t i o n} o f g } \ [ g X \equiv (\underline {{E}} i: 0 ≤ i: h (k ^ {i} X)) ] \ = {\mathrm {i s d a t i o n o f 1 s t t e r m a n d t r a n s f o r m a t i o n o f t h e d u m m y} } \ [ g X \equiv h X \vee (\operatorname {E} i: 0 ≤ i: h (k ^ {i} (k X))) ] \ = {\mathrm {d e f i n i t i o n o f} g } \ [ g X \equiv h X ^ {\prime} v ^ {\prime} g (k X) ] , \ \end{array}

hence, $g$ is a solution of (4).

In order to prove that $g$ is the strongest solution of (4), we observe for any solution $f$

o f (4)

(A X: [ g X ⇒ f X ])

\begin{array}{l} = {\mathrm {d e f i n i t i o n} o f g } \ (A X: [ (E i: h ^ {0} (k ^ {i} X)) ⇒ f X ]) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} _ {i}: (\underline {{A}} X: [ h (k ^ {i} X) ⇒ F X ]) (5) \ \end{array}

and we shall prove (5) by induction over $i$ .

For the base we observe

\begin{array}{l} t r u e \ = {f \mathrm {i s a s o l u t i o n o f} (4) } \ (A X: [ h X \vee f (k X) = f X ]) \ ⇒ {\mathrm {p r e d i c a t e c a l c u l u s a n d f u n c t h o n a l i t e r a t i o n} } \ (\underline {{A}} X:: [ h (k ^ {0} X) ⇒ f X ]) \ \end{array}

For the induction step we observe

\begin{array}{l} (A X: [ h (k ^ {i} X) ⇒ f X ]) \ ⇒ {\mathrm {r e s t r i c t i o n} x \mathrm {o f t h e f o r m k Y}; \mathrm {f u n c h i o n a l i t e r a t i o n} } \ (A Y: [ h (k ^ {i + 1} Y) ⇒ f (k Y) ]) \ ⇒ {f \mathrm {s o l v e s} (4), \mathrm {h e n c e} [ f (k Y) ⇒ f Y ] \mathrm {f o r a n y} Y } \ (\underline {{A}} Y: [ h (k ^ {i + 1} Y) ⇒ f Y ]) \ \end{array}

(End of Proof.)

3 February 1984

drs.c.s.SchoHEn

Scientific Adviser

Philips Research Laboratories

5600 JA EINDHOVEN

The Netherlands

prof. dr. Edsger W. Dyksha

Burroughs Research Fellow

Plataansstraat 5

5671 AL NUENEN

The Netherlands