For the seventeeth class, we will read Congruence Closure in Intensional Type Theory [PDF] [DOI] by Daniel Selsam and Leonardo de Moura. As a short bonus reading, we'll also read the two-pager Congruence Closure in Cubical Type Theory [PDF] by Emil Holm Gjørup and Bas Spitters.
If you were paying way too much attention to the reading before spring break, you may have seen me allude to these things called e-graphs, and cite these papers. Neither of these papers say the word e-graph, but that's what they're about.
E-graphs are these super wonderful data structures for managing equality and equivalence information. They are traditionally used inside of constraint solvers and automated theorem provers to implement congruence closure, an efficient algorithm for equational reasoning---but they can also be used to implement rewrite systems.
Probably the best explanation of e-graphs I've seen comes from the documentation for an e-graph library called egg. What the first paper we'll read this week does that is so cool is implement congruence closure with these data structures in a dependent type theory, since traditional solvers and automated theorem provers don't handle dependent types. So basically this paper takes the central insights at the core of many solvers and automated theorem provers, and lifts it into a dependently typed proof assistant. It's quite incredible.
The result is a really powerful tactic for solving proof goals that follow from series of equations. But as I hinted at in the proof repair paper from before spring break, these have the potential to help with other kinds of automation too---like a much better workflow for proof repair across type equivalences when managing a large project with many different datatypes that change! So one thing I'd love to do is build e-graphs into PUMPKIN Pi---let me know if you're interested!
Oh, but there's just one problem. Remember when I said early on that equality is one of the hardest problems in type theory? Well, equality in dependent type theory is hard and controversial, and the first paper we'll read makes a particular assumption about equality. This assumption is not one that, say, Coq makes by default, and it's actually inconsistent with Cubical Agda (and homotopy type theory more generally).
Enter the second paper---a short two-pager on e-graphs in Cubical Agda. This uses a different notion of equality that comes from cubical type theory (an implementation of homotopy type theory). But it's a short paper and, from what I gather, not yet implemented efficiently. Still, these two papers together offer a balanced view of the design space so far in implementing e-graphs for proof assistants based on dependent type theory.
Please note that this is due the morning before class, so that we can discuss it in person. And please install the artifact before Thursday's class.