---
tag: A6J731Y193
kind: concept
name: Term rewriting for equational theories
msc: [68Q42, 08B05, 03B35]
sources:
  - url: https://en.wikipedia.org/wiki/Rewriting
    locator: Term rewriting systems
---

## Summary

Term rewriting replaces the symmetric equations of an equational theory by one-way rules $l \to r$ that rewrite terms.
Two terms are equal in the theory exactly when they are connected by a chain of rule applications in either direction.
When the rules are terminating and confluent, every term has a unique normal form.
Then two terms are equal in the theory exactly when their normal forms coincide.
This turns many word problems for free algebras into a mechanical computation, and the Knuth–Bendix procedure tries to find such rules.

## Explanations

### L1 human

An equation like $0 + x = x$ can be read as an instruction: wherever $0 + t$ appears, replace it by $t$.
Applying such instructions until none applies simplifies a term to a normal form.
If the instructions always stop and the final answer never depends on the order of the steps, then comparing normal forms decides equality.
For example, with the rules $0 + x \to x$ and $s(x) + y \to s(x + y)$, the term $s(0) + s(0)$ rewrites to $s(0 + s(0))$ and then to $s(s(0))$.