Re: How to extend a patch theory to fully commute

Am 05.07.20 um 20:36 schrieb Ben Franksen:
> Am 04.07.20 um 23:59 schrieb James Cook:
>>> I think that whenever a sequence of patches starts and ends at a
>>> primitive context (e.g. this is true of an unconflicted repository)
>>> you can re-order the patches so that they are all primitive.
>>
>> I should add: this probably requires allowing new permutations that
>> weren't in the primitive theory. E.g. you can commute anything past
>> A;A^, even if you couldn't in the primitive theory. This might mean
>> some algorithms need to be changed; hopefully these changes will not
>> make them less efficient.
> 
> You need to be very careful here. A commutes past B;B^ only if A at
> least commutes with B. Otherwise you move B to an invalid context in
> which it can no longer be applied.

To put this point in a wider perspective:

From the viewpoint of inverse semigroup theory, inverse pairs are
idempotent elements. While idempotents always commute with each other
(i.e. XX^YY^=YY^XX^ for all X,Y), it is not in general true that XX^Y=YXX^.

From the corresponding viewpoint of groupoid theory (which I prefer
because it is, more or less, a "statically typed" version of inverse
semigroups), for any X:x->x', XX^=id_x is the identity /at state x/. If
y is a different state and Y:x->y, then Y=XX^Y:x->y is well-typed, and
it is true that XX^YY^=YY^XX^:x->x. But the composition YXX^ is not
well-typed and thus undefined!

Cheers
Ben