Editing Rewriting (section)

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