SK logic in egglog: part 1, encoding and reduction

submited by

Style Pass

2024-05-10 11:30:10

I’ve been really excited to try out egglog, since it seems like a great complement and application for the theory exploration systems I spent a few years playing with.

Egglog can be thought of as a powerful database, combining Datalog (a restricted form of Prolog, which is essentially first-order logic) and equality-saturation. The latter is most interesting to me, since it represents expressions via a graph of equivalence classes; very similar to the internal representation that QuickSpec v1 uses to search for conjectures (v2 switched to generating individual expressions on-the-fly, more like IsaCoSy; although much faster). I’ve played with equational systems like Maude before, but egglog seems like a sweet-spot in the design space.

This is actually just a Peano/Grassman encoding of the natural numbers, but I’m using different names since we’re going to deviate from that definition in a moment. Instead, think of it as a very simple programming language, with two sorts of expression.

The datatype keyword is a shorthand for declaring a sort (i.e. a type), and for defining any number of constructors: functions which accept inputs and return a value of this sort. Here we can see that Id is such a function. Since C is a constant, rather than a function, we declare it separately; however, this results in an auto-generated nullary function with the unhelpful name v0___. That may be fine for many applications, but for these explorations I’d like something more readable.