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

Abstract

In programming language semantics, the introduction of unbounded nondeterminacy, which amounts to the introduction of noncontinuous predicate transformers, is needed for dealing with such concepts as fair interleaving. With the semantics of the repetition given as the strongest solution of a fixpoint equation, the weakest precondition expressed in closed form would then require transfinite ordinals. Here, however, it is shown that even in the case of unbounded nondeterminacy, the fundamental theorem about the repetition can be proved by a simple and quite elementary argument.

A v G 4 5 / E W D 9 0 1 - 0

A simple fix-point argument without the restriction to continuity

b y

Edsger W. Dykstra & A.J.M. van Gaasteren

Introduction

Notation In this text, the letters B,P,Q,R,X,and Y stand for predicates on the state space of a program and square brackets are used as a 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 $\mathbf{B}\rightarrow \mathbf{S}$ od ; for any statement S and predicate R,wp(S,R) is the predicate such that starting S in any state satisfying it leads to a finite computation that ends in a state satisfying R (see [3]). (End of Notation.)

Requiring DO to be semantically equivalent

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

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

(0) $\left\lbrack {X \equiv \left( {B ∧ {wp}\left( {S,X}\right) }\right) \vee \left( {¬ B ∧ P}\right) }\right\rbrack$

A v G 4 5 / E W D 9 0 1 - 1

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

(i) the semantic definition of skip , viz $[\mathfrak{wp}(\mathfrak{skip},\mathbb{R})\equiv \mathbb{R}]$ for all R; (ii) the semantic definition of statement concatenation, viz.

[ w p (^ {\prime \prime} S 0; S 1 ^ {\prime \prime}, 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;

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

\begin{array}{l} [ w p (” i f B ^ {\prime} \rightarrow S 0) ] \cdot B \rightarrow S 1 F _ {i} ^ {\prime \prime}, R) \equiv \ (B ∧ w p (S o, R)) \lor (¬ B ∧ w p (S 1, R)) ] \ \mathrm {F o r a l l} B, S 0, S 1, \mathrm {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 exponentiation.

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

"predicate transformer $p$ is monotonic" means

"predicate transformer $f$ is or-continuous" means $\left[\underline{f}\left(\underline{E} n:n≥ 0:\mathbb{R}{n}\right)\equiv \left(\underline{E} n:n≥ 0:\underline{f}\mathbb{R}{n}\right)\right]$ for any weakening sequence of predicates, i.e. such that $(\underline{\underline{\pi}} n:n≥ 0:[\mathbb{R}n⇒ \mathbb{R}{n + 1}])$

(End of Notation and terminology.)

For monotonic predicate transformer $f$ , the equa- $[X \equiv fX]$ in $X$ 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) {f}^{n}$ false)

Proof sketch To show that (1) is at least as strong as any solution of $\left\lbrack {X \equiv f{X}^{\prime }}\right\rbrack$ , ${f}^{\prime }$ ’s monotonicity suffices; the proof is most easily carried out by mathematical induction on $n$ . To show that (1) is itself a solution of $\left\lbrack {X \equiv f{X}^{\prime }}\right\rbrack$ ,we need ${f}^{\prime }$ ’s or-continuity (which implies its monotonicity). (End of Proof sketch.)

The predicate $wp(D0,7B∧ P)$ is (see [5]) defined as the strongest solution of (0). Because $wp(S,X)$ is a monotonic function of $X$ , so is the right-hand side of (0); hence its strongest solution exists. If, in addition, $wp(S,X)$ 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 $wp(D0,7B∧ P)$

