Nominal Equational Rewriting and Narrowing

TL;DR

This paper introduces the first formal framework for nominal rewriting and narrowing modulo equational theories, addressing challenges in reasoning with binders and structural congruences in programming languages and theorem proving.

Contribution

It defines nominal rewriting and narrowing modulo equational theories, introduces the concept of nominal E-coherence, and proves the nominal E-Lifting theorem for correct nominal equational unification.

Findings

Established nominal E-coherence property for normal forms

Proved the nominal E-Lifting theorem linking rewriting and narrowing

Applied results to the equational theory of commutativity

Abstract

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.