form a (finite or infinite) sequence of strings produced by starting with an initial string and repeatedly rewriting it by making one substring-replacement at a time: A zero-or-more-steps rewriting like this is captured by the reflexive transitive closure of , denoted by (see abstract rewriting system#Basic notions). This is called the rewriting relation or reduction relation on induced by . Thue congruence In general, the set of strings on an alphabet forms a free monoid together with the binary operation of string concatenation (denoted as and written multiplicatively by dropping the symbol). In a SRS, the reduction relation is compatible with the monoid operation, meaning that implies for all strings . Since is by definition a preorder, forms a monoidal preorder. Similarly, the reflexive transitive symmetric closure of , denoted (see abstract rewriting system#Basic notions), is a congruence, meaning it is an equivalence relation (by definition) and it is also compatible with string concatenation. The relation is called the Thue congruence generated by . In a Thue system, i.e. if is symmetric, the rewrite relation coincides with the Thue congruence . Factor monoid and monoid presentations Since is a congruence, we can define the factor monoid of the free monoid by the Thue congruence in the usual manner. If a monoid is isomorphic with , then the semi-Thue system is called a monoid presentation of . We immediately get some very useful connections with other areas of algebra. For example, the alphabet {a, b} with the rules { ab → ε, ba → ε }, where ε is the empty string, is a presentation of the free group on one generator. If instead the rules are just { ab → ε }, then we obtain a presentation of the bicyclic monoid. The importance of semi-Thue systems as presentation of monoids is made stronger by the following: Theorem: Every monoid has a presentation of the form , thus it may be always be presented by a semi-Thue system, possibly over an infinite alphabet. In this context, the set is called the set of generators of , and is called the set of defining relations . We can immediately classify monoids based on their presentation. is called finitely generated if is finite. finitely presented if both and are finite. Undecidability of the word problem Post proved the word problem (for semigroups) to be undecidable in general, essentially by reducing the halting problem