Hashing Modulo Context-Sensitive 𝛼-Equivalence

The notion of 𝛼-equivalence between 𝜆-terms is commonly used to identify terms that are considered equal. However, due to the primitive treatment of free variables, this notion falls short when comparing subterms occurring within a larger context. Depending on the usage of the Barendregt convention (choosing different variable names for all involved binders), it will equate either too few or too many subterms. We introduce a formal notion of context-sensitive 𝛼-equivalence, where two open terms can be compared within a context that resolves their free variables. We show that this equivalence coincides exactly with the notion of bisimulation equivalence. Furthermore, we present an efficient 𝑂 (𝑛 log 𝑛) runtime hashing scheme that identifies 𝜆-terms modulo context-sensitive 𝛼-equivalence, generalizing over traditional bisimulation partitioning algorithms and improving upon a previously established 𝑂 (𝑛 log 2 𝑛) bound for a hashing modulo ordinary 𝛼-equivalence by Maziarz et al [20]. Hashing 𝜆-terms is useful in many applications that require common subterm elimination and structure sharing. We have employed the algorithm to obtain a large-scale, densely packed, interconnected graph of mathematical knowledge from the Coq proof assistant for machine learning purposes.

CCS Concepts: • Software and its engineering → Compilers; • Theory of computation → Lambda calculus; Design and analysis of algorithms.