Lifting E-Graphs
20 hours ago
- #Term Rewriting
- #E-Graphs
- #Context-Awareness
- The author introduces the concept of "Lifting E-Graphs" as an improvement over previous "Thinning e-graph" models, focusing on functions from R^n to R.
- Three issues with explicit names in e-graphs are identified: generative processes needing fresh names, missed sharing opportunities in terms, and too much sharing leading to conflation of distinct objects (e.g., sin(x) can ambiguously represent different functions).
- The design philosophy emphasizes that "Context is not where a term is, it is part of what a term is," rejecting bare terms like sin(x) without context.
- A naive nameless approach uses variables indexed by dimension and context, but it worsens sharing between terms of different dimensions.
- Lifting operations (represented as bitvectors) relate terms across dimensions, enabling sharing via rules like sin(lift_i(X)) = lift_i(sin(X)) and lift compaction rules.
- Smart constructors bake lifting into e-graphs by pulling lifts upward, reducing memory usage and enabling efficient comparisons, akin to alpha-aware hash cons.
- A lifting union find handles lifted eids by peeling off common liftings during unions and may generate fresh constants for irreconcilable cases.
- E-matching in lifting e-graphs involves complexities, with options like ignoring redundant variables or enumerating solutions via lift factoring.
- Connections are drawn to existing concepts like thinnings, weakenings, and related work in nominal vs. nameless representations, with discussions on lambdas and ordered slotted e-graphs.
- Implementation details include using bitvectors for compact representation and exploring trade-offs between elegance and practicality in handling scope and redundancies.