The termination theorem for unconstrained nondeterminacy (with A.J.M. van Gasteren)

The termination theorem for unconstrained nondeterminacy

Without appeal to continuity we shall prove the following theorem.

Theorem Let $\left( {C, < }\right)$ be a well-founded set. Let state- ment $S$ ,predicates $B$ and $P$ and function $f$ on state space satisfy

[ P ⇒ + \underline {{\operatorname {i n}}} C ] \tag {0}

and with fresh "thought variable" $y =$

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

Then $\left\lbrack {P ⇒ {wp}\left( {{}^{\prime \prime }{do}B \rightarrow S\underline{{ad}}{}^{\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 ] . \tag {3}

$\underline{Aa}$ (0). Note that $t$ is a function on state space, whose value may belong to $C$ or not; hence $t$ in $C$ is a predicate on state space. (End of $A$ d(0).)

Proof. Equation (3) has a strongest solution since $w p(S,?)$ is conjunctive and, hence, monotonic. Let $X$ be the strongest solution of (3).

Since (0) is the same as

[ 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 \underline {{i n}} C: + = x) ⇒ X ]

or, equivalently,

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

In view of C's well-foundedness, we shall prove (4) by mathematical induction, i.e. for any $x$ in $C$ we shall derive $[P \wedge t = x ⇒ X]$ under the hypothesis

(¬ y: y \mathrm {i n} C ∧ y < x: [ P ∧ t = y ⇒ X ]) . (5)

To begin with we observe

(5)

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

Next we observe for that $x$ and any $Z$

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

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

$⇒ {$ monotonicity of ${wp}}$

$= {$ though variable $y$ does not occur in ${wp}\left( {{S}{2}{P}{1} + < x}\right) }$

$⇒ { (6)$ and monotonicity of ${wp}}$

Eliminating 2 , we conclude

\begin{array}{l} [ Z ⇒ w p (” y := t ^ {\prime}, w p (S, P ∧ t < x)) ] \ [ Z ⇒ w p (S, P \wedge + < x) ] \ [ Z ⇒ w _ {P} (S, X) ] \ t r u e \ = {\mathrm {s e e a b o v e} } \ [ B \wedge P \wedge 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 f = x ⇒ w p (S, X) \vee \overline {{B}} ] \ = {X i s a s o l u t i o n o f (3) } \ [ P ∧ + = x ⇒ X ] \ \end{array}

(End of Proof.)

The theorem is well-known for or-continuous ${wp}\left( {S,?\right)$ and natural $t $ . The continuity permits us to write the strongest solution of (3) as the limit of a weakening chain. EWD used this expression a decade ago to prove the restricted theorem, but that proof was no 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 inter- leaving of the atomic actions of concurrent pro- grams).

This is a very nice thought.

drs. AJ.M.van Gasteren

BP Venture Research Fellow

Depth of Mathematics and

Computing Science

University of Technology

5600 MB EINDHOVEN

The Netherlands

29 February 1984

prof. dr. Edsger W. Dgkstra

Burroughs Research Fellow

Plataanstraat 5

5671 AL NUENEN

The Netherlands