How to prove equations using diagrams: A category theorist looks at e-graphs

Abstract

First invented in 1980, e-graphs are receiving new attention as a powerful and adaptable data structure to keep the books for equational reasoning. In this talk on work in progress, we explore an operational semantics for e-graphs based on category-theory. We argue that classic concepts from category theory, particularly diagrams and initial functors, provide a conceptual foundation for the diagrammatic reasoning performed in e-graphs.
https://topos.institute/blog/2025-05-27-e-graphs-1/