1122

Interleaving is associative

EWD1122 · 1991–1995 · PDF · Source language: English. · Local OCR-derived source needs manual review.

Interleaving is associative

for string $x$ and alphabets $A,B$ ,the projection operator $P$ has the properties

(0) $\left( {x \nmid A}\right) \cdot B = x \nmid \left( {A \cap B}\right)$ (1) $x \nmid \phi = \left\lbrack \;\right\rbrack$

where [] stands for the empty string.

In what follows, alphabets $B,C,D$ and strings

(2) ${B}{n}C = \phi ,{B}{n}D = \phi ,{C}_{n}D = \phi$ (3) ${b}^{ \frown }B = b,{c}^{ \frown }C = C,$ $d$ 元 $D = d$

Remark I wrote (3) rather than

$$ b \in B ^ {}, c \in C ^ {}, d \in D ^ {*} $$

because strings of infinite length are admitted. (End of Remark)

Exercise Prove, for instance, $b{PC} = \left\lbrack \right\rbrack$ . (End of Exercise.)

For a pair of strings from disjoint alphabets we define a nondeterministic operation of in-terleaving: "y is an interleaving of b and c" means that y satisfies

${y}^{ \nmid B} = b \land {y}^{ \nmid C} = c \land {y}^{ \nmid \left( {{B \cup C}}\right) } = y$

Since (BuC)nD = φ - this follows from (2) -, the last term of (4) tells us that we can now

introduce $z$ as an interleading of $y$ and $d$ ,

i.e. $z$ satisfies

(5) ${z}^{p}\left( {B{u}^{C}}\right) = y \land {z}^{p}D = d \land {z}^{p}\left( {B{u}^{C}D}\right) = z$ .

In order to show that interleaving is associative we demonstrate

(i) that $z$ as constrained by (4) and (5)

satisfies

(6) ${z}^{p}B = b \land {z}^{p}C = c \land {z}^{p}D = d \land {z}^{p}\left( {{BuC} \cup D}\right) = z$

which is symmetric in the pairs $(b,B),(c,c),$ and $(d,D)$

(ii) that for $z$ as constrained by (6), a $y$ exists such that (4) and (5) are satisfied.

Demonstration (i)

We deal with the conjuncts of (6) in turn. For the first one we observe

b

$$ \begin{array}{l} = {(4), l e a d i n g c o n j u n c t } \ y ^ {P} B \ = {(5), l e a d i n g c o n j u n c t } \ (z \mid (B o C)) \mid B \ = {0) a n d s e t t h e o r y } \ z \mapsto (B n B \cup C n B) \ = {(2) a n d s e t t h e o r y } \ 2 ^ {\prime} B \ \end{array} $$

The next conjunct of (6) follows similarly, and the remaining two follow directly from (5). (End

of Demonstration (i).)

Demonstration (ii)

The last 2 conjuncts of (5) follow directly from (6); in order to satisfy the leading conjunct we choose for $y$

$\left( 7\right) y = {2p}\left( {{B}_{U}C}\right)$

(Actually, we had little choice!). Our remaining obligation is to show that with this choice of $y$ , (4) is satisfied. We deal with its conjuncts in turn; for the leading one we observe

$$ \begin{array}{l} y ^ {p} B \ = {x \dots x; (7) \mathrm {i s} (5) \mathrm {s l e a d i n g c o n j u n c t} } \ z ^ {p} B \ = {(6), \mathrm {l e a d i n g c o n j u n c t} } \ \end{array} $$

The next conjunct of (4) follows similarly, and for the last conjunct we observe

$$ \begin{array}{l} y \mapsto (B u C) \ = {(7) } \ (2) (B u C)) P (B u C) \ = {(0) a n d s e t t h e o r y } \ z P (B _ {U} C) \ = {(7) } \ y \ \end{array} $$

(End of Demonstration (ii).)

The above demonstrations are totally trivial, and that is precisely the point. In my first effort I started with a recursive definition of being an interleaving, something like

$$ \begin{array}{l} i n t e r l e a v i n g. [ ]. y. 2 \equiv y = z \ i n t e r l e a v i n g. x. [ ]. 2 \equiv x = 2 \ i n t e r l e a v i n g. (p: x). (q: y). (r: z) \equiv \ (p = r \land i n t e r l e a v i n g. x. (q: y). z) \vee \ (q = r \land \mathrm {i n t e r l e a v i n g .} (p: x), y: z) \ \end{array} $$

which then invites an argument by mathematical induction. A grandiose mistake, for the whole problem has nothing to do with strings, and everything with projection, of which only (0) is used. (Property (1) is only needed for the exercis It refers to the empty string; property (0) leaves the type of $\mathcal{P} \times$ pretty open.)

Austin, 19 January 1992

prof. dr. Edsger W. Dgksha

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712- 1188

USA