1. From diagrammatic confluence to modularity
- Author
-
Jiaxiang Liu, Jean-Pierre Jouannaud, Formal Methods for Embedded Systems (FORMES), Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées (LIAMA), Centre de Coopération Internationale en Recherche Agronomique pour le Développement (Cirad)-Institut National de la Recherche Agronomique (INRA)-Chinese Academy of Sciences [Changchun Branch] (CAS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institute of Automation - Chinese Academy of Sciences-Centre National de la Recherche Scientifique (CNRS)-Centre de Coopération Internationale en Recherche Agronomique pour le Développement (Cirad)-Institut National de la Recherche Agronomique (INRA)-Chinese Academy of Sciences [Changchun Branch] (CAS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Institute of Automation - Chinese Academy of Sciences-Centre National de la Recherche Scientifique (CNRS)-Inria Paris-Rocquencourt, and Institut National de Recherche en Informatique et en Automatique (Inria)
- Subjects
General Computer Science ,Modulo ,Mathematics::General Topology ,0102 computer and information sciences ,02 engineering and technology ,Characterization (mathematics) ,Modularity theorem ,01 natural sciences ,Theoretical Computer Science ,localcliffs ,Computer Science::Logic in Computer Science ,0202 electrical engineering, electronic engineering, information engineering ,modularity ,Mathematics ,Modularity (networks) ,decreasing diagrams ,rewritingmodulo ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,localpeaks ,cofinal derivations ,ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.2: Grammars and Other Rewriting Systems/F.4.2.0: Decision problems ,Algebra ,Diagrammatic reasoning ,Mathematics::Logic ,Cofinal ,010201 computation theory & mathematics ,Confluence ,confluence ,Computer Science::Programming Languages ,020201 artificial intelligence & image processing ,Rewriting ,Computer Science(all) - Abstract
International audience; 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.
- Published
- 2012
- Full Text
- View/download PDF