[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)

Jason Dagit 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/ )
> Thanks,
> Eric
> --
> 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'.
>>  http://darcs.net/tests/failing-issue1609_ot_convergence.sh
> 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'
>  then
>     (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
>    then
>      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
sensible sequences.

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
Judah's paper.

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...
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20091028/9832ec5a/attachment-0001.htm>

More information about the darcs-users mailing list