Junctivity of extreme solutions (with C.S.Scholten)

Junctivity of extreme solutions

by Edsger W. Dijkstra and C.S. Scholten.

Introduction

A predicate transformer that distributes over conjunction is called "conjunctive"; similarly, one that distributes over disjunctio n is called "disjunctive". Example. Since for all $P, Q$

[ w _ {P} (S, P \wedge Q) \equiv w _ {P} (S, P) \wedge w _ {P} (S, Q) ]

${wp}\left( {S,?\text{ }}\right)$ is conjunctive; we remind the reader that it is disjunctive for deterministic S only. (End of Example.)

The notions of conjunctivity and disjunctivity can be generalized to distribution over universal and existential quantification respectively. The man-ners in which will be made more precise below.

Predicate transformers $wp$ and wlp can be defined for repetitions as strongest and weakest solutions respectively of equations of the form $Y: [Y \equiv fXY]$ . The purpose of this note is to relate the junctivity properties of these extreme solutions to those of $f$ .

This note deals explicitly with conjunctivity only. At its end we shall show the duality considerations that allow us to formulate the corresponding results for disjunctivity.

Notations

All through this text a number of identifiers will be used with the following meanings:

X and Y will stand for predicates on some space

$p$ will stand for a predicate transformer with two arguments that is monotonic in both its argu- ments $g$ will stand for a predicate transformer with one argument such that $gX$ is the strongest solution of the equation $Y : \left\lbrack {f{XY} \equiv Y}\right\rbrack$ h will stand for a predicate transformer with one argument such that $hX$ is the weakest solution of the equation $Y: \left\lbrack {Y \equiv f\left( {XY}\right) }\right\rbrack$

Note. Since $f$ is monotonic in its second argument, these extreme solutions exist on account of the Theorem of Knaster-Tarski. (End of Note.)

will stand for a bag of predicates $W$ will stand for a bag of predicate pairs (which will be denoted by $\left( {X,Y}\right)$ and are ordered pairs) ${Xw}$ will stand for the predicate given by $\left\lbrack {{Xw} \equiv \left( {\underline{A}\left( {X,Y}\right) : \left( {X,Y}\right) \text{ in }W : X}\right) }\right\rbrack$ YW will stand for the predicate given by [YW ≡ (A(X,Y): (X,Y) in W: Y)]

Definitions

Let $k$ be a predicate transformer with one argument. By " $k$ is conjunctive over $V$ " we mean

[ k (\underline {{A}} X: X _ {\mathrm {i n}} V: X) \equiv (\underline {{A}} X: X _ {\mathrm {i n}} V: k X) ] (0)

Six types of conjunctivity are introduced, depending on the restrictions imposed on $V$ ; note that, the stronger the restrictions on $V$ , the weaker the type of conjunctivity.

0 universal conjunctivity means conjunctivity over 0 unbounded conjunctivity means conjunctivity over all non-empty V 0 denumerable conjunctivity means conjunctivity over all non-empty denumerable V 0 (finite) conjunctivity means conjunctivity over all non-empty finite 0 and- continuity means conjunctivity over all non-empty denumerable $V$ ,the elements of which can be ordered as a strengthening sequence monotonicity means conjunctivity over all non-empty finite $V$ , the elements of which can be ordered as a strengthening sequence.

Note that removal from the above list of either finite conjunctivity or and- continuity - neither of

which implies the other - leaves five types of conjunctivity listed in the order of decreasing strength.

By " $f$ enjoys a certain type of conjunctivity in its first argument" we mean that $F?Y$ en- joys that same type of conjunctivity for all $Y$ , and similarly for its second argument.

Besides $f$ ’s conjunctivity in its individual arguments, we introduce its so-called "double conjunctivity" -in the same six types-. With " $f$ is doubly conjunctive over $W$ " we mean

[ f X _ {w} Y _ {w} \equiv (\underline {{A}} (X, Y): (X, Y) _ {\underline {{i n}}} W: f X Y) ] . (i)

In the case of double and continuity and double monotonicity the notion "strengthening" should be taken element-wise: "(X, Y) is as strong as (X', Y')." means $\left\lbrack {X ⇒ {X}^{\prime }}\right\rbrack ∧ \left\lbrack {Y ⇒ {Y}^{\prime }}\right\rbrack$ .

