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.