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

[Ben Franksen]

Am 08.09.20 um 17:29 schrieb James Cook:
> On Thu, 3 Sep 2020 at 14:24, Ben Franksen <ben.franksen at online.de> wrote:
>>
>>>>> If I wanted to implement it, I think it would just become this:
>>>>>
>>>>> * A repository consists of two things:
>>>>>   * A sequence S of primitive patches with distinct names, starting at
>>>>> O, with no inverses (i.e. only positive names).
>>>>>   * A set of names, called "tombstones", representing "deleted"
>>>>> patches. These names don't appear in S.
>>>>
>>>> The problem I see here is that this looses the start (or ending) state
>>>> of the "deleted" patches. And you don't even remember their content,
>>>> just their name. But even supposing you remember a start state and the
>>>> patch representation of every deleted patch, this will still mess up
>>>> your commutation. Because deleting inverse pairs AA^ from the main
>>>> sequence basically means the same as stating that such a pair commutes
>>>> with any other patch, which is clearly wrong
>>>
>>> Yes, I forgot that the repo needs to remember the content of those
>>> "deleted" patches. E.g. someone might later obliterate A^, or someone
>>> might want to pull A and not A^ to another repo; or someone might
>>> simply want to see the content of A and A^ in the output of "darcs
>>> changes -v". So, tombstones as names only clearly isn't enough.
>>>
>>> I'm a bit fuzzy about the problem with commutation that you raise.
>>> Yes, one way to delete AA^ would be to commute them all the way to the
>>> end of the sequence and then drop them. But what would go wrong if we
>>> simply declare that whenever you have a sequence B;A;A^;C you're free
>>> to simply replace it with B;C (and vice versa) as an operation
>>> distinct from commuting?
>>
>> Well, if you allow to replace parts of a sequence, then this means that
>> for the purpose of your theory you regard the two versions of the
>> sequence as equivalent. But this works out only if you can prove that
>> the equivalence is structure preserving.
>>
>> Take the integers Z as an example, and for some fixed positive integer
>> p, define n ~ m iff n%p = m%p ('%' means modulo; so this tells us that
>> we can "drop" multiples of p from any number). This equivalence
>> preserves the arithmetic structure, which is why we can regard Z_p as a
>> Ring by doing the arithmetic on an arbitrary representative of the
>> equivalence class. But it does not preserve the order structure of the
>> integers.
>>
>> In your case, for two adjacent /sequences/ A;B, and equivalences A~A',
>> B~B', we need to have that A;B commutes iff A';B' commutes. Now, suppose
>> you have patches a;b;b^;c, where none of the adjacent pairs commute.
>> You'd have to show that this implies that a;c commutes neither (taking
>> e.g. A=[a] and B=[b;b^;c]). But you can't, since it is not true. A
>> counter example consists of 3 hunks a, b, c, where a and b overlap, b
>> and c overlap, but a and c do not overlap. More concretely, take the
>> initial state as file f=[1,2,3] and
>>
>>   a=hunk f 1 [1] [1a]
>>   b=hunk f 1 [1,2,3] [1b,2b,3b]
>>   c=hunk f 3 [3] [3c]
> 
> I'm still not sure I understand the problem. I agree that in your
> example, it's possible to commute [a] with [c] but not [a] with
> [b;b^;c]. But it is possible to "rearrange" a;b;b^;c into b;b^;c;a if
> "rearrange" is defined broadly enough to allow the following three
> steps: a;b;b^;c -> a;c -> c;a -> b;b^;c;a.

Commutation means that we may have to re-arrange the /content/ of the
patches we commute, such that they make sense in their new context. You
abstracted that part away here. If we re-add it, the sequence becomes:

  a;b;b^;c -> a;c -> c';a' -> b';b'^;c';a'

But what is the new b'? It should be clear that, in general, it cannot
be the same as b: if b depends on a (which is what we assumed), then
that means that b makes no sense without having a before it.

Take the above three hunk patches and tell me how b' should be defined
such that the resulting sequence b';b'^;c';a' makes sense.

Cheers
Ben