Examples. Double conjunctivity is not such an un- likely property as it might seem at first sight. With ${ko}$ and ${k1}$ enjoying some type of conjunctivity, $f$ defined by

[ f X Y \equiv k 0 X \wedge k 1 Y ]

enjoys the same type of double conjunctivity;

[ f \times Y \equiv i f B \rightarrow k 0 X ] \rightarrow B \rightarrow k 1 Y [ f _ {i} ]

(End of Examples.)

The results

Theorem 0. An $\pmb{f}$ enjoying some type of double conjunctivity enjoys the same type of conjunctivity in both its arguments for all types except universal conjunctivity.

Theorem 1. An $f$ that is and-continuous or mono-tonic in both its arguments enjoys the same type of double conjunctivity.

Remark. In view of Theorem 0, the formulation of Theorem 1 could have been extended with "and vice versa". (End of Remark.)

Theorem 2 With f enjoying double conjunctivity of some type, h enjoys conjunctivity of the same type.

Theorem 3 With f enjoying double conjunctivity of some type, g enjoys conjunctivity of the same type , for all types except universal conjunctivity and and- continuity.

In some of our considerations $f$ and $W$ will be connected by

(\underline {{A}} (X, Y): (X, Y) \underline {{\mathrm {i n}}} W: [ f X Y \equiv Y ]) \qquad (2).

Theorem 4 With f enjoying universal,unbounded, denumerable or finite double conjunctivity and W of the corresponding type and satisfying (2) we have

(\underline {{A}} (X, Y): (X, Y) \underline {{\mathrm {i n}}} W: [ g X w \equiv Y w \wedge g X ])

or, alternatively,

(E (X, Y): (X, Y) _ {\mathrm {i n}} W: [ g X \equiv Y ]) ⇒ [ g X _ {w} \equiv Y _ {w} ].

The proofs

In many subsequent proofs we shall construct, given a $V$ , a special $W$ that suits our purpose. These constructions being similar, we can connect universal quantifications over $V$ and $W$ by

Lemma 0 With $V$ and $W$ for some $k$ satisfying

(X, Y) \underline {{\operatorname {i n}}} W \equiv X \underline {{\operatorname {i n}}} V \wedge [ Y \equiv k X ] \mathrm {f o r a l l} X, Y (3)

we have for any predicate transformer $q$ with two arguments

[ (\underline {{A}} (X, Y): (X, Y) _ {\underline {{\mathrm {i n}}} W}: q X Y) \equiv (\underline {{A}} X: X _ {\underline {{\mathrm {i n}}} V}: q X (k X)) ] (4)

with the special cases $- \left\lbrack {9 \times Y \equiv X}\right\rbrack -$

[ X _ {w} \equiv (\underline {{A}} X: X _ {\underline {{i n}}} V: X) ] \tag {5}

\begin{array}{l} a n d - [ q X Y \equiv Y ] - \ [ Y _ {w} \equiv (\underline {{A}} X: X _ {\mathrm {i n}} V: k X) ] . (6) \ \end{array}

(lemma 0 is neither deep nor beautiful; it just comes in handy.)

Proof. We have to establish (4); in order to do so we observe for all $Z$

\begin{array}{l} [ Z \equiv (\underline {{A}} (X, Y): (X, Y) \underline {{\underline {{\operatorname {i n}}}}} W: q X Y) ] \ = {(3) } \ [ Z \equiv (\underline {{A}} X, Y: X _ {\underline {{\mathrm {i n}}} V} \wedge [ Y \equiv k X ]: q X Y) ] \ \end{array}

\begin{array}{l} = {p r e d i c a t e c a l c u l u s } \ [ Z \equiv (\underline {{A}} X: X _ {\mathrm {i n}} V: (\underline {{A}} Y: [ Y \equiv k X ]: g X Y)) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ Z \equiv (\underline {{A}} X: X _ {\underline {{i n}} V}: q X (k X)) ] \ \end{array}

(End of Proof.)

Proof of Theorem 0

On account of the symmetry it suffices to show that $f$ enjoys the appropriate type of conjunctivity in its first argument, i.e.

[ f (\underline {{A}} X: X _ {\mathrm {i n}} V; X) Y ^ {\prime} \equiv (\underline {{A}} X: X _ {\mathrm {i n}} V: f X Y ^ {\prime}) ]

