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.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2012, 9032, 〈10.1016/j.tcs.2012.08.030〉
Liste complète des métadonnées
Contributeur : Jean-Pierre Jouannaud <>
Soumis le : samedi 8 septembre 2012 - 19:06:00
Dernière modification le : mardi 17 avril 2018 - 11:48:04

Lien texte intégral




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〉



Consultations de la notice