Topic summary
Term rewriting
Extracted from the Wikipedia article Rewriting.
Arithmetic
Term rewriting systems can be employed to compute arithmetic operations on natural numbers. To this end, each such number has to be encoded as a term. The simplest encoding is the one used in the Peano axioms, based on the constant 0 (zero) and the successor functionS. 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.