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

[Ben Franksen]

Am 03.07.20 um 22:22 schrieb James Cook:
>>> But yes, I realized after writing it that I never covered inverting
>>> extended patches.
>>>
>>> Thinking about it more, I think I've found some problems. Let's say s
>>> is the starting context of A and B, and A ends with a and B ends with
>>> B. Here are three problems:
>>>
>>> (a) I'm not sure inverses exist in general.
>>
>> I had thought that was the easy part:
>>
>>   (a, b, (Qi), (nj), X, Y)^ = (b, a, (Qi)^, (nj)^, Y^, X^)
>>
>> where inversion for a set of names is the set of inverted names. You do
>> need names to be invertible.
> 
> The trouble is that doesn't give compatible starting/ending contexts
> according to the definition of starting/ending context in Chapter 4.
> 
> I want the ending context of A to be the starting context of A^ and vice versa.
> 
> But, for example, let's see what happens when you commute A;B to B';A'
> and try inverting B'. (contexts aAbBc)
> 
> B' is (a, c, A;B, [B], {}, {A}). Its ending context is (a, c, A;B, {B}, {A}).
> 
> If you take B'^ to be (c, a, B^;A^, [B^], {A^}, {}), then the starting
> context of B'^ is (c, a, B^;A^, {A^}, {B^}).
> 
> Probably those two contexts should be considered equivalent, but under
> the current write-up they're not.

I see. Yes, with inversion added, every context address has two minimal
forms: forward and backward, and these denote the same extended context.

>> Okay, I see the problem now. Thanks for explaining.
>>
>> In Darcs we don't have this problem because we do not distinguish
>> between primitive and extended contexts. You can just revert the
>> conflict markup and record anything you like. If this happens to overlap
>> (i.e. depend on) the changes reverted by the conflict, then it is
>> regarded as a conflict resolution. It is clear that this cannot work in
>> your theory, so you need something else to mark a conflict as resolved.
>> Sounds like an interesting problem indeed.
>>
>> As I remarked a while ago in a different discussion, adding a proper
>> force-commute operation to darcs is unsound for the simple reason that
>> we could no longer unambiguously define what it means for a repo to have
>> (unresolved) conflicts: (force-)commuting any two patches makes the repo
>> conflicted. Your approach solves that problem nicely, but now you have
>> to find a way to get away from a conflicted repo state.
>>
>> Regarding your proposed solution, I think Proposition 5 cannot be true
>> unless you add inverses. Here is a counter example: we have prims
>> A;(B\/C), where neither A;B nor A;C commute as prims. The extended
>> universe of patches adds the force-commuted sequences B';A' and C';A'',
>> together with their mid-contexts. But that's it: you get two sides of
>> the cube, with a common edge (A). Without inversion there is no way from
>> the mid-context of B';A' to that of C';A''.
>>
>> If, however, you add inverses, then Proposition 5 is trivial.
> 
> I was assuming the primitive patch theory already has inverses. Is
> that not normal?

You are right, I forgot about that. However, your primitive patches are
named. In Darcs you cannot record a "negative" patch. So while prim
inverses can be calculated internally, they can never be stored as
patches in a repo (except as ingredients of a conflictor).

So the question is whether you want to allow inverse prim patches to be
part of the repo or not.

In any case, you already have inversion in the extended theory. You just
have to show that it has the right properties:

If you commute A;B to B';A', then the inverse of B';A' must be equal to
the commutation of B^;A^. For this to work, you *have* to identify the
mid-contexts. These two contexts exactly correspond to the above forward
and backward minimal context addresses.

Proposition 5 is still trivial with inverses: a (non-empty) complete
undirected graph is connected.

> I think I've found a new problem with Proposition 5, though.
> 
> Suppose A, B and C are three mutually conflicting patches with
> starting context s.
> 
> Suppose I merge A and B, then I use Proposition 5 to navigate back to
> the starting context s so that I can continue recording new patches.
> 
> The problem: now if I pull in C, it looks just like any other new
> patch to be recorded starting at context s. So, by marking the A\/B
> conflict as resolved, I've made my repository unaware that C should be
> considered to be a conflict.

I'd say this is a feature, not a bug. If you mark the conflict between A
and B as resolved, *without* recording a new patch, then this means you
are satisfied with the resolution that reverts both changes. There is no
reason why pulling C should conflict now. If, on the other hand, you are
not satisfied with this resolution, you may want record a "proper"
resolution, usually a mixture of A and B. This will then typically
conflict with C.

That said, there is a problem here. To arrive at the default resolution
(revert the conflicting prim patches) you add inverse patches to the
repo. But what does "adding a patch to a repo" mean, precisely, if
inverses are involved? Is a repo still a sequence of patches? Is A;A^;A
the same as A? That would be bad because resolving a conflict would then
be the same as obliterating the conflicting patches. So inverse pairs
cannot simply be cancelled.

> I hope there's another way to solve it, or that my idea above turns
> out not to be as bad as I thought, or it turns out this new problem
> isn't really a problem after all.

I think the real problem is to define what a repository is and whether
inverted patches can or should be part of a repository.

Cheers
Ben