On different notions of termination (with C.S.Scholten)

On different notions of termination

A repetition terminates for a given initial state means that after some number of iterations its guards are false. In the presence of unbounded nondeterminacy an upper bound for this number of iterations need not exist, the canonical example being

\begin{array}{l} d o x > 0 \rightarrow x := x - 1 \ \prod x < 0 \rightarrow x := a n y n a t u r a l n u m b e r \ \frac {o d}{.} \ \end{array}

So-called strong termination means that such an upper bound exists. (The above program terminates for all initial states, but only strongly for $x ≥ 0$ .)

Note. In the absence of unbounded nondeterminacy termination is always strong. (End of Note.)

We would like to relate the above rather operational notion of termination to semantics defined by predicate transformation. To this end we have to capture first the notion of machine states in terms of predicates.

Point complements

In the following $p$ and $q$ will be used to denote so-called "point complements". For each point in state space there exists one point complement, i.e. a predicate that is false in that point and true everywhere else. We postulate for point complements

\begin{array}{l} A x i o m 0: [ (E p: ¬ p) ] \ \mathrm {A x i o m 1 :} [ p v Q ] ≠ [ p v ¬ Q ] \mathrm {f o r a l l} Q \mathrm {a n d p o i n t c o m p l e m e n t} p. \ \end{array}

For a person with an intuitive appreciation of point complements, these axioms express "obvious" properties of point complements. Point complements enjoy more equally "obvious" properties. These, however, we shall prove from the above two, thus justifying their being called "Axioms".

[\left\lbrack {p \equiv q}\right\rbrack ≠ \left\lbrack {{pv}q}\right\rbrack ]

Proof of Lemma 0.

\begin{array}{l} [ p \equiv q ] \ = \left{ \begin{array}{l} \text {p r e d i c a t e c a l c u l u s} \ [ (p v 7 g) \wedge (q v 7 p) ] \end{array} \right. \ = {p r e d i c a t e c a l c u l u s } [ p v 7 9 ] \wedge [ q v 7 p \ = {A x i o m 1, a p p l i e d t o b o t h t e r m s } \ = {p r e d i c a t e c a l c u l u s } \ ≠ {p r e d i c a t e c a l c u l u s } \ \end{array}

(End of Proof of Lemma 0.)

[\left\lbrack {Q \equiv \left( {\underline{E}p : \left\lbrack {p \vee Q}\right\rbrack : ¬ p}\right) }\right\rbrack \text{for all}Q\text{.}]

Proof of Lemma 1. We have for all $Q$

true

\begin{array}{l} = {A x i o m 0 } [ Q \equiv Q ∧ (E _ {p: p}) ] \ = {\text {p r e d i c a t e c a l c u l u s} } [ Q \equiv (\underline {{E}} p: Q ∧ ¬ p) ] \ = {A x i o m 1 } \ [ Q \equiv (E _ {p}: [ p \vee Q ] \vee [ p \vee ¬ Q ]; Q \wedge ¬ p) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } [ Q \equiv (\underline {{E}} p: [ p \vee Q ]: Q \wedge ¬ p) ] \ \end{array}

\begin{array}{l} = {[ P \lor Q ] \equiv [ ¬ P \equiv Q ∧ ¬ P ] f o r a l l P a n d Q } \ [ Q \equiv (\mathrm {E} _ {P}: [ P v Q ]: - P) ] \ (E n d o f P r o o f o f L e m m a 1.) \ \end{array}

Note. The role of the above Axioms and Lemmata can be interchanged: Axiom O can be proved from Lemma1, Axiom 1 can be proved from Lemmata O and 1. (End of Note.)

Substituting in Lemma 1.7Q for $Q$ yields, by virtue of Axiom 1

Corollary O [Q= (A p : [p v Q] v p)] For all Q

For later purposes we need Lemma 2, which deals with a situation in which existential and universal quantifica-tion can be interchanged; its proof relies on Axiom 1 only.

Lemma 2. For all point complements $p$ and all sets $S$ of predicates we have

[ p v (\underline {{E}} Q: Q _ {\mathrm {i n}} S: Q) ] \equiv (\underline {{E}} Q: Q _ {\mathrm {i n}} S: [ p v Q ])

Proof of Lemma 2. We have for all $p$ and $S$

\begin{array}{l} [ p v (\underline {{E}} Q: Q \underline {{i n}} S: Q) ] \ ≠ {A x i o m 1 } \ [ p \vee ¬ (\equiv Q: Q \ln S: Q) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ p v (A Q: Q \mathrm {i n} S: 7 Q) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ (A Q: Q \mathrm {i n} S: P V ¬ Q) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} Q: Q, \underline {{i n}} S: [ p v, q ]) \ = {\tilde {A} x i o m 1 } \ (\underline {{A}} Q: Q \mathrm {i n} S: ¬ [ p v Q ]) \ ≠ {\mathrm {p r e d i c a t e c a l c u l u s} } \ \end{array}

(EQ: Q in S: [pvQ])

(End of Proof of Lemma 2.)

Let -for the time being without further qualification of the notion of termination- $wp(S,R)$ stand,as usual, for the weakest condition on the initial state such that S is guaranteed to establish R . In order to familiarize ourselves a bit more with point complements, we explore the meanings of [pvwp(S,q)] and [pvivp(S,q)].

Let sp and sq denote the single states in which $p$ and $q$ , respectively, are false. Then, $wp(S,q)$ characterizes all initial states guaranteed to lead to a final state different from $sq$ . Hence $[p \lor wp(S,q)]$ is the assertion that an execution of $S$ , started in $sp$ , will terminate in a state different from $sq$ . Conversely, $7wp(S,q)$ characterizes all initial states for which termination outside $sq$ cannot be guaranteed; hence $[p \lor 7wp(S,q)]$ is the assertion that the class of executions possible when $S$ is started in $sp$ contains at least one execution that either fails to terminate or ends in $sq$ .

On account of Axiom 1 we have

[ p \vee w p (S, T) ] ≠ [ p \vee ¬ w p (S, T) ]

and we investigate the 2 exclusive cases.

$\left\lbrack {p \vee {wp}\left( {S,T}\right) }\right\rbrack$ : in this case termination of $S$ when started in sp is guaranteed and $\left\lbrack {p \vee {twp}\left( {S,q}\right) }\right\rbrack$ then means sq is a possible final state.

[PPV]wp(S,T)]: in this case termination of S when started in sp is not guaranteed and, on account

