between fixed strings over the alphabet, called rewrite rules, denoted by
, an SRS extends the rewriting relation to all strings in which the left- and right-hand side of the rules appear as substrings, that is
The notion of a semi-Thue system essentially coincides with the presentation of a monoid.
Thus they constitute a natural framework for solving the word problem for monoids and groups.
It can also be seen as a restricted kind of a term rewriting system, in which all function symbols have an arity of at most 1.
As a formalism, string rewriting systems are Turing complete.
[1] The semi-Thue name comes from the Norwegian mathematician Axel Thue, who introduced systematic treatment of string rewriting systems in a 1914 paper.
[2] Thue introduced this notion hoping to solve the word problem for finitely presented semigroups.
Only in 1947 was the problem shown to be undecidable— this result was obtained independently by Emil Post and A.
(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.
If instead the rules are just { ab → ε }, then we obtain a presentation of the bicyclic monoid.
, thus it may be always be presented by a semi-Thue system, possibly over an infinite alphabet.
are intuitively extra internal states of the Turing machine which it transitions to when halting, whereas
marks the end of the non-blank part of the tape; a machine reaching an
The strings that are valid encodings of Turing machine states start with an
(which encodes the state of the machine), followed by one or more symbol letters, followed by an ending
In the case that we reach the end of the visited portion of the tape, we use instead lengthening the string by one letter.
This proves that string rewrite systems are Turing complete.
(In this phase the string rewrite system no longer simulates a Turing machine, since that cannot remove cells from the tape.)
belong to the same congruence class with respect to this string rewrite system.
An apparent limitation of this argument is that in order to produce a semigroup
with undecidable word problem, one must first have a concrete example of a Turing machine
A minority of authors actually define a semi-Thue system as a triple
Under this "generative" definition of semi-Thue system, an unrestricted grammar is just a semi-Thue system with a single axiom in which one partitions the alphabet into terminals and non-terminals, and makes the axiom a nonterminal.
[10] The simple artifice of partitioning the alphabet into terminals and non-terminals is a powerful one; it allows the definition of the Chomsky hierarchy based on what combination of terminals and non-terminals the rules contain.
[11] Since quantum computation is intrinsically reversible, the rewriting rules over the alphabet
, and a rewriting rule taking a substring to another one can carry out a unitary operation on the tensor product of the Hilbert space attached to the strings; this implies that they preserve the number of characters from the set
Similar to the classical case one can show that a quantum Thue system is a universal computational model for quantum computation, in the sense that the executed quantum operations correspond to uniform circuit classes (such as those in BQP when e.g. guaranteeing termination of the string rewriting rules within polynomially many steps in the input size), or equivalently a Quantum Turing machine.
Semi-Thue systems were developed as part of a program to add additional constructs to logic, so as to create systems such as propositional logic, that would allow general mathematical theorems to be expressed in a formal language, and then proven and verified in an automatic, mechanical fashion.
This method of research succeeded and now computers can be used to verify the proofs of mathematic and logical theorems.