[2025年4月2日投稿（v1）、最終改訂2026年7月30日（本バージョン、v5）]

PDFを表示

要旨:Sets of equations E play an important computational role in rewriting-based systems R. The equivalence relation =E induced by E introduces 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 such a 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. We introduce (i) 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 (ii) parametric Conditional Variable Pairs which are essential to deal with conditional rules in the analysis of E-confluence. Finally, we introduce (iii) Down Conditional Pairs which are often necessary to disprove E-confluence. Our results apply to well-known classes of rewriting-based systems, improving on previous results. As for unconditional systems, our results apply to Equational Term Rewriting Systems, first investigated by Huet and then by Jouannaud, and Jouannaud and Kirchner, among others. As for conditional systems, our results also apply to conditional rewrite theories and Maude.

投稿履歴

投稿者: Salvador Lucas [メールを表示]
[v1] 2025年4月2日 水曜日 15:55:06 UTC (184 KB)
[v2] 2025年4月3日 木曜日 14:25:55 UTC (79 KB)
[v3] 2026年1月31日 土曜日 19:58:23 UTC (123 KB)
[v4] 2026年7月29日 水曜日 15:52:35 UTC (128 KB)
[v5] 2026年7月30日 木曜日 06:03:35 UTC (128 KB)