Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compositional Confluence Criteria

Kiraku Shintani, Nao Hirokawa

TL;DR

This work addresses the problem of confluence analysis for term rewrite systems by introducing compositional criteria derived from decreasing diagrams. It develops compositional versions of key criteria—orthogonality, rule labeling, and critical-pair systems—and adds a reduction method to prune rules while preserving confluence, enabling modular reasoning. The authors show that Toyama's parallel closedness theorems are subsumed by parallel critical-pair reasoning and provide a concrete automation pipeline combining ARS decompositions, labeling, and CPS-based checks. An empirical evaluation on 462 left-linear TRSs demonstrates improved proof power and practical potential for modular, automated confluence analysis, highlighting the framework's utility for reducing and combining confluence proofs.

Abstract

We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. We also show how such a criterion can be used for a reduction method that removes rewrite rules unnecessary for confluence analysis. In addition to them, we prove that Toyama's parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem.

Compositional Confluence Criteria

TL;DR

This work addresses the problem of confluence analysis for term rewrite systems by introducing compositional criteria derived from decreasing diagrams. It develops compositional versions of key criteria—orthogonality, rule labeling, and critical-pair systems—and adds a reduction method to prune rules while preserving confluence, enabling modular reasoning. The authors show that Toyama's parallel closedness theorems are subsumed by parallel critical-pair reasoning and provide a concrete automation pipeline combining ARS decompositions, labeling, and CPS-based checks. An empirical evaluation on 462 left-linear TRSs demonstrates improved proof power and practical potential for modular, automated confluence analysis, highlighting the framework's utility for reducing and combining confluence proofs.

Abstract

We show how confluence criteria based on decreasing diagrams are generalized to ones composable with other criteria. For demonstration of the method, the confluence criteria of orthogonality, rule labeling, and critical pair systems for term rewriting are recast into composable forms. We also show how such a criterion can be used for a reduction method that removes rewrite rules unnecessary for confluence analysis. In addition to them, we prove that Toyama's parallel closedness result based on parallel critical pairs subsumes his almost parallel closedness theorem.
Paper Structure (10 sections, 27 theorems, 40 equations, 3 figures, 1 table)

This paper contains 10 sections, 27 theorems, 40 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Parallel Closedness
  4. Decreasing Diagrams with Commuting Subsystems
  5. Orthogonality
  6. Rule Labeling
  7. Critical Pair Systems
  8. Reduction Method
  9. Experiments
  10. Conclusion

Key Result

Theorem 2.2

A TRS $\mathcal{R}$ is locally confluent if and only if ${\mathrel{{_{\mathcal{R}}{\xleftarrow{}}{\rtimes}{\xrightarrow{\epsilon}_{\mathcal{R}}}}}} \subseteq {\to^*_\mathcal{R} \cdot \mathrel{\prescript{*}{\mathcal{R}}{\mathrel{\leftarrow}}}}$ holds.

Figures (3)

  • Figure 1: The claims of \ref{['lem:PML']}.
  • Figure 2: Proof of Theorem \ref{['thm:SH22a']} (\ref{['SH22a_fig_case']}).
  • Figure 3: Proof of Theorem \ref{['thm:prlc']}(\ref{['prlc_fig_case']}).

Theorems & Definitions (60)

  • Definition 2.1
  • Theorem 2.2: H80
  • Theorem 2.3: KB70
  • Definition 2.4
  • Lemma 2.5
  • Definition 3.1: H80
  • Theorem 3.2: H80
  • Definition 3.3: T88
  • Theorem 3.4: T88
  • Example 3.5
  • ...and 50 more