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

[James Cook]

> 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.)

If you don't have inverses, you could replace the balance-respecting law with:

  If two patch sequences have the same name signature, then [the two
sequences have the same starting context] iff [the two sequences have
the same ending context].

I think some desirable properties will still hold, but I haven't
thought it through carefully. (Here, names don't have signs so a "name
signature" is just a multiset of names without signs.)

When I wrote the Latex write-up, I first tried to start with this
definition, and make addinv be an operation on patch universes: so,
you can start with a fully-functional patch universe without inverses,
then add inverses on top of it. Then I tried to prove the
balance-respecting property as a consequence, but realized it doesn't
follow. So I abandoned that approach. (I don't remember offhand why I
thought the balance-respecting property is important.)

James