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 {{\ln 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{OD}}{}^{\prime \prime },\text{true}}\right) }\right\rbrack$ ,(2)

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

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

$\underline{Aa}$ (0). Note that it is a function on state space, whose value may belong to $C$ or not; hence in $C$ stands for a predicate on state space.

${Ad}\left( 1\right)$ . Note that (1) subsumes the traditional

[ P ∧ B ⇒ (\exists x: x \underline {{\operatorname {i n}}} C: x < +) ] , \tag {4}

i.e. $P ∧ B$ implies that it is not a minimal value.

Proof. Equation (3) has a strongest solution since ${wp}\left( {S,?\text{ }}\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 (\underline {{E}} x: x \mathrm {i n} C: + = x) ⇒ X ]

or,equivalently

(\underline {{A}} x: x \ln C: [ P \wedge t = x ⇒ X ]) . (5)

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

\begin{array}{l} (¬ y: y \mathrm {i n} C ∧ y < x: [ P ∧ t = y ⇒ X ]) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underset {\sim} {A} y: y \underline {{\mathrm {i n}}} C \wedge y < x: [ P \wedge + = y \wedge y \underline {{\mathrm {i n}}} C \wedge y < x ⇒ X ]) \ = {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\underline {{A}} y: y \underline {{\ln C}} \wedge y < x: [ P \wedge + = y \wedge + \underline {{\ln C}} \wedge + < x ⇒ X ]) \ = {\mathrm {p r e d i c a t e c a l c u l u s}, P \mathrm {a n d} X \mathrm {n o t} \mathrm {c o n t a i n i n g} y } \ (\underline {{A}} y: y \ln C \wedge y < x: [ P \wedge + \underline {{i n}} C \wedge + < x ⇒ X ]) \ = {() } \ (\underline {{A}} y: y \mathrm {i n} C ∧ y < x: [ P ∧ + < x ⇒ X ]) \ \end{array}

Hence, the hypothesis implies $\left\lbrack {P ∧ t < x ⇒ X}\right\rbrack$ for all $x$ such that the range for $y$ is nonempty. i.e. all $x$ that is non-minimal. For minimal $x$ , $\left\lbrack {P ∧ t < x ⇒ X}\right\rbrack$ follows on account of (0) and the definition of minimality.

Next we observe for an $x$ in $C$ and any $Z$

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

⇒ {(1) }

[ Z ⇒ w p (” y := + ”, w p (S, P ∧ + < y)) ∧ + = x ]

= {\mathrm {A x i o m o f A s s i g n e m e n t}; \mathrm {c o n j u n c t i v i t y o f w p} }

[ 2 ⇒ w p (y = t), w p (S, P ∧ y) ∧ y = x) ]

= {[ w p (S, Q) \wedge y = x \equiv w p (S, Q \wedge y = x) ]

since the thought variables $x$ and $y$ don't occur in S3

[ 2 ⇒ w p (” y := t ”, w p (S, P ∧ t < y ∧ y = x)) ]

⇒ {\mathrm {m o n o t o n i c i t y o f} w p }

[ 2 ⇒ w p (y = t ^ {n}, 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 }

[ 2 ⇒ w p (S, P ∧ + < x) ]

⇒ {\mathrm {h y p o t h e s i s}, (0) \mathrm {a n d m o n o t o n i c i t y} }

[ z ⇒ w p (S, X) ]

Eliminating Z, we conclude under the hypothesis

\begin{array}{l} [ B \wedge P \wedge f = 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 f = x ⇒ w p (S, X) \vee ¬ B ] \ = {X i s a s o l u t i o n o f (3) } \ [ P ∧ t = x ⇒ X ] \ \end{array}

(End of Proof.)

Remark. We gave a number to (4), expecting to need to refer to it. The need did not arise. (End of Remark)

*

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

27 February 1984

prof. dr. Edsger W. Dijkstra Burroughs Research Fellow Plataanstraat 5 5671 AL NUENEN The Netherlands