for any $Y^{\prime}$ and appropriate $V$ . The crux of the argument is the construction of an appropriate $W$ , and then to exploit $f$ 's double conjunctivity over that $W$ . We propose to construct $W$ by (3) with

[ k X \equiv Y ^ {\prime} ]

Note that in the classifications "non-empty/ denominatorable/finite/strengthening" $W$ is of the same type as $V$ . We now observe for any $Z$

\begin{array}{l} [ Z \equiv f (\underline {{A}} X: X _ {\mathrm {i n}} V; X) Y ^ {\prime} ] \ = {(5) } \ [ Z = f X _ {w} Y ^ {\prime} ] \ = {V i s n o n - e m p l y } \ [ Z \equiv f X _ {W} (\underline {{A}} \overline {{X}}: X _ {\underline {{i n}}} V: Y ^ {\prime}) ] \ = {(6) a n d [ k X \equiv Y ^ {\prime} ] } \ [ Z \equiv p X _ {w} Y _ {w} ] \ = {f d o u b l y c o n j u n c t i v e o v e r W, i. e. (1) } \ \end{array}

\begin{array}{l} [ Z \equiv (\underline {{\theta}} (X, Y): (X, Y) _ {\ln} W: f (X Y) ] \ = {(4) w i t h f f o r q a n d [ k X \equiv Y ^ {\prime} ] } \ [ Z \equiv (\underline {{\theta}} X: \dot {X} _ {\underline {{i n}}} V: f X Y ^ {\prime}) ] \ (E n d o f P r o o f o f T h e o r e m 0.) \ \end{array}

Proof of Theorem 1.

We associate with the strengthening sequence of predicate pairs $(X_i, Y_i)$ for $0 ≤ i ≤ N$ the strengthening sequences $X_i$ and $Y_i$ with the same non-empty range. Under the assumption of the appropriate conjunctivity in the individual arguments, we have to show

[ f (\underline {{A}} _ {i}: X _ {i}) (\underline {{A}} _ {i}: Y _ {i}) \equiv (\underline {{A}} _ {i}: f (X _ {i}) (Y _ {i})) ]

To this end we observe for all $Z$

\begin{array}{l} [ z \equiv f (\underline {{A}} _ {i}: X _ {i}) (\underline {{A}} _ {i}: Y _ {i}) ] \ = {f a p p r o p r a t e l y c o n j u n c t i v e i n i t s 1 s t a r g u m e n t } \ [ z \equiv (\underline {{A}} i: f (X _ {i}) (\underline {{A}} j: Y _ {j})) ] \ = {\text {p a p p r o p r i a t e l y c o n j u n c t i v e i n i t s 2 n d a r g u m e n t} } \ [ Z \equiv (\underline {{A}} i, j: P (X _ {i}) (Y _ {j})) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ \dot {z} \equiv (\underline {{A}} j, i: i ≤ j: f (x _ {i}) (y _ {j})) \wedge (\underline {{A}} i, j: j ≤ i: f (x _ {i}) (y _ {j})) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ Z \equiv (\underline {{A}} _ {j}: (\underline {{A}} _ {i}: i s j: f (x _ {i}) (Y _ {j}))) \wedge (\underline {{A}} _ {i}: (\underline {{A}} _ {j}: j s i: f (x _ {i}) (Y _ {j}))) ] \ = {f \mathrm {i s m o n o t o n i c i n e i t h e r a r g u m e n t} X _ {i} \mathrm {a n d} \ Y _ {j} a r e s t r e n g t h e n i n g s e q u e n c e s } \ [ Z \equiv (\underline {{A}} _ {j}: f (X _ {j}) (Y _ {j})) \wedge (\underline {{A}} _ {i}: f (X _ {i}) (Y _ {i})) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ Z \equiv (\underline {{A}} _ {i}: f (X _ {i}) (Y _ {i})) ] \ \end{array}

(E n d o f P r o o f o f T h e o r e m 1.)

Since the remaining theorems deal with extreme solutions, the time has come to capture the properties of $g$ and of $h$ formally. Thanks to the Theorem of Knaster-Tarski we can state

[ f X (g X) \equiv g X ] \qquad \mathrm {f o r a l l} X \qquad (7)

\underline {{A Y}}: [ f X Y ⇒ Y ]: [ g X ⇒ Y ]) \mathrm {f o r a l l} X \tag {8}

