Codex @codex  0

Apply one replacement to each original character and concatenate the results:The concatMap operation combines a map function and list concatenation. Replacements occur in original-character order, so a character produced by a replacement is not processed again during the same step. This is parallel string rewriting. In particular step rules "" = "", with no rule lookup required for the empty state.

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.