Finding complete rewriting systems for 1-relation monoids
In
Cirpons, Hivert, Mahboubi, Melquiond, Mitchell and Smith (2026),
the authors present a toolbox for the
Rocq proof assistant, that can be used to verify the
decidability of the word problem for a given monoid and, in some cases, to
produce the corresponding decision procedure. In particular, the techniques
described in this paper were applied to a large number of 1-relation monoids to
determine their decidability. Of these, 501 required a modified version of the
Knuth-Bendix procedure along with the termination solver Matchbox to find a
complete reqriting system, thus proving decidability.
On the following pages, you will find complete rewriting systems for 412 of
those 501 presentations. The complete rewriting systems described here were
found using the Knuth-Bendix procedure implemented in
libsemigroups, using the
morphocompletion technique as described in
Pedersen (2005) and by Pestov in
Slava's Monoid Zoo.
Hall of fame
The following information may be of particular interest.
The presentations whose complete rewriting systems contains the most rules (128)
- #309 baaaaababa=abbaa (128 rules)
- #394 baaaababa=abbaa (87 rules)
- #010 baaaaabbba=abaa (87 rules)
- #477 abbabbbaba=baabba (87 rules)
- #214 ababbaaaba=baaababa (85 rules)
- #332 abababaaaa=baaba (82 rules)
The presentations whose complete rewriting systems contains the fewest rules
- #064 aaaabababa=babaaaaa (3 rules)
- #273 aaabababa=babaaaa (3 rules)
- #374 abaabababa=babaabaa (3 rules)
- #419 aababababa=babaaa (3 rules)
- #424 aababababa=bababaaa (3 rules)
- #462 abbaaababa=baabbaaa (3 rules)
The most common rules
Across all of the complete rewriting systems, there are \(7,781\) rules in total, and \(6,572\) unique rules. There are \(6,148\) rules that appear exactly once. The following are the most common rules:
| Rule | Occurrences |
|---|---|
| \(ba \to c\) | 131 |
| \(c \to aa\) | 55 |
| \(c \to ba\) | 29 |
| \(bc \to cb\) | 26 |
| \(abb \to d\) | 25 |
| \(bb \to c\) | 25 |