Confluence by Critical Pair Analysis

Abstract

Knuth and Bendix showed that confluence of a terminating first-order rewrite system can be reduced to the joinability of its finitely many critical pairs. We show that this is still true of a rewrite system ${R_{\textit{T}}} \cup{R_{\textit{NT}}}$ such that $R_{\textit{T}}$ is terminating and $R_{\textit{NT}}$ is a left-linear, rank non-increasing, possibly non-terminating rewrite system. Confluence can then be reduced to the joinability of the critical pairs of $R_{\textit{T}}$ and to the existence of decreasing diagrams for the critical pairs of $R_{\textit{T}}$ inside $R_{\textit{NT}}$ as well as for the rigid parallel critical pairs of $R_{\textit{NT}}$.