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 algorithm that identifies $\lambda$-terms modulo context-sensitive $\alpha$-equivalence, 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 employ the algorithm to obtain a large-scale, densely packed, interconnected graph of mathematical knowledge from the Coq proof assistant for machine learning purposes.

翻译：λ项之间的α等价概念通常用于识别被认为相等的项。然而，由于对自由变量的原始处理方式，这一概念在比较更大上下文中出现的子项时存在不足。根据巴伦德雷格约定（为所有涉及的绑定器选择不同变量名）的使用方式，它要么等同过少子项，要么等同过多子项。我们引入了一种形式化的上下文敏感α等价概念，其中开放项可在解析其自由变量的上下文内进行比较。我们证明该等价性恰好与互模拟等价概念一致。此外，我们提出了一种高效运行的O(n log n)算法，用于识别模上下文敏感α等价的λ项，改进了Maziarz等人先前针对普通α等价哈希模建立的O(n log^2 n)界。λ项哈希在许多需要公共子项消除和结构共享的应用中十分有用。我们采用该算法从Coq证明助手中构建了一个用于机器学习的大规模、密集连接的知识图谱。