Categorical E-Graphs for Lambda Calculi

Aleksei Tiurin; Dan R. Ghica; Nick Hu

REVIEW 5 major objections 8 minor 49 references

Categorical E-Graphs for Lambda Calculi

T0 review · 5 major / 8 minor · reviewed 2026-08-16 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper claims that equality saturation for lambda calculi can be carried out directly on hierarchical e-hypergraphs, where binding boxes and equivalence boxes are native and the symmetric monoidal equations are absorbed by the graph…

desk verdict The paper has a plausible and well-designed framework, but the main soundness/completeness theorem is not proved: the quotient by the structural rewrite rules is asserted, not shown to be a congruence. read the letter →

arxiv 2505.00807 v2 pith:3P44M2OT submitted 2025-05-01 cs.LO math.CT

Aleksei Tiurin , Dan R. Ghica , Nick Hu This is my paper · ORCID

classification cs.LOmath.CT MSC 18M0568Q4203B40

keywords equalitysaturatione-graphslambdacalculushierarchicalhypergraphsstringdiagramsdouble-pushoutrewritingclosedsymmetricmonoidalcategoriesvariablebinding

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Equality saturation is a rewriting technique that keeps all equivalent versions of a term around instead of destroying alternatives, but it has never sat comfortably with variable binding because alpha-equivalent terms do not share syntax. This paper tries to remove that obstacle by moving the whole construction one level up: e-graphs become morphisms of a free semilattice-enriched closed symmetric monoidal category, and lambda abstraction is represented by an explicit hierarchical box rather than by names or de Bruijn indices. The central claim is an if-and-only-if theorem: two closed terms are equal modulo the symmetric monoidal laws, the semilattice equations, and distributivity exactly when their renderings as hierarchical e-hypergraphs rewrite to one another through a concrete double-pushout rule system. A sympathetic reader would care because, if the theorem holds, equality saturation for functional programs no longer needs explicit substitutions and shifting operations as add-on bookkeeping; the categorical representation itself absorbs those equations.

What carries the argument

The central object is the hierarchical e-hypergraph: a monogamous directed acyclic hypergraph with ordered external and internal interfaces, whose edges are layered by two kinds of hierarchical boxes—e-boxes, which mark equivalence classes of subdiagrams, and $\lambda$-boxes, which mark abstractions with a dangling wire for the bound variable—together with predecessor relations that record nesting and a consistency relation that records which ports of a box belong to the same equivalence class. The rewrite mechanism is convex extended DPOI rewriting, whose boundary complements and convexity conditions ensure that deleting and inserting a rule occurrence keeps the graph monogamous, directed, acyclic, and well-typed. The machinery's job is absorption: the symmetric monoidal equations are baked into hypergraph isomorphism, while the rule schema $S$, quotiented into $\mathrm{MEHypI}(\Sigma)/S$, absorbs semilattice and distributivity equations, so the only rewrites left are user equations such as $\beta$-like rules.

What would settle it

One concrete test is to search for a counterexample to the unproved congruence property: find e-hypergraphs $G$, $H$, and $K$ such that $G$ rewrites to $H$ via schema $S$ but $G$ followed by, or tensored with, $K$ does not rewrite to $H$ followed by, or tensored with, $K$ by the same rule system. Such a pair would show that $\mathrm{MEHypI}(\Sigma)/S$ is not a category and that Proposition VI.7 fails. A smaller-scale check is to enumerate all closed $\Sigma^+$-terms of small depth over a one-object signature, test term equality in the theory, and verify that their e-hypergraph interpretations land in the same rewrite-connected component exactly when term equality holds.

Watch

Extended reading notes

Core claim

The paper's central discovery is that a free closed symmetric monoidal category enriched in semilattices has exactly the structure needed to make e-graphs with bindings. Writing terms as string diagrams of this category, $\lambda$ abstraction becomes a box with a dangling bound wire, and an equivalence class of subterms becomes another kind of box; both are layered into a single hierarchical hypergraph. The paper then proves, as Proposition VI.7, that for closed $\Sigma^+$-terms $f$ and $g$, $f$ rewrites to $g$ modulo SMC laws, semilattice equations, and the distributivity law if and only if their interpretations as morphisms of $\mathrm{MEHypI}(\Sigma)/S$ rewrite to each other under convex extended double-pushout rewriting with interfaces. In other words, the graph representation does not just approximate the term theory; it is the term theory, with the symmetric monoidal equations absorbed by graph isomorphism and the semilattice and distributivity equations absorbed by the quotient rewrite rules.

Load-bearing premise

The equivalence depends on an unproved assumption: the rewrite rules that impose semilattice and distributivity laws are compatible with composing and tensoring e-hypergraphs, so that quotienting by rewrites gives a genuine category; if that fails, the main if-and-only-if does not follow.

