Switch Decomposability

Single-tag decomposabilty says that for a non null list of tagged events there must exist a decomposition into two suitable lists. We refine this property with a somewhat more constructive condition that we call switch decomposability. It says that for a non null list L of tagged events there must exist a decidable criterion Q on the times (the list indices) that satisfies a number of closure conditions. We will use the criterion Q to partition the list into two parts by defining the message closure of Q

and then partitioniong L into L-CQ, containing those L[i] for which C(Q) i, and L-notCQ, the rest.

We show that this property is a refinement of the single-tag decomposability in the following



proof: We have a switch-decomposable list L that also satisfies the other three properties and, if L is non null we must produce a single-tag decomposition. In this case there is a Q with the properties given in the definition of switch-decomposable. The first of these properties says that Q i is decidable. From this, we can show that C(Q) i is also decidable, and therefore we can filter L on C(Q) and C(Q) to get L$_{1}$ = L-notCQ and L$_{2}$ = L-CQ. We claim that this is a single-tag decomposition of L. We have to show that L$_{2}$ is non null, that L$_{2}$ is a final segment of L, that L$_{2}$ has only one tag, and that L$_{2}$ and L$_{1}$ have no messages in common. From the second property of Q we see that L$_{2}$ is non null. By definition of the message closure, C(Q), every event in L that has the same message as an event in L$_{2}$ must also be in L$_{2}$. Therefore L$_{2}$ and L$_{1}$ can have no messages in common. The fourth property of Q says that all events L[i] for which Q i holds, have the same tag. Everything in L$_{2}$ has the same message as one of these, so from the Tag-by-msg $_{\mbox{\small {E}}}$ property of L, we deduce that everything in L$_{2}$ has the same tag. To see that L$_{2}$ is a final segment of L, suppose that C(Q) i and i j. We must show that C(Q) j. Using the fifth property of Q, it's enough to find an i' with (i' i) (Q i'). But, by definition, (C(Q) i) (k:||L||. ((Q k) ((L[k] =msg= $_{\mbox{\small {E}}}$ L[i])))). We are done if we show that any such k satisfies k i. This follows from the third property of Q, which implies that L[k] is a send event, and the two properties, No-dup-send $_{\mbox{\small {E}}}$ and Causal $_{\mbox{\small {E}}}$, which imply that for every event L[i] there is a unique send event with the same message, and that that send event must occur before i.