You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Patrick Nicodemus (Sep 23 2025 at 20:23):I haven't read this paper but I'm reading it now. I'm pretty excited about equality saturation.
e-graphs really clicked for me recently and I'm very happy about how they nicely handle equational reasoning problems that would otherwise lead to infinite loops. I can imagine using e-graphs for proof-search in type theory as well by carrying out a Datalog-like procedure to flood the search space with inhabitants, using e-graphs to control the proliferation of terms.
Many problems in the equational reasoning of category theory are very simple or even decidable: it would be nice if we could make this formal by showing that equality is "saturating" for common categorical theories in the sense described in this paper.
Semantic foundations of equality saturatio - Unknown.pdf
Patrick Nicodemus (Sep 23 2025 at 20:24):@Amar Hadzihasanovic They use a syntactic acyclicity condition in this paper - seems like a research challenge! "We give a more general contractibility condition" :)
Patrick Nicodemus (Sep 23 2025 at 20:25):It's exciting that they say "we still understand very little about equality saturation...We also do not know much about when EqSat terminates." Really, seems like a good research question
Patrick Nicodemus (Sep 23 2025 at 20:29):With an appropriate cost model, EqSat can further pick
the optimal program among all programs equivalent to the input, e.g. by using Knuth’s
algorithm [16].
To me the practical upshot of this is that for formal theorem proving in category theory one can assign a cost model based on syntactic complexity and then once the algorithm finds an equivalence class of terms it can return the term of minimal syntactic compexity, which is the term you would write down by hand, one which is easy to reason about in practice. To me such a guarantee seems really important for practical applications, we cannot automate constructions in category theory unless the construction is simple enough to reason about
Ryan Wisnesky (Sep 23 2025 at 22:50):we were able to hook up Egglog, which implements EqSat, to CQL, pretty easily, for use as both an equational theorem prover and a (skolem) chase engine, thanks to many of the nice properties you mention