= String rewriting
<String rewriting> transforms a <string> by replacing an occurrence of the left side of a rule $\ell\to r$ with its right side, leaving the surrounding context unchanged. A system may offer several applicable rules or positions, so a reduction need not be deterministic.
For example, $ab\to ba$ changes $aab$ to $aba$ and then $baa$. A system is terminating if no infinite chain of rewrites exists; it is confluent if any two results reached from the same string can be rewritten to a common result. Together these properties give a unique irreducible normal form. This is useful for deciding equality in algebraic presentations and for implementing symbolic simplification.
Back to article page
