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

A simple fixpoint argument without the restriction to continuity

by

Edsger W. Dijkstra & 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.

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 a pair of square brackets is used as a notation for universal quantification of the enclosed over the program variables.

The letter S stands for a statement and DO. stands for the repetitive construct do $B\rightarrow S$ od

For any statement S and predicate R , the operational interpretation of the predicate $w p(S,R)$ is that any valid implementation of S, when started in any state satisfying $w p(S,R)$ , should lead to a finite computation that ends in a state satisfying R (see [3]). (End of Notation.)

Requiring D0 to be semantically equivalent to its first unfolding

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

yields that ${wp}\left( {{DO},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$

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

(i) the semantic definition of skip , viz.

[ w p (s k i p, R) = R ] f o r a l l R;

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

[ w p (S 0; S 1 ^ {\prime \prime}, R) \equiv w p (S 0, w p (S 1, R)) ]

f o r a l l S O, S I, a n d R;

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

[ w p (" i f B \rightarrow S 0 ] \rightarrow B \rightarrow S _ {1} F _ {i} ^ {\prime \prime}, R) \equiv

(B \wedge w p (S _ {0}, R)) \vee (¬ B \wedge w p (S _ {1}, R)) ]

\mathrm {f o r a l l} B, S _ {0}, S _ {1}, \mathrm {a n d} R.

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$ " means "[ $X ⇒ Y$ ]".

"predicate transformer $f$ is monotonic " means

"predicate transformer $f$ is or-continuous" means $\left[f\left(\underline{\mathrm{En}}: n \in \mathbb{N}: R_{n}\right) \equiv \left(\underline{\mathrm{En}}: n \in \mathbb{N}: f R_{n}\right)\right] \text{for any}$ weakening sequence of predicates, i.e. such that $(A_{n}: n \in \mathbb{N}: [R_{n} ⇒ R_{n+1}])'$ .

(End of Notation and terminology.)

For monotonic predicate transformer $f$ ,the equation $\left\lbrack {X \equiv {f}^{x}}\right\rbrack$ 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( {{\varepsilon }_{n} : n \in \mathbb{N} : {f}^{n}\text{false}}\right)$

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) itself is 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,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 the strongest solution of (0) 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,P)$ . In passing we note that $wp(D0,¬ B∧ P)$ is defined as the strongest solution of the same equation (0), i.e.

[ w p (D O, ¬ B ∧ P) \equiv w p (D O, P) ]

In programming terms, or-continuity of wp is the same as nondeterminacy being bounded. The assumption of bounded nondeterminacy is a usual one to make: the closed form for wp (D0,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 formalisms.

The theorem

Notation In what follows, $x$ and $y$ stand for elements of a set $D$ . The infix operator "e" for set-membership has a higher binding power than the logical operators. 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 [teD]. Let $C$ be a subset of $D$ ; note that then teC 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 natural numbers with " $k$ " having its traditional meaning; in the theorem as formulated below, $D$ could be the set of integers with the subset of natural numbers as $C$ .

After the above preliminaries we are ready to formulate the 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 $t$ on the state space satisfying: the predicate transformer $wp(S, ?)$ is monotonic; $[t \in D]$ ;

(2) $\left\lbrack {P ∧ B} ⇒ t \in C}\right\rbrack$ ; (3) $\left\lbrack {P ∧ B ∧ t = x ⇒ w + \left( {S,P ∧ t < x}\right) }\right\rbrack$ for all $x$ ; then (4) $\left\lbrack {P ⇒ {wp}\left( {{DO},¬ B ∧ P}\right) }\right\rbrack$ , where ${wp}\left( {{DO},¬ B ∧ 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

Avg 45a/EWD 901a - 6

"variant function", which carries the termination argument.

The proof

Our proof obligation (4) amounts to showing $\left\lbrack {P ⇒ Q}\right\rbrack$ for any $Q$ that solves (0). We do so by showing separately

(i) $\left\lbrack {P ∧ ¬ \operatorname{t} \in C ⇒ Q}\right\rbrack$ and

(ii) $\left\lbrack {P ∧ t \in C} ⇒ Q\right\rbrack$

Proof.

true

\begin{array}{l} = {(2) \mathrm {a n d p r e d i c a t e c a l c u l u s} } \ [ P ∧ ¬ + \in C ⇒ ¬ B ∧ P ] \ ⇒ \left{\lbrack ¬ B ∧ P ⇒ Q \right] \mathrm {s i n c e} Q \mathrm {s o l v e s} (0) } \ [ P ∧ ¬ t \in C ⇒ Q ] \ \end{array}

(End of Proof of (i).)

Proof of (ii)

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:

\begin{array}{l} [ P _ {\wedge} + \in C ⇒ Q ] \ = {\mathrm {p r e d i c a t e c a l c u l u s , i n p a r t i c u l a r t h e o n e - p o i n t r u l e} } [ (¬ x: t = x: P ∧ x \in C ⇒ 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 x: x \in C: P ∧ t = x ⇒ Q) ] \ = {\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} } (\underset {\sim} {A x}: x \in C: [ P ∧ t = x ⇒ Q ]) \ \end{array}

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

[ P ∧ t = x ⇒ Q ] p r o m

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

To this end we observe:

(5)

\begin{array}{l} = {\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} } \ [ (\exists y: y \in 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 \in C ∧ y < x ⇒ Q) ] \ = {\mathrm {o n e - p o i n t r u l e} } \ [ P ∧^ {\prime} t \in C ∧ t < x ⇒ Q ] \ = {[ P ∧ ¬ t \in C ∧ t < x ⇒ Q ] \mathrm {o n} a c c o u n t o f (i) } \ [ P ∧ t < x ⇒ Q ] \ ⇒ {w 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 f = x ⇒ w p (S, Q) ] \ = {\text {p r e d i c a t e c a l c u l u s} } \ [ P \wedge + = x ⇒ (B \wedge w p (S, Q)) \vee ¬ B ] \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ [ P \wedge + = x ⇒ (B \wedge w p (S, Q)) \vee (¬ B \wedge P) ] \ = {Q \text {s o l v e s} (0) } \ [ P ∧ t = x ⇒ Q ] \ \end{array}

(End of Proof of (ii).)

And this concludes our proof of the 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 fixpoint 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 fixpoint 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 Eindhoven Tuesday Afternoon Club for strengthening the theorem by replacing a former antecedent by the weaker (2), and to W.H.J.Fegen and C.S.Scholten, who independently suggested simplifications of the actual proof. Finally, we are indebted to one of the anonymous referees, whose constructive criticism led to yet a few further improvements in the presentation. (The other anonymous referee, we were sorry to observe, had done a rather poor job.)

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 , \operatorname{or} S = { x \mid ¬ Q \times }$

as a result, we have

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

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

x \in S ∧ (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" \ = {\mathrm {d e p i n i t i o n s o f m i n i m a l e l e m e n t , 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 \in C: x \in S ∧ (A y: y < x: - y \in 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} } \ \mathrm {(A S} \because S = \phi \equiv \ (\underline {{A}} x: x \in C: ¬ x \in S \vee (\underline {{E}} y: y < x: y \in S))) \ \end{array}

\begin{array}{l} = {\mathrm {r e n a m i n g t h e d u m m y w i t h (7) a n d (8)} } \ (\underset {\sim} {A} Q: (\underset {\sim} {A} x: x \in C: \underset {\sim} {Q} x) \equiv \ (A x: x \in C: Q x \vee (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 i 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 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, Concurrence 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, 13 October 1985

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. Dghsra Dept. of Computer Sciences The University of Texas at Austin AUSTIN, TX 78712-1188 United States of America