# [darcs-users] A formalization of Darcs patch theory using inverse semigroups (apfelmus)

Jason Dagit 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'
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20091029/69d91b89/attachment.htm>
```