Pangram verdict · v3.3
We believe that this document is fully human-written
AI likelihood · overall
HumanArticle text · 1,835 words · 6 segments analyzed
Return to my home page.
Contents
Introduction
The word problem Finite complete rewriting systems The goal of this investigation
Two generators, two relations
The data set ⟨a, b | aaa=a, abba=bb⟩ ⟨a, b | aba=aa, baa=aab⟩
Two generators, one relation
The data set Related work Minor results
Introduction
My interest in finitely-presented monoids stems from the Swift compiler's use of the Knuth-Bendix completion algorithm to implement same-type requirements. There are multiple possible formulations of the Knuth-Bendix algorithm, but in Swift's case, we're using it to solve the word problem in a finitely-presented monoid.
In the Swift compiler, the finitely-presented monoids are the generic signatures of function and type declarations, and the relations in each monoid correspond to the generic requirements imposed upon that declaration. This is all documented in Chapters 16--18 of Compiling Swift Generics, if you're curious.The word problem
The word problem asks the yes/no question of whether two words over a finite alphabet are equivalent under a given set of bidirectional string rewriting rules, or "relations". Here is an example. Suppose you're given these two relations:
🍌🍎🍌 = 🍎🍎🍎 🍌🍌🍌 = 🍌🍌
Can you see a way to transform a string of 8 apples "🍎🍎🍎🍎🍎🍎🍎🍎" into a string of 10 apples "🍎🍎🍎🍎🍎🍎🍎🍎🍎🍎"?
It is not at all obvious that this can be done, and in fact it takes a minimum of 15 steps. (You can discover the solution for yourself by playing this simple game.)
This is a concrete instance of the word problem: we have two words a8 and a10, and the monoid presentation ⟨a, b | bab=aaa, bbb=bb⟩, and we want to know if the two words are equivalent with respect to those two rules.
Even though the above presentation is very short, the word problem here is already quite difficult. A classic result is that the word problem for finitely-presented monoids is undecidable in the general case. A very short example of a monoid with an undecidable word problem appears in the paper An associative calculus with an insoluble problem of equivalence (for an English translation with commentary, see G. S. Tseytin's seven-relation semigroup with undecidable word problem):
⟨a, b, c, d, e | ac=ca, ad=da, bc=cb, bd=db, eca=ce, edb=de, cca=ccae⟩
Finite complete rewriting systems
Knuth-Bendix attempts to construct a finite complete rewriting system from the bidirectional equivalences that define the monoid. A finite complete rewriting system is a set of directed reduction rules which allows us to reduce any word into a normal form in a finite number of steps. This completely solves the word problem for the original monoid: given any pair of words, we can first reduce both words to their normal form by applying the reduction rules in our FCRS, and then we check if we get identical normal forms.
Knuth-Bendix completion will sometimes fail; the failure mode is that it runs forever, continuing to add new rules which never converge. At the very least, Knuth-Bendix must fail if the given input rules define a monoid with an undecidable word problem. Undecidable instances aside, one might then ask: if our monoid has a decidable word problem, can we still solve the word problem with a finite complete rewriting system? This was answered in the negative by Craig C. Squier in the late 1980's.
In a paper titled A finiteness condition for rewriting systems, Squier considered the monoid S1, with five generators and five relations: S1 := ⟨a, b, t, x, y | ab=1, xa=atx, xt=tx, xb=bx, xy=1⟩ Squier shows that this monoid does not have finite derivation type, which is a necessary condition for the existence of a finite complete rewriting system presenting the same monoid. Thus, Knuth-Bendix completion will fail with any presentation of this monoid, not just the one given above, no matter what generating set or reduction order we choose. Despite that, S1 happens to have a decidable word problem. An even shorter example, with three generators and three relations, appears in a paper titled On finite complete rewriting systems, finite derivation type, and automaticity for homogeneous monoids: ⟨a, b, c | ac=ca, bc=cb, cab=cbb⟩ The above monoid again has a decidable word problem (the relations preserve the length of the word, so we can decide if two words are equivalent by first comparing their lengths, followed by an exhaustive enumeration if both words have equal length); just not by Knuth-Bendix completion.
The goal of this investigation
The above examples serve as motivation for my investigation, which can be summarized as follows:
Goal: To find, in some subjective sense, the "smallest" or "shortest" monoid presentations whose whose word problem cannot be solved by a finite complete rewriting system (in practical terms, applying some variant of Knuth-Bendix completion).
To search for a finite complete rewriting system that presents a monoid, I use a variation of the technique described in Morphocompletion for one-relation monoids, to introduce new generators to the presentation; I then attempt completion with a variety of reduction orders simultaneously:
Shortlex for all permutations of the alphabet Recursive path for all permutations of the alphabet together with all possible distinct degree assignments
Besides solving the word problem, a finite complete rewriting system tells you if the presented monoid has a finite number of elements (distinct equivalence classes of strings), in which case it is possible to enumerate the elements, and construct a Cayley table and Cayley graph for the monoid.
It is also decidable if a finite complete rewriting system presents a group, in which case the inverses of the generators can be determined as well. My side quest has been to collect and analyze this data about short presentations, which you can find in the data sets below.
To answer the one final question you may have:
Why? Because it's an interesting problem.
Two generators, two relations
The data set
I can find a finite complete rewriting system for every two-generated two-relation monoid with sum of sides ≤ 11, with 24 exceptions that are listed on the page below.
Explore:
Monoids with two generators and two relations
A fair number of instances in the enumeration "collapse" in various trivial ways:
⟨a, b | aa=a, ab=1⟩ is the first presentation of the trivial group with one element, but there are 2030 more. ⟨a, b | aa=1, ab=1⟩ is the first presentation of the group with two elements, but there are 1990 more. ⟨a, b | aa=a, aaa=b⟩ is the other possible monoid structure with two elements; not nearly as popular, with only 46 other duplicates in the enumeration.
This enumeration also includes some nice short presentations of various classic finite groups:
⟨a, b | abba=b, baba=1⟩ is a presentation of the symmetric group of degree 3, with 6 elements. (An interesting fact is that while this is the only non-Abelian group of order 6 up to isomorphism, there are many more monoids that are not groups, for example the slightly ridiculous ⟨a, b | ab=a, bbbb=ba⟩.) ⟨a, b | aba=b, aabb=1⟩ is a presentation of the Quaternion group with 8 elements. Can you see which elements can work as i, j, k, and -1? (There are multiple possible assignments, of course.) ⟨a, b | aaa=1, abba=b⟩ is a finite monoid with 27 elements, but the group with the same presentation is SL(2, 3). (
The monoid has three more elements, the powers of a.)
⟨a, b | aaa=a, abba=bb⟩
My main result so far is that ⟨a, b | aaa=a, abba=bb⟩ is the unique two generator, two relation monoid with length 10 that cannot be presented by a finite complete rewriting system over any alphabet ("not FCRS"). In fact, just like Squier's S1, it does not have finite derivation type.
Read the proof:
A two-relation monoid does not have finite derivation type
Note that the article describes an earlier enumeration of two-relation monoids up to length 10; at the time, this monoid was one of three "hard" instances. Since then, I've found an FCRS for the other two:
⟨a, b | bab=aaa, bbbb=1⟩ ⟨a, b | aaaa=1, abbba=b⟩
⟨a, b | aba=aa, baa=aab⟩
I also have an earlier result that one of the length 11 hard instances is not FCRS. The main proof fits in two pages, and it is (relatively speaking) quite straightforward, relying only on nothing more than the preliminary definitions and the pumping lemma for regular languages. I would be very happy if this was incorporated as an example in someone's textbook on string rewriting or Knuth-Bendix completion!
Read the proof:
The monoid ⟨a, b | aba=aa, baa=aab⟩ has no finite complete presentation
An interesting question (I do not know the answer) is if this monoid also fails to have finite derivation type.
Resolving the status of the remaining length 11 hard instances in the two relation enumeration is still an open problem. (A very observant reader might notice that the "8 apples" monoid from the introduction, ⟨a, b | bab=aaa, bbb=bb⟩, appears among them. I'm pretty sure it's not FCRS.) Let me know if you figure anything out!
Two generators, one relation
I've also investigated monoids with one defining relation.
The data set
I can find a finite complete rewriting system for every two-generated one-relation monoid with sum of sides ≤ 10, with five exceptions that are listed at the page below. It is not known if every one-relation monoid can be presented by a finite complete rewriting system. Maybe it is too much to hope for, but if the answer is "no", perhaps one of these will be the such first counterexample!
Explore:
Monoids with two generators and one relation
A number of classical one-relation monoids can be found in this enumeration:
⟨a, b | ab=1⟩ is the bicyclic monoid. ⟨a, b | aba=1⟩ is the Abelian group of integers under addition. (Can you see why ba=ab, and what the integer values of a and b must be?) ⟨a, b | bab=aba⟩ is the submonoid of positive words in the Braid group B3, discussed in A finite Thue system with decidable word problem and without equivalent finite canonical system. It has no FCRS over the alphabet {a, b}, but if you extend the alphabet with one auxiliary generator equivalent to one of ab, ba, or aba, you can obtain an FCRS. ⟨a, b | abbaab=1⟩ is anti-isomorphic to the Jantzen monoid, discussed in Finite complete rewriting systems for the Jantzen monoid and the Greendlinger group. To obtain an FCRS for this monoid (which is incidentally a group), one must not only expand the generating set, but also use a recursive path order which allows for length-increasing rewrite rules.
There are no finite monoids in this enumeration, because it takes at least two relations to present a finite monoid with two generators.
A team led by James D. Mitchell at University of St Andrews has been looking at solving the word problem in one relation monoids using a variety of techniques, not just FCRS, with a larger enumeration than mine---they're enumerating all ⟨a, b | u=v⟩ where |u| ≤ 10 and |v| ≤ 10, not just |u|+|v| ≤ 10.