Hashing Modulo Alpha-Equivalence

TL;DR

This paper introduces an efficient hashing method for program syntax trees that is robust to alpha-renaming, achieving better than quadratic time complexity with low collision probability.

Contribution

The paper presents a novel hashing technique for alpha-equivalence that is asymptotically efficient using a weak hash combiner, improving over previous methods.

Findings

Achieves $ ext{O}(n ( ext{log} n)^2)$ time complexity

Proves low collision probability of the hash

Numerical benchmarks confirm asymptotic efficiency

Abstract

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 $\mathcal{O}(n^2)$ in expression size). We present a new, asymptotically efficient way to hash modulo alpha-equivalence. 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 $\mathcal{O}(n (\log n)^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.