of the monotinicity of $w p\left( {S,q}\right)$ ,we have $\left\lbrack {{pv} - {wp}\left( {S,q}\right) }\right\rbrack$

With some poetic license we shall describe the situation $[p \vee ¬ w p(S, q)]$ , regardless of the value of $[p \vee w p(S, T)]$ , as " $q$ is a successor of $p$ ".

We are interested in termination, that is in repetitions. With

DO: do $B \rightarrow S$ od and If: if $B \rightarrow S$ foci our interest in the equivalence of

DO and if $B\to \mathsf{IF};D0| ¬ B\to \mathsf{skip}$ can be translated into interest in the equivalence of

${wp}\left( {{DO},T}\right) {and} {wp}\left( {{IF},{wp}\left( {{DO},T}\right) }\right) \vee {TB}$

i.e. the question whether ${wp}\left( {{DO},T}\right)$ is a solution of

X: [ X \equiv f X ] \mathrm {w i t h} [ f X \equiv w p (I F, X) \vee ¬ B ] \mathrm {f o r a l l} X.

The predicate transformer $f$ cannot be interpreted as a weakest precondition -it violates the Law of the Excluded Miracle-, yet, stretching the notion of "successor" still further, we shall also describe the situation $[p \lor q]$ as "q is a successor of p". (Strictly speaking we should have added "with respect to $w_{P}(S, ?)$ " and "with respect to f" respectively.) For a further interpretation of [pv ifq] we consider again 2 exclusive cases.

[pvB]: in this case, DO, when started in sp , does not immediately terminate and [pvIfq] means that the class of possible executions of S when started in sp contains at least one execution that either fails to terminate or ends in sq .

[pV1B]: in this case DO, when started in sp, immediately terminates and, as will be shown, sp has no successor.

