fbpx
Wikipedia

Semi-Thue system

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, 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 , where , , , and 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. 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. A. Markov Jr.[3][4]

Definition

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

  • Σ is an alphabet, usually assumed finite.[5] The elements of the set   (* is the Kleene star here) are finite (possibly empty) strings on Σ, sometimes called words in formal languages; we will simply call them strings here.
  • R is a binary relation on strings from Σ, i.e.,   Each element   is called a (rewriting) rule and is usually written  .

If the relation R is symmetric, then the system is called a Thue system.

The rewriting rules in R can be naturally extended to other strings in   by allowing substrings to be rewritten according to R. More formally, the one-step rewriting relation relation   induced by R on   for any strings  :

  if and only if there exist   such that  ,  , and  .

Since   is a relation on  , the pair   fits the definition of an abstract rewriting system. Obviously R is a subset of  . Some authors use a different notation for the arrow in   (e.g.  ) in order to distinguish it from R itself ( ) because they later want to be able to drop the subscript and still avoid confusion between R and the one-step rewrite induced by R.

Clearly in a semi-Thue system we can form a (finite or infinite) sequence of strings produced by starting with an initial string   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 of  , denoted by   (see abstract rewriting system#Basic notions). This is called the rewriting relation or reduction relation on   induced by R.

Thue congruence

In general, the set   of strings on an alphabet forms a free monoid together with the binary operation of string concatenation (denoted as   and written multiplicatively by dropping the symbol). In a SRS, the reduction relation   is compatible with the monoid operation, meaning that   implies   for all strings  . Since   is by definition a preorder,   forms a monoidal preorder.

Similarly, the reflexive transitive symmetric closure of  , denoted   (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. The relation   is called the Thue congruence generated by R. In a Thue system, i.e. if R is symmetric, the rewrite relation   coincides with the Thue congruence  .

Factor monoid and monoid presentations

Since   is a congruence, we can define the factor monoid   of the free monoid   by the Thue congruence in the usual manner. If a monoid   is isomorphic with  , then the semi-Thue system   is called a monoid presentation of  .

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: Every monoid has a presentation of the form  , thus it may be always be presented by a semi-Thue system, possibly over an infinite alphabet.[6]

In this context, the set   is called the set of generators of  , and   is called the set of defining relations  . We can immediately classify monoids based on their presentation.   is called

  • finitely generated if   is finite.
  • finitely presented if both   and   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[7] for Turing machines to an instance of the word problem.

Concretely, Post devised an encoding as a finite string of the state of a Turing machine plus tape, such that the actions of this machine can be carried out by a string rewrite system acting on this string encoding. The alphabet of the encoding has one set of letters   for symbols on the tape (where   means blank), another set of letters   for states of the Turing machine, and finally three letters   that have special roles in the encoding.   and   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   should behave the same as if there was a blank there, and the   was in the next cell. The strings that are valid encodings of Turing machine states start with an  , followed by zero or more symbol letters, followed by exactly one internal state letter   (which encodes the state of the machine), followed by one or more symbol letters, followed by an ending  . 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.

A transition where the machine upon being in state   and seeing the symbol   writes back symbol  , moves right, and transitions to state   is implemented by the rewrite

 

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

 

with one instance for each symbol   in that cell to the left. In the case that we reach the end of the visited portion of the tape, we use instead

 ,

lengthening the string by one letter. Because all rewrites involve one internal state letter  , 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.

The reason for having two halted symbols   and   is that we want all halting Turing machines to terminate at the same total state, not just a particular internal state. This requires clearing the tape after halting, so   eats the symbol on it left until reaching the  , where it transitions into   which instead eats the symbol on its right. (In this phase the string rewrite system no longer simulates a Turing machine, since that cannot remove cells from the tape.) After all symbols are gone, we have reached the terminal string  .

A decision procedure for the word problem would then also yield a procedure for deciding whether the given Turing machine terminates when started in a particular total state  , by testing whether   and   belong to the same congruence class with respect to this string rewrite system. Technically, we have the following:

Lemma. Let   be a deterministic Turing machine and   be the string rewrite system implementing  , as described above. Then   will halt when started from the total state encoded as   if and only if   (that is to say, if and only if   and   are Thue congruent for  ).

That   if   halts when started from   is immediate from the construction of   (simply running   until it halts constructs a proof of  ), but   also allows the Turing machine   to take steps backwards. Here it becomes relevant that   is deterministic, because then the forward steps are all unique; in a   walk from   to   the last backward step must be followed by its counterpart as a forward step, so these two cancel, and by induction all backward steps can be eliminated from such a walk. Hence if   does not halt when started from  , i.e., if we do not have  , then we also do not have  . Therefore deciding   tells us the answer to the halting problem for  .

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   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 system—one that has monadic words (functions) ending in the same variable as the left- and right-hand side terms,[8] e.g. a term rule   is equivalent to the string rule  .

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.[9] A formal grammar only differs from a semi-Thue system by the separation of the alphabet into terminals and non-terminals, and the fixation of a starting symbol amongst non-terminals. A minority of authors actually define a semi-Thue system as a triple  , where   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.[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. This was a crucial development in the theory of formal languages.

In quantum computing, the notion of a quantum Thue system can be developed.[11] Since quantum computation is intrinsically reversible, the rewriting rules over the alphabet   are required to be bidirectional (i.e. the underlying system is a Thue system,[dubious ] not a semi-Thue system). On a subset of alphabet characters   one can attach a Hilbert space  , 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.

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."[12]

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

See also

Notes

  1. ^ See section "Undecidability of the word problem" in this article.
  2. ^ Book and Otto, p. 36
  3. ^ Abramsky et al. p. 416
  4. ^ Salomaa et al., p.444
  5. ^ In Book and Otto a semi-Thue system is defined over a finite alphabet through most of the book, except chapter 7 when monoid presentation are introduced, when this assumption is quietly dropped.
  6. ^ Book and Otto, Theorem 7.1.7, p. 149
  7. ^ Post, following Turing, technically makes use of the undecidability of the printing problem (whether a Turing machine ever prints a particular symbol), but the two problems reduce to each other. Indeed, Post includes an extra step in his construction that effectively converts printing the watched symbol into halting.
  8. ^ Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems (1990) p. 6
  9. ^ D.I.A. Cohen, Introduction to Computer Theory, 2nd ed., Wiley-India, 2007, ISBN 81-265-1334-9, p.572
  10. ^ Dan A. Simovici, Richard L. Tenney, Theory of formal languages with applications, World Scientific, 1999 ISBN 981-02-3729-4, chapter 4
  11. ^ J. Bausch, T. Cubitt, M. Ozols, The Complexity of Translationally-Invariant Spin Chains with Low Local Dimension, Ann. Henri Poincare 18(11), 2017 doi:10.1007/s00023-017-0609-7 pp. 3449-3513
  12. ^ Martin Davis (editor) (1965), The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, after page 292, Raven Press, New York
  13. ^ A. A. Markov (1947) Doklady Akademii Nauk SSSR (N.S.) 55: 583–586

References

Monographs

Textbooks

  • Martin Davis, Ron Sigal, Elaine J. Weyuker, Computability, complexity, and languages: fundamentals of theoretical computer science, 2nd ed., Academic Press, 1994, ISBN 0-12-206382-1, chapter 7
  • Elaine Rich, Automata, computability and complexity: theory and applications, Prentice Hall, 2007, ISBN 0-13-228806-0, 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, ISBN 0-19-853780-8.
  • Grzegorz Rozenberg, Arto Salomaa (ed.), Handbook of Formal Languages: Word, language, grammar, Springer, 1997, ISBN 3-540-60420-0.

Landmark papers

semi, thue, system, theoretical, computer, science, mathematical, logic, string, rewriting, system, historically, called, semi, thue, system, rewriting, system, over, strings, from, usually, finite, alphabet, given, binary, relation, displaystyle, between, fix. 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 R displaystyle R between fixed strings over the alphabet called rewrite rules denoted by s t displaystyle s rightarrow t 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 u s v u t v displaystyle usv rightarrow utv where s displaystyle s t displaystyle t u displaystyle u and v displaystyle v 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 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 A Markov Jr 3 4 Contents 1 Definition 2 Thue congruence 3 Factor monoid and monoid presentations 4 Undecidability of the word problem 5 Connections with other notions 6 History and importance 7 See also 8 Notes 9 References 9 1 Monographs 9 2 Textbooks 9 3 Surveys 9 4 Landmark papersDefinition EditA string rewriting system or semi Thue system is a tuple S R displaystyle Sigma R where S is an alphabet usually assumed finite 5 The elements of the set S displaystyle Sigma is the Kleene star here are finite possibly empty strings on S sometimes called words in formal languages we will simply call them strings here R is a binary relation on strings from S i e R S S displaystyle R subseteq Sigma times Sigma Each element u v R displaystyle u v in R is called a rewriting rule and is usually written u v displaystyle u rightarrow v If the relation R is symmetric then the system is called a Thue system The rewriting rules in R can be naturally extended to other strings in S displaystyle Sigma by allowing substrings to be rewritten according to R More formally the one step rewriting relation relation R displaystyle xrightarrow R induced by R on S displaystyle Sigma for any strings s t S displaystyle s t in Sigma s R t displaystyle s xrightarrow R t if and only if there exist x y u v S displaystyle x y u v in Sigma such that s x u y displaystyle s xuy t x v y displaystyle t xvy and u v displaystyle u rightarrow v Since R displaystyle xrightarrow R is a relation on S displaystyle Sigma the pair S R displaystyle Sigma xrightarrow R fits the definition of an abstract rewriting system Obviously R is a subset of R displaystyle xrightarrow R Some authors use a different notation for the arrow in R displaystyle xrightarrow R e g R displaystyle xrightarrow R in order to distinguish it from R itself displaystyle rightarrow because they later want to be able to drop the subscript and still avoid confusion between R and the one step rewrite induced by R Clearly in a semi Thue system we can form a finite or infinite sequence of strings produced by starting with an initial string s 0 S displaystyle s 0 in Sigma and repeatedly rewriting it by making one substring replacement at a time s 0 R s 1 R s 2 R displaystyle s 0 xrightarrow R s 1 xrightarrow R s 2 xrightarrow R ldots A zero or more steps rewriting like this is captured by the reflexive transitive closure of R displaystyle xrightarrow R denoted by R displaystyle xrightarrow R see abstract rewriting system Basic notions This is called the rewriting relation or reduction relation on S displaystyle Sigma induced by R Thue congruence EditIn general the set S displaystyle Sigma of strings on an alphabet forms a free monoid together with the binary operation of string concatenation denoted as displaystyle cdot and written multiplicatively by dropping the symbol In a SRS the reduction relation R displaystyle xrightarrow R is compatible with the monoid operation meaning that x R y displaystyle x xrightarrow R y implies u x v R u y v displaystyle uxv xrightarrow R uyv for all strings x y u v S displaystyle x y u v in Sigma Since R displaystyle xrightarrow R is by definition a preorder S R displaystyle left Sigma cdot xrightarrow R right forms a monoidal preorder Similarly the reflexive transitive symmetric closure of R displaystyle xrightarrow R denoted R displaystyle overset underset R leftrightarrow 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 The relation R displaystyle overset underset R leftrightarrow is called the Thue congruence generated by R In a Thue system i e if R is symmetric the rewrite relation R displaystyle xrightarrow R coincides with the Thue congruence R displaystyle overset underset R leftrightarrow Factor monoid and monoid presentations EditSince R displaystyle overset underset R leftrightarrow is a congruence we can define the factor monoid M R S R displaystyle mathcal M R Sigma overset underset R leftrightarrow of the free monoid S displaystyle Sigma by the Thue congruence in the usual manner If a monoid M displaystyle mathcal M is isomorphic with M R displaystyle mathcal M R then the semi Thue system S R displaystyle Sigma R is called a monoid presentation of M displaystyle mathcal M We immediately get some very useful connections with other areas of algebra For example the alphabet a b with the rules ab e ba e where e is the empty string is a presentation of the free group on one generator If instead the rules are just ab e 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 Every monoid has a presentation of the form S R displaystyle Sigma R thus it may be always be presented by a semi Thue system possibly over an infinite alphabet 6 In this context the set S displaystyle Sigma is called the set of generators of M displaystyle mathcal M and R displaystyle R is called the set of defining relations M displaystyle mathcal M We can immediately classify monoids based on their presentation M displaystyle mathcal M is called finitely generated if S displaystyle Sigma is finite finitely presented if both S displaystyle Sigma and R displaystyle R are finite Undecidability of the word problem EditPost proved the word problem for semigroups to be undecidable in general essentially by reducing the halting problem 7 for Turing machines to an instance of the word problem Concretely Post devised an encoding as a finite string of the state of a Turing machine plus tape such that the actions of this machine can be carried out by a string rewrite system acting on this string encoding The alphabet of the encoding has one set of letters S 0 S 1 S m displaystyle S 0 S 1 dotsc S m for symbols on the tape where S 0 displaystyle S 0 means blank another set of letters q 1 q r displaystyle q 1 dotsc q r for states of the Turing machine and finally three letters q r 1 q r 2 h displaystyle q r 1 q r 2 h that have special roles in the encoding q r 1 displaystyle q r 1 and q r 2 displaystyle q r 2 are intuitively extra internal states of the Turing machine which it transitions to when halting whereas h displaystyle h marks the end of the non blank part of the tape a machine reaching an h displaystyle h should behave the same as if there was a blank there and the h displaystyle h was in the next cell The strings that are valid encodings of Turing machine states start with an h displaystyle h followed by zero or more symbol letters followed by exactly one internal state letter q i displaystyle q i which encodes the state of the machine followed by one or more symbol letters followed by an ending h displaystyle h 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 A transition where the machine upon being in state q i displaystyle q i and seeing the symbol S k displaystyle S k writes back symbol S l displaystyle S l moves right and transitions to state q j displaystyle q j is implemented by the rewrite q i S k S l q j displaystyle q i S k to S l q j whereas that transition instead moving to the left is implemented by the rewrite S p q i S k q j S p S l displaystyle S p q i S k to q j S p S l with one instance for each symbol S p displaystyle S p in that cell to the left In the case that we reach the end of the visited portion of the tape we use instead h q i S k h q j S 0 S l displaystyle hq i S k to hq j S 0 S l lengthening the string by one letter Because all rewrites involve one internal state letter q i displaystyle q i 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 The reason for having two halted symbols q r 1 displaystyle q r 1 and q r 2 displaystyle q r 2 is that we want all halting Turing machines to terminate at the same total state not just a particular internal state This requires clearing the tape after halting so q r 1 displaystyle q r 1 eats the symbol on it left until reaching the h displaystyle h where it transitions into q r 2 displaystyle q r 2 which instead eats the symbol on its right In this phase the string rewrite system no longer simulates a Turing machine since that cannot remove cells from the tape After all symbols are gone we have reached the terminal string h q r 2 h displaystyle hq r 2 h A decision procedure for the word problem would then also yield a procedure for deciding whether the given Turing machine terminates when started in a particular total state t displaystyle t by testing whether t displaystyle t and h q r 2 h displaystyle hq r 2 h belong to the same congruence class with respect to this string rewrite system Technically we have the following Lemma Let M displaystyle M be a deterministic Turing machine and R displaystyle R be the string rewrite system implementing M displaystyle M as described above Then M displaystyle M will halt when started from the total state encoded as t displaystyle t if and only if t R h q r 2 h displaystyle t mathrel overset underset R leftrightarrow hq r 2 h that is to say if and only if t displaystyle t and h q r 2 h displaystyle hq r 2 h are Thue congruent for R displaystyle R That t R h q r 2 h displaystyle t mathrel overset underset R rightarrow hq r 2 h if M displaystyle M halts when started from t displaystyle t is immediate from the construction of R displaystyle R simply running M displaystyle M until it halts constructs a proof of t R h q r 2 h displaystyle t mathrel overset underset R rightarrow hq r 2 h but R displaystyle overset underset R leftrightarrow also allows the Turing machine M displaystyle M to take steps backwards Here it becomes relevant that M displaystyle M is deterministic because then the forward steps are all unique in a R displaystyle overset underset R leftrightarrow walk from t displaystyle t to h q r 2 h displaystyle hq r 2 h the last backward step must be followed by its counterpart as a forward step so these two cancel and by induction all backward steps can be eliminated from such a walk Hence if M displaystyle M does not halt when started from t displaystyle t i e if we do not have t R h q r 2 h displaystyle t mathrel overset underset R rightarrow hq r 2 h then we also do not have t R h q r 2 h displaystyle t mathrel overset underset R leftrightarrow hq r 2 h Therefore deciding R displaystyle overset underset R leftrightarrow tells us the answer to the halting problem for M displaystyle M An apparent limitation of this argument is that in order to produce a semigroup S R displaystyle Sigma big overset underset R leftrightarrow with undecidable word problem one must first have a concrete example of a Turing machine M displaystyle M 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 EditA semi Thue system is also a term rewriting system one that has monadic words functions ending in the same variable as the left and right hand side terms 8 e g a term rule f 2 f 1 x g x displaystyle f 2 f 1 x rightarrow g x is equivalent to the string rule f 1 f 2 g displaystyle f 1 f 2 rightarrow g 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 9 A formal grammar only differs from a semi Thue system by the separation of the alphabet into terminals and non terminals and the fixation of a starting symbol amongst non terminals A minority of authors actually define a semi Thue system as a triple S A R displaystyle Sigma A R where A S displaystyle A subseteq Sigma 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 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 This was a crucial development in the theory of formal languages In quantum computing the notion of a quantum Thue system can be developed 11 Since quantum computation is intrinsically reversible the rewriting rules over the alphabet S displaystyle Sigma are required to be bidirectional i e the underlying system is a Thue system dubious discuss not a semi Thue system On a subset of alphabet characters Q S displaystyle Q subseteq Sigma one can attach a Hilbert space C d displaystyle mathbb C d 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 Q displaystyle Q 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 EditSemi 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 12 Davis also asserts that the proof was offered independently by A A Markov 13 See also EditL system MU puzzleNotes Edit See section Undecidability of the word problem in this article Book and Otto p 36 Abramsky et al p 416 Salomaa et al p 444 In Book and Otto a semi Thue system is defined over a finite alphabet through most of the book except chapter 7 when monoid presentation are introduced when this assumption is quietly dropped Book and Otto Theorem 7 1 7 p 149 Post following Turing technically makes use of the undecidability of the printing problem whether a Turing machine ever prints a particular symbol but the two problems reduce to each other Indeed Post includes an extra step in his construction that effectively converts printing the watched symbol into halting Nachum Dershowitz and Jean Pierre Jouannaud Rewrite Systems 1990 p 6 D I A Cohen Introduction to Computer Theory 2nd ed Wiley India 2007 ISBN 81 265 1334 9 p 572 Dan A Simovici Richard L Tenney Theory of formal languages with applications World Scientific 1999 ISBN 981 02 3729 4 chapter 4 J Bausch T Cubitt M Ozols The Complexity of Translationally Invariant Spin Chains with Low Local Dimension Ann Henri Poincare 18 11 2017 doi 10 1007 s00023 017 0609 7 pp 3449 3513 Martin Davis editor 1965 The Undecidable Basic Papers on Undecidable Propositions Unsolvable Problems and Computable Functions after page 292 Raven Press New York A A Markov 1947 Doklady Akademii Nauk SSSR N S 55 583 586References EditMonographs Edit Ronald V Book and Friedrich Otto String rewriting Systems Springer 1993 ISBN 0 387 97965 4 Matthias Jantzen Confluent string rewriting Birkhauser 1988 ISBN 0 387 13715 7 Textbooks Edit Martin Davis Ron Sigal Elaine J Weyuker Computability complexity and languages fundamentals of theoretical computer science 2nd ed Academic Press 1994 ISBN 0 12 206382 1 chapter 7 Elaine Rich Automata computability and complexity theory and applications Prentice Hall 2007 ISBN 0 13 228806 0 chapter 23 5 Surveys Edit Samson Abramsky Dov M Gabbay Thomas S E Maibaum ed Handbook of Logic in Computer Science Semantic modelling Oxford University Press 1995 ISBN 0 19 853780 8 Grzegorz Rozenberg Arto Salomaa ed Handbook of Formal Languages Word language grammar Springer 1997 ISBN 3 540 60420 0 Landmark papers Edit Post Emil 1947 Recursive Unsolvability of a Problem of Thue The Journal of Symbolic Logic 12 1 1 11 doi 10 2307 2267170 JSTOR 2267170 S2CID 30320278 a href Template Cite journal html title Template Cite journal cite journal a CS1 maint url status link Retrieved from https en wikipedia org w index php title Semi Thue system amp oldid 1127156139, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.