Some properties of darcs patch theory

Ganesh Sittampalam et al.

October 17, 2005

Abstract

This is an attempt to derive some properties of darcs patch theory. We start by specifying the “axioms” that must be true of patches and commutation, and prove some theorems.

1 Notation

A, B etc are individual patches, that can’t be expressed as a sequence of two smaller patches. They could be either primitive patches or mergers or conflictors or whatever. They could be inverted.

Sequential patch composition is written with juxtaposition. Not all patches can be sequentially composed, but use of the notation AB implicitly assumes that they can. ^{1}

Commutation is written AB ↔ B′A′. If ∄B′A′ s.t. AB ↔ B′A′, then we write AB ↔ fail.

We write As to represent a (possibly empty) sequence of patches of arbitrary length The empty sequence is written as id.

We define ↔^{↑} between sequences of patches is defined as follows.

AB ↔ B′A′ ⟹ AB ↔^{↑} B′A′
As ↔^{↑} Bs ⟹ AsC ↔^{↑} BsC
As ↔^{↑} Bs ⟹ AAs ↔^{↑} CBs

This is a complete definition; As ↔^{↑} Bs implies that at least one of the above clauses applies.

We define ↔^{∗} between sequences of patches is defined as follows.

As ↔^{∗} As
As ↔^{↑} Bs ⟹ As ↔^{∗} Bs
As ↔^{∗} Bs ∧ Bs ↔^{∗} Zs ⟹ As ↔^{∗} Zs

This is also a complete definition.

The relation ∼ between individual patches is defined as follows.

1It is likely that a mechanised proof about patch theory would have to make this precondition explicit.

A ∼ A
AB ↔ B′A′ ⟹ A ∼ A′
AB ↔ B′A′ ⟹ B ∼ B′
A ∼ A′ ∧ A′ ∼ A′′ ⟹ A ∼ A′′

This is also a complete definition. We adopt a notational convention that if we mention A and A′ together,

then A ∼ A′ (etc).^{2}

2 Axioms

These are properties that we assume about individual patches and commutation. They are not quite axioms, since it would be possible to prove them about any particular implementation of patches and commutation, but for our current purposes they are.

Associativity of patch sequencing:

(AB)C = A(BC )

Since this property is required, we can omit parentheses (and it does make sense to talk about lists).

Uniqueness of commutation:

AB ↔ B′A ∧ AB ↔ B′′A′′ ⟹ A′ = A′′ ∧ B′ = B′′

Invertibility of commutation:

AB ↔ B′A′ ⟹ B′A′ ↔ AB

3-way permutivitiy of commutation: If

ABC ↔^{↑} B′A′C ↔^{↑} B′C′A′′ ↔^{↑} C′′B′′A′′ ↔^{↑} C′′A′′′B′′ ↔^{↑} A′′′′C′′′B′′ ↔^{↑} A′′′′B′′′C′′′′

Then

A = A′′′′
B = B′′′
C = C′′′′

Consistency of failure: If A ∼ A′, B ∼ B′, then AB ↔ fail ⇔ A′B′ ↔ fail.

2This is another thing that would need to be made explicit in a mechanised proof

3 Theorems

We start by explicitly writing down some “obvious” properties and constructing some useful machinery.

Theorem 1. If As ↔^{↑} Bs, then |As| = |Bs|.

If As ↔^{∗} Bs, then |As| = |Bs|.

Proof. By induction on the structure of ↔^{↑} and ↔^{∗}.

3.1 Associated permutations

We now define the concept of an associated permutation for ↔^{↑} and ↔^{∗}. If AB ↔ B′A′, then AB ↔^{↑} B′A′ has associated permutation (1 2). If As ↔^{↑} Bs has associated permutation (n n + 1), then AsA ↔^{↑} BsA has

associated permutation (n n + 1).

If As ↔^{↑} Bs has associated permutation (n n + 1), then AsA ↔^{↑} BsA has associated permutation (n + 1 n + 2).

Note that by induction, the associated permutation for ↔^{↑} is always a single transposition, so this definition makes sense.

As ↔^{∗} As has associatated permutation id.

If As ↔^{↑} Bs has associated permutation p, then so does As ↔^{∗} Bs.

If As ↔^{∗} Bs has associated permutation p and Bs ↔^{∗} Zs has associated permutation q, then As ↔^{∗} Zs has associated permutation q ⊙ p.

Note that the alphabet for the associated permutation of As ↔^{↑} Bs or As ↔^{∗} Bs is 1 … |As|.

Also, every such commutation has at least one associated permutation. ^{3}

Theorem 2. If A_{1} … A_{n} ↔^{∗} B_{p(1)} … B_{p(n)} has associated permutation p, then ∀i.1 ≤ i ≤ n.A_{i} ∼ B_{i}.

Proof. By induction on the structure of ↔^{↑} and ↔^{∗}.

We now define the concept of a canonical commutation path for a permutation p and a set of patches A_{1} … A_{n} (where the alphabet of p is 1 … n).

Such a path starts from A_{p^{−1}(1)} … A_{p^{−1}(n)} and finishes at A_{1} … A_{n}.

Informally, one is constructed by first commuting A_{1} to the left of the sequence, then commuting A_{2} to the one-but-leftmost position, and so on. It is not guaranteed that all of these commutes will succeed, so there might not be a canonical commutation path for any given p and As.

