Rewriting Systems on Arbitrary Monoids
By: Eduardo Magalhães
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.
Similar Papers
Learning neuro-symbolic convergent term rewriting systems
Artificial Intelligence
Teaches computers to solve math problems like humans.
Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version)
Logic in Computer Science
Makes computer programs run faster and use less memory.
Between Markov and restriction: Two more monads on categories for relations
Logic in Computer Science
Organizes math ideas about how things connect.