Semi-Thue system
From Wikipedia, the free encyclopedia
In computer science and mathematics a Semi-Thue system is a string rewriting system. It is named after the Norwegian mathematician Axel Thue, who introduced systematic treatment of string rewriting systems in the early 20th century.
Contents |
[edit] Definition
Let Σ be a finite alphabet and Σ * the Kleene closure over Σ. Then a Semi-Thue system is a tuple T: = (Σ,R) with
The elements of R are called productions or (rewrite) rules, and are usually written as rules 
. Note that R may be infinite. If a Semi-Thue system is symmetric (i.e. R − 1 = R), it is also called a Thue system.
[edit] 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 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.
[edit] 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: = (Σ,R) and two words 
, 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."
[edit] See also
[edit] 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.
