Semi-Thue system

In computer science and mathematics a Semi-Thue system (also called a string rewriting system [Book and Otto, p. 36] ) is a type of term rewriting system. It is named after the Norwegian mathematician Axel Thue, who introduced systematic treatment of string rewriting systems in the early 20th century.

Definition

A Semi-Thue system is a tuple $(Sigma,\; R)$ where
* $Sigma$ is a finite alphabet. Elements of the set $Sigma^*$ of finite (possibly empty) strings on $Sigma$ are called "words".
* $R$ is a binary relation on $Sigma^*$, i.e., $R\; subseteq\; Sigma^*\; imes\; Sigma^*.$ Each element $(u,v)\; in\; R$ is called a "rule" and is usually written $u\; ightarrow\; v$.

A Semi-Thue system $(Sigma,\; R)$ induces a "one-step rewrite relation" $Rightarrow\_R$ on $Sigma^*$, which formalises the notion of rewriting a string $s$ by replacing a substring $u$ within it: : $forall\; s,t\; in\; Sigma^*,\; (s\; Rightarrow\_R\; t\; iff\; exist\; x,y,u,v\; in\; Sigma^*,\; s\; equiv\; xuy,\; t\; equiv\; xvy,\; u\; ightarrow\; v)$.

A "derivation" in the Semi-Thue system is then a (finite or infinite) sequence of words produced by starting with an initial word $s\_0\; in\; Sigma^*$ and repeatedly rewriting it by making one substring-replacement at a time:

:$s\_0\; Rightarrow\_R\; s\_1\; Rightarrow\_R\; s\_2\; Rightarrow\_R\; ldots$

If the relation $R$ is symmetric, i.e., $forall\; u,\; v\; in\; Sigma^*,\; (u\; ightarrow\; v)\; Rightarrow\; (v\; ightarrow\; u)\; ;$, then the system is called a Thue system.

A Semi-Thue system is a special type of Post canonical system. A semi-Thue system is also a term-rewriting system — one that has monadic words ending in the same variable as left- and right-hand side terms [Nachum Dershowitz and Jean-Pierre Jouannaud. [http://citeseer.ist.psu.edu/dershowitz90rewrite.html Rewrite Systems] (1990) p. 6] , e.g. a term rule $f\_2(f\_1(x))\; ightarrow\; g(x)$ is equivalent with the string rule $f\_1f\_2\; ightarrow\; g$.

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. And although this program of research succeeded in that computers can now be used to verify the proofs of theorems, it also failed in a spectacular way: a computer cannot distinguish between an interesting theorem, and a boring one.

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." (Undecidable p. 292)

Davis [ibid] asserts that the proof was offered independently by A. A. Markov (C. R. (Doklady) Acad. Sci. U.S.S.R. (n.s.) 55(1947), pp. 583-586.

The Word problem for Semi-Thue systems

The word problem for Semi-Thue systems can be stated as follows: Given a Semi-Thue system $T:=(Sigma,\; R)$ and two words $u,\; v\; in\; Sigma^*$, can $u$ be transformed into $v$ by applying rules from $R$? This problem is undecidable, i.e. there is no general algorithm for solving this problem. This even holds if we limit the input to finite systems.

Martin Davis offers the lay reader a two-page proof in his article "What is a Computation?" pp. 258-259 with commentary p. 257. Davis casts the proof in this manner: "invent [a word problem] whose solution would lead to a solution to the halting problem."

See also

* Post canonical system
* Unrestricted grammar
* L-system

Notes

References

* Martin Davis ed. (1965), "The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions", Raven Press, New York.
* Emil Post (1947), "Recursive Unsolvability of a Problem of Thue," reprinted in "The Undecidable" pp. 293ff from The Journal of Symbolic Logic, vol. 12 (1947) pp. 1-11.
* Ronald V. Book and Friedrich Otto, "String-rewriting Systems", Springer (1993).