NOTE: This transcription was contributed by Martin P.M. van der Burgt, who has devised a process for producing transcripts automatically. Although its markup is incomplete, we believe it serves a useful purpose by virtue of its searchability and its accessibility to text-reading software. It will be replaced by a fully marked-up version when time permits. —HR
Copyright Notice | ||
The following manuscript | ||
EWD 675 The equivalence of bounded nondeterminacy and continuity | ||
is held in copyright by Springer-Verlag New York. | ||
The manuscript was published as pages 358–359 of | ||
Edsger W. Dijkstra, Selected Writings on Computing: A Personal Perspective, | ||
Springer-Verlag, 1982. ISBN 0–387–90652–5. | ||
Reproduced with permission from Springer-Verlag New York. | ||
Any further reproduction is strictly prohibited. | ||
The equivalence of bounded nondeterminacy and continuity.
Unbounded nondeterminacy is presented by the function “any natural number” such that
wp("x:= any natural number", 0 ≤ x) = T | |
wp("x:= any natural number", x ≤ k) = F for all k . |
for r ≥ 0 C_{r} ≠ C_{r+1} for all states |
wp(S, (E r: r ≥ 0: c_{r})) = (E s: s ≥ 0: wp(S, c_{s})) | (1) |
It is further shown that the program “x:= any natural number” is not continuous —and, hence, cannot be written in that programming language fragment— . For the sake of completeness, we repeat the proof. Assume the program S: “x2: any natural number” to be continuous. We then have:
T = wp(S, 0 ≤ x) | ||
= wp(S, (E r: r ≥ 0: 0 ≤x ≤ r)) | ||
= (E s: s ≥ 0: wp(S, 0 ≤ x ≤ s)) | ||
= (E s: s ≥ 0: F) = F |
In the sequel of this note we shall show that the inverse holds as well, viz. that the existence of a noncontinuous program implies the inclusion of unbounded nondeterminacy. (The following argument was suggested to me by C.S.Scholten almost instantaneously when I had posed the problem.) Assume the existence of a program S and an infinite sequence of predicates C such that C_{r} ⇒ C_{r+1}, such that (1) does not hold. Because in (1) the right-hand side implies the left-hand side trivially, this means that we assume
wp(S, (E r: r ≥ 0: c_{r}))and non (E s: s ≥ 0: wp(S, c_{s})) = | ||
wp(S, (E r: r ≥ 0: c_{r}))and (A s: s ≥ 0: non wp(S, c_{s})) | (2) |
Consider now the program
S; x:= (MIN: k: C_{k}) |
Here we have established the equivalence of continuity and the
boundedness of nondeterminacy. In EWD673 we have established the equivalence between
the boundedness of nondeterminacy and the equality between weak and strong
termination. Hence the three criteria
1) continuity or not
2) nondeterminacy bounded or not
3) weak and strong termination equivalent or not
are three different aspects of the same dichotomy. All this is very
satisfying. (The arguments are so simple that, presumable, this is already
known. But it was new for me, and I like the arguments.)
Plataanstraat 5 | prof.dr.Edsger W.Dijkstra |
5671 AL NUENEN | BURROUGHS Research Fellow |
The Netherlands |
Transcribed by Martin P.M. van der Burgt
Last revision