Hostname: page-component-78c5997874-v9fdk Total loading time: 0 Render date: 2024-11-06T08:21:38.583Z Has data issue: false hasContentIssue false
  • English
  • Français

Confluence of algebraic rewriting systems

Published online by Cambridge University Press:  10 December 2021

Cyrille Chenavier ,
Benjamin Dupont Open the ORCID record for Benjamin Dupont [Opens in a new window]  and
Philippe Malbos Open the ORCID record for Philippe Malbos [Opens in a new window]
Cyrille Chenavier
Affiliation:
Johannes Kepler University Altenberger Straße 69 A-4040 Linz, Austria
Benjamin Dupont*
Affiliation:
Univ Lyon, Université Claude Bernard Lyon 1 CNRS UMR 5208, Institut Camille Jordan 43 blvd. du 11 novembre 1918 F-69622 Villeurbanne cedex, France
Philippe Malbos
Affiliation:
Univ Lyon, Université Claude Bernard Lyon 1 CNRS UMR 5208, Institut Camille Jordan 43 blvd. du 11 novembre 1918 F-69622 Villeurbanne cedex, France
*
*Corresponding author. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Keywords

Term rewriting moduloalgebraic polygraphsstring rewritinglinear rewritinggroup rewriting
Type
Special Issue: Confluence
Information
Mathematical Structures in Computer Science , Volume 32 , Special Issue 7: Confluence , August 2022 , pp. 870 - 897
Check for updates
Copyright
© The Author(s), 2021. Published by Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Anick, D. J. (1986). On the homology of associative algebras. Transactions of the American Mathematical Society 296 (2) 641–659.CrossRefGoogle Scholar
Bachmair, L. and Dershowitz, N. (1989). Completion for rewriting modulo a congruence. Theoretical Computer Science 67 (2) 173–201.CrossRefGoogle Scholar
Bergman, G. M. (1978). The diamond lemma for ring theory. Advances in Mathematics 29(2) 178–218.CrossRefGoogle Scholar
Buchberger, B. (1965). Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal (An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo a Zero Dimensional Polynomial Ideal). PhD thesis, Mathematical Institute, University of Innsbruck, Austria. English translation in Journal of Symbolic Computation, Special Issue on Logic, Mathematics, and Computer Science: Interactions 41 (3–4) 475–511 (2006).Google Scholar
Buchberger, B. (1987). History and basic features of the critical-pair/completion procedure. Journal of Symbolic Computation 3 (1–2) 3–38. Rewriting techniques and applications (Dijon, 1985).CrossRefGoogle Scholar
Chouraqui, F. (2009). Rewriting systems and embedding of monoids in groups. Groups, Complexity, Cryptology 1 (1) 131–140.CrossRefGoogle Scholar
Chouraqui, F. (2011). The Knuth-Bendix algorithm and the conjugacy problem in monoids. Semigroup Forum 82 (1) 181–196.CrossRefGoogle Scholar
Cremanns, R. and Otto, F. (1996). For groups the property of having finite derivation type is equivalent to the homological finiteness condition FP3 . Journal of Symbolic Computation 22 (2) 155–177.CrossRefGoogle Scholar
Curien, P.-L., Duric, A. and Guiraud, Y. (2021). Coherent presentations of a class of monoids admitting a garside family. arXiv 2107.00498.Google Scholar
Curien, P.-L. and Mimram, S. (2017). Coherent presentations of monoidal categories. Logical Methods in Computer Science 13 (3): Paper No. 31, 38.Google Scholar
Diekert, V., Duncan, A. and Myasnikov, A. G. (2012). Cyclic rewriting and conjugacy problems. Groups, Complexity, Cryptology 4 (2) 321–355.CrossRefGoogle Scholar
Diekert, V., Duncan, A. J. and Myasnikov, A. G. (2010). Geodesic rewriting systems and pregroups. In: Combinatorial and Geometric Group Theory, Trends Math. Birkhäuser/Springer Basel AG, 55–91.CrossRefGoogle Scholar
Dotsenko, V. and Khoroshkin, A. (2010). Gröbner bases for operads. Duke Mathematical Journal 153 (2) 363–396.CrossRefGoogle Scholar
Dupont, B. and Malbos, P. (2018). Coherent confluence modulo relations and double groupoids. preprint arXiv:1810.08184, Hal-01898868.Google Scholar
Gaussent, S., Guiraud, Y. and Malbos, P. (2015). Coherent presentations of Artin monoids. Compositio Mathematica 151 (5) 957–998.CrossRefGoogle Scholar
Guiraud, Y., Hoffbeck, E. and Malbos, P. (2019). Convergent presentations and polygraphic resolutions of associative algebras. Mathematische Zeitschrift 293 (1–2) 113–179.CrossRefGoogle Scholar
Guiraud, Y. and Malbos, P. (2009). Higher-dimensional categories with finite derivation type. Theory and Applications of Categories 22 (18) 420–478.Google Scholar
Guiraud, Y. and Malbos, P. (2012). Coherence in monoidal track categories. Mathematical Structures in Computer Science 22 (6) 931–969.CrossRefGoogle Scholar
Guiraud, Y. and Malbos, P. (2012). Higher-dimensional normalisation strategies for acyclicity. Advances in Mathematics 231 (3–4) 2294–2351.CrossRefGoogle Scholar
Guiraud, Y. and Malbos, P. (2018). Polygraphs of finite derivation type. Mathematical Structures in Computer Science 28 (2) 155–201.CrossRefGoogle Scholar
Heyworth, A. and Wensley, C. D. (2003). Logged rewriting and identities among relators. In: Groups St. Andrews 2001 in Oxford. Vol. I, vol. 304. London Math. Soc. Lecture Note Ser. Cambridge Univ. Press, 256–276.CrossRefGoogle Scholar
Huet, G. (1980). Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the Association for Computing Machinery 27 (4) 797–821.CrossRefGoogle Scholar
Hullot, J.-M. (1980). A catalogue of canonical term rewriting systems. SRI International, Technical Report CSL 113.CrossRefGoogle Scholar
Iohara, K. and Malbos, P. (2020). Maurice Janet’s algorithms on systems of linear partial differential equations. Archive for History of Exact Sciences. Springer, to appear.Google Scholar
Janet, M. (1920). Sur les systèmes d’équations aux dérivées partielles. Journal de mathématiques pures et appliquées 8 (3) 65–151.Google Scholar
Jouannaud, J.-P. and Kirchner, H. (1984). Completion of a set of rules modulo a set of equations. In: Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’84. ACM, 83–92.CrossRefGoogle Scholar
Jouannaud, J.-P. and Li, J. (2012). Church-Rosser properties of normal rewriting. In: Computer Science Logic 2012, vol. 16. LIPIcs. Leibniz Int. Proc. Inform. Schloss Dagstuhl. Leibniz-Zent. Inform., 350–365.Google Scholar
Jouannaud, J.-P. and Muñoz, M. (1984). Termination of a set of rules modulo a set of equations. In: 7th International Conference on Automated Deduction (Napa, Calif., 1984), vol. 170. Lecture Notes in Computer Science. Springer, 175–193.Google Scholar
Knuth, D. and Bendix, P. (1970). Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra (Proc. Conf., Oxford, 1967). Pergamon, 263–297.Google Scholar
Kobayashi, Y. (1990). Complete rewriting systems and homology of monoid algebras. Journal of Pure and Applied Algebra 65 (3) 263–275.CrossRefGoogle Scholar
Lafont, Y. (1995). A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier). Journal of Pure and Applied Algebra 98 (3) 229–244.CrossRefGoogle Scholar
Lawvere, F. W. (1963). Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America 50 869–872.CrossRefGoogle Scholar
Le Chenadec, P. (1984). Canonical forms in finitely presented algebras. In: Shostak, R. E. (ed.) 7th International Conference on Automated Deduction, New York, NY. Springer, 142–165.CrossRefGoogle Scholar
Le Chenadec, P. (1986). A catalogue of complete group presentations. Journal of Symbolic Computation 2 (4) 363–381.CrossRefGoogle Scholar
Malbos, P. and Mimram, S. (2016). Homological computations for term rewriting systems. In: 1st International Conference on Formal Structures for Computation and Deduction, vol. 52. LIPIcs. Leibniz Int. Proc. Inform., pages Art. No. 27, 17. Schloss Dagstuhl. Leibniz-Zent. Inform.Google Scholar
Malbos, P. and Mimram, S. (2021). Cartesian polygraphic resolutions. en préparation.Google Scholar
Malbos, P. and Ren, I. (2020). Shuffle polygraphic resolutions for operads. submitted preprint, arXiv:2012.15718.Google Scholar
Malbos, P. and Ren, I. (2021). Completion in operads via essential syzygies. In: Proceedings of the 46th International Symposium on Symbolic and Algebraic Computation, ISSAC ’21. Association for Computing Machinery.Google Scholar
Marché, C. (1993). Réécriture modulo une théorie présentée par un système convergent et décidabilité des problèmes du mot dans certaines classes de théories equationnelles. PhD thesis. 1993PA112312.Google Scholar
Marché, C. (1996). Normalized rewriting: An alternative to rewriting modulo a set of equations. Journal of Symbolic Computation 21 (3) 253–288.CrossRefGoogle Scholar
Mimram, S. (2010). Computing critical pairs in 2-dimensional rewriting systems. In: RTA 2010: Proceedings of the 21st International Conference on Rewriting Techniques and Applications, vol. 6. LIPIcs. Leibniz Int. Proc. Inform. Schloss Dagstuhl. Leibniz-Zent. Inform., 227–241.Google Scholar
Nivat, M. (1973). Congruences parfaites et quasi-parfaites. In: Séminaire P. Dubreil, 25e année (1971/72), Algèbre, Fasc. 1, Exp. No. 7, p. 9. Secrétariat Mathématique, 1973.Google Scholar
Peterson, G.E. and Stickel, M.E. (1981). Complete sets of reductions for some equational theories. Journal of the Association for Computing Machinery 28 (2) 233–264.CrossRefGoogle Scholar
Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery 12 23–41.CrossRefGoogle Scholar
Shirshov, A. I. (1962) Some algorithmic problems for Lie algebras. Sib. Mat. Zh. 3 292–296.Google Scholar
Squier, C. C. (1987). Word problems and a homological finiteness condition for monoids. Journal of Pure and Applied Algebra 49 (1–2) 201–217.CrossRefGoogle Scholar
Squier, C. C., Otto, F. and Kobayashi, Y. (1994). A finiteness condition for rewriting systems. Theoretical Computer Science 131 (2) 271–294.CrossRefGoogle Scholar
Terese. (2003). Term Rewriting Systems, vol. 55. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.Google Scholar
Viry, P. (1995). Rewriting modulo a rewrite system. Technical report.Google Scholar