A cubical Squier's theorem

TL;DR

This paper introduces a cubical framework for rewriting systems, extending Squier's theorem to cubical categories, aiming to simplify the construction of polygraphic resolutions for monoids.

Contribution

It defines (2,k)-cubical categories, adapts rewriting notions to this setting, and proves a cubical version of Squier's theorem, advancing the theoretical foundation.

Findings

Defined (2,k)-cubical categories.

Adapted classical rewriting notions to cubical categories.

Proved a cubical version of Squier's theorem.

Abstract

Convergent rewriting systems are well-known tools in the study of the word-rewriting problem. In particular, a presentation of a monoid by a finite convergent rewriting system gives an algorithm to decide the word problem for this monoid. Squier proved that there exists a finitely presented monoid whose word problem was decidable but which did not admit a finite convergent presentation. To do so, Squier constructed, for any convergent presentation $(G,R)$ of a monoid $M$, a set of syzygies $S$ corresponding to relations between the relations. This construction was later extended into the construction of a polygraphic resolution $\Sigma$ of $M$, whose first dimensions coincide with Squier's construction $(G,R,S)$. However, the construction of the polygraphic resolution has proved to be too complicated to be effectively computed on non-trivial examples. Cubical categories appear to be a promising framework where Squier's theorem and the construction of the polygraphic resolution would be more straightforward. This paper is the first step towards this goal. We start by defining the notion of $(2,k)$-cubical categories. We then adapt some classical notions of word rewriting to this cubical setting. Finally, we express and prove a cubical version of Squier's theorem.