Lifting E-Graphs: A Function Isn't a Constant

Abstract

Variables are quite subtle and easy to get wrong. An approach is described to support rigid $\alpha$ canonical variables in an e-graph. The lifting e-graph has a baked-in notion of functional lifting combinator. It is implemented by fattening the usual integer identifiers with thinning bitvectors, lift-pulling smart constructors, and a special thinning-aware union find variation. The approach is inspired by slotted e-graphs and Co-de Bruijn syntax.

Presented at EGRAPHS 2026