Patch calculus

This page describes the darcs patch calculus, which I am developing, inspired by the darcs-conflicts effort. That is a version of darcs intended to perform a lot better in the presence of merge conflicts.

For David Roundy's write-up of the theory behind Darcs, please refer to the 'Theory of Patches' chapter of the Darcs manual. The patch calculus outlined above is not 'official', nor endorsed by David in any way. Please note that the notations and concepts described here, can differ from --and conflict with-- things David and others write and/or program.

The very first version of this calculus was described in an e-mail to the darcs-conflicts mailing list.

This page is under construction: I'm currently processing the comments I received from others, and new insights from the last couple of days. That said, I try to keep this page self-consistent, and I welcome feedback (see my e-mail address in the footer of this page).

Basics: patches in sequence

This section describes what a patch is, and how patches are inverted and composed in sequence. We only give the necessary axioms here, and derive useful theorems in the next section.

Patches, context and meaning

In SCM terms, a patch is a change made to a a set of source files (a 'configuration'), which leads to a new configuration. Here we call such a configuration a 'context'. We distinguish between the 'meaning' of a patch (e.g., "replace all identifiers 'start' by 'begin'"), and its 'effect' (i.e., the actual diff). The effect follows from the context and the meaning of the patch.

Therefore the two defining characteristics of a patch are its context and its meaning: 

    A = B   ==   A || B  /\  A ~~ B      "definition: equality"
Here I use some of my own [ASCII logical notations]; note that uppercase letters (A, B, ...) are of type 'patch', which may be replaced by any expression of type 'patch'.

Informally, A || B means that A and B have the same context, and A ~~ B means that A and B have the same meaning. Note how we try to keep things simple by not representing context and meaning explicitly, and only comparing them. Of course we would expect that 

    || is an equivalence relation        "axiom: || is equivalence"
    ~~ is an equivalence relation        "axiom: ~~ is equivalence"
(Reminder: an equivalence relation ~ is one which is reflexive (A~A), symmetric (A~B == B~A), and transitive (A~B /\ B~C => A~C).)

It is easy to see that this makes '=' an equivalence relation as well. This equivalence relation becomes a real equality by allowing substitution of equals for equals: 

    A = B   =>  e[C:=A] = e[C:=B]     "axiom: Leibniz' rule"
where e is any expression of type 'patch' or 'boolean' containing C as a free variable.

Inverting patches: the inv() operator

Every patch A has an inverse inv(A), which can be inverted back to the original: 
    inv(inv(A)) = A                       "axiom: inv() is an inversion"
If two patches have the same meaning, then the inverted patches also have the same meaning: 
    A ~~ B  =>  inv(A) ~~ inv(B)          "axiom: inv()-meaning"
Apart from these properties, there are no axioms for the context or meaning of inv(...) in general. Below are rules which define the inverse of each patch expression.

Null patches

'null@A' is the 'null patch applied in context A', with A null@inv(A) = null@A A = A. inv(A)A = null@inv(A). It turns out to be useful to have a 'null patch': a patch that does not change anything to its context. We write null@A for "the null patch that has the same context as A". This has the following two essential properties: 
    null@A || A                           "axiom: context of null"
    null@A ~~ null@B                      "axiom: all nulls mean the same"
Of course, the null patch is its own inverse: 
    inv(null@A) = null@A                  "axiom: null is self-inverse"

Patches in sequence: the concatenation operator

The simplest thing to do with two patches is to concatenate them: AB is patch A then B. This is only valid if the result context of A is the context of B, or formally: inv(A) || B. Therefore we only allow the concatenation notation if this condition holds.

The intuition behind concatenation immediately suggests the following rule for context manipulation: 

    AB || A                               "axiom: simplify context"
provided that inv(A) || B.

For the combination of inv() with concatenation we have the following: 

    inv(AB) = inv(B)inv(A)               "axiom: exchange inv() and sequence"
provided inv(A)||B. And for the concatenation of inverses and null patches we postulate: 
    A inv(A) ~~ null@A
    null@A A ~~ A
This is enough to derive all useful theorems combining inv(), concatenation, and null patches.

Until this point we have only introduced 'trivial' axioms, to describe our intuition of patches and there context and meaning. Now comes the first 'essential' axiom: 

    A ~~ B /\ C ~~ D  =>  AB ~~ DC        "axiom: reordering preserves meaning"
provided that inv(A)||B and inv(D)||C.

This axiom implies that two patch sequences have the same meaning if they have the same 'set of meanings'! This is what makes patch commutation possible, as we will see below. But before we can do that, we have to have a notation for, e.g., 'B commuted forward over A'.

Re-contexting patches: the move operator

If A and B have the same context (A || B), we read <A,B> as "B commuted forward over A" or "B, but applicable after A". This patch exists regardless of whether this conflicts or is really possible. Formally 
    <A,B> ~~ B                              "axiom: meaning of move"
    <A,B> || inv(A)                         "axiom: context of move"
As we will see below, this operator is the basis for all commuting and merging.

When trying to prove the commutation theorem (below) I found that we also need the following axiom: 

    inv(<A,B>) || inv(<B,A>)                "axiom"
I don't yet know whether it is possible to reduce this to a simpler axiom. It seems that this is essential: it says that <A,B> and <B,A> result in the same configuration, i.e., the same context.

Some useful theorems

The following kind of manipulation ("juggling") is done often: 
    AB = CD  ==  inv(A)C = B inv(D)    "juggle"
