2026/06/22 by Philip Zucker · 2 voices
#cs.PL
Variables are quite subtle and easy to get wrong. An approach is described to support rigid α 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.