Editorial extensions

If this is right

Equality saturation for a lambda calculus can be implemented by rewriting hierarchical e-hypergraphs directly, without explicit-substitution nodes or de Bruijn shifting; beta-reduction becomes a local rewiring when an application node meets a lambda-box.
The quotient by $S$ means all semilattice and distributivity equivalences are handled by the graph structure rather than by search, so the saturation engine only needs to fire user equations plus the structural schema rules.
Because the theorem is an if-and-only-if, unreachable graph pairs correspond exactly to non-equal terms; a saturation run that reaches a fixpoint has already closed the theory under the given equations.
The representation makes alpha-equivalence disappear: occurrences of the same bound variable share one wire, so e-graph sharing applies to bound variables as well.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Editorial inference: if the congruence gap in the proof of Proposition VI.7 is repaired, the same recipe—closed semilattice-enriched symmetric monoidal categories plus hierarchical hypergraphs—should transfer to linear, ordered, or dependent binding disciplines by changing the ambient closed category.
Editorial inference: the paper leaves algorithmics untouched; a natural next test is whether convexity and boundary-complement conditions can be checked and repaired efficiently during saturation, because those conditions govern whether each rewrite is admissible.
Editorial inference: idempotent join and absorbed distributivity suggest a normal form for e-hypergraph states as sums of join-free diagrams, which could serve as a canonical size measure and termination heuristic, although the paper does not develop one.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

The main theorem, Proposition VI.7, is not actually proved in the paper. The proof is a one-paragraph reduction to Proposition VI.6, and it never addresses the new quotient structure S. The assertion right after the rewrite schemas are collected that MEHypI(Σ)/S is a closed SLat-SMC is load-bearing, and it is asserted rather than proved. Without a proof that ⇛*_S is a congruence for composition and tensor, the graph-rewriting side of the iff has no well-defined category to live in.

What the paper does well: it gives a concrete combinatorial representation for closed semilattice-enriched SMCs using hierarchical hypergraphs, introduces extended cospans with internal interfaces, and defines convex EDPOI rewriting tailored to those cospans. The high-level idea—that the closed structure lets you absorb binding and substitution into the graph syntax, and that the SMC equations are absorbed by the combinatorial representation—is genuinely new and worth taking seriously. The paper is also honest about its place in the literature: it builds directly on [2] and [14], and the self-citation is appropriate given the subject.

The soft spots are exactly where the stress-test note lands. Lemma VI.3, the decomposition of every closed Σ+-term into a join of join-free terms, is stated without proof and is needed for the normalization step. Proposition VI.7's proof assumes that quotienting by S corresponds to rewriting modulo SLat equations and distributivity, and that the representative chosen for [[f]] is immaterial for subsequent DPOI rewriting. Neither is shown. These are gaps in the proof, not evidence of falsehood; the construction is plausible and probably repairable. But the central equivalence is not established as written.

The paper has no implementation, so the significance is conditional. That is fine for a theory paper, but it means the proof gaps are the whole ballgame.

This paper deserves a serious referee: the framework is novel and the gaps are specific enough that an expert can tell whether they close. I would send it to peer review, with the expectation of major revision—ask for a real proof of the quotient congruence and for Lemma VI.3. The reader's verdict of 'conditional' is the right one.

Referee Report

5 major / 8 minor

Summary. The paper proposes a categorical semantics for e-graphs with bindings, extending the semilattice-enriched symmetric monoidal category framework of [14] to closed symmetric monoidal categories. It defines e-hypergraphs with extended interfaces and a DPOI-style rewriting relation (EDPOI), and claims in Proposition VI.7 that term rewriting of closed Σ+-terms modulo SMC laws, SLat equations, and the distributivity law is equivalent to convex EDPOI rewriting in the quotient MEHypI(Σ)/S. The proof of this central equivalence is sketched in one paragraph and relies on unproved structural assertions about the quotient and on Lemma VI.3, which is also stated without proof.

Significance. The paper addresses a real and current problem: equality saturation for lambda calculi. The proposed representation via hierarchical hypergraphs with internal interfaces is a natural extension of prior work and, if the main theorem is established, would provide a principled way to absorb symmetric monoidal equations into the graph representation. The explicit definitions of extended cospans, boundary complements, and EDPOI rewriting are substantial pieces of work, and the paper builds openly on the soundness/completeness theorems of [2], [5], and [14]. The verification, however, is currently incomplete at exactly the load-bearing points.

major comments (5)

