Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2401.02948 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910499223896064 |
|---|---|
| author | Blaauwbroek, Lasse Olšák, Miroslav Geuvers, Herman |
| author_facet | Blaauwbroek, Lasse Olšák, Miroslav Geuvers, Herman |
| contents | 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 by Maziarz et al. Hashing $λ$-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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_02948 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Hashing Modulo Context-Sensitive $α$-Equivalence Blaauwbroek, Lasse Olšák, Miroslav Geuvers, Herman Programming Languages Logic in Computer Science 68N18 (Primary) 68N20, 03B40 (Secondary) D.3.1 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 by Maziarz et al. Hashing $λ$-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. |
| title | Hashing Modulo Context-Sensitive $α$-Equivalence |
| topic | Programming Languages Logic in Computer Science 68N18 (Primary) 68N20, 03B40 (Secondary) D.3.1 |
| url | https://arxiv.org/abs/2401.02948 |