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) = (C->D,(A->B,X)) for (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.

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->B, B->C,X) = (A->C,X). Here, Q plays no role, this can be easier to think of as a rule about arrows: (A->B, B->C = A->C).

3. (X->(A->B,X),Q) = (B->A, Q). Here, Q plays no role, this can be easier to think of as a rule about arrows: (X->(A->B,X)) = B->A. (TODO: Make this look clear)

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', X) = (Y->(A->B,X),Z) = (Y->X, X->(A->B, X), Z) = (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.