Re: How to extend a patch theory to fully commute

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.

James