Nominal Equational Narrowing: Rewriting for Unification in Languages with Binders

TL;DR

This paper introduces a novel framework for nominal rewriting and narrowing that handles binders, freshness, and equational axioms, enabling effective reasoning in programming languages and theorem proving.

Contribution

It presents a new nominal rewriting and narrowing framework with key properties and a unification procedure that addresses challenges with binders and equational theories.

Findings

Established nominal E-coherence under freshness conditions

Proved the nominal E-lifting theorem linking rewriting and narrowing

Developed a correct nominal unification procedure

Abstract

Narrowing extends term rewriting with the ability to search for solutions to equational problems. While first-order rewriting and narrowing are well studied, significant challenges arise in the presence of binders, freshness conditions and equational axioms such as commutativity. This is problematic for applications in programming languages and theorem proving, where reasoning modulo renaming of bound variables, structural congruence, and freshness conditions is needed. To address these issues, we present a framework for nominal rewriting and narrowing modulo equational theories that intrinsically incorporates renaming and freshness conditions. We define and prove a key property called nominal E-coherence under freshness conditions, which characterises normal forms of nominal terms modulo renaming and equational axioms. Building on this, we establish the nominal E-lifting theorem, linking rewriting and narrowing sequences in the nominal setting. This foundational result enables the development of a nominal unification procedure based on equational narrowing, for which we provide a correctness proof. We illustrate the effectiveness of our approach with examples including symbolic differentiation and simplification of first-order formulas.