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

[Ben Franksen]

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

Cheers
Ben