A simple fix-point argument without the restriction to continuity (with A.J.M. van Gasteren)

A simple fix-point argument without the restriction to continuity.

Edsger W. Dgksra and A.J. M.van Gaasteren

Introduction

Notation In this text, the letters $\mathcal{B},\mathcal{P},\mathcal{R},\mathcal{X}$ , and Y stand for predicates on the state space of a program and square brackets are used as notation for universal quantification of the enclosed over the program variables. The letter S stands for a statement and DO for the repetitive construct do $\mathcal{B}\rightarrow \mathcal{S}$ od (see [3]). (End of Notation.)

Requiring Do to be semantically equivalent to its first unfolding

i f B \rightarrow S; D O ] ¬ B \rightarrow s k i p f i

yields that ${wp}\left( {{DO},¬ B ∧ P}\right)$ is a solution of the equation in predicate $X$

[\left\lbrack {X \equiv \left( {B ∧ {wp}\left( {S,X}\right) }\right) \vee \left( {¬ {B ∧ P}}\right) }\right\rbrack .]

Explanation Equation (0) Follows from the required semantic equivalence and

(i) the semantic definition of skip, viz. $\left\lbrack {{wp}\left( {{}^{\prime }{skip}^{\prime },R}\right) \equiv R}\right\rbrack$ for all $R$ ;

(ii) the semantic definition of statement concatenation, viz.

\begin{array}{l} [ w p (^ {\prime \prime} S _ {0}; S _ {1}, R) \equiv w p (S _ {0}, w p (S _ {1}, R)) ] \ f o r a l l S 0, S 1, a n d R; \ \end{array}

(iii) the semantic definition of the alternative construct, in particular

