Confluence of Conditional Rewrite Systems

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 "joinabihty 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.

• Type: Conference
• Year: 1987
• Where: CTRS
• Authors: Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar
• Keywords: Conditional Rewriting, Critical Pairs, CTRS 1987, Paradigm Combining Logic, Theoretical Computer Science