Nominal Equational Rewriting and Narrowing
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915330802057216 |
|---|---|
| author | Ayala-Rincón, Mauricio Fernández, Maribel Nantes-Sobrinho, Daniele Santaguida, Daniella |
| author_facet | Ayala-Rincón, Mauricio Fernández, Maribel Nantes-Sobrinho, Daniele Santaguida, Daniella |
| contents | Narrowing is a well-known technique that adds to term rewriting mechanisms the required power to search for solutions to equational problems. Rewriting and narrowing are well-studied in first-order term languages, but several problems remain to be investigated when dealing with languages with binders using nominal techniques. Applications in programming languages and theorem proving require reasoning modulo alpha-equivalence considering structural congruences generated by equational axioms, such as commutativity. This paper presents the first definitions of nominal rewriting and narrowing modulo an equational theory. We establish a property called nominal E-coherence and demonstrate its role in identifying normal forms of nominal terms. Additionally, we prove the nominal E-Lifting theorem, which ensures the correspondence between sequences of nominal equational rewriting steps and narrowing, crucial for developing a correct algorithm for nominal equational unification via nominal equational narrowing. We illustrate our results using the equational theory for commutativity. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_05835 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Nominal Equational Rewriting and Narrowing Ayala-Rincón, Mauricio Fernández, Maribel Nantes-Sobrinho, Daniele Santaguida, Daniella Logic in Computer Science Symbolic Computation Narrowing is a well-known technique that adds to term rewriting mechanisms the required power to search for solutions to equational problems. Rewriting and narrowing are well-studied in first-order term languages, but several problems remain to be investigated when dealing with languages with binders using nominal techniques. Applications in programming languages and theorem proving require reasoning modulo alpha-equivalence considering structural congruences generated by equational axioms, such as commutativity. This paper presents the first definitions of nominal rewriting and narrowing modulo an equational theory. We establish a property called nominal E-coherence and demonstrate its role in identifying normal forms of nominal terms. Additionally, we prove the nominal E-Lifting theorem, which ensures the correspondence between sequences of nominal equational rewriting steps and narrowing, crucial for developing a correct algorithm for nominal equational unification via nominal equational narrowing. We illustrate our results using the equational theory for commutativity. |
| title | Nominal Equational Rewriting and Narrowing |
| topic | Logic in Computer Science Symbolic Computation |
| url | https://arxiv.org/abs/2506.05835 |