SK in egglog: part 4, extensional equality

submited by

Style Pass

2024-05-10 12:00:05

This post continues my explorations with egglog, using it to implement SK logic. Here’s the code so far, with some ruleset annotations sprinkled in to give us more control over what to run:

Modelling a Turing-complete system like SK requires care, to reach the desired results whilst avoiding infinite recursion. The SK reduction rules are the main danger, since they will attempt to “run” every expression in the database, so we need to avoid expressions which blow up.

Note that e-graphs are perfectly happy with infinite cycles, for example the following expression omega will be reduced by the S rule, but ends up back where it started after a few steps; that’s normally considered an “infinite loop”, but egglog’s cumulative approach keeps track of all the states, and stops as soon as the pattern repeats a previous form:

The last couple of installments explored the idea of extensionality, using Haskell to uncover a problem I was running into in egglog. The cause turned out to be using symbolic inputs to check if expressions agreed, when those expressions may have already contained those symbols. Now we’re switching back to egglog, our first task is to distinguish expressions that contain such uninterpreted symbols.