Nominal Equational Rewriting and Narrowing
Maurício Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho, Daniella Santaguida · Electronic Proceedings in Theoretical Computer Science · 2025
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.