Confluence of conditional rewrite systems

Abstract

Conditional rewriting has been studied both from the point of view of algebraic data type specifications and as a computational paradigm combining logic and functional programming. An important issue, in either case, is determining whether a rewrite system has the Church-Rosser, or confluence, property. In this paper, we settle negatively the question whether “joinability of critical pairs” is, in general, sufficient for confluence of terminating conditional systems. We review known sufficient conditions for confluence, and also prove two new positive results for systems having critical pairs and arbitrarily big terms in conditions.