On Wed, Oct 28, 2009 at 10:17 AM, Eric Kow <[email protected]> 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 <[email protected]> > To: Eric Kow <[email protected]> > 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
_______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
