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

[Jason Dagit]

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
proof?

Thanks,
Jason
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20091028/9832ec5a/attachment-0001.htm>