A cubical Squier's theorem

DOI10.1017/S0960129520000018zbMATH Open1436.18022OpenAlexW3004734796MaRDI QIDQ5220186FDOQ5220186

Authors: Maxime Lucas 

Publication date: 11 March 2020

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1612.06541

Recommendations

• Polygraphs of finite derivation type
• On some homotopical and homological properties of monoid presentations.
• scientific article; zbMATH DE number 4210420
• A new finiteness condition for monoids presented by complete rewriting systems (after Craig C. Squier)
• Higher-dimensional normalisation strategies for acyclicity

zbMATH Keywords

coherencerewritingcubical categories

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Sets with a single binary operation (groupoids) (20N02) Abstract and axiomatic homotopy theory in algebraic topology (55U35) Strict omega-categories, computads, polygraphs (18N30)

Cites Work

• Polygraphs of finite derivation type
• The algebra of oriented simplexes
• On the algebra of cubes
• Multiple categories: The equivalence of a globular and a cubical approach
• Limits indexed by category-valued 2-functors
• Word problems and a homological finiteness condition for monoids
• A finiteness condition for rewriting systems
• Higher-dimensional normalisation strategies for acyclicity
• Higher-dimensional word problems with applications to equational logic
• Coherence in monoidal track categories
• A coherence theorem for pseudonatural transformations
• Title not available (Why is that?)
• Title not available (Why is that?)
• Homomorphisms of higher categories
• Title not available (Why is that?)
• Title not available (Why is that?)
• Cubical \((\omega, p)\)-categories

Cited In (3)

• Cubical \((\omega, p)\)-categories
• Single-set cubical categories and their formalisation with a proof assistant
• An effective seven cube theorem

This page was built for publication: A cubical Squier's theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5220186)