[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)
apfelmus at quantentunnel.de
Thu Oct 29 13:50:48 UTC 2009
Jason Dagit wrote:
> Heinrich Apfelmus wrote:
>> Eric Kow wrote:
>>> 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)
(This is the property TP2 from
translated to darcs-style patch theory.)
> 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.
Yes, I meant " C (AB) commutes to (AB)' C1' " to be some kind of
shorthand notation that says that C can be commuted past A and B
C A B <-> Ac Ca B <-> Ac Bc C1'
with the understanding that
(AB)' := Ac Bc
and likewise for " C (B' A') <-> (B' A') C2' ".
Note however that in his paper, Judah extends commutation to sequences
of patches and proves that things like the above work as expected. This
is very handy!
>> 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.
Not sure, but hopefully yes. :)
> 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.
This is not true verbatim; you forgot the premise that C B' should
commute as well. Maybe you meant to include it?
Counterexample to the weaker version:
C = create file "foo"
A = change file "useless-bystander"
B = delete file "foo"
In other words, the changes C and B cannot be interchanged while A is
independent of both. Then,
C A <-> Ac Ca
A B <-> B' A'
but Ca B does not commute.
> 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.
Yes, exactly. (I'm not sure whether Judah's notion of sensible applies
here, however, at least in its current formalization.)
My amusing (to me) observation was that this "intuitively correct"
property is equivalent to the following property about merges:
Consider three concurrent patches
X = C^(-1) inverse of C
Y = A
Z = B'
+-- X +-- C --<
>---+-- Y <=> +-- A (-- B)
+-- Z +-- B'
X Y Z concurrent <=> C A B in sequence
X and Y can be merged (i.e. X and Y^(-1) commute)
Y and Z can be merged (...)
Z and X can be merged (...)
Now, is it really true that all three can be merged together? In other
words, it might be possible to merge any two of them, but you get a big
nasty conflict when trying to merge all three at once! :O
> 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
As for my intention, I do want to see a proof of the above, but only as
a test that Judah's formalization (or any other formalization) is able
to assert its correctness. I have no doubt that the intuition is
correct, I am merely offering this example as one test case to check the
adequateness of any patch theory.
In any case, I once again would like to stress that it is my belief that
commutation is already too complicated to be a suitable foundation for
understanding the semantics of merges.
In other words, thinking about the intricacies of commutation is a waste
of our precious brain cycles. :) They are better spent on a simpler
formalization where each line has its own GUID.
More information about the darcs-users