Hashing modulo alpha-equivalence

In many applications one wants to identify identical subtrees of a program syntax tree. This identification should ideally be robust to alpha-renaming of the program, but no existing technique has been shown to achieve this with good efficiency (better than O (𝑛 2 ) in expression size). We present a new, asymptotically efficient way to hash modulo alphaequivalence. A key insight of our method is to use a weak (commutative) hash combiner at exactly one point in the construction, which admits an algorithm with O (𝑛(log 𝑛) 2 ) time complexity. We prove that the use of the commutative combiner nevertheless yields a strong hash with low collision probability. Numerical benchmarks attest to the asymptotic behaviour of the method.

• Theory of computation → Design and analysis of algorithms; • Software and its engineering;