<br><br><div class="gmail_quote">On Thu, Oct 29, 2009 at 6:50 AM, Heinrich Apfelmus <span dir="ltr"><<a href="mailto:apfelmus@quantentunnel.de">apfelmus@quantentunnel.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Jason Dagit wrote:<br>
> Heinrich Apfelmus wrote:<br>
<div class="im">>> Eric Kow wrote:<br>
>><br>
>>> You may be interested in a related (but seemingly different) test for<br>
>>> something the OT people call 'convergence'.<br>
>>><br>
>>> <a href="http://darcs.net/tests/failing-issue1609_ot_convergence.sh" target="_blank">http://darcs.net/tests/failing-issue1609_ot_convergence.sh</a><br>
>>><br>
>> It appears to me that, in terms of commutators, this 'convergence' property<br>
>> from OT is to be expressed as follows:<br>
>><br>
>> patches C, A, B in that order<br>
>><br>
>> if A B commutes to B' A' and<br>
>> C (AB) commutes to (AB)' C1' and<br>
>> C (B'A') commutes to (B'A')' C2'<br>
>> then<br>
>> (AB)' C1' and (B'A')' C2' should have the same effect<br>
>><br>
>> In particular, I have chosen<br>
>><br>
>> C = invert op3<br>
>> A = op1<br>
>> B = T(op2,op1)<br>
<br>
</div>(This is the property TP2 from<br>
<br>
<a href="http://en.wikipedia.decenturl.com/ot-convergence" target="_blank">http://en.wikipedia.decenturl.com/ot-convergence</a><br>
<br>
translated to darcs-style patch theory.)<br>
<div class="im"><br>
> I'm having trouble understanding this because in darcs we don't have a<br>
> primitive to commute two patches. We can do this by repeated commutes<br>
> though. So, if you defined C (AB) commutes to (AB)' C1', as something along<br>
> the lines of A'B'C1', then I'd be happier.<br>
<br>
</div>Yes, I meant " C (AB) commutes to (AB)' C1' " to be some kind of<br>
shorthand notation that says that C can be commuted past A and B<br>
___ _____<br>
C A B <-> Ac Ca B <-> Ac Bc C1'<br>
^^^^ ^^^^^<br>
with the understanding that<br>
<br>
(AB)' := Ac Bc<br>
<br>
and likewise for " C (B' A') <-> (B' A') C2' ".<br>
<br>
<br>
Note however that in his paper, Judah extends commutation to sequences<br>
of patches and proves that things like the above work as expected. This<br>
is very handy!<br>
<div class="im"><br>
<br>
>> What my curiosity asks is slightly different, namely whether<br>
>><br>
>> if A B commutes to B' A' and<br>
>> C A commutes to Ac Ca and<br>
>> C B' commutes to B'c Cb<br>
>> then<br>
>> do Ca B or Cb A' actually commute as well?<br>
>><br>
>> In other words, it asks whether the postulated commutations in the<br>
>> convergence property actually hold. It could well be possible to commute the<br>
>> C past the A and the C past the B' separately, but impossible to commute C<br>
>> past both at the same time.<br>
>><br>
><br>
> Ah, yes, so we're wondering about the same thing.<br>
<br>
</div>Not sure, but hopefully yes. :)<br>
<div class="im"><br>
> Using Judah's idea of sensible sequence, and the 'intent' of patch theory<br>
> that says reordering a sequence via commute to another sensible sequence<br>
> doesn't change the state of the pristine, then we should have either a<br>
> theorem, lemma, or axiom that states if C A commutes to Ac Ca, and AB<br>
> commutes to B'A', then Ca B commutes.<br>
<br>
</div>This is not true verbatim; you forgot the premise that C B' should<br>
commute as well. Maybe you meant to include it?<br>
<br>
Counterexample to the weaker version:<br>
<br>
C = create file "foo"<br>
A = change file "useless-bystander"<br>
B = delete file "foo"<br>
<br>
In other words, the changes C and B cannot be interchanged while A is<br>
independent of both. Then,<br>
<br>
C A <-> Ac Ca<br>
A B <-> B' A'<br>
<br>
but Ca B does not commute.<br>
<div class="im"><br>
<br>
> The 'intent' of patch theory is that C A and Ac Ca give the same pristine<br>
> state. C and Ca represent the same transformation, but with different<br>
> domains (which means in the patch format we tweak the representation so that<br>
> a hunk applies to a different line in the file than it used it, as an<br>
> example). In other words, if C A is sensible and Ac Ca is sensible, we want<br>
> them to mean the same thing. That is, Ca and C are different<br>
> representations of the same transformation. So if one of them commutes with<br>
> B or B' then the other one should as well, assuming all the results are<br>
> sensible sequences.<br>
<br>
</div>Yes, exactly. (I'm not sure whether Judah's notion of sensible applies<br>
here, however, at least in its current formalization.)<br>
<br>
<br>
My amusing (to me) observation was that this "intuitively correct"<br>
property is equivalent to the following property about merges:<br>
<br>
Consider three concurrent patches<br>
<br>
X = C^(-1) inverse of C<br>
Y = A<br>
Z = B'<br>
<br>
visually:<br>
<br>
+-- X +-- C --<<br>
| |<br>
>---+-- Y <=> +-- A (-- B)<br>
| |<br>
+-- Z +-- B'<br>
<br>
X Y Z concurrent <=> C A B in sequence<br>
<br>
such that<br>
<br>
X and Y can be merged (i.e. X and Y^(-1) commute)<br>
Y and Z can be merged (...)<br>
Z and X can be merged (...)<br></blockquote><div><br></div><div>I don't understand the setup of this example. What does it mean for two or more patches to be concurrent? Also, the notation for your diagram is unfamiliar so I need an explanation of the symbols (>--) vs. (--<), (-- B), what does + represent, etc. At first I thought it was an ASCII art tree, but if that is true why do you say C A B is a sequence when they appear to branch from the same level of the tree? And I think you might have more than one notation for inverses, C^(-1) vs. (--B).</div>
<div><br></div><div>Do you think it would help if we used the context notation here? For example, this is what I think you mean:</div><div><br></div><div>oXx, oYy, oZz, would mean that X, Y, and Z all have the same pre-context (meaning they all apply to the same sequence of patches).</div>
<div><br></div><div>and you have, iCcAaBb as a sequence. So then, I think you mean to commute A and B so that we get cB'd.</div><div><br></div><div>In this notation the lower case letters represent the context of the patches. The context before the patch is the pre-context and it is where the patch applies, similar to the domain of a function. The post-context is the resulting context from applying the patch (so, c = i with C on the end). When patches are in a sequence we omit the contexts that are implied or redundant.</div>
<div><br></div><div>Thanks,</div><div>Jason</div></div>