Term rewriting

Term rewriting describes computation as the repeated application of pattern-based rewrite rules to a term until no rule applies. It's the mathematical foundation of algebra simplifiers, optimizing compilers, the SKI calculus reducer, theorem provers, and rule-based DSLs. In Clojure, you encounter it in tools like core.match, meander, and any macro that manipulates code as data.

The core idea

A rewrite rule is a pair pattern → replacement. The rewriting engine walks a term, looks for any subterm matching pattern, and replaces it with replacement (after substituting bound variables). Repeat until no rule matches: that's the normal form.

Example rules for simplifying arithmetic:

x + 0   →   x
0 + x   →   x
x * 1   →   x
x * 0   →   0

Applying these to ((y + 0) * 1) + 0:

((y + 0) * 1) + 0
   → (y * 1) + 0    ;; x + 0 → x
   → y + 0          ;; x * 1 → x
   → y              ;; x + 0 → x

The same engine that reduces this expression also reduces SKI calculus or runs a tax-calculation DSL — only the rules change.

A tiny rewriter in Clojure

core.match gives you the pattern-match side. Build a rewrite step around it:

That's one step. To reach a normal form, walk the term applying step repeatedly to subterms until a pass changes nothing:

The term [:+ [:* [:+ :y 0] 1] 0] simplifies to :y — the rewriter walks inside out, applies rules, repeats until fixed.

Confluence and termination

Two important properties:

• Terminating — every rewrite sequence ends. (Bad rules can loop: x → x + 0 would never terminate.)
• Confluent — different orderings of rule applications reach the same normal form. Together with termination, this means the normal form is unique no matter how you applied the rules.

Real-world systems (Stratego, Maude, Mathematica) come with theory about how to prove rule systems terminating and confluent. For most ad-hoc Clojure rewriters you just convince yourself by inspection.

Where rewriting appears

• Compiler optimization passes: peephole rules ("x * 2 → x << 1") are rewrites.
• Algebra systems: Mathematica's ReplaceAll is the pattern-rewrite workhorse.
• The SKI reducer in this site (SKI combinators) is term rewriting in miniature.
• Macros that walk and rewrite forms — core.match patterns, meander's bidirectional matching, transducer fusion.
• Tax / pricing / business-rule DSLs in production Clojure systems.

Why this is functional

• Rules are data. A rule system is a vector of pattern/replacement pairs; you can manipulate, merge, debug, generate rule sets at runtime.
• Composition. Rule systems compose: union of rules, sequencing, fixed point. The same algebra works at any scale.
• Pure transformations. Each rule is a pure function on terms. Side effects, if any, live outside the rewriter.

Check yourself

Exercise

Extend the rewriter to handle two new rules:

• (:- x x) → 0 (anything minus itself is zero)
• (:+ x x) → (:* 2 x) (x + x becomes 2 * x)

Then rewrite [:+ [:- :y :y] [:+ :z :z]] and verify the result is [:* 2 :z].