Note that any suffix of a canonical commutation path is also a canonical commutation path (for a different permutation, but the same ending sequence).

We can also define the canonical representation of a permutation as a sequence of transpositions that follow the commutes of a canonical commutation path. This will be independent of any particular As.

3I’m not sure if this is exactly one or not. Pinning down under what circumstances this is the case or not might help to resolve the current patch ids debate. Also, if it was exactly one, then I think it would be the case that if p was the associated permutation for A_{1} … A_{n} ↔^{∗} B_{1} … B_{n} and A_{i} ∼ B_{j} , then j = p(i), which would make some of the following proofs simpler.

Theorem 3. If Bs ↔^{∗} As is a canonical commutation path for p, then p is an associated permutation of Bs ↔^{∗} As.

Proof. Obvious.

Theorem 4. If Bs ↔^{∗} As is a canonical commutation path for p, and Cs ↔^{∗} As is also a canonical commutation path for p, then Bs = Cs.

Proof. Since the commutation paths must have the same structure, this follows from the “Uniqueness of commutation” and “Invertibility of commutation” axioms.

Theorem 5. Suppose that p is an associated permutation for A′_{p^{−1}(1)} … A′_{p^{−1}(n)} ↔^{∗} A_{1} … A_{n}. Then there is a canonical commutation path for p that starts with A′_{p^{−1}(1)} … A′_{p^{−1}(n)}.

Proof. Start trying to construct a path, and suppose that we reach a failing commute. Define A_{p^{−1}(1)} … A_{p^{−1}(n)} ↔^{∗} A′′_{p′(1)} … A′′_{p′(n)} with associated permutation p′ ⊙ p to be the chain of successful commutes leading up to the first failing one, and that A′′_{i}A′′_{j} ↔ fail.

Then it must be the case that i > j , because the definition of the canonical commutation path means that we would not be trying this commute otherwise. Also, p(i) < p(j ), otherwise we would not need to do this commutation as the patches would already be the right way round.

So, there must be some commutation along the path A′_{p^{−1}(1)} … A′_{p^{−1}(n)} ↔^{∗} A_{1} … A_{n} where i and j swap position, i.e. where A′′′_{i}A′′′_{j} ↔^{∗} A′′′′_{j}A′′′′_{i}. But this violates our “Consistency of failure” axiom.

Now we are ready to prove a bigger result:

Theorem 6. If A′_{p^{−1}(1)} … A′_{p^{−1}(n)} ↔^{∗} A_{1} … A_{n} is a canonical commutation path for permutation p, and A′_{p^{−1}(1)} … A′_{p^{−1}(n)} ↔^{∗} A′′_{q(p^{−1}(1))} … A′′_{q(p^{−1}(n))} has associated permutation q, then there exists A′′_{q(p^{−1}(1))} … A_{q(p^{−1}(n))} ↔^{∗} A_{1} … A_{n} which is a canonical commutation path for permutation p ⊙ q^{−1}.

Proof. By induction on the structure of A′_{p^{−1}(1)} … A′_{p^{−1}(n)} ↔^{∗} A′′_{q(p^{−1}(1))} … A′′_{q(p^{−1}(n))} it suffices to prove this for A′_{p^{−1}(1)} … A′_{p^{−1}(n)} ↔^{↑} A′′_{q(p^{−1}(1))} … A′′_{q(p^{−1}(n))}

So, q is a single transposition (i i + 1). Let As = A_{1} … A_{n}, As′ = A′_{p^{−1}(1)} … A′_{p^{−1}(n)}, As′′ = A′′_{q(p^{−1}(1))} … A′′_{q(p^{−1}(n))}, X = A′_{p^{−1}(i)}, Y = A′′_{p^{−1}(i+1)}, X′ = A_{p^{−1}(i)}, Y′ = A′′_{p^{−1}(i+1)},

We have the canonical path As′ ↔^{∗} As for p, the single commutation As′ ↔^{↑} As′′, and we want to construct a canonical path As′′ ↔^{∗} As for p ⊙ q^{−1}.

Now, we know by a previous theorem that some canonical path As′′ ↔^{∗} As′′′ for p ⊙ q^{−1} exists, so our goal is to prove that As = As′′′.

We know that As′ and As′′ are identical except for patches X and Y , and XY ↔ Y′X′. In other words As′ = … XY … and As′′ = … Y′X′ . . ..

Consider the canonical representations of p and p ⊙ q^{−1}. If one of them begins with the transposition (i i + 1) then the other does not

Corollary 1. If A_{1} … A_{n} ↔^{∗} A′_{1} … A′_{n} has associated permutation id, then ∀i.1 ≤ i ≤ n.A_{i} = A′_{i}.

Proof. Let p = id and q = id. Then A_{p^{−1}(1)} … A_{p^{−1}(n)} ↔^{∗} A_{1} … A_{n} is trivially a canonical commutation path for p, so by the theorem A′_{q(p^{−1}(1))} … A′_{q(p^{−1}(n))} ↔^{∗} A_{1} … A_{n} is a canonical commutation path for p⊙q^{−1} = id. So the result follows by the earlier theorem showing uniqueness of canonical commutation paths.