Confluence of algebraic rewriting systems
| Autor: | Cyrille Chenavier, Benjamin Dupont, Philippe Malbos |
|---|---|
| Přispěvatelé: | Malbos, Philippe, Johannes Kepler University Linz [Linz] (JKU), Institut Camille Jordan [Villeurbanne] (ICJ), École Centrale de Lyon (ECL), Université de Lyon-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université Jean Monnet [Saint-Étienne] (UJM)-Institut National des Sciences Appliquées de Lyon (INSA Lyon), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS), Algèbre, géométrie, logique (AGL), Université de Lyon-Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Centre National de la Recherche Scientifique (CNRS)-École Centrale de Lyon (ECL) |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
[INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS]
Term rewriting modulo [INFO.INFO-DS] Computer Science [cs]/Data Structures and Algorithms [cs.DS] 0102 computer and information sciences [MATH] Mathematics [math] 01 natural sciences Mathematics (miscellaneous) Computer Science::Logic in Computer Science ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION FOS: Mathematics Category Theory (math.CT) linear rewriting 0101 mathematics [MATH]Mathematics [math] [MATH.MATH-CT]Mathematics [math]/Category Theory [math.CT] [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC] algebraic polygraphs [INFO.INFO-SC] Computer Science [cs]/Symbolic Computation [cs.SC] 010102 general mathematics Mathematics - Category Theory 68Q42 18C10 group rewriting 16. Peace & justice [MATH.MATH-CT] Mathematics [math]/Category Theory [math.CT] string rewriting Computer Science Applications TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Programming Languages |
| Zdroj: | HAL |
| Popis: | Convergent rewriting systems on algebraic structures give methods to solve decision problems, to prove coherence results, and to compute homological invariants. These methods are based on higher-dimensional extensions of the critical branching lemma that proves local confluence from confluence of the critical branchings. The analysis of local confluence of rewriting systems on algebraic structures, such as groups or linear algebras, is complicated because of the underlying algebraic axioms. This article introduces the structure of algebraic polygraph modulo that formalizes the interaction between the rules of an algebraic rewriting system and the inherent algebraic axioms, and we show a critical branching lemma for algebraic polygraphs. We deduce a critical branching lemma for rewriting systems on algebraic models whose axioms are specified by convergent modulo rewriting systems. We illustrate our constructions for string, linear, and group rewriting systems. 29 pages |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|