Skip to Main content Skip to Navigation
Journal articles

From Diagrammatic Confluence to Modularity

Jean-Pierre Jouannaud 1 Jiaxiang Liu 1 
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
Abstract : 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.
Document type :
Journal articles
Complete list of metadata
Contributor : Jean-Pierre Jouannaud Connect in order to contact the contributor
Submitted on : Saturday, September 8, 2012 - 7:06:00 PM
Last modification on : Friday, February 4, 2022 - 3:08:42 AM

Links full text




Jean-Pierre Jouannaud, Jiaxiang Liu. From Diagrammatic Confluence to Modularity. Theoretical Computer Science, Elsevier, 2012, 9032, ⟨10.1016/j.tcs.2012.08.030⟩. ⟨hal-00730272⟩



Record views