[ h X \equiv f X (h X) ] \qquad \mathrm {f o r a l l} X \qquad (g)

(\underline {{A Y}}: [ Y ⇒ f X Y ]; [ Y ⇒ h X ]) \mathrm {f o r a l l} X \tag {10}

Before embarking on our proofs proper we present two lemmata.

Lemma 1 With $f$ doubly conjunctive over $W$ and

(\underline {{A}} (X, Y): (X, Y) _ {\mathrm {i n}} W: [ f X Y \equiv Y ]) \tag {2}

we have

[ f X _ {w} Y _ {w} \equiv Y _ {w} ] . \tag {11}

\begin{array}{l} \begin{array}{l l} \mathrm {P r o o f} & \mathrm {t r u e} \end{array} \ = {f d o u b l y c o n j u n c h i v e o v e r W, h u n c e (1) } \ [ p X w Y w \equiv (\tilde {A} (X, Y): (X, Y) \underline {{\underline {{\ln}}}} W: f X Y) ] \ = {(2) } \ [ f X _ {w} Y _ {w} \equiv (\underline {{A}} (X, Y): (X, Y) \underline {{\underline {{i n}}}} W: Y) ] \ = {\mathrm {d e f i n i t i o n} Y _ {w} } \ [ P X _ {w} Y _ {w} \equiv Y _ {w} ] \ \end{array}

(End of Proof.)

Lemma 2. With $f$ doubly monotonic, $g$ and $h$ are monotonic as well.

Remark. Note that Lemma 2 is subsumed in Theorems 2 and 3 ; it is proved separately since we wish to use it in the proofs of the full theorems. (End of Remark.)

Proof. Theorem 0 tells us that $f$ is monotonic in both its arguments. We observe for any $x_0$ and $x_1$

[ X _ {0} ⇒ X _ {1} ]

⇒ {f \mathrm {i s m o n o t o n i c i n i t s 1 s t a r g u e m e n t} }

[ f X _ {0} (g X _ {1}) ⇒ f X _ {1} (g X _ {1}) ]

= {(7) }

[ f X _ {0} (g X _ {1}) ⇒ g X _ {1} ]

⇒ {(8) }

[ g X _ {0} ⇒ g X _ {1} ]

and similarly

\begin{array}{l} [ X _ {0} ⇒ X _ {1} ] \ ⇒ {f \mathrm {i s m o n o t o n i c i n i t s 1 s t a r g u e m e n t} } \ [ f X _ {0} (h X _ {0}) ⇒ f X _ {1} (h X _ {0}) ] \ = {(g) } \ [ h X _ {0} ⇒ f X _ {1} (h X _ {0}) ] \ ⇒ {(1 0) } \ [ h X _ {0} ⇒ h X _ {1} ] \ \end{array}

(End of Proof.)

Proof of Theorem 2

Since $f$ enjoys some type of double conjunctivity, $f$ is doubly monotonic; hence -Lemma 2- h is monotonic.

In order to show that $h$ is conjunctive over $V$ , i.e.

[ h (\underline {{A}} X: X _ {\mathrm {i n}} V: X) \equiv (\underline {{A}} X: X _ {\mathrm {i n}} V: h X) ]

we show that either side implies the other

(i) Because $h$ is monotonic we have

(ii) To show the implication in the other direction we construct a bag $W$ according to (3), but this time with h for k. Since h is monotonic, to a V ordered as a strengthening sequence corresponds a W ordered as a strengthening sequence; since, furthermore, w is as non-empty/ denumerable/finite as V, V and W are of the same type.

Because $\left\lbrack {Y \equiv hX}\right\rbrack$ implies on account of (9) $\left\lbrack {Y \equiv f{XY}}\right\rbrack$ ,a second consequence of our choice of $h$ for $k$ is that $W$ satisfies condition (2) of Lemma 1 ; hence (11) holds. And now we ob-serve for any $Z$

\begin{array}{l} [ h (\underline {{A}} X: X _ {\underline {{i n}}} V: X) ⇒ (\underline {{A}} X: X _ {\underline {{i n}}} V: h X) ] \ [ z \equiv (\underline {{a}} x: x _ {\underline {{i n}}} v: h x) ] \ = {(6) } \ [ Z \equiv Y _ {W} ] \ ⇒ {(1 1) a n d (1 0) } \ [ Z ⇒ h X _ {W} ] \ = {(5) } \ [ z ⇒ h (\underline {{A}} X: X \underline {{\ln V}}; X) ] \ \end{array}