[§VI, after Definition VI.5] The sentence 'We collect all such rewrite schemas into a set S and then a category MEHypI(Σ)/S is a closed SLat SMC' is the load-bearing step of the whole paper and is not proved. A quotient of a category by a relation is a category only if the relation is a congruence: from G ⇛*_S H one must have C[G] ⇛*_S C[H] for every context C, in particular for composition with any cospan on either side and for tensoring with an arbitrary cospan. The paper does not show that ⇛*_S is compatible with the composition of extended cospans (Definition IV.4) or with the join operation of Fig. 8. Without this, the hom-sets of MEHypI(Σ)/S are not well-defined and the right-hand side of Proposition VI.7 has no mathematical content.
[Lemma VI.3] Lemma VI.3 is stated without proof. It asserts that every closed Σ+-term is equivalent, modulo SMC laws, SLat-equations, and the distributivity law, to a join of join-free terms. This lemma is used in Definition VI.4 to define the term-side rewrite relation and again in the proof of Proposition VI.7. Because the rewrite set S is intended to enforce exactly these equations, the lemma is essentially a normalization claim about S; it requires either a termination/confluence argument for S or a separate proof. As it stands, the main theorem depends on an unproved normalization statement.
[Proposition VI.7] The proof of Proposition VI.7 reduces the claim to Proposition VI.6, but the reduction is not valid as written. Proposition VI.6 is stated for a subcategory of MEHypI(Σ) whose carriers contain only edges from E ∪ E, i.e., before quotienting by S, whereas Proposition VI.7 concerns rewriting in MEHypI(Σ)/S. The proof notes that each fi is a Σ-term and its carrier has no E-edges, but it does not show that the equivalence class of [[f]] in MEHypI(Σ)/S is independent of the choice of decomposition f = f1 + ... + fn, nor that the S-rewrites (which implement the SLat equations and distributivity) commute with the rule rewrite ⟨[[l]],[[r]]⟩. The gap between the two propositions is exactly the quotient structure S that the new theorem claims to handle.
[Proposition VI.7, statement] The statement of Proposition VI.7 is ambiguous regarding the role of S. It reads 'f↝⟨l,r⟩ g if and only if [[f]]⇛⟨[[l]],[[r]]⟩ [[g]] in MEHypI(Σ)/S'. If rewriting on the graph side is performed in the quotient (i.e., modulo S), the rule subscript should be 'S ∪ {⟨[[l]],[[r]]⟩}' or the notation should be explained, since ⇛ is defined on objects of MEHypI(Σ), not on equivalence classes. If instead the graph side is meant to use only the single rule, then the phrase 'in MEHypI(Σ)/S' is a statement about the ambient category and the proof must show that the rewrite relation on representatives is well-defined. Neither reading is supported by the current text.
[Definition IV.4] The composition of extended cospans is defined via a pushout H, with the assertion that 'a pushout for the composition of two cospans with discrete feet always exists'. Appendix B proves pushout existence only under hypotheses (2)–(4) of Theorem A.10. The paper does not verify these hypotheses for the composition diagram of Definition IV.4, nor does it prove that composition is well-defined on the isomorphism classes of Definition IV.5. Since MEHypI(Σ)/S is constructed from this category, this is another unproved structural requirement for the statement of Proposition VI.7.

minor comments (8)

[§I.C] The sentence 'a more detailed comparison with the work of remains a future work' is incomplete; the reference to [28]'s authors or title is missing.
[§III.9] The statement of the soundness/completeness theorem imported from [5] is garbled: '/llbracketf /rrbracket⇛ /llbracketE/rrbracket/llbracketg/rrbracket' should be written as something like '[[f]] ⇛*_{[[E]]} [[g]]'.
[§II after Definition II.12] The phrase 'including the distributivity law II' refers to an unlabeled displayed equation (1); the equation should be numbered and referenced consistently.
[Definition IV.1] In the displayed definition of E, the third set in the union is not rendered (the line 'E = E ∪ E∪ E' appears to lose a symbol), and the overloaded use of E for both the edge set and one of its components makes the definition hard to read.
[Proposition A.4] In the proof, the verification that f+g is a semilattice homomorphism ends with 'f(x)+g(x)+f(y)+g(y) = f(x+y)+g(x+y)', which is a typo; the final expression should be '(f+g)(x)+(f+g)(y)'.
[Proposition A.6] The proof contains corrupted typesetting, e.g., '|B× . . .× B/bracehtipupleft /bracehtipdownright/bracehtipdownleft/bracehtipupright |A| |', and 'the fist isomorphism' should be 'the first isomorphism'.
[Definition IV.4] The notation n\m for the discrete e-hypergraph with vertices of m removed from n is only explained for the case when 'vertices of m is a sub-e-hypergraph of n'; the general case is ambiguous.
[Definition V.2] Condition (4) contains a duplicated word: 'or or v⌣w'.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: Proposition VI.7 is a substantive soundness/completeness claim; the cited [2] result is external published support, and the unproved quotient assertion is a correctness gap, not a definitional reduction.

