2026-07-22T16:45:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5982 2024-03-06T10:37:26Z ddc:004 open_access

Homological Computations for Term Rewriting Systems Malbos, Philippe Mimram, Samuel term rewriting system Lawvere theory Tietze equivalence resolution homology convergent pres entation coherent presentation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Philippe Malbos and Samuel Mimram 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.27 urn:nbn:de:0030-drops-59821 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.27 eng https://creativecommons.org/licenses/by/3.0/legalcode