From diagrammatic confluence to modularity

This paper builds on a fundamental notion of rewriting theory that characterizes confluence of a (binary) rewriting relation, Klop’s cofinal derivations. Cofinal derivations were used by van Oostrom to obtain another characterization of confluence of a rewriting relation via the existence of decreasing diagrams for all local peaks. In this paper, we show that cofinal derivations can be used to give a new, concise proof of Toyama’s celebrated modularity theorem and its recent extensions to rewriting modulo in the case of strongly-coherent systems, an assumption discussed in depth here. This is done by generalizing cofinal derivations to cofinal streams, allowing us in turn to generalize van Oostrom’s result to the modulo case.