full rationale

The derivation chain is not circular. Term rewriting in Definition VI.4 is defined by decomposing a closed Σ+-term into a join of join-free terms and rewriting one summand by E, while the graph side lives in the quotient MEHypI(Σ)/S; the quotient is generated by rewrite schemas S for SLat and distributivity axioms, but the paper never proves these two relations coincide, so the iff is a substantive soundness/completeness assertion rather than a definitional equality. The main non-trivial ingredient, Proposition VI.6, is imported as "Proposition 26 and Proposition 27 [2]"; this is a self-citation (Ghica is an author of both papers), but [2] is an external FSCD publication and the cited result is not a uniqueness theorem forbidding alternatives, so it is independent evidence rather than a circular premise. The one genuinely problematic passage is "We collect all such rewrite schemas into a set S and then a category MEHypI(Σ)/S is a closed SLat SMC" (Section VI, after Definition VI.5): for the quotient to exist, ⇛_S must be a congruence compatible with composition and tensor, and this is asserted, not proved; likewise Lemma VI.3 is asserted without proof. These are correctness/completeness gaps that would invalidate the theorem if unfixable, but they do not make the derivation circular because no equation is defined to be the target result and no fitted parameter is renamed as a prediction.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No physical or empirical entities are introduced. The only new constructs are mathematical definitions, e-hypergraphs with extended interfaces, which are the paper's contribution rather than ad hoc explanatory entities.

assumptions (4)

domain assumption Semilattice enrichment on hom-sets models e-graph equivalence classes.
Adopted from prior work [14] (Definitions II.9 to II.11). If this modeling choice is wrong, the entire notion of categorical e-graphs fails, but the paper does not re-derive it.
domain assumption Lambda abstraction and evaluation are represented by hierarchical boxes and the equations of closed monoidal categories.
Uses the representation of [13] and [2] via Fig. 4, Definitions II.7 and II.8, and the interpretation in Fig. 7. This is the load-bearing bridge from lambda calculus to string diagrams.
ad hoc to paper MEHypI(Σ)/S is a well-defined closed SLat-SMC.
Asserted in Section VI after Definition VI.5 and used in Proposition VI.7, but no proof is given that the rewrite relation is a congruence for composition and tensor.
standard math Every closed Σ+ term can be rewritten into a join-free sum f1 + ... + fn.
Stated as Lemma VI.3 without proof. It is plausible from associativity, commutativity, idempotence of + and the distributivity law (1), but it is load-bearing for Definition VI.4 and Proposition VI.7.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Categorical E-Graphs for Lambda Calculi." pith.science (2026). https://pith.science/paper/3P44M2OT

@misc{pith2026250500807,
  author       = {Pith},
  title        = {Pith review of: Categorical E-Graphs for Lambda Calculi},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3P44M2OT}},
  note         = {Machine review of arXiv:2505.00807}
}

abstract

Equality saturation, a technique for program optimisation and reasoning, has gained attention due to the resurgence of equality graphs (e-graphs). E-graphs represent equivalence classes of terms under rewrite rules, enabling simultaneous rewriting across a family of terms. However, they struggle in domains like $\lambda$-calculus that involve variable binding, due to a lack of native support for bindings. Building on recent work interpreting e-graphs categorically as morphisms in semilattice-enriched symmetric monoidal categories, we extend this framework to closed symmetric monoidal categories to handle bindings. We provide a concrete combinatorial representation using hierarchical hypergraphs and introduce a corresponding double-pushout (DPO) rewriting mechanism. Finally, we establish the equivalence of term rewriting and DPO rewriting, with the key property that the combinatorial representation absorbs the equations of the symmetric monoidal category.

Figures

Figures reproduced from arXiv: 2505.00807 by the authors.

**Figure 1.** String-diagrammatic representation of λf.f((λx.fx)2). String diagrams provide a topological framework for understanding monoidal categories, representing objects as strings and morphisms as nodes, where input strings flow in and output strings flow out. Key structures in monoidal categories—such as the monoidal product, tensor unit, braiding, and dualities—are represented graphically, through operations like juxtapo… view at source ↗

