Hashing Modulo Context-Sensitive Alpha-Equivalence
summary
Defines context-sensitive alpha-equivalence as fork equivalence that coincides with bisimulation and gives a concrete hashing procedure that computes hashes modulo that relation in O(n log n) time improving on the prior O(n log^2 n) bound. Key idea globalize binders into labeled closed globals, avoid quadratic substitution by delaying work and only materializing when equal-size parts meet. Implements hashing on Coq term graphs to produce a densely deduplicated graph of hundreds of millions of nodes used for machine learning.
AI-written summary · about
chapters (13)
- 0:00Context-sensitive alpha-equivalence intro
- 1:05Motivation and real-world apps
- 3:14Why standard approaches fail
- 6:06Alpha-equivalence limits and alternatives
- 7:30Fork equivalence definition
- 9:36Narrowing and transitivity in fork eq
- 11:20Fork equivalence equivalence to bisimulation
- 12:45Hashing via globalization
- 14:09Globalization algorithm walkthrough
- 15:59Why globalization works
- 17:04Optimizing to O(n log n)
- 17:48Paper contents and experiments
- 18:10Question and answer session
related talks
48mHashing Modulo Alpha Equivalence
19mTowards Relational Contextual Equality Saturation
59mUnification Modulo Equational Theories in Languages with Binding Operators
18mAssociativity and Commutativity in Equality Saturation
27mTail Recursion Modulo Context: An Equational Approach
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
09mDynamic Dispatch of Context-Sensitive Optimizations
12mContextual Algebraic Theories: Generic Boilerplate beyond Abstraction