Why the importance of continuity seems to be overrated (with A.J.M. van Gasteren)

Why the importance of continuity seems to be overrated

Without an appeal to continuity and without using fixed-point induction, we shall prove the following theorem.

Theorem Let $(C, < )$ be a well-founded set. Let predicates $B$ and $P$ , statement $S$ , and function $t$ be such that

[ P ⇒ + \underline {{i n}} C ] (0)

and with fresh "thought variable" $y$

[ B \wedge P ⇒ w p (” y := t ”, w p (S, P \wedge t < y)) ] . (1)

Then $\left\lbrack {P ⇒ {wp}\left( {{}^{\prime \prime }\underline{d}0B \rightarrow S\underline{0}d\text{,true}}\right) }\right\rbrack$ , (2)

in which the right-hand side is defined as the strongest solution of

X: [ (B \wedge w p (S, X)) \vee ¬ B \equiv X ] . (3)

Proof. Equation (3) has a strongest solution since $\omega p\left( {S,?\right)$ is conjunctive and,hence,monotonic. Let $X$ be the strongest solution of (3). Since we can conclude from (0)

[ P ⇒ (\underline {{E}} x: x \ln C: + ≤ x) ]

(2) -i.e. $\left\lbrack {P ⇒ X}\right\rbrack -$ is proved by demonstrating

[ P \wedge (E x: x \mathrm {i n} C: + ≤ x) ⇒ X ]

or,equivalently,

(\underline {{A}} x: x \underline {{\mathrm {i n}}} C: [ P \wedge t ≤ x ⇒ X ]) . (4)

In view of $C$ ’s well-foundedness, (4) will be shown by mathematical induction, i.e. for an $x$ in $C$ , we shall derive $\left\lbrack {P ∧ t ≤ x ⇒ X}\right\rbrack$ under the hypothesis $\left\lbrack {P ∧ t < x ⇒ X}\right\rbrack$ .

We observe for any $z$

[ Z \equiv B \wedge P \wedge t ≤ x ]

$⇒ { \left( 1\right) }$

\begin{array}{l} [ Z ⇒ w p (” y := t ^ {\prime}, w p (S, P ∧ t < y)) ∧ t ≤ x ] \ = {A x i o m o f \tilde {A s s i g n m e n t}; c o n j u n c t i v i t y o f w p } [ Z ⇒ w p (” y := t ^ {\prime}, w p (S, P \wedge + < y) \wedge y < x) ] \ = {[ w p (S, Q) \wedge y ≤ x \equiv w p (S, Q \wedge y ≤ x) ] \mathrm {f o r a n y} Q \mathrm {s i n c e} y \mathrm {a n d} x \mathrm {a r e t h o u g h t v a r i a l} \ [ Z ⇒ w p (” y := t, w p (S, P ∧ < y ∧ y \le x)) ] \ ⇒ {\mathrm {m o n o t o n i c i t y} \circ p, \mathrm {t r a n s i f i v i t y} \circ p < } [ Z ⇒ w p (” y := t ”, w p (S, P ∧ t < x)) ] \ = {y i s a t h o u g h t v a r i a b l e } \ ⇒ {H y p o t h e s i s a n d m o n o t o n i c i l y o f w p } [ Z ⇒ w p (S, X) ] \ \end{array}

Eliminating $Z$ ,we conclude under the hypothesis

[ B \wedge P \wedge + ≤ X ⇒ B \wedge w _ {P} (S, X) ] ;

furthermore we have

[ ¬ B ∧ P ∧ t ≤ x ⇒ ¬ B ]

Hence

[ P ∧ \vdash x ⇒ (B ∧ w p (S, X)) \lor ¬ B ]

and, since $X$ is a solution of (3),

[ P ∧ t ≤ x ⇒ X ]

(End of Proof.)

The theorem is well-known for or-continuous $wp(S, ?)$ and natural $t$ . The continuity permits us to write the strongest solution of (3) in closed form, viz. as the limit of a weakening chain. I (EWD) used this expression a decade ago to prove the restricted theorem, but that proof was by no means simpler than our current one.

The above proof casts serious doubts on the supposed need of fancy things such as transfinite induction for reasoning about programs with unbounded nondeterminacy (as we might, for instance, encounter in an abstract program containing the unrefined statement "establish P" or with fair interleaving of the atomic actions of concurrent programs). This is a very nice thought.

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

22 February 1984

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