Getting Started
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
- Install the Rust programming language and the corresponding Cargo package manager following these instructions.
- 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.
- Scroll down on the same instructions page to the "adding dependencies" section. Add a dependency
egg = "0.7.1"
to your project. - 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.