Knuth-Bendix attempts to construct a finite complete rewriting system from the bidirectional equivalences that define the monoid. A finite complete rewriting system is essentially a data structure which allows us to reduce any word into a normal form in a finite number of steps. This allows us to solve 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 rewriting rules in our FCRS, and then we check if these normal forms are identical.
Knuth-Bendix completion will sometimes fail; the failure mode is that it runs forever, continuing to add new rules which never converge. The word problem for finitely-presented monoids is known to be undecidable in the general case, so at the very least, Knuth-Bendix must fail if the given input rules define a monoid with an undecidable word problem.
A classic 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⟩
S1 := ⟨a, b, t, x, y | ab=1, xa=atx, xt=tx, xb=bx, xy=1⟩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⟩This all leads to my investigation:
Goal: To find, in some subjective sense, the "smallest" or "shortest" presentation that defines a monoid whose word problem cannot be solved by Knuth-Bendix completion.Besides solving the word problem, a finite complete rewriting system can also answer if the presented monoid is finite, or if it is a group. A minor side quest here is to collect and analyze this data about all short presentations.
I can find a finite complete rewriting system for every two-generated two-relation monoid with sum of sides ≤ 11, with 24 exceptions.
Explore my data set:
Read the proof:
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:Read the proof:
An interesting question (I do not know the answer) is if this monoid also fails to have finite derivation type.I can find a finite complete rewriting system for every two-generated one-relation monoid with sum of sides ≤ 10, with five exceptions. It is not known if every one-relation monoid can be presented by a finite complete rewriting system; perhaps one of these could be a counterexample, but I have no formal results in this area.
Explore my data set:
(ii) (Victor Maltcev) Does there exist a normal form or other useful description for the monoid presented by generators a, b and the relation abbab = baabb ? (I do not know the answer.)The monoid ⟨a, b | abbab=baabb⟩ is anti-isomorphic to ⟨a, b | abaab=aabba⟩, which admits a finite complete rewriting system.
(2) The next example appears in the fantastic survey of The Word Problem for One-Relation Monoids by C.F. Brodda, where he writes:
We note in passing that the smallest monadic one-relation monoid to which no result in the literature appears to be available to solve the word problem for is ⟨a, b | bababbbabba=a⟩. The author has not found a finite complete rewriting system for this monoid, but has solved the word problem for this monoid by other means.This presentation does not appear in my enumeration, for it has length 12. It has the following finite complete rewriting system, once we add a letter c=bba:
The 1-relation Thue systems for which the decidability of the word problem is unknown to us: {baabbbaba ↔ a} {baaabaaa ↔ aba}.The first one is anti-isomorphic to ⟨a, b | ababbbaab=a⟩, which admits a finite complete rewriting system. The second one has length 11 so it does not appear in my enumeration, but it can also be solved by FCRS if we add c=aaaba and d=abaaa: