Class 18: Using E-Graphs

This class, we are going to walk through a tutorial on e-graphs! But the e-graphs we looked at on Tuesday are quite complicated, since they deal with a complex notion of equality particular to dependent types. Instead of looking at those, we are going to look at the tutorial for an e-graph library called egg, perhaps best known for the corresponding POPL 2021 best paper.

The egg library is thus far used in much more traditional use cases for e-graphs, like rewrite systems in programming languages tools and compilers. But it does now have some proof-producing abilities, as you'll see in the third part of the tutorial! So you'll see how one could use e-graphs to implement automatic rewriting and get proof objects, which is incredibly cool.

Still, they will be in a simpler logic with a simpler notion of equality than what we typically use inside of our proof assistants. This is OK. The tutorial is the best tutorial I have seen thus far for getting acquainted with e-graphs. So what I hope they will do is give folks an understand of what it's like to use e-graphs, so that if at some point folks want to use them for proof automation, it will "just" amount to adapting them to the proof assistant of choice. Of course, "just" is in quotes there for a reason---as we saw in the last reading, this can get quite complex!

Installation Instructions

1. Install the Rust programming language and the corresponding Cargo package manager following these instructions.
2. Scroll down on the same instructions page to the "generating a new project" section. Follow those instructions to generate and run new Rust project that prints "Hello, world!" when you run it.
3. Scroll down on the same instructions page to the "adding dependencies" section. Add a dependency egg = "0.7.1" to your project.
4. If you are new to Rust, you will likely also want to add the dependency on same instructions page, and then implement the small Rust application and play around with it. Otherwise, you are ready to go!

If you have any trouble, please post your questions in this class forum thread. Please also drop any installation tips you have in that thread.

If installation fails, and the class forums are no help, do not panic; we will try to match you with someone in class for whom installation worked.

You can find the exercise we will do together in class below.

During class, we will again divide up into groups. We will then do the egg tutorial---all three parts as time allows. You can do this on your own if you cannot make it to class, or enter a Zoom breakout if you're remote. Let me know if you can't attend, but would like me to find you a partner or make an exception.

If you have extra time at the end, I recommend playing around and modifying the code you write as part of the tutorial, and exploring what happens.

As usual, the only graded part will be a discussion question: Thinking back to the proof automation you've used so far and the problems you've encountered so far, how might you use an e-graph library like egg to solve some of those problems? What challenges would you anticipate encountering---either at the level of design or implementation---and how might you go about trying to solve them?

Please have your group post your answers in the class forum thread, listing all group members in your response.