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

[Ben Franksen]

Am 18.08.20 um 22:42 schrieb James Cook:
> Okay, I wrote something up: https://www.falsifian.org/a/xxOw/misc.pdf

I like it. Especially the part where you define commutation in terms of
the balance-respecting property. This is very elegant. It confirms what
I have long since suspected, namely that the whole theory becomes
simpler and more regular if we concentrate on patch /sequences/ instead
of individual patches.

The fact that your patches have no "content" is of of course a result of
starting out with "enriched" contexts. As you note in 2.2
Interpretation, your contexts can *not* in general be understood simply
as "working tree states": the mapping from contexts to states is not
injective. It is not yet clear to me if that will have consequences when
it comes to implementing your theory.

One a minor note, your patch universe definition is not suitable for
extended patches as defined in Darcs: For these, the square commute law
(which you call rotation, perhaps a better name) does not hold. Though
to be fair, a while ago we have stopped treating them as invertible in
the first place, so nowadays we couldn't even /state/ that property for
them. (This remark is largely irrelevant for your theory.)

I'll comment on the new context address definition in another message.

Cheers
Ben