تقرير
Hashing Modulo Context-Sensitive $\alpha$-Equivalence
| العنوان: | Hashing Modulo Context-Sensitive $\alpha$-Equivalence |
|---|---|
| المؤلفون: | Blaauwbroek, Lasse, Olšák, Miroslav, Geuvers, Herman |
| سنة النشر: | 2024 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Programming Languages, Computer Science - Logic in Computer Science, 68N18 (Primary) 68N20, 03B40 (Secondary), D.3.1 |
| الوصف: | 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. Comment: 33 pages |
| نوع الوثيقة: | Working Paper |
| DOI: | 10.1145/3656459 |
| URL الوصول: | http://arxiv.org/abs/2401.02948 |
| رقم الأكسشن: | edsarx.2401.02948 |
| قاعدة البيانات: | arXiv |
| DOI: | 10.1145/3656459 |
|---|