[darcs-devel] force-commute
Ben Franksen
ben.franksen at online.de
Thu Nov 2 12:50:58 UTC 2017
I made a mistake in my presentation (it works fine in the code, I just
didn't translate my changes correctly to the written notation).
We cannot use the notation c:p for a contexted patch. It works only if
we restrict to "forward" (not inverted) contexted patches as in the
paper. Our contexted patches should be invertible, which means we need a
notation that can distinguish between forward and backward contexted
patches. Let's use c/p for forward contexted patches and c\p for the
backward variant. Then we define
(c/p)⁻¹ = c⁻¹\p⁻¹
and
(c\p)⁻¹ = c⁻¹/p⁻¹
The operation that adds a patch to the context also needs to take the
direction into account. So
q(q⁻¹c/p) = c/p
q(c/p) = c/p if qc <-> c'q' and q'p <-> p'q''
q(c/p) = qc/p otherwise
and for backward contexted patches we define
q(qc\p) = c\p
q(c\p) = c\p if q⁻¹c <-> c'q' and q'p <-> p'q''
q(c\p) = q⁻¹c\p otherwise
which means, basically, that we first invert the patch before we add it
to the context.
Note that backward contexted patches are anchgored at the target state:
if c::X->Y and p::Y->Z, then c/p is anchored at X, and (c/p)⁻¹=c⁻¹\p⁻¹
is anchored at X, too, because c⁻¹p⁻¹::Z->X.
> So what I did is to invert the internals of a conflictor, instead, like> this:> > (1) [e,X,p]⁻¹ = [e⁻¹,eX⁻¹,ep⁻¹]
This is still correct if contexted patches are interpreted as above. But
the force-commute of [p][q], where q depends on p, should be written
[p,{/p⁻¹},/q] [q⁻¹,{/q},/p⁻¹]⁻¹
=
[p,{/p⁻¹},/q] [q,{q\q⁻¹},q\p]
Now at least the contexts make sense.
> Anyway, looking at the effects is interesting: the first conflictor
> represents q and has effect p, the second one represents p and has
> effect q. So, these two conflictors do /not/ remove effects! Instead
> they /exchange/ the effects of two patches.
>
> This is weird but fascinating and perhaps we can learn something from it.
Ganesh wrote:
> It's actually a property of any generic conflict representation
You are right, of course. The specifics of the conflictor representation
are irrelevant to this result. It suffices to assume that a conflictor
inverts the effect of the patch it conflicts with.
What does this all mean anyway?
Suppose we unpull the conflictor representing q. We are left with
[p,{/p⁻¹},/q]
This has the effect of p, represents q and conflicts with p⁻¹. How
should we represent this conflict (think: markup-conflicts)? We should
offer the choice between p⁻¹ and q, *after* applying the effect p. That
actually makes sense.
What about the second conflictor:
[q,{q\q⁻¹},q\p]
It has the effect of q, conflicts with q⁻¹, and represents p. So its
markup should be offering the choice between q⁻¹ and p.
Then how can we present to the user the combined conflicts of
[p,{/p⁻¹},/q] [q,{q\q⁻¹},q\p]
?
Cheers
Ben
More information about the darcs-devel
mailing list