[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