License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.27
URN: urn:nbn:de:0030-drops-59821
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/5982/
Go to the corresponding LIPIcs Volume Portal

Malbos, Philippe ; Mimram, Samuel

Homological Computations for Term Rewriting Systems

pdf-format:
LIPIcs-FSCD-2016-27.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{malbos_et_al:LIPIcs:2016:5982,
  author =	{Philippe Malbos and Samuel Mimram},
  title =	{{Homological Computations for Term Rewriting Systems}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{27:1--27:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/5982},
  URN =		{urn:nbn:de:0030-drops-59821},
  doi =		{10.4230/LIPIcs.FSCD.2016.27},
  annote =	{Keywords: term rewriting system, Lawvere theory, Tietze equivalence, resolution, homology, convergent pres entation, coherent presentation}
}

Keywords: term rewriting system, Lawvere theory, Tietze equivalence, resolution, homology, convergent pres entation, coherent presentation
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI