Conegation rewriting
category theory
logic
rewriting
Abstract
Rewriting theory studies rules for turning things into other things. Typically, one considers various types of graph, and looks at rewriting rules that have a form like this: “whenever you see a subgraph shaped like I, replace it with one shaped like O, using the common subgraph K to attach it”. It turns out that this informally-sketched procedure is somewhat ambiguous, and rewriting theorists have developed a few different ways of resolving the edges cases. In this post, I’ll briefly sketch this picture, and introduce a new type of graph rewriting: “conegation rewriting”.
Rewriting theory studies rules for turning things into other things. Typically, one considers various types of graph, and looks at rewriting rules that have a form as follows: “whenever you see a subgraph shaped like I, replace it with one shaped like O, using the common subgraph K to attach it”. It turns out that this informally-sketched procedure is somewhat ambiguous, but rewriting theorists have developed a few different ways of resolving the edge cases. In this post, I’ll briefly sketch this picture, and introduce a new type of graph rewriting: conegation rewriting. The conegation (dual to the negation) of a subobject is a particular way of interpreting the idea “remove a subgraph shaped like I” from the above procedure, which turns out to be well-suited to rewriting.
The ideas in this post were developed in collaboration with David Spivak, who also taught me about the conegation procedure (although the terminology “conegation” is my own coinage).
1 Rewriting
A typical application of rewriting theory is in logic, where you might describe a logical system as a set of rewriting rules such that each of the rules preserve correctness of a logical sentence — then a proof is exactly a list of applications of the rules which transform some sort of trivial sentence into the desired statement. Similarly, you might think of the axioms of e.g. a compact monoidal category as a set of rewriting rules on string diagrams, which you can use to prove identities for compact categories.
It’s common in the study of rewriting theory to use category theory to study rewriting systems more generically — allowing you to speak about rewriting on strings of symbols, on string diagrams, or on something else.1
A rewriting rule in a category \mathcal{C} is simply a span I \leftarrow K \to O of objects in \mathcal{C}. We call I the input, K the context, and O the output. The idea is that whenever we see a copy of I “inside” an object G, we want to replace is with the object O. The context K tells us something about how I is supposed to be “attached” to the rest of G, and we want to use this information to attach O.
There are a few different ways to actually interpret such a rule. The simplest is double-pushout rewriting (or “DPO” for short). Given a rule, we can rewrite G into G' if we can find a diagram like so:
\begin{CD} I @<<< K @>>> O \\@VVV @VVV @VVV \\G @<<< \bar{G} @>>> G' \end{CD}
where both squares are pushouts. The arrows K \to \bar{G} \to G are called a pushout complement to K \to I \to G.
The existence of the left-hand pushout square requires, informally, that G can be viewed as some object \bar{G} which contains K, with I attached to K. Then to compute the rewritten object, we attach O instead.
Pushout complements are a little weird from the point of view of category theory. For example, they’re not characterized by a universal property, so there doesn’t seem to be any reason they should even be unique. And in fact, pushout complements are not in general unique2. However, for a certain nice class of categories called adhesive categories, they are. A category is adhesive if - It admits pullbacks and pushouts of monomorphisms - Any pushout of a monomorphism is also a pullback, and these are stable under pullback.
(Note that there are many other equivalent definitions out there). Any topos is adhesive, which covers the category of graphs we’ll be concerned with in this post, as well as many other categories of interest. I won’t go into a detailed study of adhesive categories here, but I will just note the properties I need as they come up.
Another version of rewriting is called single-pushout rewriting (SPO). Here we interpret a rule as a single morphism in the category \mathsf{Par}(\mathcal{C}) of partial maps in \mathcal{C}, where a partial map is a(n equivalence class of) span(s) A \hookleftarrow U \to B, where the left leg is a monomorphism. Then we can ask for a pushout in \mathsf{Par}(\mathcal{C}) of the rule and the map I \to G. Since
- In adhesive categories, a pushout of ordinary maps is also a pushout in \mathsf{Par}(\mathcal{C})
- Any pushout complement to a monomorphism is a pushout diagram in \mathsf{Par}(\mathcal{C}),
it follows that any DPO rewrite is a valid SPO rewrite, but there may exist a pushout in \mathsf{Par}(\mathcal{C}) even if the pushout complement does not exist.
In between these is so-called sesqui-pushout (SqPO) rewriting (“sesqui-” means “one-and-a-half”, meaning it’s in between single and double). Since any pushout complement is also a pullback complement, perhaps looking at pullback complements can give us a useful notion of rewriting?
The notion people came up with is called a final pullback complement (FPC). This is slightly complicated to define explicitly, although as you might expect it boils down to receiving a unique map from every pullback complement in a certain sense. A slick way to define it is to say that, when K \to I is a monomorphism, an FPC is exactly a pushout of the two maps I \to G, I \to K in the category of partial maps.
This obviously implies that, if a pushout complement exists, it’s the final pullback complement as well, so any DPO rewrite is also a SqPO rewrite. Since pushouts compose, we can see that any diagram like the above where the left square is a FPC and the right square is pushout, is a pushout diagram in \mathsf{Par}(\mathcal{C}) — hence any SqPO rewrite is also a SPO rewrite.
Finally, to give an idea of the flavor of the relationship between final pullback complements and pushout complements: for the category of graphs we’ll consider here, it’s known that the final pullback complement U of K \hookrightarrow I \hookrightarrow G is given by deleting the vertices and edges that are in I but not in K from G, then also deleting any edges which are now missing one of their endpoints3. This is a pushout complement if and only if there are no extra edges that have to be deleted in the final step.
2 Conegations
The basic idea that the various notions of rewriting try to capture is: “delete the stuff that’s in I but not in K, then add the stuff from O”. They all agree that “add the stuff from O” should be interpreted as a pushout, but vary in their interpretation of “delete the stuff that’s in I but not in K”. I’m about to explain my new interpretation of this, but first we need to do a small amount of legwork.
In any lattice, we can ask for a negation of an element a, which is the largest element with the property a \wedge \neg a = \bot. If furthermore a \vee \neg a = \top, we call it a complement, and if all elements have complements we say the lattice is a boolean algebra, or that we’re working with classical logic — you’ll recognize the above formula as the law of excluded middle.
However, if we’re not in a Boolean algebra, we can also ask for something else, namely the smallest element \sim a such that a \vee \sim a = \top. This could be called the conegation of a.
An example is the lattice of closed sets in a toplogical space. Here there is no negation in general, but the conegation of any closed set is the closure of its complement. The set a \wedge \sim a is the boundary of a, which is only empty if a is also open. (This is dual to the lattice of open sets, which is a typical case of a lattice with negations where LEM doesn’t hold).
The family of examples we’re gonna be interested today is that of subobject lattices of presheaf topoi. Start with a (small) category \mathcal{C} and consider the category of functors \mathcal{C} \to \mathcal{Set} . This is a presheaf topos. All topoi have various very nice properties — among others, the poset of subobjects Sub(X) for c \in \mathcal{C} is always a Heyting algebra, and in particular has negations. For a presheaf topos, however, the situation is even nicer, because the subobject lattice also has conegations. For U \subset X a subfunctor, the negation is given by (\neg U)(c) = \{x \in X(c) \mid X(f)(x) \notin U(c') \forall f: c \to c' \in \mathcal{C}\}. Another way to state this is that \neg U is the largest subfunctor contained in the set difference X(c) \setminus U(c). On the other hand, the conegation is given by (\sum U)(c) = \{X(f)(x) \mid x \notin U(c'), f: c' \to c \in \mathcal{C}\}. This is the smallest subfunctor containing the set differences X(c) \setminus U(c).
2.1 Example: Graphs
Consider the category \mathcal{G} which has two objects E and V, and two nonidentity morphisms s,t: E \to V. A presheaf G: \mathcal{G} \to Set is a type of graph: G(V) is the set of vertices, G(E) is the set of edges, and G(s),G(t) pick out the source and target vertex of each edge. This type of graph has only directed edges, and allows multiple edges and self-edges. It’s sometimes called a quiver. We simply write \mathbf{Gph} for the category of graphs. Since it’s a presheaf topos, we can apply the above theory to it.
Consider the above picture. It depicts a graph G with a subgraph U picked out by the dashed outline. The negation \neg U consists of everything in the complement of U, except for those things which “see” something inside U. The edges that cross the boundary are in the complement of U, but since their source happens to be inside U, they are not in \neg U — if they were included, it wouldn’t be a functor!
In the bottom left we see the conegation \sim U. Here we include those edges, which means we must include everything they “see” inside U — in this case, the second vertex.
3 Conegation rewriting
With that done, we can define conegation rewriting as follows. Given a span I \hookleftarrow K \to O, and a map f: I \to G, the conegation rewrite is the following pushout:
\begin{CD} K @>>> O \\@VVV @VVV \\\sim f(I) \cup f(K) @>>> (\sim f(I) \cup f(K)) +_K O \end{CD}
where f(I) and f(K) denote the images of I and K under f, and where the union and the conegation are computed in the subobject lattice of G.
If you think of \sim U as meaning “everything not in U”, then this is a pretty straightforward interpretation of “everything not in I, and also the stuff in K”, which after all is what we’re trying to get at. The question you might have here is why I went to so much trouble to introduce the conegation instead of just using the negation. The answer is that \neg I \cup K does not include edges that connect a vertex in K to a vertex outside I. Since such an edge has a vertex in K and hence in I, it can’t be included in \neg I, but since it also has a vertex outside I, it can’t be in K either. Hence such edges are always deleted when passing to \neg I \cup K. This means that a rewrite using this formula always disconnects K entirely from the rest of the graph before replacing it with O. This is clearly not the right behaviour.
Since all the previous notions of rewriting agree in the case where a pushout complement exists, and only disagree about how to handle the exceptions, we might hope that our notion has this property as well. And indeed it does:
Proof. We’ll need the following property of adhesive categories: if a pushout complement of K \hookrightarrow I \overset{f}{\to} G exists, it’s necessarily given by \forall_f K. Here as usual \forall_f denotes “universal quantification”, i.e the right adjoint to pullback along f. Note that it’s not the claim that this right adjoint always exists in an adhesive category, or that if it exists, it’s always a pushout complement. Only that if a pushout complement exists, then it has the universal property of \forall_f. A proof of this can be found in [Behr 2019].
We first show \sim f(I), f(K) \subset U. It’s clear the f(K) \subset U, since the map from K to G factors over U by assumption. To show \sim f(I) \subset U, using the universal property of \sim I, it suffices to observe that U \cup f(I) = G, which follows since pushouts can be computed object-wise in a presheaf topos, and clearly on the level of sets each element in the pushout comes either from U or from I.
Hence \sim f(I) \cup f(K) \subset U.
To show the other inclusion, we note that f^*U \subset K, by the universal property of U. Hence f(f^*U)) \subset f(K), and so f(f^*(U)) \cup \sim f(I) \subset f(K) \cup \sim f(I). Since \sim f(I) contains every element not in the image of f, clearly f(f^*(U)) \cup \sim f(I) must contain U, so we get U \subset f(K) \cup \sim f(I) as desired.
(Note that this theorem fails if we use \neg f(I) instead)
In the specific case of matches where I \to G is a monomorphism, we can easily check if this is in fact a pushout
Proof. By using once again the fact that pushouts are objectwise, we see that a diagram of monomorphisms is a pushout if and only if it’s a pullback, i.e if K = I \cap (\sim I \cup K), which clearly holds if and only if K contains I \cap \sim I.
In the general case we would need a more complicated condition asserting that the map f: I \to G is injective except on elements in K.
In light of the theorem, we can describe the difference between DPO, SqPO, and “conegation” rewriting as follows: DPO rewriting requires that, whenever the rewrite rule wants to delete a vertex (i.e it’s in I and not in K), all its edges are also in I (and therefore not in K, or the vertex would also be in K); SqPO allows us to delete a vertex without explicitly deleting its edges, and in this case we simply also delete the edges; finally, conegation rewriting also allows a rewrite to happen in this case, but resolves the conflict by not deleting the vertex.
I want to conjecture that the final pullback complement can be characterized as the implication I \Rightarrow K. This is the largest subobject such that (I \Rightarrow K) \cap I \leq K. Note that conjunction of subobjects is pullback, and “largest” is the same thing as “final” (i.e. terminal), so this conjecture seems pretty plausible, but I haven’t verified it. In a Boolean topos, I \Rightarrow K. is equivalent to \neg I \cup K = \sim I \cup K, which is another point of comparison between these two variants of rewriting.
Footnotes
See Span Rewriting on nLab for more on this, as well as a number of references.↩︎
An easy way to see this is that, if they were, pullback complements would also be unique by duality. But the string \emptyset \to \{1\} \to \{1,2\} in \mathsf{Set} admits the two pullback complements \{2\} \to \{1,2\} and \emptyset \to \{1,2\} (and many others).↩︎
See [Behr 2019], Lemma A.4↩︎