Homological Computations for Term Rewriting Systems

Authors Philippe Malbos, Samuel Mimram

Thumbnail PDF


  • Filesize: 0.49 MB
  • 17 pages

Document Identifiers

Author Details

Philippe Malbos
Samuel Mimram

Cite AsGet BibTex

Philippe Malbos and Samuel Mimram. Homological Computations for Term Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)


An important problem in universal algebra consists in finding presentations of algebraic theories by generators and relations, which are as small as possible. Exhibiting lower bounds on the number of those generators and relations for a given theory is a difficult task because it a priori requires considering all possible sets of generators for a theory and no general method exists. In this article, we explain how homological computations can provide such lower bounds, in a systematic way, and show how to actually compute those in the case where a presentation of the theory by a convergent rewriting system is known. We also introduce the notion of coherent presentation of a theory in order to consider finer homotopical invariants. In some aspects, this work generalizes, to term rewriting systems, Squier's celebrated homological and homotopical invariants for string rewriting systems.
  • term rewriting system
  • Lawvere theory
  • Tietze equivalence
  • resolution
  • homology
  • convergent pres entation
  • coherent presentation


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Jiří Adámek and Jiří Rosicky. Locally presentable and accessible categories, volume 189. Cambridge University Press, 1994. Google Scholar
  2. Michael Barr. Cartan-Eilenberg cohomology and triples. Journal of Pure and Applied Algebra, 112(3):219-238, 1996. Google Scholar
  3. Jonathan Mock Beck. Triples, algebras and cohomology. PhD thesis, Columbia Univ, 1967. Google Scholar
  4. Albert Burroni. Higher-dimensional word problems with applications to equational logic. Theoretical computer science, 115(1):43-62, 1993. Google Scholar
  5. Yves Guiraud, Philippe Malbos, and Samuel Mimram. A homotopical completion procedure with applications to coherence of monoids. In RTA, volume 21, pages 223-238. Dagstuhl, 2013. Google Scholar
  6. Allen Hatcher. Algebraic Topology. Cambridge University Press, 2002. Google Scholar
  7. Graham Higman and B. H. Neumann. Groups as groupoids with one law. Publicationes Mathematicae Debrecen, 2(215-227):228, 1952. Google Scholar
  8. Mamuka Jibladze and Teimuraz Pirashvili. Cohomology of algebraic theories. Journal of Algebra, 137(2):253-296, 1991. Google Scholar
  9. Mamuka Jibladze and Teimuraz Pirashvili. Quillen cohomology and Baues-Wirsching cohomology of algebraic theories. Cahiers de top. et géom. diff. cat., 47(3):163-205, 2006. Google Scholar
  10. Donald E Knuth and Peter B Bendix. Simple word problems in universal algebras. In Automation of Reasoning, pages 342-376. Springer, 1983. Google Scholar
  11. Yuji Kobayashi. Complete rewriting systems and homology of monoid algebras. Journal of Pure and Applied Algebra, 65(3):263-275, 1990. Google Scholar
  12. Yves Lafont and Alain Prouté. Church-rooser property and homology of monoids. Mathematical Structures in Computer Science, 1(03):297-326, 1991. Google Scholar
  13. F William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences of the United States of America, 50(5):869, 1963. Google Scholar
  14. Jean-Louis Loday and Bruno Vallette. Algebraic operads, volume 346 of Grundlehren der Mathematischen Wissenschaften. Springer, Heidelberg, 2012. Google Scholar
  15. Saunders Mac Lane. Homology. Springer-Verlag, Berlin, 1995. Google Scholar
  16. Philippe Malbos. Critères de finitude homologique pour la non convergence des systèmes de réécriture de termes. PhD thesis, Université de Montpellier II, 2004. Google Scholar
  17. William Mccune et al. Single Axioms: With and Without Computers. In Computer Mathematics: Proceedings of the Fourth Asian Symposium (ASCM 2000), page 83. World Scientific, 2000. Google Scholar
  18. William McCune, Ranganathan Padmanabhan, and Robert Veroff. Yet another single law for lattices. Algebra Universalis, 50(2):165-169, 2003. Google Scholar
  19. William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist, and Larry Wos. Short single axioms for Boolean algebra. Journal of Automated Reasoning, 29(1):1-16, 2002. Google Scholar
  20. Ralph McKenzie. Equational Bases for Lattice Theories. Math. Scandinavica, 27:24-38, 1970. Google Scholar
  21. Paul-André Melliès. Axiomatic rewriting theory VI: Residual theory revisited. In Rewriting techniques and applications, pages 24-50. Springer, 2002. Google Scholar
  22. Barry Mitchell. Rings with several objects. Advances in Mathematics, 8(1):1-161, 1972. Google Scholar
  23. B. H. Neumann et al. Yet another single law for groups. Illinois Journal of Mathematics, 30(2):295-300, 1986. Google Scholar
  24. Bernhard Hermann Neumann. Another single law for groups. Bulletin of the Australian Mathematical Society, 23(01):81-102, 1981. Google Scholar
  25. Maxwell Herman Alexander Newman. On theories with a combinatorial definition of "equivalence". Annals of mathematics, pages 223-243, 1942. Google Scholar
  26. R Padmanabhan and RW Quackenbush. Equational theories of algebras with distributive congruences. Proceedings of the American Mathematical Society, 41(2):373-377, 1973. Google Scholar
  27. DH Potts. Axioms for semi-lattices. Canad. Math Bulletin, 8:519, 1965. Google Scholar
  28. Craig Squier and Friedrich Otto. The word problem for finitely presented monoids and finite canonical rewriting systems. In Rewriting Techniques and Applications, pages 74-82. Springer, 1987. Google Scholar
  29. Craig C Squier, Friedrich Otto, and Yuji Kobayashi. A finiteness condition for rewriting systems. Theoretical Computer Science, 131(2):271-294, 1994. Google Scholar
  30. Alfred Tarski. Ein Beitrag zur Axiomatik der Abelschen Gruppen. Fundamenta Mathematicae, 1(30):253-256, 1938. Google Scholar
  31. Heinrich Tietze. Über die topologischen Invarianten mehrdimensionaler Mannigfaltigkeiten. Monatsh. Math. Phys., 19(1):1-118, 1908. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail