PROPs and patches

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 [tex]D_n[/tex] the set of all lists of length [tex]n[/tex], and we'll set [tex]P_n^m[/tex] 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 [tex]\circ_i:P_n^m\times P_r^s\to P_n^{m+s-r}[/tex] 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.

social