On Thu, Oct 29, 2009 at 6:50 AM, Heinrich Apfelmus < [email protected]> wrote:
> 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'. > >>> > >>> 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) > > (This is the property TP2 from > > http://en.wikipedia.decenturl.com/ot-convergence > > 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 > >> 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. > > 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' > > visually: > > +-- X +-- C --< > | | > >---+-- Y <=> +-- A (-- B) > | | > +-- Z +-- B' > > X Y Z concurrent <=> C A B in sequence > > such that > > 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 (...) > 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). Do you think it would help if we used the context notation here? For example, this is what I think you mean: 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). and you have, iCcAaBb as a sequence. So then, I think you mean to commute A and B so that we get cB'd. 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. Thanks, Jason
_______________________________________________ darcs-users mailing list [email protected] http://lists.osuosl.org/mailman/listinfo/darcs-users
