Editing Rewriting (section)

== String rewriting systems ==
{{Main|String rewriting system}}

A ''string rewriting system'' (SRS), also known as ''semi-Thue system'', exploits the [[free monoid]] structure of the [[String (computer science)|strings]] (words) over an [[Alphabet (computer science)|alphabet]] to extend a rewriting relation, <math>R</math>, to ''all'' strings in the alphabet that contain left- and respectively right-hand sides of some rules as [[substring]]s. Formally a semi-Thue system is a [[tuple]] <math>(\Sigma, R)</math> where <math>\Sigma</math> is a (usually finite) alphabet, and <math>R</math> is a binary relation between some (fixed) strings in the alphabet, called the set of ''rewrite rules''. The ''one-step rewriting relation'' <math>\underset{R}\rightarrow</math> induced by <math>R</math> on <math>\Sigma^*</math> is defined as: if <math>s, t \in \Sigma^*</math> are any strings, then <math>s \underset{R}\rightarrow t</math> if there exist <math>x, y, u, v \in \Sigma^*</math> such that <math>s = xuy</math>, <math>t = xvy</math>, and <math>u R v</math>. Since <math>\underset{R}\rightarrow</math> is a relation on <math>\Sigma^*</math>, the pair <math>(\Sigma^*, \underset{R}\rightarrow)</math> fits the definition of an abstract rewriting system. Since the empty string is in <math>\Sigma^*</math>, <math>R</math> is a subset of <math>\underset{R}\rightarrow</math>. If the relation <math>R</math> is [[symmetric relation|symmetric]], then the system is called a ''Thue system''.

In a SRS, the reduction relation <math>\overset{*}\underset{R}\rightarrow</math> is compatible with the monoid operation, meaning that <math>x \overset{*}\underset{R}\rightarrow y</math> implies <math>uxv \overset{*}\underset{R}\rightarrow uyv</math> for all strings <math>x, y, u, v \in \Sigma^*</math>. Similarly, the reflexive transitive symmetric closure of <math>\underset{R}\rightarrow</math>, denoted <math>\overset{*}{\underset R \leftrightarrow}</math>, is a [[Congruence relation|congruence]], meaning it is an [[equivalence relation]] (by definition) and it is also compatible with string concatenation. The relation <math>\overset{*}\underset{R} \leftrightarrow</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>\overset{*}\underset{R}\rightarrow</math> coincides with the Thue congruence <math>\overset{*}{\underset R \leftrightarrow}</math>.

The notion of a semi-Thue system essentially coincides with the [[presentation of a monoid]]. Since <math>\overset{*}{\underset R \leftrightarrow}</math> is a congruence, we can define the [[factor monoid]] <math>\mathcal{M}_R = \Sigma^*/\overset{*}{\underset R \leftrightarrow}</math> of the free monoid <math>\Sigma^*</math> by the Thue congruence. 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 <math>\{ a,b \}</math> with the rules <math>\{ ab \rightarrow \varepsilon, ba \rightarrow \varepsilon \}</math>, where <math>\varepsilon</math> is the [[empty string]], is a presentation of the [[free group]] on one generator. If instead the rules are just <math>\{ ab \rightarrow \varepsilon \}</math>, then we obtain a presentation of the [[bicyclic monoid]]. Thus semi-Thue systems constitute a natural framework for solving the [[word problem (mathematics)|word problem]] for monoids and groups. In fact, every monoid has a presentation of the form <math>(\Sigma, R)</math>, i.e. it may always be presented by a semi-Thue system, possibly over an infinite alphabet.

The word problem for a semi-Thue system is undecidable in general; this result is sometimes known as the ''Post–Markov theorem''.<ref>Martin Davis et al. 1994, p.&nbsp;178</ref>