Brent Yorgey wrote a post on using category theory to formalize patch theory. In the middle of it, he talks about the need to commute a patch to the end of a patch series, in order to apply a patch undoing it. He suggests a necessary condition to do this is that, given patches P and Q, we need to be able to find patches Q’ and P’ such that PQ=Q’P', and preferably such that Q’ and P’ capture some of the info in P and Q.

However, as such, this is not enough to solve the issue. For one thing, we can set Q’=P and P’=Q, and things are the way he asks for.

Now, I wonder whether we can solve this by using PROPs (or possibly di-operads or something like that). Let’s represent a document as a list of some sort of tokens. We’ll set the set of all lists of length , and we’ll set to denote operations that take a list of length n and returns a list of length m.

One operation here is obvious – the identity operation. So we’ll take that into the mix. And we’ll also want to have some manner of composing operations. So, set to be the operation that applies the second argument to the elements i,i+1,…,i+m of the list outputted by the first argument.

This way, we can make patch trees – using the identities to fill out when a patch doesn’t influence everything; and have composition of operations represent composition of patches.

Now, the commutativity that Brent asks for would manifest as an additional relation – on top of those inherent in the definition of a PROP – to rebuild trees. One obvious one pops out immediately – as long as the trees don’t overlap, in other words, as long as the subtree we want to reorganize is contractible (in the topological sense), we can commute patches freely.

When trees -do- overlap, however, the undo operation Brent asks for is much more tricky. Consider the following sequence of edits:

[] -> [a] -> [b] -> [cbd]

Now, undo the insertion of [a].

Sure, taken this way, we cheat a little. Maybe we want to restrict edit descriptions to explicit deletions and additions. So we would have

[] -> [a] -> [] -> [b] -> [cb] -> [cbd]

and here we could probably move things around a bit easier. I don’t quite see how to do it, right now, though.

I think this highlights the point of the problem. What does it mean to undo []->[a] without also undoing [a]->[] ?

That is, perhaps the proper way to think about things is not in terms of insertions and deletions to a constant state, but rather to think in terms of reachability on a graph of edits. Thus, we have a graph from nil with a cycle to [a] and back before moving on to [b] and so forth. Now what does it mean to “remove [a]“? Rather than thinking of it as removing the arc from nil to [a], think of it as removing the [a] node itself.

Alternatively, consider the process of pushing A to the end of AA^-1BCD. Since AA^-1 = [], then AA^-1 = A^-1′A’ implies A^-1′A’ = []. There’s an abstruse study of strings with these sorts of “negative” letters in mathematics, though I forget the name it goes by.