In programming terms, or continuity of $\mathbf{w}\mathbf{p}$ is the same as nondeterminacy being bounded. The assumption of bounded nondeterminacy is a usual one to make: the closed form for $\mathbf{w}\mathbf{p}(\mathbf{D}\mathbf{o},¬ \mathbf{B}∧ \mathbf{P})$ , which is then available, is traditionally 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 unbounded 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 of a set $D$ . Set-membership will be denoted by the infix operator "in" (with a higher

binding power than the logical operators: our con- vention can thus be summarized by $\underline{x\ln D} \wedge y\overline{\ln D}$ . Function $t$ is a mapping from the state space (of the program) to $D$ , i.e. in each point of the state space, the value of $t$ is an element of $D$ . which can be summarized by $\left\lbrack {t\text{in}D}\right\rbrack$ . Let $C$ be a subset of $D$ ; note that then $t\overline{\text{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 carries the argument is a regularly recurring theme in arguments about algorithms. The best-known (but very special) well-founded set is the set of the natural numbers with $"<$ with its traditional meaning; in the theorem as formulated below, $D$ could be the set of integers with the subset of the natural numbers as $C$ .

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

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

A v G 4 5 / E W D 9 0 1 - 5

satisfy:

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

[t in D]

(2) $\left\lbrack {P ∧ B} ⇒ + \underline{a}C}\right\rbrack ;$ (3) $\left\lbrack {P ∧ B ∧ t = x ⇒ {wp}\left( {S,P ∧ t < x}\right) }\right\rbrack$ for all $x$ ; then (4) $\left\lbrack {P ⇒ {wp}\left( {{DO},{iB} ∧ P}\right) }\right\rbrack$ ,

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

(0) $\left\lbrack {X \equiv \left( {B ∧ {wp}\left( {S,X}\right) }\right) \vee \left( {¬ B ∧ P}\right) }\right\rbrack$

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

The proof

The theorem is proved by showing $[\mathcal{P} ⇒ Q]$ for any $Q$ that solves (0). We do so by showing separately

(i) $\left\lbrack {P ∧ ¬ \operatorname{tin}C ⇒ Q}\right\rbrack$ and (ii) $\left\lbrack {P ∧ \operatorname{fin}C ⇒ Q}\right\rbrack$

A v g 4 5 / E W D 9 0 1 - 6

Proof of (i)

true

$= { \left( 2\right)$ and predicate calculus

[ P \wedge ¬ + \ln^ {\prime} C ⇒ ¬ B \wedge P ]

$⇒ \left{ {\left\lbrack {¬ B ∧ P} ⇒ Q}\right\rbrack \text{since}Q\text{solves}\left( 0\right) }\right}$

[ P \wedge ¬ \underline {{t i n}} C ⇒ Q ]

(End of Proof of (i).)

Proof- $\alpha = f\left( {ii}\right)$

This part of the proof uses the fact that $C$ is well-founded. First we manipulate our demonstrandum so as to make it amenable to a proof by mathematical induction:

[ P \wedge + \underline {{i n}} C ⇒ Q ]

$= {$ predicate calculus,in particular the one-point rule $}$

[ (\underline {{A}} x: t = x: P \wedge x \underline {{\mathrm {i n}}} C ⇒ Q) ]

$= {$ range and term manipulation $}$

[ (¬ x: x \mathrm {i n} C: P ∧ t = x ⇒ Q) ]

$= {$ interchange of universal quantifications

(\underline {{A}} x: x \mathrm {i n} C: [ P \wedge + = x ⇒ Q ])

In view of $C$ ’s well-foundedness, the latter is proved by deriving - for any $x$ in $C$ -

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

from

(6) $\left( {A,y : y \in C ∧ y < x : \left\lbrack {P ∧ t = y ⇒ Q}\right\rbrack }\right) .$

To this end we observe:

(6)

= {\mathrm {i n t e r c h a n g e o f u n i v e r s a l q u a n t i f i c a t i o n s} }

[ (\underline {{A}} y: y \mathrm {i n} C ∧ y < x: P ∧ t = y ⇒ Q) ]

= {\mathrm {r a n g e a n d t e r m m a n i p u l a t i o n} }

[ (¬ A y: t = y: P ∧ y \equiv C ∧ y < x ⇒ Q) ]

= {\mathrm {o n e - p o i n} } \mathrm {r u l e} }

[ P ∧ + \operatorname {i n} C ∧ t < x ⇒ Q ]

= {[ P \wedge ¬ + \ln C \wedge f < x ⇒ Q ] \mathrm {o n a c c o u n t} o f (i) }

[ P ∧ t < x ⇒ Q ]

⇒ {\omega p (S,?) i s m o n o t o n i c }

[ w p (S, P ∧ t < x) ⇒ w p (S, Q) ]

⇒ {(3) }

[ P \wedge B \wedge + = x ⇒ w p (S, Q) ]

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

[ P \wedge t = x ⇒ (B \wedge w p (S, Q)) \vee ¬ B ]

= {\text {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, Q)) \vee (f B \wedge P) ]

= {Q \mathrm {s o l v e s} (0) }

[ P ∧ t = x ⇒ Q ]

= {\mathrm {d e f i n i t i o n} }

(5)

(End of Proof of (ii).)

And this concludes the proof of our theorem.

Conclusion

As far as we are aware, 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 en vogue 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 argument is the first one to connect well-foundedness in its full generality 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 formulation, to the Tuesday Afternoon Club for strengthening the theorem by weakening antecedent (2), and to W.H.J. Feigen and C.S. Scholten, who independently suggested simplifications of the actual proof.

A short appendix on well-foundedness

In the following,

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

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

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

Q is a predicate on $C$ ,

where $S$ and $Q$ are coupled by

(7) $Q \times \equiv ¬ x$ In $S$ ,or $S = { x \mid ¬ Q \times }$

as a result, we have

(8) $S = \phi \equiv \left( {\underline{A}x : x\text{ in }C : Qx}\right)$

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

x \underline {{\mathrm {i n}}} S \wedge (\underline {{A}} y: y < x: ¬ y \underline {{\mathrm {i n}}} 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" \ = {\mathrm {d e f i n i t i o n s o f m i n i m a l e l e m e n t}, \mathrm {w e l l - f o u n d e d n e s s a n d} \emptyset } \ (A S: S ≠ \phi = \ (E x: x \underline {{i n}} C: x \underline {{i n}} S \wedge (A y: y < x: ¬ y \underline {{i n}} S))) \ = {\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 \ (\underline {{A}} x: x \ln C: - x \ln S \vee (\underline {{E}} y: y < x: y \ln S))) \ \end{array}

A v G 45 / EWD901-10

(A Q: (A x: x \mathrm {i n} C: Q x) \equiv

(\underline {{A}} x: x \mathrm {i n} C: Q x \vee (\underline {{E}} y: y < x: ¬ Q y)))

$= {$ renaming the dummy with (7) and (8) $}$ $= {$ definition of mathematical induction $}$ mathematical induction over $C$ is valid

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 programming. 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] Stoy, 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.

Austin, 11 November 1984

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

prof. dr. Edsger W. Dgksta Dept. of Computer Sciences The University of Texas at Austin AUSTIN, TX 78712-1188 United States of America