Re: How to extend a patch theory to fully commute

Am 06.07.20 um 19:37 schrieb James Cook:
> On Mon, 6 Jul 2020 at 10:29, Ben Franksen <[email protected]> wrote:
>> 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!
> 
> Yes, I should have been more careful about what can commute past what.
> The email I sent just now suggests you can commute any two cycles;
> maybe that's enough.
> 
> Also, thanks for the reference to groupoids. I have been wondering how
> to think about a primitive patch theory and just had a vague sense
> it's sort of like a category.

For a category you need composition and identities. Patches themselves
have neither so they do not form a category. But patch /sequences/ do.
(This is well-known construction: the category of all paths in a
directed graph, there's a name for that but I forgot it.)

If you add inverses and allow them to cancel in a sequence, then this
becomes a groupoid. But remember that we must not allow cancellation of
inverses for repositories, or in general for sequences involving
conflicted merges. So unfortunately groupoids can serve as a framework
only for primitive patches.

For extended patches we need something weaker; I am currently exploring
if perhaps inverse categories fit the bill. (I haven't found much
literature on inverse categories, though.)

Cheers
Ben