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

Ben Franksen ben.franksen at online.de
Thu Jul 2 07:53:17 UTC 2020


Am 02.07.20 um 00:37 schrieb James Cook:
>> The construction works by inductively taking any pair of incommutable
>> patches (in sequence, i.e. with a common middle state) and then
>> "formally" commuting it. The new node is represented as that pair of
>> patches. Is that, essentially, the idea?
> 
> Sorry, I should add one note here: I'm not sure it's accurate to say
> the construction "inductively" makes pairs of incommutable patches
> commute. That sounds like you're saying everything's built out of
> transpositions. Maybe there's some equivalent formulation that works
> that way, but e.g. if you want to commute A;B;C to C;B;A there's
> nothing in my construction that says it's done one transposition at a
> time. Instead, you identify each patch in the sequence C;B;A with a
> "patch address", then simplify that patch address as much as you can.

I see. But if you can prove permutivity (and from skimming through to
the end of your story it loks like you can) then it should be possible
to arrive at the same result(s) by doing it one transposition at a time.

That is, we start with A;B;C, then first commute B;C to C';B', then A;C'
to C'';A'. The result C'';A';B' should be the same as if we do it in one
stroke and simplify as in the definition.

It could very well be that your approach is more efficient. Your proofs
are surprisingly short which suggests that your "global" approach to
commutation (define it immediately for sequences instead of first for
pairs and then generalize inductively) has some advantages.

But first I'll have to understand how extended patches commute in your
theory and I still haven't come that far.

Cheers
Ben



More information about the darcs-users mailing list