**Figure 2.** E-graph example (top) and its equivalent string diag [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗

**Figure 4.** String diagrams for closed semilattice-enriched sy [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗

Figures from the paper (7 more)

**Figure 5.** Figure 5: DPO and DPOI squares B. DPOI-Rewriting for Hypergraphs with Interfaces DPO rewriting is a standard technique for formalising graph transformations categorically. The intuitive notion of (hyper- )graph rewriting is as expected: given a rewrite rule L R and a graph G, we…

**Figure 6.** Figure 6: Cospan of e-hypergraphs example Consider an example in the middle part of [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]

**Figure 7.** Figure 7: JevK (left) and JΛ(f)K (right) 1) i + j → C → G is a boundary complement; 2) the internal interfaces of H are such that: n ′′ = n ′ \ (i ′ \ i) + (i ′′ \ i) and k ′′ = k ′ \ (j ′ \ j) + (j ′′ \ j) 3) the map f1 = [g1, h1] : n ′′ → H in the diagram above consists of g1 …

**Figure 8.** Figure 8: + of two morphisms in MEHypI(Σ) distributivity law II. The join of two cospans is defined as in [PITH_FULL_IMAGE:figures/full_fig_p015_8.png]

**Figure 9.** Figure 9: Pushout in EHyp(Σ) [idI ] := [id1] := v1 v1 v1 [sym1,1 ]:= v1 v1 v1 v2 v2 v2 [o] := v1 v1 w1 vm vm wn where o : v1 ⊗ . . . ⊗ vm → w1 ⊗ . . . ⊗ wn ∈ ΣM o . . . . . . . . . w1 wn . . [PITH_FULL_IMAGE:figures/full_fig_p021_9.png]

**Figure 10.** Figure 10: Base cases for [−] : SMT(Σ) → MHypI(Σ) • for any sequence ([x1], . . . , [xn]) such that [xi ] ∈ ⌣# X + Y / ∼ (ι∗/ ∼([xi+1])) or [xi+1] ∈ ⌣# X + Y / ∼ (ι∗/ ∼([xi ])) for i < n both [x1] ∈ (⌣# X + Y / ∼ (ι∗/ ∼([xn])))c and [xn] ∈ (⌣# X + Y / ∼ (ι∗/ ∼([x1])))c This cons…