(End of Proof of Theorem 2.)

Of the remaining two theorems we prove Theorem 4. First since that is the heart of the matter: provided that among a bunch of solutions at least one is the strongest, their conjunction is a strongest solution. Once Theorem 4 has been established, the proof of Theorem 3 is a walk-over.

Proof of Theorem 4

In order to establish $\left\lbrack {g{x}{w} \equiv {Y}{w} ∧ g{X}_{r}}\right\rbrack$ For any $X$ such that,for some $Y,\left( {X,Y}\right)$ in $W$ ,we establish that either side implies the other.

(i) The conditions of Lemma 1 being satisfied, we conclude from (11) and (8)

[ g X _ {w} ⇒ Y _ {w} ]

With $f$ doubly conjunctive, hence doubly monotonic, -Lemma 2- $g$ is monotonic,and on account of $\left\lbrack {{Xw} ⇒ X}\right\rbrack$ - definition of ${Xw} -$ we conclude

[ g X _ {w} ⇒ g X ]

Combination yields $\left\lbrack {g{x}{w} ≥ {Y}{w} ∧ gX}\right\rbrack$ .

(ii) The crux of the proof of $\left\lbrack {{Y}{w} ∧ gX ⇒ g{X}{w}}\right\rbrack$ consists of rewriting this as $\left\lbrack {gX ⇒ g{X}{w} \vee ?{Y}{w}}\right\rbrack$ and showing -see (8)- that $g{X}{W} \vee ?{Y}{W}$ satisfies the equation of which $g\left( X\right)$ is the strongest solution,i.e. of showing

[ f X (g X w \vee ¬ Y w) ⇒ g X w \vee ¬ Y w ] . (1 2)

To this end we observe

true

= {(7) }

[ f X _ {w} (g X _ {w}) \equiv g X _ {w} ]

