Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Nominal Equational Narrowing: Rewriting for Unification in Languages with Binders

Maribel Fernández, Daniele Nantes-Sobrinho, Daniella Santaguida

TL;DR

The paper presents a framework for nominal rewriting and narrowing modulo equational theories to reason about languages with binders, freshness constraints, and structural axioms. Central contributions include the nominal $\\mathcal{E}$-coherence property, the nominal $\\mathcal{E}$-lifting theorem linking rewriting and narrowing, and a correctness proof for a unification procedure based on closed nominal narrowing (RuE-unification). It also develops basic closed narrowing results and demonstrates the approach via a symbolic differentiation example under commutativity, while candidly addressing termination and finiteness limitations and outlining directions for future work. The work advances practical unification and reasoning in nominal settings, enabling applications in programming languages and theorem proving where reasoning modulo renaming and equational axioms is essential.

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.

Nominal Equational Narrowing: Rewriting for Unification in Languages with Binders

TL;DR

The paper presents a framework for nominal rewriting and narrowing modulo equational theories to reason about languages with binders, freshness constraints, and structural axioms. Central contributions include the nominal -coherence property, the nominal -lifting theorem linking rewriting and narrowing, and a correctness proof for a unification procedure based on closed nominal narrowing (RuE-unification). It also develops basic closed narrowing results and demonstrates the approach via a symbolic differentiation example under commutativity, while candidly addressing termination and finiteness limitations and outlining directions for future work. The work advances practical unification and reasoning in nominal settings, enabling applications in programming languages and theorem proving where reasoning modulo renaming and equational axioms is essential.

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.

Paper Structure

This paper contains 27 sections, 17 theorems, 37 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Nominal Equational Reasoning At a Glance
  3. Nominal Equational Reasoning
  4. Nominal Rewriting
  5. Nominal Rewriting Modulo a Theory
  6. Unification Modulo a Theory via Closed Narrowing
  7. Refinements and Challenges
  8. Organisation of the paper
  9. Preliminaries
  10. Nominal Syntax
  11. Nominal Constraints and Judgements
  12. Equality Modulo an Equational Theory $\mathcal{E}$
  13. Nominal $\mathcal{E}$-unification
  14. Nominal Rewriting Modulo Theories
  15. Closed Rewriting Modulo Theories
  16. ...and 12 more sections

Key Result

Proposition 1

Equational theories are compatible with substitutions, that is, whenever $\langle \Delta\theta\rangle_{nf}$ exists, if $\Delta \vdash Pr$ then $\langle \Delta\theta\rangle_{nf} \vdash Pr\theta$.

Figures (6)

  • Figure 1: This work: nominal rewriting modulo theories
  • Figure 2: Rules for $\#$ and $\approx_{\alpha}$
  • Figure 3: Infinitely branching tree
  • Figure 4: Corresponding Narrowing to Rewriting Derivations
  • Figure 5: $\mathcal{R}_\mathit{diff}$ -- Rules for Symbolic Differentiation Modulo Commutativity
  • ...and 1 more figures

Theorems & Definitions (56)

  • Example 1
  • Example 2
  • Example 3
  • Proposition 1: $\mathcal{E}$-Compatibility with substitutions
  • Lemma 1
  • Definition 1
  • Example 4
  • Definition 2: Nominal $\mathcal{R/E}$-rewriting
  • Example 5: Prenex normal form rules
  • Definition 3: Nominal $\mathcal{R,E}$-rewriting
  • ...and 46 more