Prototype refinement e-graphs add inequality to compiler optimization

Compiler rewrites as refinement

The prototype introduces a baked-in inequality relation with status similar to an e-graph's native equality relation. The motivation is that compiler rewrites are often directional: they move an abstract or underspecified program toward a more concrete form that can run on a machine. Source languages may leave evaluation order unspecified or leave results such as integer overflow and division by zero open, creating optimization and translation opportunities.

The source presents a prototype based on Max Willsey's microegg, along with a WASM demo. Its Python code extends the equality-centered model with inequality union-find operations, including ways to add, test and enumerate less-than-or-equal-to relationships.

Choosing values for unsupported circuit inputs

A central example is the "don't care" value in digital circuits. If an input is unsupported, the output can be treated as a don't care, allowing an optimizer to select whichever result produces the best circuit. The prototype can refine that value to true or false without equating it globally to either one, allowing separate uses to make independent choices.

Its semantics maps a term to a set of Boolean values, with less-than-or-equal-to representing pointwise set containment. Rules named rewrite-le and rewrite-ge handle directional refinement. The extraction process can search above, below or only at equality, depending on which kind of refined term is requested.

Variance across the e-graph

To propagate relations through function symbols, the implementation records whether each argument is monotone, anti-monotone or neither. Set difference is used as an example: it is monotone in its first argument and anti-monotone in its second. These declarations support refinement closure, inequality-aware e-matching and extraction.

Beyond circuits, the proposal identifies logic implication, relation algebra, subtyping, query containment and first-class lattice analyses as possible applications. The author describes refinement as a comparatively direct extension of standard e-graph concepts, while noting questions about finer pattern syntax and the algebraic view of upper and lower relation sets.