[darcs-users] Why darcs? What does the 'physicists proof' actually prove?

[David Roundy]

Just one more thought I had on the differences between VAP and darcs.  That
is that if you don't view the commute as a fundamental operation, you are
likely to lose the benefit of a number of the properties that darcs has.
For example, because

A || B => A'B <---> B'A

the order in which you perform the merge doesn't matter.  If your merge
doesn't have this property then the merge theorem doesn't apply and the
VAP(inv(A),B) method of doing a commute may be irreversible--it would
depend on what constraints you did place on the VAP function.

On Tue, Jul 22, 2003 at 06:01:13PM +1000, William Uther wrote:
> Question 3: Is the simple darcs merge case the same as VAP?
> 
> In the section "How merges are actually performed", the darcs manual 
> states: "The first case is that in which the two merges don't actually 
> conflict, but don't trivially merge either (e.g. hunk patches on the 
> same file, where the line number has to be shifted as they are merged). 
>  This kind of merge can actually be very elegantly dealt with using 
> only commutation and inversion."
> 
> This sounds to me very similar to VAP.  In particular, Definition 3 
> states that:
> 
> P1 || P2 => P2'.P1 <-> P1'.P2
> 
> where using VAP we might write:
> 
> P2' = VAP(P1, P2)
> P1' = VAP(P2, P1)
> 
> Is this the sort of calculation darcs performs, in this case?

Yes, with the above-mentioned caveat that without the commute property of
merges (which I'm not sure that VAP has) you may get a different answer
depending on which of the above solutions you chose.  But assuming they get
that right, the two should be equivalent for the unconflicted case.

> Question 4: How does Theorem 2 help merging?
> 
> Theorem 2 states that P2'.P1 <-> P1'.P2 iff Inv(P1').P2' <-> P2.Inv(P1) 
>  (assuming everything is actually calculable).
> 
> This tells us when certain things commute.  In addition, we know P2 and 
> Inv(P1) and can hence get Inv(P1').P2'.

I would say rather that this tells us when certain patches merge--without
conflict, that is.

> But, how do you get Inv(P1') and/or P2' from Inv(P1').P2'?  What tells 
> us how to break this patch apart?

The key thing here is that commute is a function that takes two inputs and
give two outputs (as it must, in order to be useful).  So when you commute
P2 and Inv(P1) we get out Inv(P1') and P2' already broken apart.  The
"multiplication" notation is just intended to make clear the relationship
between the two patches.

So to summarize, Theorem 2 tells us (with regard to merging--it also has
other uses) how to take a commutation function and turn it into a merge
function.  This is very cool, because commutation has more and simpler
properties than the merge does.  Most importantly, commutation is a
self-inverse function--commute twice and you get back the same result.
Also, the composed commuted patches must be equivalent to the original
composed patches.

One example of the beauty of the merge theorem is if you consider the merge
of a file change (say a hunk) with a file rename of that file.  It isn't
too hard to figure out that the correct thing is to either first rename the
file and then modify the file with the new name, or first modify the file
with the old name and then rename it.  But you don't have to worry about
this if you've defined the commutation of these patches (which in my
opinion is simpler to think about, and has only one case needing to be
defined instead of two--you get the other case from the commutation of the
inverse of the composition of the two patches).
-- 
David Roundy
http://www.abridgegame.org