|
|
| (312 intermediate revisions by more than 100 users not shown) |
| Line 1: |
Line 1: |
| In [[theoretical computer science]] and [[mathematical logic]] a '''string rewriting system''' ('''SRS'''), historically called a '''semi-Thue system''', is a [[rewriting]] system over [[String (computer science)|strings]] from a (usually [[Finite set|finite]]) [[Alphabet (computer science)|alphabet]]. Given a [[binary relation]] <math>R</math> between fixed strings in the alphabet, called '''rewrite rules''', denoted by <math>s\rightarrow t</math>, an SRS extends the rewriting relation to all strings in which the left- and right-hand side of the rules appear as [[substring]]s, that is <math>usv\rightarrow utv</math>, where <math>s</math>, <math>t</math>, <math>u</math>, and <math>v</math> are strings.
| | This is a preview for the new '''MathML rendering mode''' (with SVG fallback), which is availble in production for registered users. |
|
| |
|
| 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 (mathematics)|word problem]] for monoids and groups.
| | If you would like use the '''MathML''' rendering mode, you need a wikipedia user account that can be registered here [[https://en.wikipedia.org/wiki/Special:UserLogin/signup]] |
| | * Only registered users will be able to execute this rendering mode. |
| | * Note: you need not enter a email address (nor any other private information). Please do not use a password that you use elsewhere. |
|
| |
|
| 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]]. The semi-Thue name comes from the Norwegian mathematician [[Axel Thue]], who introduced systematic treatment of string rewriting systems in a 1914 paper.<ref>Book and Otto, p. 36</ref> Thue introduced this notion hoping to solve the word problem for finitely presented semigroups. It wasn't until 1947 the problem was shown to be [[undecidable problem|undecidable]]— this result was obtained independently by [[Emil Post]] and [[Andrey Markov (Soviet mathematician)|A. A. Markov Jr.]]<ref>Abramsky et al. p. 416</ref><ref>Salomaa et al., p.444</ref>
| | Registered users will be able to choose between the following three rendering modes: |
|
| |
|
| ==Definition== | | '''MathML''' |
| | :<math forcemathmode="mathml">E=mc^2</math> |
|
| |
|
| A '''string rewriting system''' or '''semi-Thue system''' is a [[tuple]] <math>(\Sigma, R)</math> where
| | <!--'''PNG''' (currently default in production) |
| * <math>\Sigma</math> is an alphabet, usually assumed finite.<ref>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.</ref> The elements of the set <math>\Sigma^*</math> (* is the [[Kleene star]] here) are finite (possibly empty) strings on <math>\Sigma</math>, sometimes called ''words'' in [[formal languages]]; we will simply call them strings here.
| | :<math forcemathmode="png">E=mc^2</math> |
| * <math>R</math> is a [[binary relation]] on strings from <math>\Sigma</math>, i.e., <math>R \subseteq \Sigma^* \times \Sigma^*.</math> Each element <math>(u,v) \in R</math> is called a ''(rewriting) rule'' and is usually written <math>u \rightarrow v</math>.
| |
|
| |
|
| If the relation <math>R</math> is [[symmetric relation|symmetric]], then the system is called a '''Thue system'''.
| | '''source''' |
| | :<math forcemathmode="source">E=mc^2</math> --> |
|
| |
|
| The rewriting rules in <math>R</math> can be naturally extended to other strings in <math>\Sigma^*</math> by allowing substrings to be rewritten according to <math>R</math>. More formally, the '''one-step rewriting relation''' relation <math>\rightarrow_R</math> induced by <math>R</math> on <math>\Sigma^*</math> for any strings <math>s</math>, and <math>t</math> in <math>\Sigma^*</math>:
| | <span style="color: red">Follow this [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering link] to change your Math rendering settings.</span> You can also add a [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering-skin Custom CSS] to force the MathML/SVG rendering or select different font families. See [https://www.mediawiki.org/wiki/Extension:Math#CSS_for_the_MathML_with_SVG_fallback_mode these examples]. |
|
| |
|
| : <math>s \rightarrow_R t</math> if and only if there exist <math>x</math>, <math>y</math>, <math>u</math>, <math>v</math> in <math>\Sigma^*</math> such that <math>s = xuy</math>, <math>t = xvy</math>, and <math>u \rightarrow v</math>.
| | ==Demos== |
|
| |
|
| Since <math>\rightarrow_R</math> is a relation on <math>\Sigma^*</math>, the pair <math>(\Sigma^*, \rightarrow_R)</math> fits the definition of an [[abstract rewriting system]]. Obviously <math>R</math> is a subset of <math>\rightarrow_R</math>. Some authors use a different notation for the arrow in <math>\rightarrow_R</math> (e.g. <math>\Rightarrow_R</math>) in order to distinguish it from <math>R</math> itself (<math>\rightarrow</math>) because they later want to be able to drop the subscript and still avoid confusion between <math>R</math> and the one-step rewrite induced by <math>R</math>.
| | Here are some [https://commons.wikimedia.org/w/index.php?title=Special:ListFiles/Frederic.wang demos]: |
|
| |
|
| Clearly in a semi-Thue system we can form a (finite or infinite) sequence of strings produced by starting with an initial string <math>s_0 \in \Sigma^*</math> and repeatedly rewriting it by making one substring-replacement at a time:
| |
|
| |
|
| :<math>s_0 \ \rightarrow_R \ s_1 \ \rightarrow_R \ s_2 \ \rightarrow_R \ \ldots </math> | | * accessibility: |
| | ** Safari + VoiceOver: [https://commons.wikimedia.org/wiki/File:VoiceOver-Mac-Safari.ogv video only], [[File:Voiceover-mathml-example-1.wav|thumb|Voiceover-mathml-example-1]], [[File:Voiceover-mathml-example-2.wav|thumb|Voiceover-mathml-example-2]], [[File:Voiceover-mathml-example-3.wav|thumb|Voiceover-mathml-example-3]], [[File:Voiceover-mathml-example-4.wav|thumb|Voiceover-mathml-example-4]], [[File:Voiceover-mathml-example-5.wav|thumb|Voiceover-mathml-example-5]], [[File:Voiceover-mathml-example-6.wav|thumb|Voiceover-mathml-example-6]], [[File:Voiceover-mathml-example-7.wav|thumb|Voiceover-mathml-example-7]] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-Audio-Windows7-InternetExplorer.ogg Internet Explorer + MathPlayer (audio)] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-SynchronizedHighlighting-WIndows7-InternetExplorer.png Internet Explorer + MathPlayer (synchronized highlighting)] |
| | ** [https://commons.wikimedia.org/wiki/File:MathPlayer-Braille-Windows7-InternetExplorer.png Internet Explorer + MathPlayer (braille)] |
| | ** NVDA+MathPlayer: [[File:Nvda-mathml-example-1.wav|thumb|Nvda-mathml-example-1]], [[File:Nvda-mathml-example-2.wav|thumb|Nvda-mathml-example-2]], [[File:Nvda-mathml-example-3.wav|thumb|Nvda-mathml-example-3]], [[File:Nvda-mathml-example-4.wav|thumb|Nvda-mathml-example-4]], [[File:Nvda-mathml-example-5.wav|thumb|Nvda-mathml-example-5]], [[File:Nvda-mathml-example-6.wav|thumb|Nvda-mathml-example-6]], [[File:Nvda-mathml-example-7.wav|thumb|Nvda-mathml-example-7]]. |
| | ** Orca: There is ongoing work, but no support at all at the moment [[File:Orca-mathml-example-1.wav|thumb|Orca-mathml-example-1]], [[File:Orca-mathml-example-2.wav|thumb|Orca-mathml-example-2]], [[File:Orca-mathml-example-3.wav|thumb|Orca-mathml-example-3]], [[File:Orca-mathml-example-4.wav|thumb|Orca-mathml-example-4]], [[File:Orca-mathml-example-5.wav|thumb|Orca-mathml-example-5]], [[File:Orca-mathml-example-6.wav|thumb|Orca-mathml-example-6]], [[File:Orca-mathml-example-7.wav|thumb|Orca-mathml-example-7]]. |
| | ** From our testing, ChromeVox and JAWS are not able to read the formulas generated by the MathML mode. |
|
| |
|
| A zero-or-more-steps rewriting like this is captured by the [[reflexive transitive closure]] of <math>\rightarrow_R</math>, denoted by <math>\stackrel{*}{\rightarrow}_R</math> (see [[abstract rewriting system#Basic notions]]). This is called the '''rewriting relation''' or '''reduction relation''' on <math>\Sigma^*</math> induced by <math>R</math>.
| | ==Test pages == |
|
| |
|
| == Thue congruence ==
| | To test the '''MathML''', '''PNG''', and '''source''' rendering modes, please go to one of the following test pages: |
| | *[[Displaystyle]] |
| | *[[MathAxisAlignment]] |
| | *[[Styling]] |
| | *[[Linebreaking]] |
| | *[[Unique Ids]] |
| | *[[Help:Formula]] |
|
| |
|
| In general, the set <math>\Sigma^*</math> of strings on an alphabet forms a [[free monoid]] together with the [[binary operation]] of [[string concatenation]] (denoted as <math>\cdot</math> and written multiplicatively by dropping the symbol). In a SRS, the reduction relation <math>\stackrel{*}{\rightarrow}_R</math> is compatible with the monoid operation, meaning that <math>x\stackrel{*}{\rightarrow}_R y</math> implies <math>uxv\stackrel{*}{\rightarrow}_R uyv</math> for all strings <math>x</math>, <math>y</math>, <math>u</math>, <math>v</math> in <math>\Sigma^*</math>. Since <math>\stackrel{*}{\rightarrow}_R</math> is by definition a [[preorder]], <math>(\Sigma^*, \cdot, \stackrel{*}{\rightarrow}_R)</math> forms a [[preordered monoid]].
| | *[[Inputtypes|Inputtypes (private Wikis only)]] |
| | | *[[Url2Image|Url2Image (private Wikis only)]] |
| Similarly, the [[reflexive transitive symmetric closure]] of <math>\rightarrow_R</math>, denoted <math>\stackrel{*}{\leftrightarrow}_R</math> (see [[abstract rewriting system#Basic notions]]), is a [[Congruence relation|congruence]], meaning it is an [[equivalence relation]] (by definition) and it is also compatible with string concatenation. The relation <math>\stackrel{*}{\leftrightarrow}_R</math> is called the '''Thue congruence''' generated by <math>R</math>. In a Thue system, i.e. if <math>R</math> is symmetric, the rewrite relation <math>\stackrel{*}{\rightarrow}_R</math> coincides with the Thue congruence <math>\stackrel{*}{\leftrightarrow}_R</math>.
| | ==Bug reporting== |
| | | If you find any bugs, please report them at [https://bugzilla.wikimedia.org/enter_bug.cgi?product=MediaWiki%20extensions&component=Math&version=master&short_desc=Math-preview%20rendering%20problem Bugzilla], or write an email to math_bugs (at) ckurs (dot) de . |
| == Factor monoid and monoid presentations == | |
| Since <math>\stackrel{*}{\leftrightarrow}_R</math> is a congruence, we can define the '''factor monoid''' <math>\mathcal{M}_R = \Sigma^*/\stackrel{*}{\leftrightarrow}_R</math> of the [[free monoid]] <math>\Sigma^*</math> by the Thue congruence in the [[factor monoid|usual manner]]. If a monoid <math>\mathcal{M}</math> is [[isomorphic]] with <math>\mathcal{M}_R</math>, then the semi-Thue system <math>(\Sigma, R)</math> is called a [[monoid presentation]] of <math>\mathcal{M}</math>.
| |
| | |
| 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 <math>(\Sigma, R)</math>, thus it may be always be presented by a semi-Thue system, possibly over an infinite alphabet.<ref>Book and Otto, Theorem 7.1.7, p. 149</ref>
| |
| | |
| In this context, the set <math>\Sigma</math> is called the '''set of generators''' of <math>\mathcal{M}</math>, and <math>R</math> is called the set of '''defining relations''' <math>\mathcal{M}</math>. We can immediately classify monoids based on their presentation. <math>\mathcal{M}</math> is called
| |
| * '''finitely generated''' if <math>\Sigma</math> is finite.
| |
| * '''finitely presented''' if both <math>\Sigma</math> and <math>R</math> are finite.
| |
| | |
| == The word problem for semi-Thue systems == | |
| | |
| The word problem for semi-Thue systems can be stated as follows: Given a semi-Thue system <math>T:=(\Sigma, R)</math> and two words (strings) <math>u, v \in \Sigma^*</math>, can <math>u</math> be transformed into <math>v</math> by applying rules from <math>R</math>? This problem is [[Undecidable problem|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]]."
| |
| | |
| == Connections with other notions == | |
| | |
| A semi-Thue system is also a [[term-rewriting]] system—one that has [[monadic (arity)|monadic]] words (functions) ending in the same variable as left- and right-hand side terms,<ref>Nachum Dershowitz and Jean-Pierre Jouannaud. [http://citeseer.ist.psu.edu/dershowitz90rewrite.html Rewrite Systems] (1990) p. 6</ref> e.g. a term rule <math>f_2(f_1(x)) \rightarrow g(x)</math> is equivalent with the string rule <math>f_1f_2 \rightarrow g</math>.
| |
| | |
| 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 formalism are [[Turing complete]], and thus equivalent to [[Noam Chomsky]]'s [[unrestricted grammar]]s, which are sometimes called ''semi-Thue grammars''.<ref>D.I.A. Cohen, Introduction to Computer Theory, 2nd ed., Wiley-India, 2007, ISBN 81-265-1334-9, p.572</ref> A [[formal grammar]] only differs from a semi-Thue system by the separation of the alphabet in 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 <math>(\Sigma, A, R)</math>, where <math>A\subseteq\Sigma^*</math> 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 in terminals and non-terminals, and makes the axiom a nonterminal.<ref>Dan A. Simovici, Richard L. Tenney, ''Theory of formal languages with applications'', World Scientific, 1999 ISBN 981-02-3729-4, chapter 4</ref> The simple artifice of partitioning the alphabet in terminals and non-terminals is a powerful one; it allows the definition of the [[Chomsky hierarchy]] based on the what combination of terminals and non-terminals rules contain. This was a crucial development in the theory of [[formal languages]].
| |
| | |
| ==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 grammar]]s, which in turn are known to be isomorphic to [[Turing machine]]s. 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." (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.
| |
| | |
| == See also ==
| |
| | |
| * [[L-system]]
| |
| * [[MU puzzle]]
| |
| | |
| == Notes ==
| |
| {{reflist}}
| |
| | |
| == References ==
| |
| | |
| === Monographs ===
| |
| | |
| * [[Ronald V. Book]] and Friedrich Otto, ''String-rewriting Systems'', Springer, 1993, ISBN 0-387-97965-4.
| |
| * Matthias Jantzen, ''Confluent string rewriting'', Birkhäuser, 1988, ISBN 0-387-13715-7.
| |
| | |
| === 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 ===
| |
| | |
| <!--TODO: find article names/authors from the reflist above.-->
| |
| * 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 ===
| |
| | |
| * [[Emil Post]] (1947), ''Recursive Unsolvability of a Problem of Thue'', The Journal of Symbolic Logic, vol. 12 (1947) pp. 1–11. Reprinted in [[Martin Davis]] ed. (1965), ''The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions'', Raven Press, New York. pp. 293ff
| |
| | |
| [[Category:Formal languages]]
| |
| [[Category:Theory of computation]]
| |
| [[Category:Rewriting systems]]
| |
| | |
| [[ja:文字列書き換え系]]
| |
