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

[Ben Franksen]

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