Re: [darcs-users] How to extend a patch theory to fully commute
>> Conflictors in Darcs can be seen as "internalizing" the relevant parts >> of the above tree structure /into/ the (conflicted) patch >> representation. This is the source of their complexity. What we gain >> form that is the possibility arrange all patches in a repo in a linear >> sequence where commutation is the only allowed (and required) form of >> sequence re-arrangement. > > Maybe it would be helpful to formalize this connection. If nothing > else, it might be an alternative way of explaining the Camp theory. > Actually, for all I know this is exactly how I'm supposed to think of > conflictors in Camp. I never fully understood that write-up; maybe I > should take another look. In camp/darcs-3 (see src/Darcs/Patch/V3) a conflictor consists of three parts (all prim patches are of course named): * The effect (a sequence of prim patches that negate all patches that we conflict with, unless already negated by a previous conflictor), * a set of "contexted" (prim) patches (those we conflict with) * the (prim) patch itself (its "identity"), also as a contexted prim patch. Contexted patches should be visualized as forking off to the side, the only part that is actually applied is the effect. The "contexted" here means that the actual prim patch is prefixed by a sequence of prim patches that re-context the original patch such that it applies at the end of the conflictor. The camp paper visualizes this as (arrows point rightward): / (context+)conflicts / *--effect--*--(next patch)-- \ (context+)identity \ In principle it would be possible to replace the contexted patches in the set of conflicts with patch names, since it is guaranteed (by a global invariant) that they must occur in the context (preceding patches). The above representation makes conflictors self-contained with respect to commute and merge i.e. we don't have to consult (or know) the context. Also note that the "context" in a contexted patch usually consists of negated patches (we have to walk backwards along the history to reach the patch we reference). BTW, to keep them minimal we do use cancellation of inverses in these "contexts" and also commute any patch past (and then drop it) if possible. The only difficult thing here is to determine the proper side-conditions when commuting and merging conflictors, so that the patch laws (mainly permutivity) are satisfied. The source code in Darcs has a number of comments to explain what is going on but may still be hard to follow for someone unfamiliar with the code base. The last chapter of teh camp paper explains each case in detail and motivates the various side conditions with examples. The tree view can only be equivalent to this if we somehow store additional information about which patches are in (direct) conflict with each other. This is because given only the tree view we cannot distinguish between a conflict (between say patches d and e) and its (manual) resolution c (recorded after the conflict), since all three patches start from the same "context" (node in the tree). In Darcs the conflict resolution patch *depends* on the conflicted patches, but it does not conflict with them. Also, whenever we have multiple conflicts at the same point (say, a conflicts with b, which conflicts with c, but a doesn't conflict directly with c), then we have to either store or re-calculate that information because camp conflictors only store direct conflicts and thus only considers these in the merge and commute rules. If we have this extra information (as, say, a finite map from patch names to sets of patch names), and a way to look up the (unique, per repo) patch representation plus its context (preceding patches) by name, then we can reconstruct the conflictor representation from that. Conversely, given a sequence of (possibly conflicted) patches, we can reconstruct the tree by traversing "contexted" patches in a conflictor backwards until we reach the patch they reference, then create a branch of the tree at that point. (This is just a rough sketch but I hope you get the idea). I still wonder if a consistent patch theory *different* from camp/darcs-3 could be devised in which conflict resolutions really are freely exchangeable with the conflicted patches instead of depending on them. In other words, we may *choose* one of the conflicting patches as the resolution (creating a new one if none are suitable). I think this would require, in the tree view, to add a special flag to mark such patches as the chosen resolution. This would make the theory more symmetric and would perhaps also make resolving conflicts easier to handle; and perhaps simplify commute and merge, too. I haven't thought this through, though, and it may turn out that this doesn't work. Cheers Ben ___ darcs-users mailing list darcs-users@osuosl.org https://lists.osuosl.org/mailman/listinfo/darcs-users
Re: [darcs-users] How to extend a patch theory to fully commute
Am 17.09.20 um 01:51 schrieb James Cook:
>> So this can succeed only if c does not conflict with either of its
>> sibling cancelled branches, that is, if c^ commutes with all sequences
>> ("paths") in the cancelled branches, that is, all elements of {d, e;f,
>> e;g, e;h;i}. We then get
>>
>> a--b'-c'
>> |\
>>d' e'-f'
>> |\
>> g' h'-i'
>>
>> where we dropped the result of commuting c^ past.
>
> I think I'm missing a piece (or maybe you made a mistake).
>> Where does
> c^ come into the picture? Also, shouldn't b be unmodified?
I don't think so, see below.
> Let me go through this in a bit more detail, to explain what I mean
> and help myself make sure I understand.
>
> I'll simplify your example a bit to this:
>
> a--b--c
>|\
>d e
>
> Actually, I'd rather put the patches on the edges.
Yes, this notation is a lot clearer and less error prone. I should have
stuck to it.
> I guess the above tree becomes:
>
> a b c
> *--*--*--*
> |\
> d| \e
> * *
Yes. And the question I raised is: suppose b;c (taken in isolation)
commute to c';b', what are the side-conditions that allow us to make
them commute in the full picture?
Let me give a name to some of contexts involved:
a b c
*---L---X---R
|\
d| \e
| \
* *
Now, if we commute
b c
L---X---R
to
c' b'
L---Y---R
then this creates a new context Y that wasn't there before, whereas the
old context X has vanished. So *the least* we have to ensure is that we
can somehow transform d and e so that they can be attached somewhere to
the trunk a;c';b'.
I am going to discuss only d here, we need to do the same for e of
course. So we have a commuting square with d hanging off the bottom:
Y
/ \
c' b'
/ \
L R
\ /
b c
\ /
X--d--*
Note that all arrows point rightward here (which is why we have to
(temporarily) invert c to c^ to make it point leftward). We can attach d
to either L, Y, or R, which gives us three possibilities to re-attach d
to the upper part of this diagram:
* commute b';c^ past d to get Y--d'--*
* commute only c^ past d to get R--d'--*
* commute b past d to get L--d'--*
Whatever we choose, we have to make sure these commutatations succeed.
> I can see two ways to represent that tree with linear sequence of patches:
>
> (a) Create a conflictor e' by commuting (d^, e) <-> (e'', d'^), and
> represent the above tree as a b d e'' c. I guess this is the Darcs
> way.
In principle yes, except that the conflictor cannot be defined in terms
of commutation alone, you need a primitive merge operation here i.e.
merge(d\/e)=(e'/\d') that satisfies the merge-commute law. This law
states that d;e' then commutes to e;d', which is required because we
want the result of merges to be independent of the order in which we
merge. (Remember that we regard sequences that differ only with respect
to re-ordering via commutation as equivalent.)
> (b) a b d d^ e e^ c. This follows my idea of handling conflicts by
> cancelling out everything involved in the conflict.
>
> Now, we want to rearrange it to:
>
> a b c'
> *--*--*--*
> |\
>d'| \e'
> * *
>
> In version (a), that just means re-ordering d e'' c to c' d' e'. In
> version (b), it means reordering d d^ e e^ c to c' d' d'^ e' e'^. Does
> that all sound correct?
I think you misunderstood the point I was trying to make. I hope my
above explanations made that clearer.
I agree that it is very tempting to linearize the tree representation
with a depth first traversal involving inverses, as you suggested:
a;b;d;d^;e;e^;c.
In fact, *if* the conflictor for e could be expressed as e'=(d^;e;e^),
then the above sequence would be identical to
a;b;d;e';c
Unfortunately this conflictor representation is too simple. It cannot
handle three-way conflicts correctly. The corresponding diagram involves
a commuting *cube* which is difficult to paint using ASCII graphics, but
easy with pencip and paper. The equations that must hold according to
the law of permutivity can then be directly read off the diagram. Doing
this is a very instructive exercise.
I'll respond to your further remarks in a separate message.
We have veered off your initial idea quite a bit! I think it may still
be worth resurrecting your extended contexts and patches to see where
this gets us if we try to complete all proofs and flesh out the
requirements properly.
Cheers
Ben
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users
