Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Confluence of Conditional Rewriting Modulo

Salvador Lucas

TL;DR

This work develops Equational Generalized Term Rewriting Systems (EGTRSs) to study confluence modulo a set of equations E in the presence of conditional rules. It extends Jouannaud and Kirchner's abstract framework by introducing novel constructs—Logic-based Conditional Critical Pairs (LCCPs), parametric Conditional Variable Pairs (CVPs), and Down Conditional Pairs (DCPs)—that avoid reliance on potentially infinite E-unifiers. The authors provide sufficient criteria for E-confluence via joinability of multiple peak families (R-peaks, PS-r/PS-c peaks) and demonstrate how these criteria apply to EGTRSs and equational TRSs, including left-linear cases. They also outline procedures to disprove E-confluence and discuss practical computation via first-order theories and model generators, with implications for verification of rewriting-based specifications. The work paves the way for practical confluence reasoning in sophisticated conditional and equational rewrite theories and identifies future work on termination proof strategies and tooling support.

Abstract

Sets of equations E play an important computational role in rewriting-based systems R by defining an equivalence relation =E inducing a partition of terms into E-equivalence classes on which rewriting computations, denoted ->R/E and called *rewriting modulo E*, are issued. This paper investigates *confluence of ->R/E*, usually called *E-confluence*, for *conditional* rewriting-based systems, where rewriting steps are determined by conditional rules. We rely on Jouannaud and Kirchner's framework to investigate confluence of an abstract relation R modulo an abstract equivalence relation E on a set A. We show how to particularize the framework to be used with conditional systems. Then, we show how to define appropriate finite sets of *conditional pairs* to prove and disprove E-confluence. In particular, we introduce *Logic-based Conditional Critical Pairs* which do not require the use of (often infinitely many) E-unifiers to provide a finite representation of the *local peaks* considered in the abstract framework. We also introduce *parametric Conditional Variable Pairs* which are essential to deal with conditional rules in the analysis of E-confluence. Our results apply to well-known classes of rewriting-based systems. In particular, to *Equational (Conditional) Term Rewriting Systems*.

Confluence of Conditional Rewriting Modulo

TL;DR

This work develops Equational Generalized Term Rewriting Systems (EGTRSs) to study confluence modulo a set of equations E in the presence of conditional rules. It extends Jouannaud and Kirchner's abstract framework by introducing novel constructs—Logic-based Conditional Critical Pairs (LCCPs), parametric Conditional Variable Pairs (CVPs), and Down Conditional Pairs (DCPs)—that avoid reliance on potentially infinite E-unifiers. The authors provide sufficient criteria for E-confluence via joinability of multiple peak families (R-peaks, PS-r/PS-c peaks) and demonstrate how these criteria apply to EGTRSs and equational TRSs, including left-linear cases. They also outline procedures to disprove E-confluence and discuss practical computation via first-order theories and model generators, with implications for verification of rewriting-based specifications. The work paves the way for practical confluence reasoning in sophisticated conditional and equational rewrite theories and identifies future work on termination proof strategies and tooling support.

Abstract

Sets of equations E play an important computational role in rewriting-based systems R by defining an equivalence relation =E inducing a partition of terms into E-equivalence classes on which rewriting computations, denoted ->R/E and called *rewriting modulo E*, are issued. This paper investigates *confluence of ->R/E*, usually called *E-confluence*, for *conditional* rewriting-based systems, where rewriting steps are determined by conditional rules. We rely on Jouannaud and Kirchner's framework to investigate confluence of an abstract relation R modulo an abstract equivalence relation E on a set A. We show how to particularize the framework to be used with conditional systems. Then, we show how to define appropriate finite sets of *conditional pairs* to prove and disprove E-confluence. In particular, we introduce *Logic-based Conditional Critical Pairs* which do not require the use of (often infinitely many) E-unifiers to provide a finite representation of the *local peaks* considered in the abstract framework. We also introduce *parametric Conditional Variable Pairs* which are essential to deal with conditional rules in the analysis of E-confluence. Our results apply to well-known classes of rewriting-based systems. In particular, to *Equational (Conditional) Term Rewriting Systems*.

Paper Structure

This paper contains 53 sections, 37 theorems, 90 equations, 15 figures, 7 tables.

Table of Contents

  1. Introduction
  2. Rewriting with conditional systems
  3. Critical pairs in the analysis of rewriting modulo
  4. Plan and contributions of the paper
  5. Preliminaries
  6. Peaks and joins in abstract reduction
  7. Jouannaud and Kirchner's abstract approach to confluence of $\mathsf{R}/\mathsf{E}$
  8. Basic notions
  9. Church-Rosser and confluence properties
  10. Local confluence and local coherence properties
  11. Proving and disproving $\mathsf{E}$-confluence of $\mathsf{R}$
  12. Huet's approach vs. Jouannaud and Kirchner's
  13. Discussion
  14. Equational Generalized Term Rewriting Systems
  15. First-order theory of an EGTRS
  16. ...and 38 more sections

Key Result

Proposition 1

Let $\mathsf{R},\mathsf{R}',\mathsf{S},\mathsf{S}'$ be relations on $A$. If $\mathsf{R}\subseteq\mathsf{R}'$ and $\mathsf{S}\subseteq\mathsf{S}'$, then ${{}_{\mathsf{R}}\!\!\Uparrow_{\mathsf{S}}}\subseteq {{}_{\mathsf{R}'}\!\!\Uparrow_{\mathsf{S}'}}$, ${J({{{}_{\mathsf{R}}\!\!\Downarrow_{\mathsf{S}}

Figures (15)

  • Figure 1: $E$-confluence
  • Figure 2: $\mathsf{R}$ Church-Rosser modulo $\mathsf{E}$ and $\mathsf{R}$ confluent modulo $\mathsf{E}$ in JouKir_CompletionOfASetOfRulesModuloASetOfEquations_SIAMJC86
  • Figure 3: $\mathsf{R}$ is $\mathsf{R}^{\mathsf{E}}$-Church-Rosser modulo $\mathsf{E}$ ($1^{st}$ diagram in JouKir_CompletionOfASetOfRulesModuloASetOfEquations_SIAMJC86)
  • Figure 4: $\mathsf{R}$ is $\mathsf{R}^{\mathsf{E}}$-Church-Rosser modulo $\mathsf{E}$ for $\mathsf{R}^{\mathsf{E}}$ terminating
  • Figure 5: Confluence and coherence properties: $3^{rd}$ and $5^{th}$ diagrams in JouKir_CompletionOfASetOfRulesModuloASetOfEquations_SIAMJC86
  • ...and 10 more figures

Theorems & Definitions (125)

  • Example 1
  • Definition 1
  • Proposition 1
  • Definition 2
  • Definition 3: Joinability modulo
  • Definition 4: $\mathsf{R}^{\mathsf{E}}$-Church-Rosser modulo $\mathsf{E}$
  • Proposition 2
  • proof
  • Definition 5: Right-strict joinability modulo
  • Definition 6: Local confluence and local coherence
  • ...and 115 more