Nominal Equational Rewriting and Narrowing

TY - CHAP

T1 - Nominal Equational Rewriting and Narrowing

AU - Ayala-Rincón, Mauricio

AU - Fernández, Maribel

AU - Nantes-Sobrinho, Daniele

AU - Santaguida, Daniella

N1 - Publisher Copyright: © M. Ayala-Rincón, M. Fernández, D. Nantes-Sobrinho & D. Santaguida.

PY - 2025/6/6

Y1 - 2025/6/6

N2 - 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 α-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.

AB - 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 α-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.

UR - https://www.scopus.com/pages/publications/105008205379

U2 - 10.4204/EPTCS.421.5

DO - 10.4204/EPTCS.421.5

M3 - Conference paper

AN - SCOPUS:105008205379

VL - 421

T3 - Electronic Proceedings in Theoretical Computer Science, EPTCS

SP - 80

EP - 97

BT - Proceedings of LSFA 2024

PB - Electronic Proceedings in Theoretical Computer Science

T2 - 19th International Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2024

Y2 - 18 September 2024 through 20 September 2024

ER -