Confluence of Conditional Rewriting Modulo

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. In this realm, our E-confluence results strictly subsume previous approaches by Huet and Jouannaud and Kirchner.