A correction of EWD851b

Thanks to the scrutiny of F.E.J. Kruseman Aretz, an error in EWD851b was discovered, which is in urgent need of correction. The Tuesday Afternoon Club, in particular W.H.J.Fegen, designed a more convincing derivation of the correct invariant, and that is what is recorded in this note. (Fegen also convincingly argued that the rules of our formal game should be stated explicitly; I agree, but under the present circumstances the design of such a calculus has to be postponed.)

We search for the transitive closure of

(0) ${\left( \operatorname{wn}u\right) }^{ * }\operatorname{wn}u$

under the following list of transformations - with the numbering of EWD851b but in an order that suits our current purpose-

${wn} \cdot u \rightarrow {wd}s$ (n.1)

$\mathrm{s}$ wn u $\rightarrow$ U bn S (s.o) $\rightarrow \quad u\;{bd}$ (n.2) $\Rightarrow u\;{bd}$ (5.1) $S{w}{n} \rightarrow + {w}{n}$ (s.2)

${W}{n}u \rightarrow {W}{c}u$ (n.o) ${W}{c}u \rightarrow \;{W}{n}u$ (c.0) [{u}{1} \leq {u}{0}] $u\;{B}_{C}u \rightarrow + {wn}u$ (c.i) $\operatorname{wd} \rightarrow \operatorname{Wc}u$ (t.2) $u\;{bn}\;t\; \rightarrow \;t\;{wn}\;u$ (t.1)

$$ u b d + \rightarrow u B C u $$

The transitive closure of (0) under (n.1) is

${\left( Wn u \mid wds\right) }^{ * }W \cap u$

Since (i) the transitive closure of $s$ (wn u) under (s.o) equals ${\left( u\;{bn}\right) }^{ * }s{\left( wnu\right) }^{ * }$ and (ii) (0) can be rewritten as ${\left( wnu\right) }^{1}{wd}s{\left( wnu\right) }^{ * }$ ? Wn u, the transitive closure of ${0}^{\prime }$ ) under (s.o) equals (wn u/wd (u bn)s (wn u))** Wn u which can be simplified to

(1) ${\left( \operatorname{wn}u\right) }^{2} = \left( {u + b}\right) u{\left( }^{ * }s\right) }^{2}$ .

which is also closed under (n.1).

The transitive closure of (1) under (n.2) is

(2) ${\left( wn \cdot u\right) }^{w}d{\left( u \cdot {bn}\right) }^{l}{b}^{s}{\left( s\right) }^{ * }{W}_{n}u$

which we write as

(2) ${H}^{ * }{Wn}u$ with (3) $H = \left| {{wn} + {Qs}}\right|$ with $\left( 4\right) \;Q = {wd}\left( {u{b}{n} \mid u{b}{d}}\right)$

and we note that the substrings $H,H^{}$ ,and $H^{}Q$ are closed under the transitions considered so far. And so is (2), neither H Wn nor u H introducing the possibility of applying any of the transformations. Strings $H,H^{},H^{}Q$ and ring (2) are also closed under (s1). The reason is that the substring s w d can only occur in the substring H Q of the form Q s Q, written out in full $\operatorname {wd}\left(\mathbf{u}\operatorname {bn}\mid \mathbf{u}\operatorname {bd}\right)^{*}$ s wd (u bn | u bd)

Hence the only possible effect of (s.t.) is to replace a string of the form Q s Q by one of the

Inclusion of the next transformation (s.2) is more complicated. In (2) we can make the only way in which the substring s Wn u can occur explicit by adding the superfluous term Q s Wn u :

$$ H ^ {*} (W _ {n} u | Q s W _ {n} u) $$

and we conclude that the transitive closure of (2) under (s.2) is

$$ H ^ {*} (W n u | Q + W n u) $$

which is no longer closed under (n.1); that closure gives

$$ H ^ {*} (W n u | Q + (w n u | w d s)) $$

In view of the structure of $H$ and the fact that our expressions represent circular structures, this equals

$$ H ^ {} (W n u | Q + (w n u | w d s (w n u) ^ {})) $$

which yields under (s.o)

$$ H ^ {} (w n u | Q + (w n u | w d (u b n) ^ {} s (w n u) ^ {*})) $$

which yields under (n.2)

(5) ${H}^{ * }\left( {{W}_{n}u \mid Q + H}\right)$

${H}^{ * }Q$ and $H{H}^{ * }$ being closed under all transformations,(5) is closed under the transformations considered so far.

Closing (5) under the next transformation (n.o) yields

(6) ${H}^{ * }\left( {{W}{n}u \mid {W}{c}u \mid Q + H}\right)$

which is closed under the transformations considered so far, and obviously under the next one (c.o) as well.

In order to accommodate (5.3), we observe that s We can only occur in the substring Q's We u, which can be added as superfluous term in which the substitution can be performed to construct the next

(7) ${H}^{ * }\left( {{W}{n}u\left| {{W}{c}u}\right| Q + H\left| {{QuBc}u}\right) }\right)$

No further extensions are now required. Transformation (c.1) can only transform $Q \cup B \subset u$ , which becomes $Q + wn u$ , a special case of the preceding alternative. $Q + H$ is either of the form $wd + H$ or not. In the former case the next transformation (t.2) may transform it into $W \cup H$ , a case subsumed by the previous alternative (thanks to the circularity). Otherwise $Q + H$ is of the form $Q \cup b n + H$ or of the form $Q \cup bd + H$ . Transformation (t.1) generates from the former $Q + wn u H$ , subsumed by $Q + H$ , transformation (t.0) transforms the latter into $Q \cup Bc u H$ , which is subsumed in the last alternative.

The above derivation is not as calculational as we would like it to be; the development of the calculus is something for later.

One remark about the number of elements in the string. Our regular expressions define a language of strings of arbitrary lengths. For a circular arrangement of a given number of machines, only those strings that are of the appropriate length are applicable. Some machine or ring states and some transformations cannot occur if the ring is too small, but this does not contradict our claim that we are deriving the strongest invariant in the sense that each string of the language may occur.

Plataanstraat 5

5671 AL NUENEN

The Netherlands

13 April 1983

prof. dr. Edsger W. Dgikstra

Burroughs Research Fellow