Term rewriting is computation by replacing a matching part of a structured expression according to a directed rule. It explains how a symbolic simplifier, an evaluator or part of a proof tool can transform expressions step by step. The essential questions are whether the rules preserve the intended meaning, whether rewriting stops, and whether different permitted choices lead to compatible answers.
The gold standard is a transformation you can audit: identify the matched subexpression, record the substitution, justify the rule and check the result under explicit assumptions. This guide develops a small arithmetic system completely, then changes its rules to expose loops, conflicting answers and misleading shortcuts. The examples are mathematical teaching models, not certification of a compiler or production software.
Use the Gold Standard collection for the wider subject map and How X Works for mechanisms. Automated Reasoning connects transformations to evidence and search. Model Theory explains interpretations. The Education guide supplies the learning test: can you rebuild the reasoning when an assumption changes?
Choose your term rewriting route
Chapters 1–3: Understand terms and rules
Chapters 4–6: Calculate and prove stopping
Chapters 7–9: Resolve choices and overlaps
Chapters 10–12: Verify and transfer
Chapter index
Understand terms and rules · Chapters 1–3
1. Start with a tree, not a line of text
Calculate and prove stopping · Chapters 4–6
4. Calculate a complete result and count the work
Resolve choices and overlaps · Chapters 7–9
7. Understand how local disagreements become global guarantees
Verify and transfer · Chapters 10–12
10. Keep algebraic laws inside their semantic boundaries
Diagnose and learn · Chapters 13–14
CHAPTER 1 OF 14 · Understand terms and rules
1. Start with a tree, not a line of text
Give every symbol a job
Consider the expression add(s(0),s(s(0))). The constant 0 represents zero, the unary symbol s represents successor, and the binary symbol add represents addition. Each symbol has a fixed arity: zero arguments for 0, one for s and two for add. The expression is a tree whose root is add and whose children are the two numeral trees.
A term is built from these symbols and, when allowed, variables. A term without variables is called ground. Thus add(s(0),s(s(0))) is ground, while add(x,0) contains the variable x. The variable can stand for a whole term, not merely one printed character. Substituting s(s(0)) for x inserts that entire subtree.
Tree structure prevents an easy misunderstanding. Replacing the text “0” everywhere is different from applying one rule at one selected tree position. A rewrite step has a particular location and a particular matching rule. An implementation that uses unstructured text replacement may accidentally alter identifiers, parenthesisation or multiple occurrences that were supposed to remain separate.
Understand the grammar before the calculation
With our signature, s(0,0) is not a well-formed term because s takes one argument. Likewise, add(0) lacks an argument. A parser should reject these expressions before the rewriting engine tries to simplify them. Otherwise a syntax error may be misreported as a mathematical result or as a normal form.
For a first exercise, draw the tree of s(add(0,s(0))). The root is s; its child is add; add has children 0 and s(0). There are five symbol occurrences. The subtree add(0,s(0)) can be rewritten without removing the outer s. Keeping the surrounding context intact is the central discipline of a local transformation.
The Berkeley term-rewriting lecture introduces this view of terms, directed replacement and choices of strategy. The important practical habit is to separate the expression’s structure from the way it happens to be printed.
CHAPTER 2 OF 14 · Understand terms and rules
2. Distinguish an equation from an instruction
Equality permits both directions; a rule chooses one
The arithmetic equation add(0,y)=y says its two sides have the same value under the intended natural-number interpretation. The rewrite rule add(0,y) → y additionally chooses a direction of computation. It removes the addition node and the zero argument whenever the pattern matches.
If both directions were available as unrestricted rules, an expression could grow and shrink indefinitely: y could become add(0,y), then return to y, then grow again. Nothing about the correctness of the equality prevents this operational loop. Semantic validity and a useful evaluation procedure are separate requirements.
Our second rule is add(s(x),y) → s(add(x,y)). It moves one successor out of the first argument and places it around the remaining addition. Together, the two rules define addition by recursion on the first argument. The direction is deliberate: the first argument loses one successor on each recursive root application.
Record what the rule promises
A rule needs an interpretation if it is supposed to preserve meaning. Under natural-number arithmetic, s means adding one, so both rules preserve numerical value. Under an arbitrary interpretation of the symbols, that claim need not hold. A symbol named add does not force its mathematical meaning merely by its spelling.
For example, if someone interprets add as subtraction, add(0,y) → y is generally false. At y=2, the left side would mean −2 and the right side 2. The rewrite engine could still perform the syntactic replacement perfectly. Its successful execution would not establish semantic correctness.
Write the intended domain and operations beside the rules. This is a small version of the specification boundary discussed in proving software correct before it runs. Correct manipulation of a formal object is valuable only when that object represents the property or computation you actually intended.
CHAPTER 3 OF 14 · Understand terms and rules
3. Match a pattern and preserve its context
Work through one substitution
Take the rule add(s(x),y) → s(add(x,y)) and the term add(s(s(0)),s(0)). Matching the left side binds x to s(0) and y to s(0). Applying the same substitution to the right side produces s(add(s(0),s(0))). No variable may silently receive a different value halfway through that step.
Now place the same reducible expression inside another term: add(0,add(s(s(0)),s(0))). Rewriting the inner addition gives add(0,s(add(s(0),s(0)))). The outer add and its zero argument remain in place because they belong to the context around the selected occurrence.
There is also a different permitted step at the outer root: add(0,add(s(s(0)),s(0))) → add(s(s(0)),s(0)). A rewrite relation records which steps are permitted; a strategy decides which one to take next. Conflating these two levels makes it hard to tell whether a problem comes from the rules or from the engine’s choices.
Repeated variables constrain the match
A pattern pair(x,x) matches pair(s(0),s(0)), with x=s(0). It does not match pair(0,s(0)), because a single substitution cannot make x equal to two different terms. This is a structural consistency requirement, not a question of whether two expressions might later evaluate to the same number.
For example, pair(add(0,0),0) does not syntactically match pair(x,x) before simplifying its first argument. After that argument rewrites to 0, the term becomes pair(0,0), and the repeated-variable pattern matches. The availability of a rule can therefore depend on earlier transformations.
A useful trace names four things for every step: the selected position, the rule, the substitution and the resulting term. If a result is disputed, these details allow another person to reproduce the transformation without guessing which occurrence the engine changed.
CHAPTER 4 OF 14 · Calculate and prove stopping
4. Calculate a complete result and count the work
Two plus one in successor notation
Begin with add(s(s(0)),s(0)), representing 2+1. Apply the successor rule at the root to obtain s(add(s(0),s(0))). Apply it again inside the outer s to obtain s(s(add(0,s(0)))). Apply the zero rule to the remaining addition and obtain s(s(s(0))).
The final term is the numeral three. Exactly three rewrite steps were used: two successor-rule applications and one zero-rule application. Counting the final displayed expression as another step would be an off-by-one mistake; steps count transitions, not the number of states in the written sequence.
For add(s^m(0),s^n(0)), where s^m means m nested successors, the same strategy uses m+1 steps. There are m successor removals from the first argument, followed by one zero-rule step. The output is s^(m+n)(0). This count assumes both inputs are already numerals and counts each tree rewrite as one abstract operation.
An abstract step is not a complete runtime model
The result does not say that adding large machine integers takes time proportional to their numerical value in ordinary software. Unary successor notation stores a number using that many successor nodes. Binary representations have very different sizes and implementations. A statement about m+1 rewrites must keep the representation attached to it.
Even within this representation, memory allocation and traversal can change actual running time. A persistent tree implementation may share unchanged subtrees. Another implementation may copy them. Searching the whole tree for each next redex may cost more than following a known recursive position. The rewrite count is one measurement, not every measurement.
To test your understanding, compare 1+4 with 4+1. Their normal forms are the same numeral five, but this particular rule orientation uses two steps for the first and five for the second. Equal values do not imply equal evaluation traces or equal costs.
CHAPTER 5 OF 14 · Calculate and prove stopping
5. Prove termination with a decreasing quantity
A positive-integer interpretation for the whole system
For our two addition rules, assign every term a positive integer weight. Set the weight of 0 to 1; define the weight of s(t) as weight(t)+1; and define the weight of add(t,u) as 2×weight(t)+weight(u). Variables may receive any positive integer weights.
For add(0,y) → y, the left weight is 2+weight(y), so the step decreases weight by two. For add(s(x),y) → s(add(x,y)), the left weight is 2×weight(x)+2+weight(y); the right weight is 2×weight(x)+weight(y)+1. The decrease is one.
Both interpretations are strictly increasing in every argument. Therefore a decrease inside a subtree also decreases the weight of the complete surrounding term. This matters because rewriting can occur below the root. A proof checking only root steps would leave those contextual applications unexplained.
Why the argument rules out every infinite path
A strictly decreasing sequence of positive integers cannot continue forever. Since every allowed rewrite decreases our weight, there can be no infinite rewrite sequence. This establishes termination for these rules, not merely for the example 2+1 or for one chosen strategy.
For add(s(s(0)),s(0)), the weights along the displayed calculation are 8,7,6,4. They need not decrease by the same amount at every step. The final zero-rule application removes weight two, while the preceding applications each remove one. Strict decrease is the requirement.
Do not assume that counting printed characters proves termination in general. Some useful rules temporarily increase expression size. Moreover, a comparison of patterns before substitution may change when a variable is replaced by a large term. The Iowa rewriting notes explain why a termination ordering must behave properly under substitution and context. Our explicit weight calculation addresses both for this small system.
Termination does not guarantee one answer
Consider a different system with constants a,b,c and just two rules: a → b and a → c. Both b and c are irreducible. Every rewrite sequence stops after at most one step, but the same starting term has two different normal forms. Termination alone did not make the outcome independent of the choice.
A normal form is simply a term to which no rule applies. It is not automatically the intended answer, the shortest expression or a unique representative. The meaning of “normal” is relative to a particular rule set. Changing the rules can make yesterday’s normal form reducible today.
Confluence asks whether any two results reachable from the same starting term can be rewritten further to a common result. In the a,b,c example, the branches cannot meet because neither b nor c can move. The system is therefore not confluent.
Agreement does not guarantee stopping
Now use a single rule f(x) → f(f(x)). A term beginning with f can keep growing. For a ground starting term f(a), every step produces one more nested f; any two such results can be extended to the longer one. This example exposes compatible outcomes along a nonterminating chain.
The lesson is not that growth is always useless. It is that confluence and termination answer different questions. A computation may preserve the possibility of agreement without ever reaching an irreducible answer. A practical normaliser needs a justified route to a result, not merely compatible intermediate states.
When someone reports that a simplifier “works”, ask which property was established. Does it preserve meaning? Stop on this input? Stop on every input? Produce a unique normal form? Finish within a useful resource bound? These claims are connected but cannot replace one another.
CHAPTER 7 OF 14 · Resolve choices and overlaps
7. Understand how local disagreements become global guarantees
Examine the immediate fork
Local confluence concerns two single steps from the same term. It asks whether their results can eventually meet. Confluence permits the initial branches to contain any finite number of steps. The distinction is between the size of the initial divergence, not a requirement that the repair happen in one step.
Newman’s lemma provides a powerful bridge: termination together with local confluence implies confluence. The termination assumption is essential to this route of proof. A collection of examples where immediate forks rejoin does not itself establish the hypothesis for every possible term.
For our addition rules, the two root patterns cannot both match the same term: a first argument cannot simultaneously have root 0 and root s. Reductions in disjoint subtrees can be performed in either order. Nested reductions inside a substituted variable remain available after the enclosing rule, because these rules neither duplicate nor discard that variable’s occurrence.
Apply the reasoning to a visible fork
Take add(0,add(s(0),0)). The outer zero rule yields add(s(0),0), then s(add(0,0)), then s(0). Alternatively, first reduce the inner addition to s(add(0,0)), obtaining add(0,s(add(0,0))); continue until the outer zero and inner zero steps are completed. The final term is again s(0).
The example illustrates the structural argument rather than replacing it. Together with the decreasing weight from the preceding chapter, the rule-shape analysis supports unique normal forms for this system. On ground terms built only from 0,s,add, those normal forms are numerals: any remaining add node with numeral arguments would still match a rule.
This is why proving a normaliser dependable requires both a statement about possible infinite behaviour and a statement about competing finite choices. Testing several different evaluation orders is useful evidence during development, but it should be described honestly as testing unless a general argument has also been supplied.
CHAPTER 8 OF 14 · Resolve choices and overlaps
8. Repair an overlap without creating a loop
A small conflicting system
Use constants a,b and a unary symbol f. Consider f(a) → b and a → b. The term f(a) can become b directly, or it can become f(b) by rewriting its argument. Neither b nor f(b) reduces under these two rules. The system has a concrete unjoinable fork.
One proposed repair is to add f(b) → b. Now the second branch reaches b as well. For this tiny system, assign weight 2 to a, weight 1 to b, and weight(t)+1 to f(t). Every rule decreases weight, including the new rule. Thus the repair has not introduced an infinite descending computation.
The new rule is also justified by the original equations: a=b implies f(a)=f(b), while f(a)=b, so f(b)=b. This matters. Adding an arbitrary rule that forces two outputs together may repair a diagram while changing the intended equational theory.
Completion is a problem to solve, not a promise
Completion procedures systematically seek rules that resolve important overlaps while respecting an ordering. They may generate further overlaps, fail to orient a needed equation under the selected ordering, or continue indefinitely. A useful example of successful repair is not evidence that every equation set admits a convenient finite convergent presentation.
For the repaired toy system, remaining nested occurrences of a can be replaced independently, and f(a) or f(b) can collapse to b. Repeatedly nested f terms eventually collapse after their arguments are reduced. The example is small enough that these interactions can be examined directly rather than hidden behind a claim that a tool handled them.
Before accepting a new rule, ask three questions: does it follow from the intended equations, does it preserve the termination argument, and what new overlaps does it introduce? Keeping those questions together prevents the common cycle of fixing one failing test by creating another failure elsewhere.
CHAPTER 9 OF 14 · Resolve choices and overlaps
9. Choose an evaluation strategy deliberately
The relation permits choices; the engine must make them
An innermost strategy reduces eligible subterms before an enclosing expression. An outermost strategy prefers an enclosing reducible expression. These labels describe broad policies; an implementation still needs tie-breaking rules when several positions qualify. A reproducible experiment records that policy rather than treating the printed trace as inevitable.
For the terminating, confluent addition system, complete reduction reaches the same normal form under every strategy that keeps taking available steps until none remain. Costs can nevertheless differ. The engine may search different positions, create different intermediate trees or reuse different previously computed subterms.
Now add an erasing rule first(x,y) → x and a constant loop with rule loop → loop. The term first(0,loop) can reach 0 immediately by reducing the root. A strategy that insists on reducing the second argument first can repeat loop forever. This larger system is not terminating, although this particular term has a normal form.
A step limit is a limit on evidence
Suppose an engine stops after 1,000 steps. If a redex remains, it has not produced a normal form. Report the unfinished term and the resource limit. Calling the result “simplified completely” would confuse interruption with completion.
A loop detector may recognise a repeated term, as in loop → loop. It will not necessarily recognise unbounded growth such as f(a) → f(f(a)) → f(f(f(a))). A cache of previously visited exact trees is not a general termination proof.
The existing memoization explanation helps distinguish repeated subproblems from repeated call occurrences. In rewriting, cached results also depend on the rule set, assumptions and chosen normalisation procedure. Reusing an answer after changing these can make a correct cache implementation return an inappropriate result.
CHAPTER 10 OF 14 · Verify and transfer
10. Keep algebraic laws inside their semantic boundaries
A valid mathematical identity can be an unsafe program rewrite
Over mathematical integers, x+0=x and x×1=x. But a program expression is more than a mathematical value when evaluation can produce side effects, exceptions or nontermination. Replacing an expression with a shorter one may change which computations occur even when the numerical identity looks familiar.
For a simple abstract example, imagine a function tick() that increments a visible counter and returns a number. Replacing 0×tick() by 0 removes the call if the original language evaluates the argument. The returned numerical value may be unchanged, but the observable counter behaviour differs. The intended notion of equivalence must say whether that observation matters.
Likewise, floating-point arithmetic is not unrestricted real arithmetic. Rearrangement may change rounding, and special values require care. A compiler transformation must follow the actual operation semantics and permitted assumptions. The LLVM language reference is an example of the detailed specification an implementation must consult; a school algebra identity alone is insufficient evidence.
State conditional rules explicitly
The simplification x/x → 1 over real numbers requires x≠0. Without that condition, it removes an undefined case. A symbolic tool may carry the condition, restrict the input domain or decline the rewrite. Silently dropping the exceptional input changes the meaning of the original expression.
For a concrete check, use x=5, then x=0. The first supports the conditional identity; the second exposes why the unrestricted version is unacceptable. Testing only ordinary nonzero inputs would miss the domain boundary that determines correctness.
These examples distinguish equational reasoning from convenient visual simplification. A shorter result is useful only if it preserves the observations and domain conditions that the task requires. In practice, put the assumptions beside the transformed result so that a later reader does not apply it in a broader setting.
CHAPTER 11 OF 14 · Verify and transfer
11. Test a rewriting engine with independent checks
Build tests around possible faults
A useful test suite checks malformed input, successful matches, failed matches, repeated variables, nested positions and terms already in normal form. For our addition system, include add(0,0), add(s(0),0), s(add(0,0)) and a term with two separate additions. These cases exercise different parts of the engine.
Check every trace step independently: locate the old subtree, confirm the left pattern under the recorded substitution, construct the right side with that substitution, and verify the unchanged context. This catches mistakes that a final numerical check can miss. Two erroneous steps can accidentally cancel and leave a plausible final answer.
For ground arithmetic cases, evaluate both the original and resulting terms with a separate interpreter. The numerical values should match. That provides a second kind of check, but it does not establish termination or confluence for all terms. Each test should state the property it actually examines.
Keep failures reproducible
When a test fails, save the smallest input that still demonstrates the problem. For a suspected context bug, compare add(0,0) with s(add(0,0)): the first checks the root replacement, while the second checks whether the surrounding successor survives. If the engine returns zero for both, the outer context was lost. This diagnosis is more informative than simply recording that a large arithmetic example returned the wrong value.
Keep the rule identifiers and the engine version with that example. After a repair, rerun the same failing case and a neighbouring case that previously passed. A correction to subtree replacement should not accidentally change the matching behaviour of repeated variables.
Bound an experiment without overstating it
Enumerate all pairs m,n from 0 through 4. There are 25 numeral-addition inputs. For each, verify that normalisation yields m+n and that the displayed recursive strategy uses m+1 steps. This tests the implementation on a complete finite grid; the earlier argument explains why the formula holds beyond that grid.
Next change one rule deliberately to add(s(x),y) → add(x,y), omitting the outer successor. The test for 1+0 should now fail: the result becomes zero instead of one. A test suite that accepts this mutation is not checking numerical preservation adequately.
Finally, introduce both directions of an identity in a disposable test system. Confirm that the engine reports a limit or detects the repeated state rather than falsely claiming a normal form. These negative tests are particularly valuable because they check whether the reporting layer distinguishes success, failure and unresolved computation.
CHAPTER 12 OF 14 · Verify and transfer
12. Transfer the method by changing one assumption
Reverse the recursive argument
Replace the two addition rules with add(x,0) → x and add(x,s(y)) → s(add(x,y)). Now recursion consumes the second argument. For numeral inputs representing m+n, this orientation uses n+1 steps. The mathematical answer remains m+n, but the operational cost has changed.
For 1+4, the original orientation used two steps and the new orientation uses five. For 4+1, the counts reverse. Explain the difference by pointing to the argument whose successor constructors are removed; do not memorise a step formula without its rule set.
A matching weight proof also changes. Use weight(add(t,u))=weight(t)+2×weight(u), keeping zero at 1 and successor as an increment. The zero rule decreases weight by two, and the successor rule decreases it by one. Reusing the earlier weighting without checking the new inequalities would be an unjustified shortcut.
Add commutativity and inspect the consequence
Now add an unrestricted rule add(x,y) → add(y,x). Starting with add(0,s(0)), repeated swapping gives add(s(0),0), then add(0,s(0)), and so on. Other terminating choices may exist, but the enlarged rewrite relation admits an infinite sequence.
Commutativity is a valid equation for natural-number addition. The problem is its unrestricted use as a directed rule with a matching inverse instance. A practical canonicalisation scheme might order arguments and swap only when they violate that order. Such a scheme needs its own precise ordering, conditions and interaction checks.
The transfer exercise is to record three separate outcomes: arithmetic validity remains, unrestricted termination fails, and the old termination proof no longer applies. This separation is the point of the exercise. A single verdict such as “commutativity works” hides the difference between a mathematical law and an evaluation procedure.
Is a normal form always the simplest expression?
No. It means no rule in the selected system applies. If the system contains no arithmetic rules, a complicated arithmetic expression may already be normal. If the rules expand products, the normal form may be longer than the input. Simplicity needs its own objective, such as tree size, evaluation cost or a chosen presentation convention.
Can two different normal forms mean the same thing?
Yes. Under an incomplete simplification system, two irreducible expressions can have equal values. Unique syntactic representatives require stronger properties and a suitable relationship between the rules and the intended equations. Comparing outputs from an arbitrary simplifier is therefore not automatically a decision procedure for mathematical equality.
Does one successful strategy prove termination?
No. It proves that the observed computation finished. Even if a chosen strategy always finds a normal form for a class of inputs, other permitted paths may be infinite. The first(0,loop) example makes the distinction concrete. State whether a claim concerns one run, one strategy or every possible rewrite sequence.
What should I inspect when two runs disagree?
First compare the exact input trees, rules, assumptions and versions. Then compare the first divergent steps. A different choice can reveal nonconfluence; an invalid substitution can reveal an implementation error; different arithmetic domains can reveal different semantics. These require different repairs.
Should I add more rules whenever simplification gets stuck?
Only after identifying why it is stuck and what result is intended. A new rule may be valid yet create a loop, or may resolve one overlap while creating another. Check its semantic justification, orientation and interactions. A smaller reliable rule set can be more useful than an expanding collection of unexplained transformations.
Where do automated tools fit?
They can help analyse termination, confluence, complexity and completion for supported inputs. The research paper Tools in Term Rewriting for Education describes a collection built for these tasks. Read a tool’s result in the scope of its input language and supported method; unsuccessful proof search is not automatically a counterexample.
Produce three connected records
Start with a one-page specification containing the signature, grammar, intended interpretation and rules. Next produce a trace notebook with complete substitutions and positions for several examples. Finally produce an evidence record distinguishing mathematical arguments from finite implementation tests. These records answer different questions and should agree with one another.
In the first session, calculate 2+1 and 1+4 using successor terms. Count transitions and compare them with the formula m+1. In the second, derive the weight inequalities and explain why a contextual step also decreases weight. In the third, investigate the conflicting f(a) example and justify the repair f(b) → b.
For an independent handover, ask another learner to reproduce one calculation using only your specification. If they need to guess the arity of a symbol, the rewrite direction or the strategy, improve the specification. If they can reproduce the trace but cannot explain why it stops, improve the termination argument.
Continue with the question you actually have
Use the Berkeley lecture to explore rewriting and strategy, the Iowa notes for reduction orderings and canonical systems, and the Innsbruck researchers’ tools paper for automated analysis. These sources supply deeper treatments; the arithmetic and diagnostic cases above are deliberately small enough to audit by hand.
Return to Automated Reasoning when the task is to interpret computational evidence. Return to the software-correctness article when a transformation must preserve a program property. Use the memoization guide when repeated work, rather than logical validity, is the immediate bottleneck.
The final test is a changed rule. Explain what it means, show a valid step, identify the property it preserves and try to break the property it threatens. A dependable understanding of term rewriting makes those distinctions visible before a plausible-looking transformation becomes an unexplained answer.