Table of Contents
Fetching ...

Rewriting Systems on Arbitrary Monoids

Eduardo Magalhães

TL;DR

This work develops Monoidal Rewriting Systems (MRS) to rewrite over arbitrary monoids $(M,\cdot)$, addressing the freeness limitations of classical string rewriting. It builds the strict 2-category $\mathbf{NCRS_2}$ of Noetherian Confluent MRS and proves a canonical biadjunction with $\mathbf{Mon}$ via the left adjoint $G$ yielding canonical presentations $G(M)=(F_{M^+},\oplus,R_M)$ and the right adjoint $I$ selecting the monoid of irreducibles $\overline{M}$; the unit is identity and the counit $\varepsilon$ is a strong transformation. It introduces Generalized Elementary Tietze Transformations (GETTs) and shows that any two Noetherian confluent MRS presenting the same monoid are connected by GETTs, giving a complete GETT-equivalence classification. Together these results provide a universal, structure-preserving bridge between monoid theory and syntactic rewriting systems, enabling internal, first-order-style analysis of monoid presentations and canonical transformations between presentations.

Abstract

In this paper, we introduce monoidal rewriting systems (MRS), an abstraction of string rewriting in which reductions are defined over an arbitrary ambient monoid rather than a free monoid of words. This shift is partly motivated by logic: the class of free monoids is not first-order axiomatizable, so "working in the free setting" cannot be treated internally when applying first-order methods to rewriting presentations. To analyze these systems categorically, we define $\mathbf{NCRS_2}$ as the 2-category of Noetherian Confluent MRS. We then prove the existence of a canonical biadjunction between $\mathbf{NCRS_2}$ and $\mathbf{Mon}$. Finally, we classify all Noetherian Confluent MRS that present a given fixed monoid. For this, we introduce Generalized Elementary Tietze Transformations (GETTs) and prove that any two presentations of a monoid are connected by a (possibly infinite) sequence of these transformations, yielding a complete characterization of generating systems up to GETT-equivalence.

Rewriting Systems on Arbitrary Monoids

TL;DR

This work develops Monoidal Rewriting Systems (MRS) to rewrite over arbitrary monoids , addressing the freeness limitations of classical string rewriting. It builds the strict 2-category of Noetherian Confluent MRS and proves a canonical biadjunction with via the left adjoint yielding canonical presentations and the right adjoint selecting the monoid of irreducibles ; the unit is identity and the counit is a strong transformation. It introduces Generalized Elementary Tietze Transformations (GETTs) and shows that any two Noetherian confluent MRS presenting the same monoid are connected by GETTs, giving a complete GETT-equivalence classification. Together these results provide a universal, structure-preserving bridge between monoid theory and syntactic rewriting systems, enabling internal, first-order-style analysis of monoid presentations and canonical transformations between presentations.

Abstract

In this paper, we introduce monoidal rewriting systems (MRS), an abstraction of string rewriting in which reductions are defined over an arbitrary ambient monoid rather than a free monoid of words. This shift is partly motivated by logic: the class of free monoids is not first-order axiomatizable, so "working in the free setting" cannot be treated internally when applying first-order methods to rewriting presentations. To analyze these systems categorically, we define as the 2-category of Noetherian Confluent MRS. We then prove the existence of a canonical biadjunction between and . Finally, we classify all Noetherian Confluent MRS that present a given fixed monoid. For this, we introduce Generalized Elementary Tietze Transformations (GETTs) and prove that any two presentations of a monoid are connected by a (possibly infinite) sequence of these transformations, yielding a complete characterization of generating systems up to GETT-equivalence.
Paper Structure (5 sections, 20 theorems, 61 equations)

This paper contains 5 sections, 20 theorems, 61 equations.

Key Result

Theorem 1

Let $(A, \to)$ be a ARS. Then $(A, \to)$ is confluent if and only if it has the Church-Rosser property.

Theorems & Definitions (53)

  • Theorem
  • Definition
  • Definition
  • Theorem
  • Definition
  • Definition 3.1
  • Lemma 3.2
  • proof
  • Lemma 3.3
  • proof
  • ...and 43 more