The notion of $\alpha$-equivalence between $\lambda$-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 $\alpha$-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 $O(n\log n)$ runtime hashing scheme that identifies $\lambda$-terms modulo context-sensitive $\alpha$-equivalence, generalizing over traditional bisimulation partitioning algorithms and improving upon a previously established $O(n\log^2 n)$ bound for a hashing modulo ordinary $\alpha$-equivalence by Maziarz et al. Hashing $\lambda$-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.

翻译：λ项之间的α等价概念通常用于识别被视为相等的项。然而，由于对自由变量的原始处理方式，在较大上下文中比较子项时，这一概念存在不足。根据Barendregt约定（为所有涉及的绑定符选择不同的变量名）的使用方式，它要么会等同过少的子项，要么会等同过多的子项。我们引入了一种形式化的上下文敏感α等价概念，其中两个开放项可以在解析其自由变量的上下文中进行比较。我们证明这种等价恰好与互模拟等价的概念一致。此外，我们提出了一种高效的O(n log n)运行时哈希方案，该方案能识别基于上下文敏感α等价的λ项，推广了传统的互模拟划分算法，并改进了Maziarz等人先前为基于普通α等价的哈希建立的O(n log² n)界限。对λ项进行哈希在需要公共子项消除和结构共享的许多应用中非常有用。我们已采用该算法，从Coq证明助手中获取了一个大规模、密集打包、相互关联的数学知识图，用于机器学习目的。