\begin{array}{l} \left[ w p \left(" i f B \rightarrow S 0 ∥ i B \rightarrow S _ {1} f _ {i} ^ {\prime \prime}, R\right) \equiv \right. \ (B ∧ w p (S _ {0}, R)) \lor (¬ B ∧ w p (S _ {1}, R)) ] \ f o r a l l B, S _ {0}, S _ {1}, a n d R \ \end{array}

For further details, see [3]. (End of Explanation.)

Notation and terminology With the exception of ${wp}$ , functional application is denoted by juxtaposition and iterated functional composition by exponentia-tion.

${}^{\prime \prime }X$ is at least as strong as ${Y}^{\prime \prime }$ means" ${\left\lbrack X ⇒ Y\right\rbrack }^{\prime \prime }$ .

predicatetransformer $f$ ismonotonic"means

[ X ⇒ Y ] ⇒ [ f X ⇒ f Y ] \mathrm {f o r a l l} X \mathrm {a n d} Y.

"predicate transformer $f$ is or-continuous means

[{\left\lbrack f\left( \underline{E}n : n ≥ 0 : {R}{n}\right) \equiv \left( \underline{E}n : n ≥ 0 : f{R}{n}\right) \right\rbrack for}]

weakening sequence of predicates $R_{n}$ , i.e. such that $(A_{n}:n≥ 0:[R_n⇒ R_{n + 1}])$

(End of Notation and Terminology.)

For monotonic predicate transformer $f$ ,the equation in $X \left\lbrack {X \equiv f{X}^{\prime }}\right\rbrack$ has a strongest solution (see [8]). If, in addition, $f$ is or-continuous, its strongest solution is given in closed form by

(1) $\left( {{E}_{n} : n ≥ 0}\right)$ false

Proof sketch Let $Y$ be the strongest solution of $[X \equiv fX]$ . Showing $[Y \equiv (\underline{E} n: n ≥ 0: f^n \text{false})]$ is done by showing separately

(i) $\left\lbrack {\left( {{E}_{n} : n ≥ 0}\right) {P}^{n}\text{false}}\right) ⇒ Y\rbrack$ and (ii) $\left\lbrack {Y ⇒ \left( {{En} : n ≥ 0 : {f}^{n}\text{ false }}\right) }\right\rbrack$

The proof of (i) is by mathematical induction on n and relies on the monotonicity of $f$ ; it uses that $Y$ is a solution of $\left\lbrack {X \equiv {f}^{\prime }X}\right\rbrack$ .

The proof of (ii) consists in showing that (Eni: 0. pf' false) is a solution of $[X \equiv fX]$ (of which $Y$ is the strongest solution); it relies on the or-continuity of $f$ (and on its monotonicity for the demonstration that the predicates ${f}^{n}$ false form a weakening sequence). (End of Proof Sketch.)

The predicate $w p\left( {{D0},¬ {B}^{ ∧ }P}\right)$ is (see [5]) defined as the strongest solution of (0). (Because $w p\left( {S,X}\right)$ is a monotonic function of $X$ ,so is the right-hand side of (0); hence its strongest solution exists.) If, in addition, $w p\left( {S,X}\right)$ is an or- continuous function of $X$ ,so is the right-hand side of (0),and an expression of the form of (1) gives a closed expression for $w p\left( {{D0},¬ {B}^{ ∧ }P}\right)$ .

In programming terms, or continuity of $w\rbrack$ is the same as nondeterminacy being bounded. The assumption of bounded nondeterminacy is a usual one to make: the closed form for

wp (DO, INP), which is then available, is tradi- tionally considered an advantage because it readily caters for the avoidance of fancy - and in practice cumbersome (see [1,2])- techniques like transfinite induction.

Since unbounded nondeterminacy cannot be implemented, the restriction to or-continuity has for a long time been regarded as quite reasonable. It has, however, led to theorems in which the restriction to or-continuity has been introduced not because the theorems demanded it but for the sake of their proofs. The restriction also became a nuisance in the mathematical treatment of abstract programs. Firstly, an abstract program may well contain the as yet unrefined statement "establish $\mathbb{P}$ " where $\mathbb{P}$ , viewed as equation, may have infinitely many solutions, an observation we owe to [0]. Secondly, the modelling of concurrency as a "fair" interleaving of atomic actions introduces undoubted nondeterminacy (see [6]).

We are therefore very pleased to show for the main theorem about the repetitive construct an elementary proof that, though not relying on or continuity, does not require transfinite formulas.

The theorem

Notation In the sequel, $x$ and $y$ stand for elements from a set $D$ . Set membership will be denoted by the infix operator "in"; our convention can thus be summarized by $x$ in $D$ and $y$ in $D$ . Function $t$ is a mapping from the state space (of a program) to $D$ , i.e. in each point of the state space the value of $t$ is an element of $D$ , a state of affairs that can be summarized by $[t$ in $D]$ . Let $C$ be a subset of $D$ ; note that then $t$ in $C$ stands for a predicate that may be true in some points of the state space, and false in others. (End of Notation.)

For the notion "well-founded" we refer to the appendix in which we show that well-foundedness is the same as the validity of a proof by mathematical induction. (For that reason, the design of a well-founded set that does the job is a regularly recurring theme in arguments about algorithms.)

After the above preliminaries we are ready to formulate our - well-known-

Theorem let $(D, < )$ be a partially ordered set; let $C$ be a subset of $D$ such that $(C, < )$ is well-founded; let statement $S$ , predicates $B$ and $P$ , and function $f$ on the state space satisfy

the predicate transformer $w p\left( {S,?}\right)$ is mono-

[ + \mathrm {i n} D ] ;

(2) $\left\lbrack {P ∧ B} \right\rbrack ⇒ f\underline{in}C\rbrack$ (3) $\left\lbrack {P ∧ B ∧ f = x ⇒ {wp}\left( {S,P ∧ f < x}\right) }\right\rbrack$ for all $x$ .

T h e n

(4) $\left\lbrack {P ⇒ {wp}\left( {{DO},¬ B ∧ P}\right) }\right\rbrack$ ,

where ${wp}\left( {{DO},7B ∧ P}\right)$ is defined as the strongest solution of (0).

In the above, the well-informed reader will recog- nize in $P$ the "invariant" of the repetition and in $t$ its "variant function", which is the vehicle for the termination argument.

The proof

The proof consists of three phases. In the first phase, we derive two lemmata we need for the justification of manipulations in the sequel. In the second phase, we massage the proof obligation so as to make it amenable to a proof using mathematical induction (since that is the only way of exploiting the well-foundedness of $(C, < )$ ). In the third phase, we carry out the inducive argument.

Conclusion (4) is proved by proving $\left\lbrack {P ⇒ X}\right\rbrack$ with $X$ any solution of (0).

(i) In the following, $y$ is a variable that may occur in $R$ only; as if need not occur in $R$ , $R_{t}^{y}$ stands for any predicate on the state space. We observe

\begin{array}{l} [ P \wedge R _ {x} ^ {y} ⇒ X ] () \ = {\mathrm {s i n c e}, \mathrm {f r o m} (0), [ X \equiv X \vee (¬ B \wedge P) ] } \ [ P ∧ R ] ⇒ X \lor (Y B ∧ P) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ P \wedge (B \vee ¬ P) \wedge R _ {\xi} ^ {4} ⇒ X ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ P \wedge B \wedge R ^ {2} ⇒ X ] (x x) \ = {(2) } \ [ P \wedge B \wedge f _ {\ln C} \wedge R _ {t} ^ {y} ⇒ X ] \ = {\mathrm {e q u i v a l e n c e o f} (x) \mathrm {a n d} (y x) \mathrm {w i t h} R := y \mathrm {i n} C ∧ R } \ [ P \wedge f _ {\ln} C \wedge R _ {t} ^ {y} ⇒ X ] \ = {\mathrm {o n e - p o i n t r u l e} } \ [ (\exists y: y = t: P ∧ y \in C ∧ R ⇒ X ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (A y: y \underline {{\underline {{\mathrm {i n}}}}} C \wedge R: [ P \wedge y = t ⇒ X ]) ( *) \ \end{array}

(ii) Next we massage our demonstrandum:

\begin{array}{l} [ P ⇒ X ] \ = {\mathrm {e q u i v a l e n c e o f} () \mathrm {a n d} ( * *) \mathrm {w i t h} R := \mathrm {t r u e a n d} \mathrm {a n d c h a n g i n g t h e d u m m y t o t h e f r e s h v a r i a b l e} x } \ \end{array}

(5) $\left( {\underline{A}x : x\underset{\text{ in }}{ = }C : \left\lbrack {P ∧ x = t ⇒ X}\right\rbrack }\right)$

In view of $C$ ’s well-foundedness,(5) is proved

by deriving - for any $x$ in $C$ -

(6) $\left\lbrack {P ∧ x = t ⇒ X}\right\rbrack$

under the hypothesis

(7) $\left( {A,y : y = c ∧ y < x : \left\lbrack {P ∧ y = f ⇒ X}\right\rbrack }\right)$

(iii) To this end we observe

(7)

\begin{array}{l} = {\mathrm {e q u i v a l e n c e o f} (x) \mathrm {a n d} (x + x) \mathrm {w i t h} R := y < x) } \ [ P ∧ t < x ⇒ X ] \ ⇒ {w p (S, ?) i s m o n o t o n i c } \ [ w p (S, P ∧ t < x) ⇒ w p (S, X) ] \ ⇒ {(3) } \ [ P ∧ B ∧ t = x ⇒ w p (S, X) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ P \wedge B \wedge f = x ⇒ B \wedge w _ {P} (S, X) ] \ = {\text {p r e d i c a t e} \mathrm {c a l c u l u s} } \ [ P \wedge (B \vee ¬ P) \wedge f = x ⇒ B \wedge w p (S, X) ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ P \wedge f = x ⇒ (B \wedge w p (S, X) \vee (f B \wedge P) ] \ = {(0) } \ [ P \wedge x = f ⇒ X ] , \ \end{array}

hence (6) has been proved under hypothesis (7).

(End of The Proof.)

Conclusion

To the best of our knowledge, Floyd (see [4]) has been the first one to formulate termination arguments in terms of well-founded sets; he did, however, restrict himself to deterministic programs, for which the natural numbers suffice.

In the fix-point theory that became envogue during the seventies, continuity was strictly adhered to, with the result that again the natural numbers sufficed (see [7]).

To the best of our knowledge, the above argu- ment is the first one to connect well-foundedness in its full generality directly to a non-operational notion of termination, i.e. to the strongest solution of a fix-point equation. Its simplicity should dispel the myth that the restriction to continuity for the sake of convenience is justified.

Finally we would like the reader to regard the effectiveness and austere rigour of our argument as a plea for the calculational proof method employed.

Acknowledgements

We are greatly indebted to C.A.R. Hoare for his formulation of antecedent (3), which he showed to

lead to a shorter proof than our original formula- tion, to C.S. Schohen for simplifying the formulation of the induction hypothesis, to W.H.J. Feyn for shortening our proof by the introduction of $(\ast \ast \ast)$ and to the Tuesday Afternoon Club for strengthening the theorem by weakening antecedent (2).

A short appendix on well-foundedness

In the following,

$\left( {C,k}\right)$ is a partially ordered set,

$x,y $ are elements of $C$ ,

$S$ is a subset of ${C}^{\prime }$ ,and

Q is a predicate on $C$ ,

where $S$ and $Q$ are coupled by

(8) Q x \equiv ¬ (x \in S), \mathrm {o r} S = {x | ¬ Q x }.

As a result we have

(g) S = \phi \equiv (\underset {\sim} {A} x: x \in C: Q x)

" $x$ is a minimal element of ${S}^{\prime \prime }$ means

x \in S ∧ (\underline {{A}} y: y < x: ¬ (y \in S))

"C is well-founded" means that any non-empty subset of $C$ contains a minimal element.

We observe

\begin{array}{l} C i s w e l l - f o u n d e d \ \begin{array}{r l} & {= {\mathrm {d e f i n i t i o n s o p w e l l - f o u n d e d n e s s a n d m i n i m a l e l e m e n t} }} \ & { (\underline {{A}} S:: (S ≠ \emptyset) \equiv} \end{array} \ (E x: x \in C: x \in S ∧ (A y: y < x: ¬ (y \in S))) \ \begin{array}{r l} & {= {\mathrm {p r e d i c a t e c a l c u l u s , d e M o r g a n i n p a r t i c u l a r} }} \ & { (\underline {{A}} S:: (S = \varnothing) \equiv} \end{array} \ (A x: x \in C: ¬ (x \in S) \vee (E y: y < x: y \in S))) \ \begin{array}{l} {= {\mathrm {r e n a m i n g t h e d u m m y w i t h (8) a n d (9)} }} \ { (\underline {{A}} Q: (\underline {{A}} x: x \in C: Q x) \equiv} \end{array} \ (A x: x \in C: Q x v (E y: y < x: ¬ Q y))) \ = {\mathrm {d e f i n i t i o n o f m a t h e m a t i c a l i n d u c t i o n} } \ " m a t h e m a t h a c a l i n d u c t i o n o v e r C i s v a l i d". \ \end{array}

Among mathematicians, well-foundedness is not as well-known as it deserves to be: there is, for instance, after half a century not yet a Dutch name for it. One cannot escape the impression

that Emmy Noether, besides being Jewish and female, had the additional disadvantage of having been preceded by Georg Cantor with his stress on countability.

References

[0] Back, R.J.R., Correctness preserving program refinements: proof theory and applications. Mathematical Centre Tracts nr 131, Amsterdam 1980. [1] Back, R. J. R., Proving Total Correctness of Nondeterministic Programs in Infinitary Logic. Acta Informatica vol. 15, Fasc. 3, 1981, pp. 233-249. [2] Boom, H.J. A Weaker Precondition for Loops. ACM Transactions on Programming Languages and Systems, vol. 4, 1982, pp. 668-677. [3] Dijkstra, Edsger W., A discipline of program- ming. Prentice-Hall, Inc., Englewood Cliffs,NJ,1976. [4] Floyd, R. W., Assigning meanings to programs. Amer. Math. Soc. Symposia in Applied Mathematics, vol. 19, 1967, pp. 19-31. [5] Park, David, On the semantics of fair parallelism. Lecture Notes in Computer Science, vol. 86, Springer-Verlag, Berlin-Heidelberg 1980, pp. 504 - 526. [6] Park, David, Concurrency and automata on

infinite sequences. Lecture Notes in Computer Science, vol. 104. Springer-Verlag, Berlin-Heidelberg 1981. [7] Slay, J., Denotational Semantics: The Scott-Strachey Approach to Programming. MIT Press, Cambridge, MA, 1977. [8] Tarski, A., A. Lattice-theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, vol. 5 (1955). pp. 285-309.

drs. A.J.M.van Gaasteren BP Venture Research Fellow Dept. of Mathematics and Computing Science University of Technology 5600 MB EINDHOVEN The Netherlands

19 July 1984

prof. dr. Edsger W.Dgkstra Burroughs Research Fellow Plataansstraat 5 5671 AL NUENEN The Netherlands