**Figure 11.** Figure 11: β-rule DPOI example. D. DPOI rewriting Consider an example of DPOI rewriting in [PITH_FULL_IMAGE:figures/full_fig_p022_11.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

49 extracted references · 48 canonical work pages

[2]

R., S PRUNGER , D., AND ZANASI , F

A LVAREZ -P ICALLO , M., G HICA , D. R., S PRUNGER , D., AND ZANASI , F. Rewriting for monoidal closed categories. In 7th International Conference on F ormal Structures for Computation and Deduction, FSCD 20 22, August 2-5, 2022, Haifa, Israel (2022), A. P . Felty, Ed., vol. 228 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, pp. 29:1–29:2 0

work page 2022
[14]

R., B ARRETT , C., AND TIURIN , A

G HICA , D. R., B ARRETT , C., AND TIURIN , A. Equivalence hypergraphs: E-graphs for monoidal theori es, 2024

work page 2024
[5]

String diagram rewrite theory ii: Rewriting with symmet ric monoidal structure

B ONCHI , F., G ADDUCCI , F., K ISSINGER , A., S OBOCINSKI , P., AND ZANASI , F. String diagram rewrite theory ii: Rewriting with symmet ric monoidal structure. Mathematical Structures in Computer Science 32 , 4 (2022), 511–541

work page 2022
[1]

A nonstandard standardization theorem

A CCATTOLI , B., B ONELLI , E., K ESNER , D., AND LOMBARDI , C. A nonstandard standardization theorem. ACM SIGPLAN Notices 49 , 1 (2014), 659–670

work page 2014
[3]

String diagram rewrite theory i: Rewriting with frobeni us structure

B ONCHI , F., G ADDUCCI , F., K ISSINGER , A., S OBOCINSKI , P., AND ZANASI , F. String diagram rewrite theory i: Rewriting with frobeni us structure. J. ACM 69 , 2 (mar 2022)

work page 2022
[4]

String diagram rewrite theory i: Rewriting with frobeni us structure

B ONCHI , F., G ADDUCCI , F., K ISSINGER , A., S OBOCINSKI , P., AND ZANASI , F. String diagram rewrite theory i: Rewriting with frobeni us structure. J. ACM 69 , 2 (Mar. 2022)

work page 2022
[6]

Handbook of Categorical Algebra II

B ORCEUX , F. Handbook of Categorical Algebra II . Encyclopedia of Mathematics and its Applications. Cambri dge University Press, 1994, p. 291–348

work page 1994
[7]

An algebra of hierarchical graphs and its application to structural encoding

B RUNI , R., G ADDUCCI , F., AND LLUCH -L AFUENTE , A. An algebra of hierarchical graphs and its application to structural encoding. Sci. Ann. Comput. Sci. 20 (2010), 53–96

work page 2010

Show all 49 references

[8]

Gs.lambda theories: A syntax for higher-order graphs

C OCCIA , M., G ADDUCCI , F., AND MONTANARI , U. Gs.lambda theories: A syntax for higher-order graphs. I n Category Theory and Computer Science, CTCS 2002, Ottawa, Canada, August 15-17, 2002 (2002), R. Blute and P . Selinger, Eds., vol. 69 of Electronic Notes in Theoretical Co...

2002
[9]

D E BRUIJN , N. G. Lambda calculus notation with nameless dummies, a too l for automatic formula manipulation, with application to t he church-rosser theorem. In Indagationes mathematicae (proceedings) (1972), vol. 75, Elsevier, pp. 381–392

1972
[10]

Hierarchical graph transformation

D REWES , F., H OFFMANN , B., AND PLUMP , D. Hierarchical graph transformation. J. Comput. Syst. Sci. 64 , 2 (2002), 249–283

2002
[11]

Small Proofs from Congruence Closure

F LATT, O., C OWARD , S., W ILLSEY , M., T ATLOCK , Z., AND PANCHEKHA , P. Small Proofs from Congruence Closure. pp. 75–83. Accept ed: 2022-10- 12T10:02:40Z

2022
[12]

F ONG , B., AND SPIVAK , D. I. Seven sketches in compositionality: An invitation to applied category theory, 2018

2018
[13]

String diagrams for λ -calculi and functional computation, 2024

G HICA , D., AND ZANASI , F. String diagrams for λ -calculi and functional computation, 2024. To appear, CUP

2024
[15]

R., M UROYA , K., AND AMBRIDGE , T

G HICA , D. R., M UROYA , K., AND AMBRIDGE , T. W. Local reasoning for robust observational equivalenc e. CoRR abs/1907.01257 (2019)

2019 arXiv
[16]

Proceedings of the 22nd Conference on Formal Methods in C omputer-Aided Design – FMCAD 2022

G RIGGIO , A., AND RUNGTA , N. Proceedings of the 22nd Conference on Formal Methods in C omputer-Aided Design – FMCAD 2022. Publisher: TU Wien

2022
[17]

Eine algebraisierung des syntheseproblems von schaltk reisen

H OTZ , G. Eine algebraisierung des syntheseproblems von schaltk reisen. EIK, Bd. 1, 1965

1965
[18]

The geometry of tensor calculus, I

J OYAL, A., AND STREET , R. The geometry of tensor calculus, I. Advances in Mathematics 88 , 1 (July 1991), 55–112

1991
[19]

Sketch-guided equality saturation: Scaling equality s aturation to complex optimizations of functional programs, 2022

K OEHLER , T., T RINDER , P., AND STEUWER , M. Sketch-guided equality saturation: Scaling equality s aturation to complex optimizations of functional programs, 2022

2022
[20]

Categories for the W orking Mathematician

M ACLANE , S. Categories for the W orking Mathematician . Springer-V erlag, New Y ork, 1971. Graduate Texts in Mathem atics, V ol. 5

1971
[21]

Functorial boxes in string diagrams

M ELLI `ES , P.-A. Functorial boxes in string diagrams. In Computer Science Logic (Berlin, Heidelberg, 2006), Z. ´Esik, Ed., Springer Berlin Heidelberg, pp. 1–30

2006
[22]

Monoidal categories enriched in braided monoidal categ ories

M ORRISON , S., AND PENNEYS , D. Monoidal categories enriched in braided monoidal categ ories. International Mathematics Research Notices 2019 , 11 (10 2017), 3527–3579

2019
[23]

N ELSON , C. G. Techniques for program veriﬁcation . Stanford University, 1980

1980
[24]

Algebraic hierarchical graph transformation

P ALACZ , W. Algebraic hierarchical graph transformation. J. Comput. Syst. Sci. 68 , 3 (2004), 497–520

2004
[25]

Spinors and space-time , vol

P ENROSE , R., AND RINDLER , W. Spinors and space-time , vol. 1. Cambridge university press, 1984

1984
[26]

An introduction to string diagrams for computer scienti sts, 2023

P IEDELEU , R., AND ZANASI , F. An introduction to string diagrams for computer scienti sts, 2023

2023
[27]

P ITTS , A. M. Nominal Sets: Names and Symmetry in Computer Science . Cambridge Tracts in Theoretical Computer Science. Cambri dge University Press, 2013

2013
[28]

R UDI SCHNEIDER , T HOMAS KOEHLER , M. S. Slotted e-graphs — ﬁrst-class support for (bound) var iables in e-graphs. Accepted for PLDI 2025, 2025

2025
[29]

A Survey of Graphical Languages for Monoidal Categories

S ELINGER , P. A Survey of Graphical Languages for Monoidal Categories . Springer Berlin Heidelberg, 2010, p. 289–355

2010
[30]

Colored e-graph: Equality reasoning with conditions, 2 023

S INGHER , E., AND ITZHAKY , S. Colored e-graph: Equality reasoning with conditions, 2 023
[31]

Equality saturation: A new approach to optimization

T ATE, R., S TEPP , M., T ATLOCK , Z., AND LERNER , S. Equality saturation: A new approach to optimization. SIGPLAN Not. 44 , 1 (jan 2009), 264–276

2009
[32]

R., F LATT, O., T ATLOCK , Z., AND PANCHEKHA , P

W ILLSEY , M., N ANDI , C., W ANG , Y. R., F LATT, O., T ATLOCK , Z., AND PANCHEKHA , P. Egg: Fast and extensible equality saturation. Proc. ACM Program. Lang. 5 , POPL (jan 2021)

2021
[33]

R., W ILLSEY , M., AND TATLOCK , Z

Z HANG , Y., W ANG , Y. R., W ILLSEY , M., AND TATLOCK , Z. Relational e-matching. Proceedings of the ACM on Programming Languages 6 , POPL (Jan. 2022), 1–22. APPENDIX A. SLat In this section we will deﬁne the category of semilattices th at we use as a base for enrichment thro...

2022
[34]

φ is hypergraph homomorphism
[36]

When x is not a top-level vertex such that <(ιV (x)) is deﬁned, φE(<µ F (ιVF (x))) = <µ G (φV ; ιVG (x)) and φE(<µ F (ιEF (x))) = <µ G (φE; ιEG (x)) when x is a not top-level edge
[37]

When x∈ EF [φV ; ιVG , φE; ιEG ]∗(⌣F (ιEF (x)))⊆ ⌣G(φE; ιEG (x)) where φV ; ιVG : VF→ VG + EG, and similarly for φE; ιEG so that [φV ; ιVG , φE; ιEG ] : VF + EF→ VG + EG
[38]

Theorem A.10 (Existence of pushouts in EHyp(Σ) )

When x∈ VF [φV ; ιVG , φE; ιEG ]∗(⌣F (ιVF (x)))⊆ ⌣G(φV ; ιVG (x)). Theorem A.10 (Existence of pushouts in EHyp(Σ) ). Consider the following span in EHyp(Σ) Z X Y f g such that
[39]

Z is a discrete e-hypergraph
[40]

[fV (vi)) = [ fV (vj )) and [gV (vi)) = [ gV (vj)) for all vi, vj in VZ
[41]

If [fV (v))⁄= ∅ then [gV (v)) = ∅ and if [gV (v))⁄= ∅ then [fV (v)) = ∅
[42]

then the pushout X +f,g Y exists

⌣(fV (vi)) = ⌣(fV (vj)) and ⌣(gV (vi)) = ⌣(gV (vj)) for all vi, vj in VZ. then the pushout X +f,g Y exists. Proof. We next explicitly construct a pushout. Consider the diagra m below. Z X Y X + Y / ∼ R Q f g ι1/ ∼ R j1 ι2/ ∼ R j2 u Then, the pushout of e-hypergraphs X and Y is...
[43]

If there exists v such that <µ X+Y (ιVX +VY (v)) is deﬁned and u∼ v we let <µ X + Y / ∼ (ιVX + VY / ∼([u])) = [ <µ X+Y (ιVX +VY (v))]
[44]

u has no pre-image in VZ and <µ X+Y (ιVX +VY (u)) is undeﬁned ( i.e., [u) = ∅ ). If there exists v such that <µ X+Y (ιVX +VY (v)) = e′ and such that there is an undirected path from [u] to [v], then we deﬁne <µ X + Y / ∼ (ιVX + VY / ∼[u]) =<µ X + Y / ∼ (ιVX + VY / ∼[v]) Otherw...
[45]

Then we deﬁne <µ X + Y / ∼ (ιEX + EY / ∼[e]) = [ <µ X+Y (ιEX +EY (e))]

<µ X+Y (ιEX +EY (e)) = e′. Then we deﬁne <µ X + Y / ∼ (ιEX + EY / ∼[e]) = [ <µ X+Y (ιEX +EY (e))]
[46]

Clearly, all the cases above are disjoint

[e) = ∅ and there exists v such that <µ X+Y (ιVX +VY (v)) = e′ and such that there is an undirected path from [e] to [v], we deﬁne <µ X + Y / ∼ (ιEX + EY / ∼[e]) = <µ X + Y / ∼ (ιVX + VY / ∼[v]) Otherwise we leave <µ X + Y / ∼ (ιEX +EY∼([e])) undeﬁned. Clearly, all the cases a...
[47]

If there exists v such that ⌣X+Y (ιVX +VY (v))⁄= ∅ and u∼ v, we let ⌣# X + Y / ∼(ιVX + VY / ∼([u])) = [[] ⌣ V , []⌣ E ]∗(⌣X+Y (ιVX +VY (v)))
[48]

Then we let ⌣# X + Y / ∼(ιVX + VY / ∼([u])) = ⌣# X + Y / ∼(ιVX + VY / ∼([v])) Next we deﬁne ⌣# X + Y / ∼ for edges

u has no pre-image in VZ and ⌣X+Y (ιVX +VY (u)) = ∅ and there exists v such that ⌣X+Y (ιVX +VY (v))⁄= ∅ and such that there is an undirected path from [u] to [v]. Then we let ⌣# X + Y / ∼(ιVX + VY / ∼([u])) = ⌣# X + Y / ∼(ιVX + VY / ∼([v])) Next we deﬁne ⌣# X + Y / ∼ for edges
[49]

If ⌣X+Y (ιEX +EY (e))⁄= ∅ , then ⌣# X + Y / ∼(ιEX + EY / ∼([e]E)) = [[] ⌣ V , []⌣ E ]∗(⌣X+Y (ιEX +EY (e)))
[50]

Then we deﬁne ⌣X + Y / ∼(ιVX + VY / ∼([v])) and ⌣X + Y / ∼(ιEX + EY / ∼([e])) as closures of ⌣# X + Y / ∼ as below

⌣X+Y (ιEX +EY (e)) = ∅ and there exists v such that ⌣X+Y (ιVX +VY (v))⁄= ∅ and such that there is an undirected path from [e] to [v] then ⌣# X + Y / ∼(ιEX + EY / ∼([e]E)) = ⌣# X + Y / ∼(ιVX +VY ([v])) The well-deﬁnedness of this construction follows by the sam e argument as th...

Pith tools

Reviewed August 16, 2026 · model on record in the stance chip above.

[1] [2]

R., S PRUNGER , D., AND ZANASI , F

A LVAREZ -P ICALLO , M., G HICA , D. R., S PRUNGER , D., AND ZANASI , F. Rewriting for monoidal closed categories. In 7th International Conference on F ormal Structures for Computation and Deduction, FSCD 20 22, August 2-5, 2022, Haifa, Israel (2022), A. P . Felty, Ed., vol. 228 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum f¨ ur Informatik, pp. 29:1–29:2 0

work page 2022

[2] [14]

R., B ARRETT , C., AND TIURIN , A

G HICA , D. R., B ARRETT , C., AND TIURIN , A. Equivalence hypergraphs: E-graphs for monoidal theori es, 2024

work page 2024

[3] [5]

String diagram rewrite theory ii: Rewriting with symmet ric monoidal structure

B ONCHI , F., G ADDUCCI , F., K ISSINGER , A., S OBOCINSKI , P., AND ZANASI , F. String diagram rewrite theory ii: Rewriting with symmet ric monoidal structure. Mathematical Structures in Computer Science 32 , 4 (2022), 511–541

work page 2022

[4] [1]

A nonstandard standardization theorem

A CCATTOLI , B., B ONELLI , E., K ESNER , D., AND LOMBARDI , C. A nonstandard standardization theorem. ACM SIGPLAN Notices 49 , 1 (2014), 659–670

work page 2014

[5] [3]

String diagram rewrite theory i: Rewriting with frobeni us structure

B ONCHI , F., G ADDUCCI , F., K ISSINGER , A., S OBOCINSKI , P., AND ZANASI , F. String diagram rewrite theory i: Rewriting with frobeni us structure. J. ACM 69 , 2 (mar 2022)

work page 2022

[6] [4]

String diagram rewrite theory i: Rewriting with frobeni us structure

B ONCHI , F., G ADDUCCI , F., K ISSINGER , A., S OBOCINSKI , P., AND ZANASI , F. String diagram rewrite theory i: Rewriting with frobeni us structure. J. ACM 69 , 2 (Mar. 2022)

work page 2022

[7] [6]

Handbook of Categorical Algebra II

B ORCEUX , F. Handbook of Categorical Algebra II . Encyclopedia of Mathematics and its Applications. Cambri dge University Press, 1994, p. 291–348

work page 1994

[8] [7]

An algebra of hierarchical graphs and its application to structural encoding

B RUNI , R., G ADDUCCI , F., AND LLUCH -L AFUENTE , A. An algebra of hierarchical graphs and its application to structural encoding. Sci. Ann. Comput. Sci. 20 (2010), 53–96

work page 2010