20.10 Scratch pad

This section develops a possible axiomatic basis for full database states, composite operations, factorisation and merge. It is a working reconstruction rather than part of the historical paper.

Full database states

Let V be the set of causally valid vector times and let v∅ be the empty vector time. A full database state records the effects of all atomic operations in the extent of some v ∈ V. For a full state S, vout(S) denotes that vector time. Its input vector time is always v∅.

Axiom (empty state):
There is an empty database state S∅ satisfying vout(S∅) = v∅.
Axiom (full-state merge):
There is a merge operation ⊕ on full database states satisfying:

S ⊕ S = S

S1 ⊕ S2 = S2 ⊕ S1

(S1 ⊕ S2) ⊕ S3 = S1 ⊕ (S2 ⊕ S3)

S∅ ⊕ S = S

vout(S1 ⊕ S2) = vout(S1) ↑ vout(S2)

The first three laws are idempotence, commutativity and associativity. Idempotence prevents an operation already represented by both inputs from being applied twice. Commutativity and associativity make the result independent of message order and grouping.

Convergence of full states:
If every site eventually receives the same generated changes, all sites converge to the same full database state.
Proof:
At quiescence, each site has a merge expression containing the same generated changes. The expressions may differ in ordering, grouping and repetition. Commutativity removes dependence on ordering, associativity removes dependence on grouping, and idempotence removes repetition. Hence all expressions have the same value.
State at a vector time:
Every causally valid vector time v determines a unique full database state, denoted by State(v).
Proof:
State(v) is the merge of the generated changes identified by χ(v). Any construction of that merge contains exactly those changes. The full-state merge laws make its value independent of ordering, grouping and repetition.

In particular, State(v∅) = S∅ and vout(State(v)) = v.

Composite operations

A composite operation represents the change between two full states. The existence of such an operation for every causally valid vector-time interval is assumed rather than derived.

Axiom (interval operation):
For every v1,v2 ∈ V satisfying v1 ≤ v2, there is a unique composite operation representing all changes in χ[v1,v2) = χ(v2) \ χ(v1). It is denoted by
∑[v1,v2).
It satisfies:

vin(∑[v1,v2)) = v1

vout(∑[v1,v2)) = v2

Ψ(∑[v1,v2)) = χ(v2) \ χ(v1)

State(v1) + ∑[v1,v2) = State(v2)

Full states are interval operations:
State(v) = ∑[v∅,v).
Proof:
Both sides represent all changes in χ(v) and produce State(v) from the empty state. Uniqueness of the interval operation gives the result.
Empty interval:
∑[v,v) is the unique identity operation on State(v).
Proof:
Its extent is χ(v) \ χ(v) = ∅ and applying it maps State(v) to State(v).

Factorisation

Definition:
Let O = ∑[v1,v2) and let v satisfy v1 ≤ v ≤ v2. Define:

Lf(O,v) = ∑[v1,v), called the Lfactor of O with respect to v.

Rf(O,v) = ∑[v,v2), called the Rfactor of O with respect to v.

Contexts of factors:
For every defined factorisation:

vin(Lf(O,v)) = vin(O)

vout(Lf(O,v)) = v

vin(Rf(O,v)) = v

vout(Rf(O,v)) = vout(O)

Proof:
These equations follow from the input and output axioms for interval operations.

Merge of composite operations

Let O1 = ∑[v1,v2) and O2 = ∑[v3,v4). Put v = v2 ↓ v4. The operations have sufficient history when v1 ≤ v and v3 ≤ v. This condition ensures that their combined extents contain the entire interval represented by the result.

Definition:
For composite operations with sufficient history, define:
∑[v1,v2) ⊕ ∑[v3,v4) = ∑[v1↓v3,v2↑v4).
Contexts of merge:

vin(O1 ⊕ O2) = vin(O1) ↓ vin(O2)

vout(O1 ⊕ O2) = vout(O1) ↑ vout(O2)

Proof:
Immediate from the definition of merge and the context axioms for interval operations.
Extent of merge:
Ψ(O1 ⊕ O2) = Ψ(O1) ⋃ Ψ(O2).
Proof:
The sufficient-history condition allows the set identity
(A⋃B) \ (C⋂D) = (A\C) ⋃ (B\D)
to be applied with A = χ(v2), B = χ(v4), C = χ(v1) and D = χ(v3).
Commutativity of merge:
O1 ⊕ O2 = O2 ⊕ O1.
Proof:
Both input contexts are the same meet and both output contexts are the same join. Uniqueness of the corresponding interval operation gives equality.
Idempotence of merge:
O ⊕ O = O.
Proof:
If O = ∑[v1,v2), then O ⊕ O = ∑[v1↓v1,v2↑v2) = O.
Associativity of merge:
Whenever the merges on both sides are defined,
(O1 ⊕ O2) ⊕ O3 = O1 ⊕ (O2 ⊕ O3).
Proof:
The input context on either side is the meet of the three input contexts, and the output context is the join of the three output contexts. Associativity of ↓ and ↑ makes these contexts equal. Uniqueness of the interval operation then gives equality.
Merge of full states:
State(v1) ⊕ State(v2) = State(v1↑v2).
Proof:
Replace each state by its interval operation from v∅. Their merged input context is v∅ and their merged output context is v1↑v2.

Theorems about factorisation

Reconstruction from factors:
Lf(O,v) ⊕ Rf(O,v) = O.
Proof:
If O = ∑[v1,v2), then the left side is
∑[v1,v) ⊕ ∑[v,v2) = ∑[v1↓v,v↑v2) = ∑[v1,v2).
Nested left factors:
If vin(O) ≤ v1 ≤ v2 ≤ vout(O), then
Lf(Lf(O,v2),v1) = Lf(O,v1).
Proof:
Both sides are the interval operation ∑[vin(O),v1).
Nested right factors:
If vin(O) ≤ v1 ≤ v2 ≤ vout(O), then
Rf(Rf(O,v1),v2) = Rf(O,v2).
Proof:
Both sides are the interval operation ∑[v2,vout(O)).
Middle interval:
If vin(O) ≤ v1 ≤ v2 ≤ vout(O), then
Rf(Lf(O,v2),v1) = Lf(Rf(O,v1),v2) = ∑[v1,v2).
Proof:
Each expression has input context v1 and output context v2; the result follows from the definitions of Lf and Rf.
Factors distribute over merge:
Let v be a valid factorisation point for O1, O2 and O1 ⊕ O2. Then:

Lf(O1 ⊕ O2,v) = Lf(O1,v) ⊕ Lf(O2,v)

Rf(O1 ⊕ O2,v) = Rf(O1,v) ⊕ Rf(O2,v)

Proof:
On each line, both sides have the same input and output vector times. Equality follows from uniqueness of the corresponding interval operation.

Convergence using composite operations

Convergence of composite histories:
If every site eventually incorporates the same atomic operations, their composite histories and full database states converge at quiescence.
Proof:
The merge of composite operations is associative, commutative and idempotent. Therefore each site's merged history is independent of reception order, grouping and duplication. Its value is the unique interval operation ∑[v∅,v), where v contains every generated operation. This is State(v), so the full database states also agree.

Obligation on a concrete representation

The interval-operation axiom is deliberately strong. A concrete representation must show that it contains enough information to construct the unique ∑[v1,v2) and implement the merge and factorisation definitions above. In particular, it must retain every causal distinction on which its merge result depends. If discarded causal information can change the result, the representation does not realise this abstract model.