Definitions
Nearby Words

Semi-Thue system

In computer science and mathematics a Semi-Thue system (also called a string rewriting system) 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 $\left(Sigma, R\right)$ 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^* times Sigma^*.$ Each element $\left(u,v\right) in R$ is called a rule and is usually written $u rightarrow v$.

A Semi-Thue system $\left(Sigma, R\right)$ 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^*, \left(s Rightarrow_R t iff exist x,y,u,v in Sigma^*, s equiv xuy, t equiv xvy, u rightarrow v\right)$.

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^*, \left(u rightarrow v\right) Rightarrow \left(v rightarrow u\right) ;$, 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, e.g. a term rule $f_2\left(f_1\left(x\right)\right) rightarrow g\left(x\right)$ is equivalent with the string rule $f_1f_2 rightarrow 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:=\left(Sigma, R\right)$ 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."

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).

Search another word or see Semi-Thue grammaron Dictionary | Thesaurus |Spanish