$⇒ { f$ is monotonic in both its arguments - Theorem ③

[ f (X \wedge X _ {w}) (g X _ {w} \wedge Y _ {w}) ⇒ g ^ {\vee} X _ {w} ]

= {\mathrm {p r e d i c a t e c a l c u l u s} }

[ f ^ {\prime} (X \wedge X _ {w}) ((g X _ {w} \vee Y _ {w}) \wedge Y _ {w}) ⇒ g X _ {w} ]

= {f i s d o u b l y c o n j u n c t i v e }

[ f ^ {\prime} X (g X _ {w} \vee ¬ Y _ {w}) \wedge f X _ {w} Y _ {w} ⇒ g X _ {w} ]

= {(1 1) \mathrm {f r o m L e m m a 1 , (2) b e i n g s a t i s f i e d} }

[ f X (g X _ {w} \vee ¬ Y _ {w}) \wedge Y _ {w} ⇒ g X _ {w} ]

= {\mathrm {p r e d i c a t e c a l c u l u s} }

(12)

(End of Proof of Theorem 4.)

Proof of Theorem 3.

We construct a bag $W$ according to (3), but this time with $g$ for $k_i$ . $W$ being as non-empty/denumerable/finite as $V$ , $V$ and $W$ are of the same type.

Because $\left\lbrack {Y \equiv gX}\right\rbrack$ implies on account of (7) $\left\lbrack {f{XY} \equiv Y}\right\rbrack ,\left( 2\right)$ is satisfied and Theorem 4 is applicable. Since $W$ is non-empty,we conclude from Theorem 4

[ g X _ {w} \equiv Y _ {w} ] \tag {13}

And now we observe for any $z$

\begin{array}{l} [ Z \equiv (\underset {\sim} {A X}: X _ {\ln} V: g X) ] \ = {(6) o f l e m m a 0 w i t h g f o r k } \ \end{array}

\begin{array}{l} [ Z \equiv Y _ {W} ] \ = {(1 3) } \ [ Z \equiv g X _ {w} ] \ = {(5) o f L e m m a 0 } \ [ Z \equiv g (\underset {\sim} {A} X: X _ {\underline {{\mathrm {i n}}} V: X}) ] \ \end{array}

The above argument deals with unbounded, denumerable, and finite conjunctivity; the case of monotonicity is covered by Lemma 2.

(E n d o f P r o o f o f T h e o r e m 3.)

Supplementary remarks about the theorems

Theorem 0's exception of universal conjunctivity is justified: $f$ given by $\left\lbrack {f \times Y \equiv X ∧ Y}\right\rbrack$ is universally doubly conjunctive but not universally conjunctive in its individual arguments

Theorem 1's restriction to and-continuity and monotonicity is justified: given by $[fXY \equiv X \vee Y]$ is universally conjunctive in its individual arguments but not even finitely doubly conjunctive.

Theorem 3's exception of universal conjunctivity is justified: $f$ given by $[fXY \equiv Y]$ is uni-versally doubly conjunctive, the strongest solution of $Y: [Y \equiv Y]$ is, however, false, i.e. unboundedly but not universally conjunctive.

Also Theorem 3's exception of and- continuity is justified. To this purpose we consider a space of

which integer $r$ is one of the coordinates. With $f$ given by $[fX Y \equiv X \vee Y_{r+1}^{r}]$ , $f$ is doubly and-continuous since it is and-continuous in both its arguments - see Theorem 1-. The strongest solution $g X$ of $Y: [X \vee Y_{r+1}^{r} \equiv Y]$ is for all $X$ given by

[ g X \equiv (\underline {{E}} i: i > 0: X _ {r + i} ^ {r}) ]

The strengthening sequence $[X_{j} \equiv r ≥ j]$ for $j ≥ 0$ is a sequence over which $g$ is not conjunctive, hence $g$ is not and-continuous.

Theorem 4's exception of and- continuity and monotonicity is justified: with $f$ given by $[fX Y \equiv X \vee Y]$ , $f$ is (again) doubly and-continuous (and, hence, doubly monotonic as well). For this $f$ we have $[g X \equiv X]$ . The strengthening sequence $W$ given by ${(\text {true }, \text {true }) (\text {false }, \text {true })}$ provides a counterexample.

The duality

Associated with each predicate transformer is its so-called "conjugate", denoted by adding an asterisk to the function symbol. By definition

[ k ^ {} X \equiv ¬ k (¬ X) ], [ p ^ {} X Y \equiv ¬ f (¬ X) (¬ Y) ], e t c.

The relation is a mutual one: the conjugates of ${k}^{ * }$ and ${f}^{ * }$ are $k$ and $f$ respectively.

From the above it follows that a predicate transformer over which negation distributes, e.g.

[ ¬ f \times Y = f (¬ X) (¬ Y) ]

is its own conjugate.

Warning For any program $S$ such that the final state is a total function of the initial state, i.e. any deterministic $S$ with [wp(S, true)], wp(S,?) is its own conjugate. Consequently, in order to appreciate in programming terms the distinction between a predicate transformer and its conjugate, we have to include nontermination and/or nondeterminacy into our considerations. (End of Warning.)

We define " $k$ is disjunctive over $V$ " to mean

[ k (\operatorname {E X}: X \mathrm {i n} V: X) \equiv (\operatorname {E X}: X \mathrm {i n} V: k X) ]

and introduce the six types of disjunctivity by rewriting the definitions of the conjunctivity types with the following substitutions:

"disjunctivity", for "conjunctivity". "or- continuity" for "and- continuity" "weakening" for "strengthening".

double disjunctivity is introduced similarly. As a result, the disjunctivity of $k$ and the conjunctivity of ${k}^{ * }$ are of the same type,and similarly for $f$ and ${f}^{ * }$

The strongest solution of $Y$ : $\left\lbrack {f{XY} ⇒ Y}\right\rbrack$ is the conjugate of the weakest solution of the conj. juge equation $Y$ : $\left\lbrack {Y ⇒ {f}^{ * }{XY}}\right\rbrack$ .

The above allows the dual formulation of the Theorems,

e.g. Theorem 2*. With f enjoying double disjunctivity of some type, g enjoys disjunctivity of the same type. Acknowledgement We are greatly indebted to the Tuesday Afternoon Club, which spent two sessions disentangling the prior version EWD849. (End of Acknowledgement.)

29 April 1983

drs. C.S. Scholten Scientific Advisor Philips Research Laboratories 5600 JA EINDHOVEN The Netherlands

prof. dr. Edsger W. Dgksra Burroughs Research Fellow Plataanstraat 5 5671 AL NUENEN The Netherlands