Conflicts

TODO: Add a note about how this is likely a portion of Pijul's "patch theory".

Let us use the notation A'=(A->B,X) to say that A' is the result of rebasing a revision A with parent B on top of X. We'll also use the notation (C->D,A->B,X) for (C->D,(A->B,X)) = (C->D, A').

Claim. Every conflict (defined as the result of any sequence of rebases of above objects) can be represented this way, as a sequence (A_1->B_1, ..., A_n -> B_n, X) for some un-conflicted revisions A_i, B_i, X.

This can be thought of as a bunch of diffs on top of X. In jj's terms, this corresponds to a conflict where the A_is and X are "adds" and the B_is are "removes".

Before proving that, let's develop some rules of algebra that should hold for all conflicts.

1. (A->B,B)=A.

2. (A->C,X) = (A->B, B->C,X). Here, X plays no role, this can be easier to think of as a rule about arrows (a.k.a. diffs): (A->C)=(A->B, B->C).

3. (A->B, (B->A, X)) = X. The arrow rule here would be: (A->B, B->A) = (trivial diff). (follows from above. What about the other way?)

4. (X->(A->B,X),Q) = (B->A, Q). Here, Q plays no role, and the arrow rule is again simpler: (X->(A->B,X)) = B->A. (TODO: Make this look clear. Does this follow from others?)

Aside: In fact, all these rules can be thought of as rules about arrows and often look simpler this way. A revision A can be thought of as an arrow A->0 where 0 is the empty revision.

From the above, we get a tricky rule:

(Y->A', Z) = (Y->(A->B,X),Z) =rule3= (Y->X, X-> (A->B,X), Z) =rule4= (Y->X, B->A, Z)

Proof of Claim: TODO.

The above rule is the hard part. Also, (A'->Y,Z) = ((A->B,X)->Y,Z) = (A->B, X-> Y, Z). (Is this a separate rule, or does it follow from the others?)

---

Note on merges

Two ways to represent them: a merge of A and C with base B can be represented in two ways: (A->B,C) ~ (C->B, A). This is not an equality, leads to different-looking diffs.

Questions:

1. Is (A->B, C->D, X) = (C->D, A->B, X)? My feeling from reading about Pijul is that this is not always true.