Proof. [pvtnB] $= { {Axiom} 1}$ $n \in [p \vee B\rbrack$ $⇒ { {by} {pred} {a}^{c}t{e} {cal} {culus} {for} {any} g}$ $¬ \left\lbrack {{p}^{v}\left( {B ∧ {twp}\left( {I{F}{q}}\right) }\right) }\right\rbrack$ $= {$ definition of ${f3}$ ${71}\left\lbrack {{pv}{f}{q}}\right\rbrack$ (End of Proof.)

In the case of nested repetitions an infinite computation obviously implies that at least one repetition fails to ter- minate; stronger, in any infinite computation precisely one repetition displays infinite repetition: its interior repetitions obviously terminate and its embracing repetitions don't make progress. Therefore, investigations about termination or infinite repetition of do $B\rightarrow S$ od can be carried out in isolation, i.e. under the assumption that each activation of S terminates . Under this assumption, [p v ifq] means that, operationally speaking, sq is a genuine possible successor of sp .

A "decreasing chain" is defined to be a non-empty sequence of point complements such that of any two consecutive predicates in this sequence the second one is a successor of the first one; a decreasing chain is said "to start at" its first predicate. A maximal decreasing chain is a decreasing chain that cannot be extended, i.e. does not end at a predicate with one or more successors. A maximal decreasing chain of finite length therefore ends at a predicate with no successor. The length of a decreasing chain is defined as the number of predicates in the chain.

After the above we can now formulate the two main results of this note, viz.

Theorem 0. For unboundedly conjunctive $f$ and any point complement $p$

[ p v (E i: i \ge 0: f ^ {i} F) ] \equiv

(there exists an upper bound for the lengths

Theorem 1. For unboundedly conjunctive $f$ ,let $Q$ be the strongest solution of ${X}^{ \circ }\left\lbrack {{fX} \equiv X}\right\rbrack$ ; then for any point complement $p$

[ p \vee Q ] \equiv

(all decreasing chains starting at p are of finite length)

Remark on nomenclature. Predicate transformer $f$ is unboundedly conjunctive means

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

for any non-empty set $S$ of predicates. (End of Re- mark on nomenclature.)

Note that Theorem 1 could have stated that $\mathbb{Q}$ is the weakest predicate such that the solutions of $p: [p \vee Q]$ are well-founded with respect to the successor relation.

We have shown earlier - see EWD 822- that for monotonic $f$ - and hence for unboundedly conjunctive $f - \left( {{E}_{i} : i ≥ 0 : {p}^{i}F}\right)$ is at least as strong as any solu-tion of $X : \left\lbrack {{pX} \equiv X}\right\rbrack$ . Fortunately, this is compatible with "of bounded length" being a stronger property than "of finite length".

In EWD822 we have also shown that for or-continuous $f$ -i.e. in the absence of unbounded nondeterminacy- $[Q\equiv (\underline{E} c:c≥ 0:\underline{F}^i)]$ . In that case it is irrelevant whether we define $wp(D_{0,T})$ as $Q$ or as (Ec:c:c:F) Otherwise we have to distinguish between wpb and wpf -for "bounded"and finite" respectively-,the general formulae being

[ w p b (D O, R) \equiv (\underline {{E}} c: c \ge 0: f ^ {i} F) ]

\begin{array}{l} {[ w p f (D O, R) \equiv Q ]} \ {\mathrm {w i t h} Q \mathrm {t h e s t r u n g e s t s o l u t i o n}} \ {\mathrm {o f} X: [ f X = X ]} \end{array}

where $f$ is defined by $\left\lbrack {{f}^{X} \equiv {w\rbrack }\left( {{IF},X}\right) \vee {¬ B} ∧ R}\right\rbrack$ .

In order to prove Theorems O and 1 we need a lemma connecting $fQ$ for general $Q$ with the successor relation, which is one between point complements: Lemma 3 For unboundedly conjunctive $f$ and any predicate $Q$ satisfying $¬ [Q] \vee [fT]$ and any point complement $p$

[ p v f Q ] \equiv (\underline {{A}} q: [ p v ¬ f q]: [ q v Q ])

Proof. The somewhat mysterious condition $¬ [Q] \lor [F T]$ occurs because, in combination with $f$ 's unbounded conjunctivity, it allows us to conclude

[ f (\underline {{A}} q: [ q \vee ¬ Q ]; q) \equiv (\underline {{A}} q: [ q \vee ¬ Q ]; f q) ] . ^ {*}

In the case $¬ \left\lbrack Q\right\rbrack$ the above follows from ${f}^{\prime }s$ unbounded conjunctivity and the fact that the range of $q$ is not empty; in the case [PT] the above follows because then $f$ is universally conjunctive.

The remainder of the proof proceeds as follows. For any $p$

\begin{array}{l} [ p \vee f Q ] \ = {\text {C o r o l l a r y} 0 } \ [ p \vee f (\underline {{A}} q:: [ q \vee Q ] \vee g) ] \ = {\text {p r e d . c a l c . a n d A x i o m 1} } \ [ p \vee f (\underline {{A}} q: [ q \vee ¬ Q ]: q) ] \ = {\text {s e c} ^ {*} \mathrm {a b o v e} } \ [ p \vee (\underline {{A}} q: [ q \vee ¬ Q ]: f q) ] \ = {\mathrm {p r e d . c a l c .} } \ [ (\underline {{A}} q: [ q \vee ¬ Q ]: p \vee {q }) ] \ = {\mathrm {p r e d . c a l c .} } \ (\underline {{A}} q: [ q \vee ¬ Q ]: [ p \vee f q ]) \ = {\mathrm {p r e d . c a l c . a n d A x i o m} 1 } \ (\underline {{A}} q: [ p \vee ¬ f q ]: [ q \vee Q ]) \ \end{array}

(End of Proof.)

We shall first use Lemma 3 with $F$ for $Q$ , yielding -using the definition of functional composition - Lemma 4. For unboundedly conjunctive $f$ , natural $i$ , and point complement $p$

[ p \vee f ^ {i + 1} F ] \equiv (\underline {{A}} q: [ p \vee f q ]: [ q \vee f ^ {i} F ])

Proof. In order to justify the appeal to Lemma 3, we have to demonstrate $[f^{i}T] ⇒ [f^{i}T]$ . For $i = 0$ , this is trivial; for the remaining cases we observe

\begin{array}{l} \mathbf {t r u e} \ = \left{ \begin{array}{l} p r e d. c a l c. \ [ f ^ {i - 1} F ⇒ T ] \end{array} \right} \ ⇒ {f ^ {i} \mathrm {i s m o n o t o n i c} } [ f ^ {i} F ⇒ f T ] \ ⇒ {\mathrm {p r e d . c a l c .} } [ f ^ {i} F ] ⇒ [ f T ] \ \end{array}

(End of Proof.)

In order to prove Theorem 0, one further step is needed: using Lemma 4, we shall interpret $[p v f^{\prime} F]$

in terms of decreasing chains.

Lemma 5. For unboundedly conjunctive $f$ ,natural $i$ ,and point complement

[ p \vee f ^ {c} F ] \equiv

(the length of any decreasing chain

starting at $p$ is at most i)

Proof. For $i = 0$ the above equivalence holds, both sides being false for all $p$ . For the remainder we proceed by mathematical induction over $i$ :

$= {$ definition of successor and induction hypothesis $}$ (Aq: q is a successor of p: the length of any decreasing chain starting at q is at most i)

$= {$ definition of decreasing chain starting at $p}$ (the length of any decreasing chain starting at $p$ is at most $i + 1$ )

\begin{array}{l} [ p \vee f ^ {i + 1} F ] \ = {l e m m a 4 } \ (\underline {{A}} q: [ p \vee ¬ f q ]: [ q \vee f ^ {i} F ]) \ \end{array}

(End of Proof)

Proof of Theorem 0.

[ p \vee (\underline {{E}} i: i \ge 0: f ^ {i} F) ]

= {\text {l e m m a} 2 }

(E i: i \ge 0: [ p \vee f ^ {i} F ])

= {\mathrm {L e m m a} 5 }

(Elc: c: 0: the length of any decreasing chain

$= {$ definition of upper bound $}$

(there exists an upper bound for the lengths

of the decreasing chains starting at $p$ )

In order to prove Theorem 1, we use Lemma 3 a second time, viz. with for $Q$ a solution of $X: [fX \equiv X]$ .

Lemma 6. For unboundedly conjunctive $p,q$

[ p \vee Q ] \equiv (\underline {{A}} q: [ p \vee f q ]: [ q \vee Q ])

Proof. Since $[p \vee Q] \equiv [p \vee fQ]$ , the above is nothing but the equivalence from Lemma 3. In order to justify the appeal to Lemma 3, we have to demonstrate $[Q] ⇒ [fT]$ .

\begin{array}{l} f r u e \ = {\mathrm {d e f i n i t i o n} o f Q } \ [ Q ^ {\prime} \equiv f Q ] \ ⇒ {f i s m o n o t o n i c } \ [ \dot {Q} ⇒ f T ] \ ⇒ {\text {p r e d . c a l c .} } \ [ Q ] ⇒ [ P T ] \ \end{array}

(End of Proof.)

Proof of Theorem 1. We shall prove Theorem 1 in the

\lnot [ p \lor Q ] \equiv

(there exists an infinite decreasing chain

s t a r t i n g a t p)

by showing that either side implies the other.

Applying de Morgan's Law to the conclusion of Lemma 6, we obtain

\begin{array}{l} ¬ [ p \vee Q ] \equiv (\mathrm {E q}: [ p \vee ¬ f q ]; ¬ [ q \vee Q ]) \ = {\mathrm {d e f i n i t i o n o f s u c c e s s o r} } \ \lnot [ p \lor Q ] \equiv (\mathrm {E q}: q \mathrm {i s a s u c c e s s o r o f} p: \lnot [ q \lor Q ]) \ \end{array}

H e n c e

\lnot [ p \lor Q ] ⇒ (\mathrm {t h e r e e x i s t s a n i n f i n i t e d e c r e a s i n g}

chain starting at $p$ )

Conversely, let $q$ i for $i ≥ 0$ and $\left\lbrack {{90} \equiv p}\right\rbrack$ be an infinite decreasing chain starting at $p$ . We have for any $Z$

\begin{array}{l} [ Z \equiv f (\underline {{\alpha}} i: i \ge 0: q i) ] \ = {{f } \mathrm {i s u n b o u n d e d l y c o n j u n c t i v e a n d r a n g e i n o n - e m p l y} } [ Z \equiv (\underline {{A}} i: i \ge 0: f (q i)) ] \ ⇒ {\mathrm {p r e d . c a l c} } \ [ Z ⇒ (\underset {A} {A} i: i ≥ 1: f (q _ {i})) ] \ = {\mathrm {r e n a m i n g t h e d u m m y} } \ [ Z ⇒ (A c: c ≥ 0: f (q (c + 1))) ] \ ⇒ {\mathrm {s i n c e} [ q \vdash v \vdash p (q (c + 1)) ] } \ [ Z ⇒ (\underline {{A}} i: < > 0: q i) ] \ \end{array}

hence (Ac: i.i.o. q.i) is a solution of $X$ : $\left\lbrack {{p}{X} ⇒ X}\right\rbrack$ Since $Q$ ,the strongest solution of $X$ : $\left\lbrack {{p}{X} \equiv X}\right\rbrack$ is -see EuD822 - also the strongest solution of $X$ : $\left\lbrack {{p}_{X} ⇒ X}\right\rbrack$ ,

\begin{array}{l} t r u e \ = {\mathrm {p r e v i o u s} k } \ [ Q ⇒ (A i: i \ge 0: q i) ] \ ⇒ {\mathrm {p r e d . c a l c . a n d} [ q 0 \equiv p ] \ [ \stackrel {\circ} {Q} ⇒ p ] \ = {\mathrm {p r e d . c a l c . a n d A x i o m 1} } \ \lnot [ p \lor Q ] \ \end{array}

(End of Proof of Theorem 1.)

15 October 1982

drs. C.S. Schohen

Scientific Adviser

Philips Research Laboratories

5600 JA EINDHOVEN

The Netherlands

pror. dr. Edsger W. Dyrkstra

Burroughs Research Fellow

Plataanstraat 5

5671 AL NUENEN

The Netherlands