How to prove equations using diagrams, part 2

Weak equivalence and E-diagrams

This is the second part in a series about diagrammatic reasoning, inspired by e-graphs. Last time, we reviewed the concept of initial functor and showed by example how to calculate with diagrams and initial functors. This time, we make that calculus more systematic and we reconceive e-graphs in terms of initial functors.

1 Weak equivalence of diagrams

We’ve been deriving equations by chaining together initial functors between diagrams, going in either direction. Let’s give a name to this equivalence relation on diagrams.

Definition 1 A weak equivalence from a diagram D: \mathsf{J} \to \mathsf{C} to another diagram D': \mathsf{J}' \to \mathsf{C} is an initial functor R: \mathsf{J} \twoheadrightarrow \mathsf{J}' making the triangle commute:

Two diagrams in a category are said to be weakly equivalent if they can be connected by a zig-zag of weak equivalences.

Why call this relation weak equivalence? First, it is not equivalence in any familiar 2-category of diagrams. Moreover, though initial functors are closed under composition and any isomorphism of categories is initial, as follows directly from the definition, initial functors are most interesting when they’re not invertible. So, in order to make weak equivalence be an equivalence relation, we have to consider zig-zags of initial functors.¹

Weak equivalence versus commutativity

By definition, weak equivalence of diagrams preserves limits whenever they exist. Sometimes this property can be used to extract commutation relations from diagrams, as we saw last time. However, we caution that weak equivalence does not preserve commutativity:² if a commutative diagram D is weakly equivalent to another diagram D', it need not be the case that D' commutes.

The following weak equivalence of diagrams is a minimal counterexample.

The functor shown is initial because the limit of both diagrams is the equalizer of g \circ f and h \circ f, whenever it exists. However, if we suppose that

g \circ f = h \circ f \qquad\text{but}\qquad g \neq h,

so that limit of both diagrams is X, then the first diagram commutes but the second does not.

It can be a useful feature of weak equivalence that it works just as well regardless of whether the diagrams involved commute. As it happens, I first got into this topic by studying “Tonti diagrams,” which present partial differential equations in physics (Patterson et al. 2023). These diagrams do not commute; if they did, the equations would already be solved!

2 E-diagrams

We now attempt to make contact with e-graphs. That’s less straightforward than it might seem since, taken at face value, the concrete descriptions of e-graphs offered by Nelson (1980; see also Detlefs, Nelson, and Saxe 2005, sec. 4.2) and by Willsey et al. (2021, sec. 2.1) look rather different. We reproduce features of both without claiming to be fully faithful to either.

Definition 2 An e-diagram over a diagram D: \mathsf{J} \to \mathsf{C} is a factorization of D through an initial functor, comprising a category \mathsf{H}, an initial functor E: \mathsf{J} \twoheadrightarrow\mathsf{H}, and a diagram P: \mathsf{H} \to \mathsf{C} such that D = P \circ E.

The pieces constituting an e-diagram have interpretations in e-graph jargon:

• The target category \mathsf{C} is a theory, most clearly when \mathsf{C} is finitely presented, so that its generating graph is a signature, defining types and (unary) operations, and its path equations are equational axioms.
• The diagram D: \mathsf{J} \to \mathsf{C} is a term graph in the theory \mathsf{C}, particularly when the indexing category \mathsf{J} is freely generated by a finite graph. The objects of \mathsf{J} are e-class IDs.
• The category \mathsf{H} is something like a hash cons. Its objects are canonical e-class IDs.³ Below, we give conditions on the functor P: \mathsf{H} \to \mathsf{C} that make the morphisms of \mathsf{H} encode the mapping of a hash cons.
• As for the functor E: \mathsf{J} \twoheadrightarrow\mathsf{H}, the object map \mathop{\mathrm{Ob}}E: \mathop{\mathrm{Ob}} \mathsf{J} \to \mathop{\mathrm{Ob}}\mathsf{H} assigns each e-class ID to a canonical e-class ID, like in a union-find, while the morphism map just exists to witness the initiality of E.

We now define the category of all e-diagrams over a diagram.

