Hashing Modulo Alpha Equivalence
summary
Presents an algorithm that hashes lambda terms modulo alpha‑equivalence by summarizing each node into a structure + free‑variable map and then hashing those summaries with ordinary hashconsing. Key techniques: only adjust the smaller map when merging (gives n log n work per level), record depths and a bigger‑side flag in structures, and use XOR as a weak commutative hash combiner so deletions are cheap. Achieves O(n*(log n)^2) time, low collision probability, Haskell prototype, and better practical performance than locally‑nameless approaches.
AI-written summary · about
chapters (28)
- 0:00Introduction
- 0:41Problem Statement
- 1:48Hashconzing
- 2:50Example
- 3:38Avoiding false positives
- 4:10False negative example
- 5:04Hashconzing example
- 6:19Divine Notation
- 10:25The Problem
- 10:50ESummary
- 12:35Free Variable Map
- 16:58Summary
- 21:57Hash Constable
- 22:33Hash Summary
- 26:52App Node
- 27:03App Node Example
- 30:04App Depth Example
- 35:12Positivity in Substitution
- 36:08Haskell Program Example
- 38:23Hash of Depleted Variable Map
- 39:15Hash Exponential
- 40:58Collisions
- 42:06Rough Summary
- 42:48Proof
- 45:23Synthetic Benchmarks
- 46:37Big Expressions
- 46:47Conclusion
- 47:02Conclusions
related talks
21mHashing Modulo Context-Sensitive Alpha-Equivalence
59mUnification Modulo Equational Theories in Languages with Binding Operators
34mHash Maps: more room at the bottom
17mHefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
18mAssociativity and Commutativity in Equality Saturation
15mSealing Pointer-Based Optimizations Behind Pure Functions
23mBetter Defunctionalization through Lambda Set Specialization
36mDependently Typed Multi-Stage Programming, Revisited