[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)
dagit at codersbase.com
Wed Oct 28 18:02:27 UTC 2009
On Wed, Oct 28, 2009 at 10:17 AM, Eric Kow <kowey at darcs.net> wrote:
> Hi everybody,
> Just forwarding some comments from Apfelmus regarding the recent paper
> by Judah on Darcs patch theory
> ( http://www.math.ucla.edu/~jjacobson/patch-theory/ )
> Eric Kow <http://www.nltg.brighton.ac.uk/home/Eric.Kow>
> PGP Key ID: 08AC04F9
> ---------- Forwarded message ----------
> From: Heinrich Apfelmus <apfelmus at quantentunnel.de>
> To: Eric Kow <kowey at darcs.net>
> Date: Wed, 21 Oct 2009 21:40:58 +0200
> Subject: Re: A formalization of Darcs patch theory using inverse semigroups
> Hello Eric,
> On Tue, Oct 20, 2009 at 21:03:11 +0200, Heinrich Apfelmus wrote:
>>> For instance, concerning merges, the following curiosity occurred to me:
>>> imagine three people working in parallel and making three patches A,B
>>> and C respectively against some common repository R. And now, imagine
>>> the following weird situation:
>>> There is a conflict when trying to merge all three patches A,B and C,
>>> but you can merge any two of them, i.e. A and B can be merged,
>>> B and C can be merged and A and C can be merged.
>> You may be interested in a related (but seemingly different) test for
>> something the OT people call 'convergence'.
> It appears to me that, in terms of commutators, this 'convergence' property
> from OT is to be expressed as follows:
> patches C, A, B in that order
> if A B commutes to B' A' and
> C (AB) commutes to (AB)' C1' and
> C (B'A') commutes to (B'A')' C2'
> (AB)' C1' and (B'A')' C2' should have the same effect
> In particular, I have chosen
> C = invert op3
> A = op1
> B = T(op2,op1)
I'm having trouble understanding this because in darcs we don't have a
primitive to commute two patches. We can do this by repeated commutes
though. So, if you defined C (AB) commutes to (AB)' C1', as something along
the lines of A'B'C1', then I'd be happier.
> What my curiosity asks is slightly different, namely whether
> if A B commutes to B' A' and
> C A commutes to Ac Ca and
> C B' commutes to B'c Cb
> do Ca B or Cb A' actually commute as well?
> In other words, it asks whether the postulated commutations in the
> convergence property actually hold. It could well be possible to commute the
> C past the A and the C past the B' separately, but impossible to commute C
> past both at the same time.
Ah, yes, so we're wondering about the same thing.
Using Judah's idea of sensible sequence, and the 'intent' of patch theory
that says reordering a sequence via commute to another sensible sequence
doesn't change the state of the pristine, then we should have either a
theorem, lemma, or axiom that states if C A commutes to Ac Ca, and AB
commutes to B'A', then Ca B commutes.
The 'intent' of patch theory is that C A and Ac Ca give the same pristine
state. C and Ca represent the same transformation, but with different
domains (which means in the patch format we tweak the representation so that
a hunk applies to a different line in the file than it used it, as an
example). In other words, if C A is sensible and Ac Ca is sensible, we want
them to mean the same thing. That is, Ca and C are different
representations of the same transformation. So if one of them commutes with
B or B' then the other one should as well, assuming all the results are
Okay, so I'm talking about 'intent' here because I'm not sure if there is a
rigorous argument to support the intuition (yet). I'm still working through
Does this help? I suspect you want a proof that the above works, but I
don't know one. Hopefully you can take my intuition and form a rigorous
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the darcs-users