Hashing Modulo Context-Sensitive $\alpha$-Equivalence

The notion of $\alpha$-equivalence between $\lambda$-terms is commonly usedto identify terms that are considered equal. However, due to the primitivetreatment of free variables, this notion falls short when comparing subtermsoccurring within a larger context. Depending on the usage of the Barendregtconvention (choosing different variable names for all involved binders), itwill equate either too few or too many subterms. We introduce a formal notionof context-sensitive $\alpha$-equivalence, where two open terms can be comparedwithin a context that resolves their free variables. We show that thisequivalence coincides exactly with the notion of bisimulation equivalence.Furthermore, we present an efficient $O(n\log n)$ runtime algorithm thatidentifies $\lambda$-terms modulo context-sensitive $\alpha$-equivalence,improving upon a previously established $O(n\log^2 n)$ bound for a hashingmodulo ordinary $\alpha$-equivalence by Maziarz et al. Hashing $\lambda$-termsis useful in many applications that require common subterm elimination andstructure sharing. We employ the algorithm to obtain a large-scale, denselypacked, interconnected graph of mathematical knowledge from the Coq proofassistant for machine learning purposes.