67 SUN triples
A recursively defined merge operation on (s,u,n) triples provides an elegant and efficient way to calculate the effective siteids of a maximal set of q-contiguous insertion intervals.
SUN triple
Definition: In a SUN triple (s,u,n):
- s is a siteid
- u is a temporal index (an integer that respects the precedes relation on the insertion intervals)
- n is an integer denoting the multiplicity of (s,u)
In the cxOT library it is defined as follows:
template<typename S, typename T>
struct TSun
{
S s;
T u;
T n;
};Example
Consider that a maximal q-contiguous list of insertion intervals has the following list of (s,u) values
[(2,6), (4,0), (6,7), (8,4), (2,6), (5,5), (5,3), (3,2)]
The merge algorithm defined below can be used to transform this to the following list of (s,u,n) values with weakly monotonic increasing siteids (weakly means non-strict - i.e. non-decreasing):
[ (2,6,1), (4,0,7) ]
Merge operation
Def: Let L1,L2 be lists of triples (s,u,n) where n denotes the "multiplicity" of (s,u).
Let L1, L2 have monotone increasing siteids.
We define a binary merge operator @ (that preserves the monotone increase
property) as follows:
1) L1 @ [] = L1
2) [] @ L2 = L2
3) (L1 + [(s1,u1,n1)]) @ ([(s2,u2,n2)] + L2) =
L1 + [(s1,u1,n1)] + [(s2,u2,n2)] + L2 if s1 <= s2
(L1 + [(s1,u1,(n1+n2))]) @ L2 if s1 > s2 and u1 < u2
L1 @ ([(s2,u2,(n1+n2))] + L2) if s1 > s2 and u2 < u1
Properties
a) This recursive definition necessarily terminates.
Reason: Termination occurs when either L1=[] or L2=[] or else the siteids
are ordered. Otherwise each recursive step necesarily decrements the value
of |L1|+|L2|. Since the lists are finite the recursion must terminate.
b) The definition unambiguously covers all cases
The cases 1) 2), 3) cover all cases and the only overlap is where L1=L2=[]
in which case 1) and 2) agree that []@[] = []
The cases in 3) are obviously mutually exclusive.
To show that they conver all cases we first need the following lemma:
Lemma: Let i1 = (s1,u1,n1) and i2 = (s2,u2,n2) be two adjacent intervals.
Then i1 || i2 => s1 < s2
Proof: [informal] There is no landmark character separating them. Therefore
since they are concurrent their order should depend on siteid
comparisons
Using the lemma we now show that s1 > s2 => u1 != u2, as follows
s1 > s2 => not (i1 || i2) (by contrapositive of lemma)
=> i1 --> i2 or i2 --> i1 (by defn of i1 || i2)
=> u1 < u2 or u2 < u1 (temporal index preserves causality)
=> u1 != u2
Therefore there is no case of s1 > s2 and u1 = u2, so the cases in 3) cover all
possibilities
c) In the recursion to (L1 + [(s1,u1,(n1+n2))]) @ L2
i) L2 has monotone increasing siteids because it is a sublist of the original
list on the RHS; and
ii) L1 + [(s1,u1,(n1+n2))] has monotone increasing siteids because it has the same
sequence of siteids as the original list on LHS.
So this recursion necessarily preserves the assumption that the two lists have
monotone increasing siteids.
Similarly for the recursion to L1 @ ([(s2,u2,(n1+n2))] + L2).
d) Conceptually when two lists are merged, elements can be "eaten" from where they
touch. This process terminates when the overall list is ordered (which may happen
trivially because one of the lists has been eaten away to []).
Def: Let Elist(L1,L2) be the sublist of L1+L2 that either
ended up eating a neighbour or else was eaten by a neighbour (or both) in the
calculation of L1@L2.
An element is only eaten if it has a higher u value. It follows that the winner
in Elist(L1,L2) is always the s,u with the smallest u.
Monotone increase of siteids
Claim: L1 @ L2 preserves monotone increase of siteids.
Proof: (by induction on n = |L1|+|L2|)
n = 0 L1 @ L2 = []
n = 1 [x] @ [] = [x]
[] @ [x] = [x]
n --> n+1
(L1 + [(s1,u1,n1)]) @ ([(s2,u2,n2)] + L2) =
L1 + [(s1,u1,n1)] + [(s2,u2,n2)] + L2 if s1 <= s2
- this necessarily monotone increases in s
(L1 + [(s1,u1,(n1+n2))]) @ L2 if s1 > s2 and u1 < u2
- this necessarily monotone increases in s, by induction
L1 @ ([(s2,u2,(n1+n2))] + L2) if s1 > s2 and u2 < u1
- this necessarily monotone increases in s, by induction
Associativity
Claim: @ is associative
Proof: We show
(L1 @ L2) @ L3 = L1 @ (L2 @ L3)
(informal)
Eating can occur at the boundary between L1,L2 and at the boundary between L2,L3.
There are four Elists of interest: Elist(L1,L2), Elist(L1@L2,L3), Elist(L2,L3),
Elist(L1,L2@L3).
If exists x in L2 such that x not in Elist(L1,L2) and x not in Elist(L2,L3)
L1 L2 L3
------------ --------x-------- ---------------
<------------> <------------>
Elist(L1,L2) Elist(L2,L3)
(the outcome is independent of the order because no interaction is possible)
else
(we have interaction)
L1 L2 L3
------------ ----------------- ---------------
<-------------------->
<------------------->
Elist(L1,L2) Elist(L2,L3)
<--------------- E ------------------>
Note that Elist(L1,L2) and Elist(L2,L3) don't necessarily overlap, but in that
case they do touch. That still allows for them to interact.
It seems readily apparent that the Elist with the smaller u will end up eating
the other Elist, and possibly more as well. Furthermore the same outcome arises
irrespective of the order.
Let E1 = Elist(L1,L2) union Elist(L1@L2,L3)
E2 = Elist(L1,L2@L3) union Elist(L2,L3)
It is sufficient to show that E1 = E2, a sublist of L1+L2+L3.
For then the winning (s,u) will be the one with minimum u.
Let E = Elist(L1,L2) union Elist(L2,L3).
Claim: E is a sublist of E1 and E is a sublist of E2.
Let u1 = min u in Elist(L1,L2), u2 = min u in Elist(L2,L3).
If u1 < u2 then
in (L1 @ L2) @ L3, Elist(L1,L2) reduces to u1, and u1 then eats all elements
of Elist(L2,L3)
in L1 @ (L2 @ L3), Elist(L1,L2) reduces to u2, and u1 necessarily imposes itself
on the RHS.
???? hardly a formal proof!
(by induction on n = |L1|+|L2|+|L3|)
n = 0:
L1 @ (L2 @ L3) = [] = (L1 @ (L2) @ L3
n-->n+1:
if s1 <= s2
L1 @ ((L2 + [(s2,u2,n2)]) @ ([(s3,u3,n3)] + L3)) =
L1 @ (L2 + [(s2,u2,n2)] + [(s3,u3,n3)] + L3) =
????
TSun.h in cxOT
Source: Ceda/cxOT/TSun.h