Diagram Techniques for Confluence

Abstract

We develop diagram techniques for proving confluence in abstract reductions systems. The underlying theory gives a systematic and uniform framework in which a number of known results, widely scattered throughout the literature, can be understood. These results include Newman's Lemma (1942), Lemma 3.1 of Winkler and Buchberger (1985), the Hindley-Rosen Lemma (1964), the Request Lemmas of Staples (1975), the Strong Confluence Lemma of Huet (1980) and the Lemma of De Bruijn (1978).