E-graph rewriting is one of the more interesting ideas in modern compilers and program synthesis. The reference Rust library is `egg`, and most write-ups stay close to that ecosystem. A new post by Philip Zucker shows the same machinery can be expressed inside Constraint Handling Rules, the multiset rewriting language embedded in Prolog, in about a line of code.
The punchline is almost too short. One congruence rule plus a way to ground terms into the constraint store gives you a working e-graph for free. We dug into the post and the CHR book chapter it leans on so you can see exactly what is going on.
What CHR brings to the table
CHR is built into SWI-Prolog. Rules come in two flavors:
- Propagation rules like `foo, biz ==> bar` keep all three, just adding `bar`.
- Simplification rules like `foo, biz <=> bar` remove `foo` and `biz`, keeping `bar`.
That second shape, where you delete premises and assert a conclusion, is what lets you collapse equivalent terms. Most CHR programs rely on this simple distinction, and it turns out to map almost perfectly onto what an e-graph needs to do internally.
The one-line encoding
Define a single constraint `eclass(T, E)` saying term `T` belongs to e-class `E`. The e-class id can be a Prolog unification variable, which is itself a union-find data structure under the hood.
The rule:
`congruence @ eclass(T, E1), eclass(T, E2) <=> E1 = E2.`
That is the whole e-graph. Whenever the same term appears under two different e-class ids, the rule fires and unifies them. Because unification is transitive, the closure is automatic.
Adding ground terms is just flattening them into nested `eclass` constraints and letting the rule run. A term like `f(f(a))` becomes three constraints, one per node, and they normalize themselves.
Worked example
Say you assert `insert(f(f(a)), FFA)` and `insert(a, A)`, then unify `FFA = A`. The CHR engine fires the congruence rule, normalizes the e-graph, and ends up with two e-classes containing three enodes. The author's test produces exactly that: classes for `a` and `f(a)`, with `f(f(a))` collapsed into the first.
If you then assert a deeper term like `f(f(f(f(a))))` with the same root, the rule normalizes it down to whichever class it shares. That is exactly the e-graph behavior `egg` gives you, with far less infrastructure and zero external dependencies.
Our analysis
The embedding is gorgeous because of how well CHR's two rule shapes map to the operations an e-graph needs. Propagation does term insertion. Simplification does term unification. The author also flags a real limitation: CHR's execution order grabs from the top of the constraint store and applies rules in order. Equality saturation does not generally terminate, so you have to stop the engine early. Naively running the store burns cycles on rules that no longer matter.
The author works around this by introducing a second constraint, `eclass2`, and a `collect` rule that batches rewrite candidates into a list. A `process` predicate feeds the list back as fresh `eclass` constraints, and a top-level `batch(N)` wrapper caps the number of iterations. It is the same trick `egg` uses with its iteration budget, just expressed in Prolog.
This is not a free lunch. You lose some control over rule scheduling, and large e-graphs will stress Prolog's garbage collector. But there is a deeper point here. Datalog, CHR, and e-graph rewriting share a lot of structure. Once you have seen them all next to each other, the boundaries blur. Anyone maintaining an e-graph implementation should know they have alternatives, especially when teaching or prototyping.
What it means for you
Say you are prototyping a small program synthesizer in Prolog and want equality saturation. Instead of pulling in `egg`, you can drop a CHR module, define `eclass/2`, and get the rewrite engine for free. It will not scale to industrial compiler middle-ends, but for a research prototype, a teaching demo, or a DSL optimizer with a few hundred rules, it is an excellent starting point. You also get Prolog's backtracking for free, which `egg` does not offer.
Bottom line
One congruence rule plus Prolog unification is a working e-graph. Try it before reaching for an external library, and reach for `egg` only when you have measured the gap.
Key takeaways
- E-graph rewriting fits in CHR with a single congruence rule
- Prolog unification variables double as e-class ids with built-in union-find
- CHR's rigid execution order means you need an iteration cap to mimic equality saturation
- This approach is best for prototypes, not production compilers
Frequently asked questions
Do I need SWI-Prolog specifically?
The post uses SWI-Prolog, but any Prolog with CHR support (SICStus, GNU Prolog with constraints) should work with minor syntax changes.
Can this scale to real compiler middle-ends?
Probably not. CHR's rule application order and memory management are not designed for the volumes equality saturation handles in systems like `egg`.
How is this related to Datalog?
The author previously embedded e-graphs in Souffle Datalog. CHR is similarly expressive, and the two systems can encode each other with the right primitives.
What is an e-class id in this encoding?
A Prolog unification variable. CHR's congruence rule unifies the variables whenever the same term appears in two classes.
Where can I read more about CHR?
The CHR book, Anne Ogborn's tutorial series, and the SWI-Prolog CHR documentation are the standard starting points.