Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Proving Confluence in the Confluence Framework with CONFident

Raúl Gutiérrez, Salvador Lucas, Miguel Vítores

TL;DR

The confluence framework is described, a novel framework for proving and disproving confluence using a divide-and-conquer modular strategy, and its implementation in CONFident.

Abstract

This article describes the *Confluence Framework*, a novel framework for proving and disproving confluence using a divide-and-conquer modular strategy, and its implementation in CONFident. Using this approach, we are able to automatically prove and disprove confluence of *Generalized Term Rewriting Systems*, where (i) only selected arguments of function symbols can be rewritten and (ii) a rather general class of conditional rules can be used. This includes, as particular cases, several variants of rewrite systems such as (context-sensitive) *term rewriting systems*, *string rewriting systems*, and (context-sensitive) *conditional term rewriting systems*. The divide-and-conquer modular strategy allows us to combine in a proof tree different techniques for proving confluence, including modular decompositions, checking joinability of (conditional) critical and variable pairs, transformations, etc., and auxiliary tasks required by them, e.g., joinability of terms, joinability of conditional pairs, etc.

Proving Confluence in the Confluence Framework with CONFident

TL;DR

The confluence framework is described, a novel framework for proving and disproving confluence using a divide-and-conquer modular strategy, and its implementation in CONFident.

Abstract

This article describes the *Confluence Framework*, a novel framework for proving and disproving confluence using a divide-and-conquer modular strategy, and its implementation in CONFident. Using this approach, we are able to automatically prove and disprove confluence of *Generalized Term Rewriting Systems*, where (i) only selected arguments of function symbols can be rewritten and (ii) a rather general class of conditional rules can be used. This includes, as particular cases, several variants of rewrite systems such as (context-sensitive) *term rewriting systems*, *string rewriting systems*, and (context-sensitive) *conditional term rewriting systems*. The divide-and-conquer modular strategy allows us to combine in a proof tree different techniques for proving confluence, including modular decompositions, checking joinability of (conditional) critical and variable pairs, transformations, etc., and auxiliary tasks required by them, e.g., joinability of terms, joinability of conditional pairs, etc.
Paper Structure (56 sections, 8 theorems, 49 equations, 5 figures, 12 tables)

This paper contains 56 sections, 8 theorems, 49 equations, 5 figures, 12 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Abstract Reduction Relations.
  4. Signatures, Terms, Positions.
  5. Replacement Maps.
  6. Unification.
  7. First-Order Logic.
  8. Feasibility Sequences.
  9. Grounding variables.
  10. Generalized term rewriting systems
  11. Confluence framework
  12. Problems
  13. Processors
  14. Proofs in the confluence framework
  15. List of processors
  16. ...and 41 more sections

Key Result

Theorem 4.6

Let $\mathcal{}\hbox{$\mathcal{R}$}$ be a GTRS and $\mathcal{}\hbox{$\mathcal{T}$}$ be a confluence proof tree for $\mathcal{}\hbox{$\mathcal{R}$}$. Then:

Figures (5)

  • Figure 1: Sentences for different semantics of CS-CTRSs
  • Figure 2: Non-joinability as infeasibility in Example \ref{['ExCOPS_387_CS_CTRS_pCCPs_iCCPs_CVPs_joinability']}
  • Figure 3: Proof trees for confluence problems of CTRSs and CS-CTRSs in the confluence framework
  • Figure 5: Proof strategy for (CS-)TRSs
  • Figure 7: The CS-CTRS $\mathcal{}\hbox{$\mathcal{R}$}_\bot$ in Example \ref{['ExCOPS_387_CS_CTRS']} in COPS (left) and TPDB (right) format

Theorems & Definitions (54)

  • Example 1.1
  • Definition 3.1: Rewriting as deduction
  • Definition 3.2: Confluence and termination of GTRSs
  • Remark 3.3: Confluence and termination of CS-TRSs and CS-CTRSs
  • Definition 3.4: Extended critical pairs of a GTRS, Lucas_LocalConferenceOfConditionalAndGeneralizedTermRewritingSystems_JLAMP24
  • Example 3.5
  • Example 3.6
  • Definition 4.1: Confluence Problems
  • Definition 4.2: Joinability Problems
  • Remark 4.3: Relationship between problems
  • ...and 44 more