Slava's Monoid Zoo

⟨🍎🍌🐈🐶🐘 | Slava's Monoid Zoo | 🐘🐶🐈🍌🍎⟩

Contents

Introduction

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

🍌🍎🍌 = 🍎🍎🍎 🍌🍌🍌 = 🍌🍌

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

... continue reading