Re: [darcs-users] How to extend a patch theory to fully commute

[James Cook]

> 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).

Thanks. I have not read through the details in the camp paper or the
Darcs V3 source code yet, but I think your explanation of conflictors
above, and the connection to the tree point of view, gives me some good
intuition to start with.

I wonder if some of this could go on the wiki?

(Incidentally, I just discovered http://darcs.net/Ideas/Graphictors which
seems related to this tree point of view.)
 
> 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

I think the goal I described in my other email just now would end up
looking something like this, but with inverses on all the not-chosen
branches instead of a flag on the chosen branch.

-- 
James
___
darcs-users mailing list

Re: [darcs-users] How to extend a patch theory to fully commute

[James Cook]

(new email address)

I'm hoping to do a little write-up of my idea for avoiding conflictors,
after working out some details. (Maybe I'll discover it doesn't work
out.)

For now though I have waited long enough to answer your email so here
goes...

> 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.

Thanks for the explanation. I think I had something different in mind
for my version (a) of representing a tree with a sequence, but there are
still problems.

Representation (a) from my last email inserts the sequence d e'' between
b and c: so the tree is represented as a b d e'' c, where (using your
correction) merge(d\/e) = (e''/d').

This means that the context X in your diagram doesn't exist: the ending
context of b and the starting context of c are different. We have:

O--a--L--b--X1--d--Z--e''--X2--c--R

I think with this representation there's no need for c^, but commuting b
and c clearly does require some interaction with d and e''.

Also, it's not clear to me how freely the branches of the tree could be
re-ordered with this representation.

Anyway, I am more interested in my version (b), which doesn't involve
conflictors.

> > 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.)

That sounds right; thanks.

> 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.

Version (b) (linearizing with DFS) isn't supposed to involve conflictors
at all.

I think it would be better if I wait until I have a more careful write-up
of how I imagine this working.

> 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.

Yes, I should probably return to that at some point.

-- 
James
___
darcs-users mailing list
darcs-users@osuosl.org
https://lists.osuosl.org/mailman/listinfo/darcs-users