| Up: | Monoid Zoo |
|---|
My interest in finitely-presented monoids started with the realization that the Swift compiler can use 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 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 obvious how 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.)
The above 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 tricky. 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⟩
While the general case is undecidable, the word problem can be successfully solved in many cases using Knuth-Bendix completion.
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 by a process which can 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, does Knuth-Bendix completion always succeed?
The answer there is "no". Successful completion can depend on the choice of a reduction order and a generating set for the presented monoid. In many examples, it is not just a matter of waiting long enough, but making the right choices before we begin. One might then ask, if our monoid has a decidable word problem, and we apply Knuth-Bendix completion with carefully chosen initial parameters, and we wait long enough, do we always get an FCRS that can solve our word problem?
The answer is also "no", as shown 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 an FCRS presenting the same monoid. Thus, Knuth-Bendix completion will fail with any presentation of this monoid, not just the one given above. 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.
Goal: To find, in some subjective sense, the "smallest" or "shortest" monoid presentation(s) whose whose word problem cannot be solved by a finite complete rewriting system.
I got the idea from Bogdan Grechuk's wonderful book, Polynomial Diophantine Equations: A Systematic Approach. Much like the word problem, no general approach exists that can solve all Diophantine equations, because the general case is undecidable. Grechuk defines an ordering of all such equations, and then proceeds to work through the list, applying various techniques to solve as many instances as possible in order of increasing size. I'm doing a scaled down variation of that, with finitely-presented monoids instead.
Besides solving the word problem, various properties of the presented monoid can be determined from an FCRS (details can be found in the book String Rewriting Systems, for example):
I've been collecting and analyzing this data for all solved instances. When you visit the page for a monoid in the enumeration, you'll see these properties summarized, together with Cayley tables for finite monoids up to size 24, and Cayley graphs for finite monoids up to size 1083. For example, see ⟨a, b | bab=aaa, bbb=1⟩.
To actually construct finite complete rewriting systems, I use an adaptation of Knuth-Bendix completion known as morphocompletion, due to John Pedersen. I describe it on the page below:
My main discovery 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. This provides an even shorter counterexample than those previously known, cited in Finite complete rewriting systems above.