Why is this true? Well, it helps me to look at it this way: 
    o -------( A )------> o
    |                   / |
    |          /       /  |
  ( C )  /----<-------/ ( B )
    |   /      \          |
    | |/                  |
    V /--                 V
    o -------( D )------> o
The "arrow" in the middle shows that A-inverted followed by C is the same as B followed by D-inverted. (This kind of diagram seems also helpful in more complex cases.)

Commuting and merging by adding context

Patches overtaking each other: commutation

Now we have enough to do commutations: given patches A and B with inv(A)||B, we look for A' and B' for which 
    AB = B'A'
    A ~~ A'
    B ~~ B'
    inv(B') || A'
So we need to find a B' for which B'||A (from the commutation equation) and B'~~B. Looking at the axioms for the <,> notation, it is easy to see that B' = <inv(A),B>: 
    B' = <inv(A),B>
==    "definition of equality"
    B' || <inv(A),B>  /\  B' ~~ <inv(A),B>
==    "context and meaning of <inv(A),B>"
    B' || inv(inv(A))  /\  B' ~~ B
==    "simplify"
    B' || A  /\  B' ~~ B
Similarly we find that 
    A' = inv(<B,inv(A)>)
==    "definition of equality"
    A' || inv(<B,inv(A)>)  /\  A' ~~ inv(<B,inv(A)>)
==    "context and meaning of inv(<B,inv(A)>)"
    A' || inv(<inv(A),B>)  /\  A' ~~ inv(inv(A))
==    "introduce B'; simplify"
    A' || inv(B')  /\  A' ~~ A
Summarizing, we proved that if AB makes sense, then 
    AB = <inv(A),B> inv(<B,inv(A)>)   "theorem: commutation"

Patches in parallel: the merge operator

Using this, we can define for all A || B: 
    A + B = A<A,B>             "definition: merge"
As one would expect, merging is symmetrical: 
    A + B = B + A              "axiom: merge is symmetrical"
which immediately gives us 
    A + B = B<B,A>             "alternative definition: merge"
Intermezzo on null patches: we obviously want 
    A + null@A = A             "axiom: null merge"
Through the definition and symmetry of merge, this implies that 
    <A,null@A> = null@inv(A)  "theorem: null patch is not affected"
    <null@A,A> = A            "theorem: null context has no effect"

More laws for context changes

Let me repeat two laws that I gave earlier: 
    <BC,A> = <C,<B,A>>     "axiom: stepwise context addition"
Justification: adding BC to the context of A means first adding B, then adding C. This immediately leads to 
    <inv(A),<A,B>> = B     "theorem: add/remove context cancel out"
Proof: 
  <inv(A),<A,B>>
=   "stepwise context addition"
  <A inv(A), B>
=   "property of inv()"
  <null@A, B>
=   "null context has no effect"
  B
Without justification for now (try drawing a diagram like above, but now for a merge of A and B), I think the following is valid: 
    inv(<A,B>) = <<B,A>,inv(B)>     "axiom? theorem?"

Conflictors

Now, at the end, it is time for introducting conflictors. I propose to split the set of patches in to 'defined patches' (notation: def(P)) and 'conflictor patches' (notation [A,B]), and to let exactly one of the following be true for any A || B: 
    <A,B> = [A,B]
    def(<A,B>)
(I don't have the time now to work this out more formally. Also, I think that def(A) == def(inv(A)) should hold.)

This makes all of the above general laws work for conflictors, provided we really do have a conflict (i.e, if for a certain <A,B> there is no non-conflictor patch equivalent to it). So all the laws above are really independent of whether merging works or not. This gives us the following formal definition whether a commute 'works': for every A and B with inv(A) || B, 

    A followed by B commutes  ==  def(<inv(A),B>) and def(<B,inv(A)>)
(This definition is inspired by the right hand side of the commute theorem.)
This page is brought to you by Marnix Klooster, and is part of his home page. Feel free to e-mail me with comments on the form and content of this page. 
Changes to darcs/patch-calculus.html:

Sat May  7 12:26:48 MEST 2005  Marnix Klooster
  * Updated concatenation axioms: added a few that I forgot, and simplified the rest.

Sat May  7 10:54:29 MEST 2005  Marnix Klooster
  * Minor wording improvements.

Sat May  7 10:51:58 MEST 2005  Marnix Klooster
  * Major addition: added axioms, and proved the commutation theorem from these axioms.

Wed May  4 07:13:41 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Removed superfluous sentence.

Wed May  4 07:13:09 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Clarified the meaning of the <A,B> notation.

Wed May  4 07:12:39 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Formatting change.

Tue May  3 10:25:31 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Switched to the null@A notation for null patches.

Tue May  3 08:33:08 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Elaborated the 'equality' part, and formalized 'the same meaning' of patches.

Tue May  3 08:32:00 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Renamed 'identity patches' to 'null patches', to prevent confusion with the 'identity' of a patch.

Mon May  2 17:09:42 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Minor word change.

Mon May  2 17:09:21 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Added 'under construction' warning.

Mon May  2 17:07:50 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Refactored the existing content: split into basics/theorems/advanced structure.

Sat Apr 30 15:19:36 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * HTML-ified the ASCII text of the original e-mail.

Sat Apr 30 11:55:04 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Made clear that my patch calculus is not official in any way.

Fri Apr 29 21:48:35 MEST 2005  Marnix Klooster <myfirstname.mylastname@solcon.nl>
  * Added initial version of 'patch calculus' page.