[darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)
dagit at codersbase.com
Thu Oct 29 15:48:29 UTC 2009
On Thu, Oct 29, 2009 at 6:50 AM, Heinrich Apfelmus <
apfelmus at quantentunnel.de> 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'
> >> 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
> 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
> > 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
> >> C past the A and the C past the B' separately, but impossible to commute
> >> 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
> > 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
> > them to mean the same thing. That is, Ca and C are different
> > representations of the same transformation. So if one of them commutes
> > 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
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the darcs-users