How to prove equations using diagrams: A categorical and operational semantics for e-graphs

Evan Patterson

Home/Archive/arXiv

arXiv · 2611.05924

How to prove equations using diagrams: A categorical and operational semantics for e-graphs

Evan Patterson

View original source ↗Read source document ↗Export metadata ↓

Abstract

E-graphs are a powerful algorithmic technique for automated equational reasoning but have resisted a conceptual understanding independent of issues of presentation and implementation. We propose an operational semantics for e-graphs based on the fundamental category-theoretic concepts of diagrams, limits, and initial functors. We illustrate the formalism through numerous example calculations and establish its soundness and completeness. Technical prerequisites are kept to a minimum in the main text; less standard elements of the mathematical theory are developed in two appendices.

Explore related subjects

math.CT cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Evan Patterson. 2026-11-04. How to prove equations using diagrams: A categorical and operational semantics for e-graphs. https://arxiv.org/abs/2611.05924

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Composing Double Categories

Many kinds of generalised syntax, including internal categories, T-categories or polynomial monads, arise as monads in bicategories of a certain flavour: maps are some kind of span, and composition is some kind of pullback. We explain the pattern behind these similarities: each bicategory is stitched together from two simpler pieces by a distributive law, where the distributivity is governed by pullback. A key novelty is in the kind of distributive law we consider; where Rosebrugh and Wood considered distributive laws between categories, we instead consider pseudo-distributive laws between double categories. A key construction, drawing on work of Weber, obtains such a distributive law from a so-called co-crossed double category: one whose codomain functor is a fibration, and whose cartesian cells are stable under horizontal composition. We show the horizontal Kleisli double category of a monad T is co-crossed just when T is cartesian, and that the composite double category recovers T-spans; that the double category associated to an identity-on-objects functor is co-crossed just when that functor is a calibration in the sense of Bénabou; and that Street's calibrated bicategories yield co-crossed double categories in a similar manner, recovering the double category of polynomials of Gambino--Kock.

math.CT↗

arXiv2026

Object ideals and idempotent completeness

We construct an idempotent complete Frobenius exact category with an idempotent complete stable category in which a complete ideal cotorsion pair of object ideals induces a cotorsion pair of objects that fails to be complete. This gives a negative answer to the question of Fu, Guil Asensio, Herzog and Torrecillas under idempotent completeness. The construction uses a lemma on dense triangulated subcategories and an example of Bondarko and Sosnilo in which a weight structure fails to extend to the idempotent completion. The induced cotorsion pair is hereditary, and every object admits an ordinary precover from its left class and an ordinary preenvelope into its right class. We characterize which objects admit special precovers and which admit special preenvelopes.

math.CT↗

arXiv2026

Presenting Point-Glued Self-Similar Objects as Final Coalgebras in Metric Spaces via Completion: A Categorical Hutchinson Theorem

We study self-similar spaces obtained by repeatedly gluing finitely many scaled copies of a pointed metric space along prescribed boundary points. A finite gluing specification defines endofunctors on suitable categories of pointed sets and pointed metric spaces. Under non-degeneracy and metric admissibility assumptions, the initial algebra of the set functor carries a canonical metric. Its Cauchy completion is a final coalgebra for the metric functor and, after forgetting the metric, also for the underlying set functor. We compare this construction with Iterated Function Systems. When the orbit algebra is injective and its comparison with the initial algebra is bi-Lipschitz, the attractor is isomorphic to the completed final coalgebra. This gives a categorical analogue of Hutchinson's theorem for overlaps captured by finitely many distinguished points. Examples include the unit interval, Cantor spaces, the Sierpiński gasket and $p$-adic integers.

math.CT↗