Editing Rewriting (section)

== Example cases ==
=== Logic ===
In [[logic]], the procedure for obtaining the [[conjunctive normal form]] (CNF) of a formula can be implemented as a rewriting system.<ref name="MarriottStuckey1998">{{cite book|author1=Kim Marriott|author2=Peter J. Stuckey|title=Programming with Constraints: An Introduction|url=https://books.google.com/books?id=jBYAleHTldsC&q=%22conjunctive+normal+form%22+%28%22%28rewrite+OR+rewriting%29+%28system+OR+engine%29%22+OR+%22term+rewriting%22%29+-wikipedia&pg=PA436|year=1998|publisher=MIT Press|isbn=978-0-262-13341-8|pages=436–}}</ref> For example, the rules of such a system would be:

:<math>\neg\neg A \to A</math> ([[double negation elimination]])
:<math>\neg(A \land B) \to \neg A \lor \neg B</math> ([[De Morgan's laws]])
:<math>\neg(A \lor B)  \to \neg A \land\neg B</math>
:<math> (A \land B) \lor C \to (A \lor C) \land (B \lor C)</math> ([[distributivity]])
:<math> A \lor (B \land C) \to (A \lor B) \land (A \lor C),</math><ref group=note>This variant of the previous rule is needed since the commutative law ''A''∨''B'' = ''B''∨''A'' cannot be turned into a rewrite rule. A rule like ''A''∨''B'' → ''B''∨''A'' would cause the rewrite system to be nonterminating.</ref>
For each rule, each [[variable (mathematics)|variable]] denotes a subexpression, and the symbol (<math>\to</math>) indicates that an expression matching the left hand side of it can be rewritten to one matching the right hand side of it. In such a system, each rule is a [[logical equivalence]], so performing a rewrite on an expression by these rules does not change the truth value of it. Other useful rewriting systems in logic may not preserve truth values, see e.g. [[equisatisfiability]].

=== Arithmetic ===
Term rewriting systems can be employed to compute arithmetic operations on [[natural number]]s.
To this end, each such number has to be encoded as a [[term (logic)|term]].
The simplest encoding is the one used in the [[Peano axioms]], based on the constant 0 (zero) and the [[successor function]] ''S''. For example, the numbers 0, 1, 2, and 3 are represented by the terms 0, S(0), S(S(0)), and S(S(S(0))), respectively.
The following term rewriting system can then be used to compute sum and product of given natural numbers.<ref>{{cite book | author1=Jürgen Avenhaus | author2=Klaus Madlener | contribution=Term Rewriting and Equational Reasoning | pages=1&ndash;43 | title=Formal Techniques in Artificial Intelligence | editor=R.B. Banerji | publisher=Elsevier | series=Sourcebook | year=1990 }} Here: Example in sect.4.1, p.24.</ref>

: <math>\begin{align}
A + 0        &\to A               & \textrm{(1)}, \\
A + S(B)     &\to S (A + B)       & \textrm{(2)}, \\
A \cdot 0    &\to 0               & \textrm{(3)}, \\
A \cdot S(B) &\to A + (A \cdot B) & \textrm{(4)}.
\end{align}</math>

For example, the computation of 2+2 to result in 4 can be duplicated by term rewriting as follows:
:<math>S(S(0)) + S(S(0))</math> <math> 
\;\;\stackrel{(2)}{\to}\;\; </math> <math>S( \; S(S(0)) + S(0) \; ) </math> <math>
\;\;\stackrel{(2)}{\to}\;\; </math> <math>S(S( \; S(S(0)) + 0 \; )) </math> <math>
\;\;\stackrel{(1)}{\to}\;\; </math> <math>S(S( S(S(0)) )),</math>
where the notation above each arrow indicates the rule used for each rewrite.

As another example, the computation of 2⋅2 looks like:
:<math>S(S(0)) \cdot S(S(0))</math> <math> 
\;\;\stackrel{(4)}{\to}\;\; </math> <math>S(S(0)) + S(S(0)) \cdot S(0) </math> <math>
\;\;\stackrel{(4)}{\to}\;\; </math> <math>S(S(0)) + S(S(0)) + S(S(0)) \cdot 0</math> <math>
\;\;\stackrel{(3)}{\to}\;\; </math> <math>S(S(0)) + S(S(0)) + 0</math> <math>
\;\;\stackrel{(1)}{\to}\;\; </math> <math>S(S(0)) + S(S(0))</math> <math>
\;\;\stackrel{\textrm{s.a.}}{\to}\;\; </math> <math>S(S( S(S(0)) )),</math>
where the last step comprises the previous example computation.

=== Linguistics ===
In [[linguistics]], [[phrase structure rule]]s, also called '''rewrite rules''', are used in some systems of [[generative grammar]],<ref name="Freidin1992">{{cite book|author=Robert Freidin|title=Foundations of Generative Syntax|url=https://books.google.com/books?id=YPCVQxYmKsgC&q=%22rewrite+rules%22|year=1992|publisher=MIT Press|isbn=978-0-262-06144-5}}</ref> as a means of generating the grammatically correct sentences of a language. Such a rule typically takes the form <math>\rm A \rightarrow X</math>, where A is a [[syntactic category]] label, such as [[noun phrase]] or [[sentence (linguistics)|sentence]], and X is a sequence of such labels or [[morpheme]]s, expressing the fact that A can be replaced by X in generating the constituent structure of a sentence. For example, the rule <math>\rm S \rightarrow NP\ VP</math> means that a sentence can consist of a noun phrase (NP) followed by a [[verb phrase]] (VP); further rules will specify what sub-constituents a noun phrase and a verb phrase can consist of, and so on.