> 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 _______________________________________________ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users