一句话：提出上下文敏感 α-等价，证明其等价于互模拟，并给出 O(n log n) 哈希算法。
λ-项通常用 α-等价识别相等项，但自由变量的原始处理使子项在更大上下文中比较时，会因 Barendregt 约定不同而等得过少或过多。论文引入上下文敏感 α-等价：两个开项可在解决其自由变量的上下文中比较，并证明该等价恰好等于互模拟等价。作者进一步提出 O(n log n) 的哈希方案，用于识别模上下文敏感 α-等价的 λ-项，推广了传统互模拟划分算法，改进了 Maziarz 等人关于普通 α-等价哈希的 O(n log^2 n) 上界。该哈希适用于公共子项消除与结构共享，并已用于从 Coq 证明助手提取大规模、密集互联的数学知识图以服务机器学习。
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 O ( n log n ) runtime hashing scheme that identifies 𝜆-terms modulo context-sensitive 𝛼 -equivalence, generalizing over traditional bisimulation partitioning algorithms and improving upon a previously established O ( n log 2 n ) bound for a hashing modulo ordinary 𝛼-equivalence byMaziarz et al [ 21 ]. Hashing 𝜆-terms is useful in many applications that require common subterm elimination and structure sharing. We hav employed the algorithm to obtain a large-scale, densely packed, interconnected graph of mathematical knowledge from the Coq proof assistant for machine learning purposes.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BlaauwbroekOG24,
title = {Hashing Modulo Context-Sensitive α-Equivalence},
author = {Lasse Blaauwbroek and Miroslav Olšák and Herman Geuvers},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656459}
}