Re: How to extend a patch theory to fully commute
Ben Franksen <[email protected]> Thu, 2 Jul 2020 09:53:17 +0200
| Newsgroups | gmane.comp.version-control.darcs.user |
|---|---|
| Message-ID | <[email protected]> |
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