In theoretical computer science and mathematical logic a string rewriting system (SRS), historically called a semi-Thue system, is a rewriting system over strings from a (usually finite) alphabet. Given a binary relation between fixed strings over the alphabet, called rewrite rules, an SRS extends the rewriting relation to all strings in which the left- and right-hand side of the rules appear as substrings are strings.

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.

An SRS can be defined directly as an abstract rewriting system. 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. The semi-Thue name comes from the Norwegian mathematician Axel Thue, who introduced systematic treatment of string rewriting systems in a 1914 paper. 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. A. Markov Jr.

Definition

A string rewriting system or semi-Thue system is a tuple where

• is an alphabet, usually assumed finite. (* is the Kleene star, sometimes called words in formal languages; we will simply call them strings here.

• is a binary relation is called a (rewriting) rule.

is symmetric, then the system is called a Thue system.

. More formally, the one-step rewriting relation:

1. .

fits the definition of an abstract rewriting system.

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 (see abstract rewriting system#Basic notions). This is called the rewriting relation or reduction relation.

Thue congruence

of strings on an alphabet forms a free monoid together with the binary operation of string concatenation is by definition a preorder forms a monoidal preorder.

Similarly, the reflexive transitive symmetric closure (see abstract rewriting system#Basic notions), is a congruence, meaning it is an equivalence relation is called the Thue congruence generated by . In a Thue system, i.e. if .

Factor monoid and monoid presentations

is a congruence, we can define the factor monoid of the free monoid by the Thue congruence in the usual manner is isomorphic is called a monoid presentation.

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, thus it may be always be presented by a semi-Thue system, possibly over an infinite alphabet.

is called the set of generators is called the set of defining relations is called

• finitely generated is finite.

• finitely presented 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 for Turing machines to an instance of the word problem (see Post correspondence problem).

. The symbol letters are straight off the contents of the tape, and the internal state letter marks the position of the head; the symbol after the internal state letter is that in the cell currently under the head of the Turing machine.

is implemented by the rewrite

whereas that transition instead moving to the left is implemented by the rewrite

in that cell to the left. In the case that we reach the end of the visited portion of the tape, we use instead

1. ,

, the valid encodings only contain one such letter, and each rewrite produces exactly one such letter, the rewrite process exactly follows the run of the Turing machine encoded. This proves that string rewrite systems are Turing complete.

is that we want all halting Turing machines to terminate at the same total state, not just a particular internal.

belong to the same congruence class with respect to this string rewrite system. Technically, we have the following:

Lemma.).

does not, i.e., if we do not, then we also do not.

for which the halting problem is undecidable, but the various Turing machines figuring in the proof of the undecidability of the general halting problem all have as component a hypothetical Turing machine solving the halting problem, so none of those machines can actually exist; all that proves is that there is some Turing machine for which the decision problem is undecidable. However, that there is some Turing machine with undecidable halting problem means that the halting problem for a universal Turing machine is undecidable (since that can simulate any Turing machine), and concrete examples of universal Turing machines have been constructed.

Connections with other notions

A semi-Thue system is also a term-rewriting systemone that has monadic words (functions) ending in the same variable as the left- and right-hand side terms,.

A semi-Thue system is also a special type of Post canonical system, but every Post canonical system can also be reduced to an SRS. Both formalisms are Turing complete, and thus equivalent to Noam Chomsky's unrestricted grammars, which are sometimes called semi-Thue grammars. A formal grammar only differs from a semi-Thue system by the separation of the alphabet into terminals is called the set of axioms. 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. 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. This was a crucial development in the theory of formal languages.

In quantum computing, the notion of a quantum Thue system can be developed. are required to be bidirectional (i.e. the underlying system is a Thue system,. 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.

History and importance

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. The hope was that the act of theorem proving could then be reduced to a set of defined manipulations on a set of strings. It was subsequently realized that semi-Thue systems are isomorphic to unrestricted grammars, which in turn are known to be isomorphic to Turing machines. This method of research succeeded and now computers can be used to verify the proofs of mathematic and logical theorems.

At the suggestion of Alonzo Church, Emil Post in a paper published in 1947, first proved "a certain Problem of Thue" to be unsolvable, what Martin Davis states as "...the first unsolvability proof for a problem from classical mathematics -- in this case the word problem for semigroups."

Davis also asserts that the proof was offered independently by A. A. Markov.

See also

• L-system

• Markov algorithm a variant of string rewriting systems

• MU puzzle

Notes

References

Monographs

• Ronald V. Book and Friedrich Otto, String-rewriting Systems, Springer, 1993, .

• Matthias Jantzen, Confluent string rewriting, Birkhäuser, 1988, .

Textbooks

• Martin Davis, Ron Sigal, Elaine J. Weyuker, Computability, complexity, and languages: fundamentals of theoretical computer science, 2nd ed., Academic Press, 1994, , chapter 7

• Elaine Rich, Automata, computability and complexity: theory and applications, Prentice Hall, 2007, , chapter 23.5.

Surveys

• Samson Abramsky, Dov M. Gabbay, Thomas S. E. Maibaum (ed.), Handbook of Logic in Computer Science: Semantic modelling, Oxford University Press, 1995, .

• Grzegorz Rozenberg, Arto Salomaa (ed.), Handbook of Formal Languages: Word, language, grammar, Springer, 1997, .

Landmark papers

ja:文字列書き換え系