[darcs-users] How to extend a patch theory to fully commute

[Ben Franksen]

> Definition: A context address (a, b, (Qi), X, Y) is a /simplification/
> of a context address (a', b', (Q'i), X', Y') if X and Y are subsets of
> (or equal to) X' and Y' and the sequence (Q'i) can be permuted so that
> it first follows the patches in X' \ X from a' to a, then follows the
> sequence (Qi), then follows the patches in Y' \ Y from b to b'.
> 
> Assumption 2: If a context address A has two different simplifications B
> and B' that are both canonical addresses, then B = B'. (I suspect this
> assumption may be false for Darcs 2 due to duplicate patches.)
>
> Remark: This is essentially saying that if you move as many patches in Y
> as possible to the end of the sequence, and as many patches in X as
> possible to the beginning, the final set of remaining patches you end up
> with is deterministic.

Two remarks.

(1) I think you may be able to prove this assuming general permutivity
for the primitive patch theory.

(2) As you already remarked, canonicity here is not essential for the
theory. For an equivalence class of things you can take an arbitrary
element as representative. But what you *do* have to show is that (a)
this is actually an equivalence class (easy, I think) and (b) that the
choice of representative doesn't matter. (b) is usually the harder part.
You also need to prove it for every operation you define on the
equivalence classes (if you define it in terms of a representative
member). In a practical implementation you would indeed have to fix a
deterministic algorithm to choose the representative, but for the theory
I think it is clearer to abstract over this choice.

Cheers
Ben