90
this can’t be true since for any address c = (X
1 …X
n , m),Ids(Dest(c) ˝ Refs(X
1 ), which contra-
dicts the initial assumption. v
Lemma 4.2:<
d is an irreflexive partial order.
Proof:This is a straightforward consequence ofLemma 4.1 and the assumption thatSis a
causal change set. v
Definition 4.7:The destination chain of anDestX(a)addressa = (I
1 …I
n , i), is a sequence
of addressesa
o , …, a
I , awherea
i–1 = Dest(X)
, and a
i = (X…X’, j)
.
The destination chain of an address is the result of repeatedly finding the destination of
the initial in an address’s change path. For a causal change set, this will be a finite sequence
with an initial address of nil.
Definition 4.8:For elementsa, bofA(S)given a minimally consistent change setS,
a <
SA bis defined as (in order of priority):
1. For any addressesa, b = (I
1 …I
n , I), IfDest(I
1 ) = a,thena <
SA b.
2. Fora = (I, i), b = (I, j), a <
SA b iff i < j.
3. Fora = (I
1 , i), b = (I
2 , j)), I
1 „ I
2 , letX, X’ be the initial items of DestC(a), DestC(b),
after the removal of their common prefix. The a <
SA b iff X<
SA X’.
4. Fora = (I
1 …I
n , i), b = (I’
1 …I’
n , j), I
1 „ I’
1 , a <
SA b iff Dest(I
1 ) <
SA Dest(I’
1 ).
5. Fora = (I
1 …I
n , i), b = (I’
1 …I’
n , j), I
1 = I’
1 , a <
SA b iff (I
2 …I
n , i) <
SA (I’
2 …I’
n , j).
Lemma 4.3:The ordering<
SA of Definition4.8 is well founded.
Proof:The recursion in this definition is well founded under the ordering<
wf , defined as
a <
wf biffa <
d borahas a shorter path thanb.Since the the elementnilis minimal under
both orderings, any set of addresses will have a minimal element under <
wf . v
Theorem 4.2:the relation<
SA is a total order.
Proof:We will prove this by induction over the following extension of<
wf to pairs. A pair
(a, b) <
wf (c, d)iff eitheraorbis less than either one ofcand d. The base case is an address
set containing only nil, which is totally ordered. Now, consider each case of the definition
this can’t be true since for any address c = (X
1 …X
n , m),Ids(Dest(c) ˝ Refs(X
1 ), which contra-
dicts the initial assumption. v
Lemma 4.2:<
d is an irreflexive partial order.
Proof:This is a straightforward consequence ofLemma 4.1 and the assumption thatSis a
causal change set. v
Definition 4.7:The destination chain of anDestX(a)addressa = (I
1 …I
n , i), is a sequence
of addressesa
o , …, a
I , awherea
i–1 = Dest(X)
, and a
i = (X…X’, j)
.
The destination chain of an address is the result of repeatedly finding the destination of
the initial in an address’s change path. For a causal change set, this will be a finite sequence
with an initial address of nil.
Definition 4.8:For elementsa, bofA(S)given a minimally consistent change setS,
a <
SA bis defined as (in order of priority):
1. For any addressesa, b = (I
1 …I
n , I), IfDest(I
1 ) = a,thena <
SA b.
2. Fora = (I, i), b = (I, j), a <
SA b iff i < j.
3. Fora = (I
1 , i), b = (I
2 , j)), I
1 „ I
2 , letX, X’ be the initial items of DestC(a), DestC(b),
after the removal of their common prefix. The a <
SA b iff X<
SA X’.
4. Fora = (I
1 …I
n , i), b = (I’
1 …I’
n , j), I
1 „ I’
1 , a <
SA b iff Dest(I
1 ) <
SA Dest(I’
1 ).
5. Fora = (I
1 …I
n , i), b = (I’
1 …I’
n , j), I
1 = I’
1 , a <
SA b iff (I
2 …I
n , i) <
SA (I’
2 …I’
n , j).
Lemma 4.3:The ordering<
SA of Definition4.8 is well founded.
Proof:The recursion in this definition is well founded under the ordering<
wf , defined as
a <
wf biffa <
d borahas a shorter path thanb.Since the the elementnilis minimal under
both orderings, any set of addresses will have a minimal element under <
wf . v
Theorem 4.2:the relation<
SA is a total order.
Proof:We will prove this by induction over the following extension of<
wf to pairs. A pair
(a, b) <
wf (c, d)iff eitheraorbis less than either one ofcand d. The base case is an address
set containing only nil, which is totally ordered. Now, consider each case of the definition
