Categories, Homotopy and Rewriting – CATHRE

The Cathre project is rooted in the works of Squier, Anick and others on homological properties of presentations of monoids and algebras. Squier showed in particular that if a monoid M can be presented by a finite, confluent and terminating rewriting system, then its third integral homology group H_3(M,Z) is finitely generated as an abelian group. He later refined this result by showing that, under the same hypotheses, M has finite derivation type, a property of homotopical nature. We believe that these are not isolated results, but rather ought to be part of a wide homotopical theory of rewriting, encompassing words, terms, linear combinations of terms, as well as diagrams of various shapes.
The project aims at developing such a theory, together with computational tools based on it, starting from the following two observations:
- all objects of study, such as words, terms or rewriting rules can be expressed very naturally in the language of strict, globular, higher-dimensional categories;
- the category of these higher categories has a non-trivial homotopy structure.
Even in the simple case of monoids, arbitrary high dimensions appear in the process of resolution: the computation of homological or homotopical invariants involves not only 1-dimensional words and 2-dimensional rewriting paths, but also 3-dimensional deformations between paths and so on. Our approach is supported by strong results already obtained in this direction, namely
- the analysis of numerous examples of higher-dimensional rewriting by Yves Guiraud and Philippe Malbos,
- the discovery of a natural model structure on strict higher categories by Yves Lafont, François Métayer and Krzysztof Worytkiewicz.
The Cathre project intends to develop these two lines of research with the aim of implementing a computational system which is able to handle various kinds of algebraic structures and, moreover, to explore three main fields of application
- in symbolic algebra, for computation in algebras and operads,
- in combinatorial group theory, for computation in groups involved in algebra and geometry,
- in term rewriting, for functional programming.