Definition 3 A morphism of e-diagrams (\mathsf{H}, E, P) \to (\mathsf{H}', E', P') over a common diagram D: \mathsf{J} \to \mathsf{C} is a functor R: \mathsf{H} \to \mathsf{H}' making the two triangles commute:

We do not assume that the functor R is initial but, as we will see shortly, a cancellation property of initial functors ensures that R is automatically initial. So there is not actually a choice to make.

In other words, the category of e-diagrams over a diagram D is the full subcategory of the factorization category of D spanned by factorizations whose left component is initial. The factorization category construction goes back at least to Lawvere (1986).

3 The trivial e-diagram

Any diagram D: \mathsf{J} \to \mathsf{C} trivially has an e-diagram over it, given by the factorization (1_\mathsf{J}, D). This e-diagram is initial in the category of e-diagrams over D:

The terminology is apt because the initial e-diagram is, in practice, how an e-diagram will be initialized from an existing diagram (term graph).

4 The ideal e-diagram

What is not so obvious is that the category of e-diagrams over a fixed diagram also has a terminal object. This follows from the foundational theorem by Street and Walters (1973) that initial functors form the left class of morphisms in an orthogonal factorization system (OFS) on \mathsf{Cat}, called the comprehensive factorization system.

Theorem 1 (Comprehensive factorization) Initial functors and discrete opfibrations form the left and right classes, respectively, of an orthogonal factorization system on \mathsf{Cat}. Thus, any functor F: \mathsf{C} \to \mathsf{D} admits a factorization \mathsf{C} \twoheadrightarrow\mathsf{E} \rightarrowtail\mathsf{D} as initial functor followed by a discrete opfibration, and this factorization is unique up to unique isomorphism.

Recall that a functor P: \mathsf{E} \to \mathsf{C} is a discrete opfibration, here denoted⁴ P: \mathsf{E} \rightarrowtail \mathsf{C}, if, for every morphism f: X \to Y in \mathsf{C} and every object x \in \mathsf{E} with P(x) = X, there exists a unique morphism \bar f: x \to y in \mathsf{E} such that P(\bar f) = f.

The existence of the comprehensive factorization system is a powerful result with many consequences, such as:

• the cancellation property of the left class in an OFS implies that any functor R: \mathsf{H} \to \mathsf{H}' constituting a morphism of e-diagrams is initial, as noted above;
• a closure property of the left class states that initial functors are stable under pushout, as used below.

Moreover, comprehensive factorization implies that the factorization of a diagram D: \mathsf{J} \to \mathsf{C} as an initial functor \mathsf{E}_*: \mathsf{J} \twoheadrightarrow\mathsf{H}_* followed by a discrete opfibration P_*: \mathsf{H}_* \rightarrowtail \mathsf{C} is terminal in the category of e-diagrams over D:

The existence and uniqueness of a functor R filling the square is a direct application of initial functors being left orthogonal with respect to discrete opfibrations.

The e-diagram produced by comprehensive factorization is ideal in the sense that the “hash cons invariant” (Willsey et al. 2021, Definition 2.7) is satisfied for any canonical e-node that can be formed. Rephrased in e-graph jargon, the functor P_*: \mathsf{H}_* \rightarrowtail\mathsf{C} being a discrete opfibration says that for every canonical e-class ID x \in \mathsf{H}_* and every operation f: X \to Y in \mathsf{C} with domain X = P_*(x)—that is, for every canonical e-node “f(x)”—there exists a unique lift of f through P_* to a morphism \bar f: x \to y. The codomain y = \operatorname{cod}(\bar f) of this unique lift is the canonical e-class ID associated with the canonical e-node “f(x)”. Thus, in the ideal e-diagram, the relation from canonical e-nodes to canonical e-class IDs is a function, and evaluating this function decides whether canonical e-nodes are equivalent.

So, is the ideal e-diagram the only e-diagram we’ll ever need? No, because in general it cannot be computed. As we’ll have occasion to study in a future post, the comprehensive factorization of a functor F: \mathsf{C} \to \mathsf{D} is constructed by left Kan extending the terminal copresheaf on \mathsf{C} along F. Left Kan extensions generally cannot be computed, for two reasons. First, even when all the input data is finite, the output may be infinite. Second, even when the output is finite, it still might not be possible to compute it. Left Kan extension is formally uncomputable: it includes solving the word problem for categories, hence also the word problem for groups, an early and famous undecidable problem. Thus, to suggest that comprehensive factorization or left Kan extension “solves” the problem of reasoning with e-graphs would be entirely backward; rather, it is because left Kan extension is uncomputable that we need a flexible e-graph data structure supporting a variety of reasoning heuristics.⁵ Iteratively approximating a left Kan extension is just one important application of e-graphs.

5 Rewriting e-diagrams

Having codified the objects of interest as e-diagrams, we turn to manipulating e-diagrams using the formalism of pushout-based rewriting. The goal is to show that calculations similar to last time’s can be carried out by applying rewrite rules, where each rule application is guaranteed to preserve weak equivalence of diagrams. Note that this scheme is not intended as a guide to implementation. Though e-graphs can be implemented using rewriting techniques, it should likely not be in terms of initial functors between categories. Rather, having proved the procedure correct, we can forget about initiality and compile to rewrite rules operating directly on the graphs generating the diagram shapes. As a proof of concept, my colleague Kris Brown has implemented e-graphs using hypergraph rewriting (Brown 2025).

Rewrites of an e-diagram \mathsf{J} \twoheadrightarrow\mathsf{H} \to \mathsf{C} may affect just the category \mathsf{H} or both \mathsf{J} and \mathsf{H}. Below we imagine that the “term graph” \mathsf{J} only ever grows by introducing new terms, whereas the “hash cons” \mathsf{H} is also reduced through equation introduction and congruence closure. Other schemes are also possible.

5.1 Rewriting over a fixed diagram

The simplest rewrites change the e-diagram (\mathsf{H}, E, P) without changing the diagram D: \mathsf{J} \to \mathsf{C} it is over. Given a rewrite rule of the form

along with a match of its left-hand side, namely any map \mathsf{L} \to \mathsf{H} in \mathsf{Cat}/\mathsf{C}, we take a pushout

to obtain a new e-diagram (\mathsf{H}', E', P') over D. We use the fact that initial functors are stable under pushout.

Rule: congruence reduction

Each morphism f: X \to Y in \mathsf{C} generates a rewrite rule

that can be applied in this fashion to perform congruence reduction in \mathsf{H}.

Rule: equation introduction

Any path equation in \mathsf{C}, say g \circ f = k \circ h, generates a rewrite rule

where the checkmark indicates that the square in the indexing category itself commutes. Thus, at the expense of using diagram shapes that are not free, we can apply an equation in \mathsf{C} using a single initial functor, rather than a span of initial functors as in previous post.

5.2 Rewriting the diagram itself

Given a rewrite rule R: \mathsf{L} \twoheadrightarrow\mathsf{R} in \mathsf{Cat}/\mathsf{C} as above along with a match \mathsf{L} \to \mathsf{J}, now in \mathsf{J}, we produce a compatible match in \mathsf{H} by post-composing with E: \mathsf{J} \twoheadrightarrow \mathsf{H}. We then apply the rule along both matches by taking two pushouts, which the pasting law for pushout squares allows us to express as:

The result is a new e-diagram (\mathsf{H}', E', P') over the new diagram D' \coloneqq P' \circ E' and, by construction, D' is weakly equivalent to the original diagram D = P \circ E. Again, we use that initial functors are stable under pushout.

Rule: term introduction

Each morphism f: X \to Y in \mathsf{C} generates a rewrite rule

\big\{ X \big\} \quad\twoheadrightarrow\quad \left\{ X \xrightarrow{f} Y \right\}

that can be applied as above to introduce a new term in both \mathsf{J} and \mathsf{H}.

6 Outlook

In this second post on diagrammatic reasoning, we filled in aspects of the formalism neglected in the first post, proposing a definition of e-diagram and showing how to rewrite e-diagrams by applying rules in the form of initial functor motifs. While this is all “just” formalism, with the key ideas already present in the examples and calculations from last time, it has been a good excuse to review the comprehensive factorization system on \mathsf{Cat}, a powerful theorem that, among other consequences, points to the ideal object of e-graph computation.

Having set out the basic formalism, we are now free to embelish it by considering categories with extra structure. Next time we’ll study diagrams and initial functors for categories with finite products, recovering the standard setting of e-graphs that allows constants and operations of arity greater than one. More ambitiously, in future posts, we hope to show the benefits of a clean categorical semantics by generalizing to new settings where e-graphs are not standardly applied.

7 References

Brown, Kris. 2025. “CSetEGraphs.jl.” https://github.com/kris-brown/CSetEGraphs.jl.

Carlson, Kevin, James Fairbanks, Tim Hosgood, and Evan Patterson. 2024. “The Diagrammatic Presentation of Equations in Categories.” https://arxiv.org/abs/2401.09751.

Detlefs, David, Greg Nelson, and James B. Saxe. 2005. “Simplify: A Theorem Prover for Program Checking.” Journal of the ACM 52 (3): 365–473. https://doi.org/10.1145/1066100.1066102.

Lawvere, F. William. 1986. “State Categories and Response Functors.” https://github.com/mattearnshaw/lawvere/blob/master/pdfs/1986-state-categories-and-response-functors.pdf.

Nelson, Greg. 1980. “Techniques for Program Verification.” PhD thesis, Stanford University.

Patterson, Evan, Andrew Baas, Timothy Hosgood, and James Fairbanks. 2023. “A Diagrammatic View of Differential Equations in Physics.” Mathematics in Engineering 5 (2): 1–59. https://doi.org/10.3934/mine.2023036.

Street, Ross, and R. F. C. Walters. 1973. “The Comprehensive Factorization of a Functor.” Bulletin of the American Mathematical Society 79 (5): 936–41. https://doi.org/10.1090/S0002-9904-1973-13268-9.

Willsey, Max, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. “Egg: Fast and Extensible Equality Saturation.” Proceedings of the ACM on Programming Languages 5 (POPL): 1–29. https://doi.org/10.1145/3434304.

Footnotes

1. Instead of passing to a mere relation of weak equivalence, which forgets how two diagrams are weakly equivalent, the believing structuralist would rather localize at the initial functors, formally inverting that class of morphisms within the category of diagrams. In a paper led by Kevin Carlson (Carlson et al. 2024), we proved that localizing at initial functors is equivalent to localizing at the largest class of diagram morphisms that preserve solutions to equations (lifts against any discrete opfibration). This justifies defining weak equivalences of diagrams to be initial functors.

2. Recall from the first post that a diagram commutes if, for every pair of parallel morphisms in the diagram’s shape, their images in the target category are equal.

3. Calling a chosen representative of an equivalence class “canonical” is traditional in computer science but should not be confused with “canonical” as a term of art in mathematics. Far from being mathematically canonical, the choice of elements to play the role of canonical e-class IDs is completely arbitrary. In a union-find data structure, the canonical IDs are usually taken to be a subset of the set of all IDs—a set-theoretic distinction meaningless in structuralist mathematics. What is canonical is the ideal e-diagram introduced later, since it is unique up to unique isomorphism.

4. Writing initial functors with “\twoheadrightarrow” arrows and discrete opfibrations with “\rightarrowtail” arrows calls to mind the ur-example of a factorization system, the epi-mono factorization in \mathsf{Set}. However, the analogy runs deeper than that: the comprehensive factorization in \mathsf{Cat} categorifies the epi-mono factorization in \mathsf{Set}. A discrete opfibration (as well as a discrete fibration) is a map into a 1-category whose fibers are 0-categories, i.e., sets, while an injection is a map into a 0-category whose fibers are (-1)-categories, i.e., propositions. Moreover, an initial functor is a functor R: \mathsf{J} \to \mathsf{K} such that each comma category (“lax pullback”) R/k is non-empty and connected, while a surjection is a function R: J \to K such that each pullback R \times_K k is nonempty. I thank David Jaz Myers for pointing out this analogy to me.

5. In the e-graph engine egglog, these heuristics take of the form of schedules for applying rewrite rules.