Rewriting Systems

Arithmetic feels fundamental. It isn't. It's rewriting.

The Peano construction defines natural numbers with two symbols: 0 and S (successor). The number 3 is S(S(S(0))). Three applications of a rule to zero. No magnitude, no quantity. Just structure.

Addition needs only two rewrite rules:

Rule 1:  add(0, y)    → y
Rule 2:  add(S(x), y) → S(add(x, y))

Watch add(S(S(0)), S(0)) — that is, 2 + 1:

  add(S(S(0)), S(0))
→ S(add(S(0), S(0)))      [Rule 2]
→ S(S(add(0, S(0))))      [Rule 2]
→ S(S(S(0)))              [Rule 1]

Three. No arithmetic was performed. Symbols were shuffled according to two rules until they stopped moving. The result was always there, folded into the structure of the expression.

In Clojure:

(defn peano-add [x y]
  (if (zero? x)
    y
    (inc (peano-add (dec x) y))))

Every recursive function is a rewriting system in disguise. The base case is the rule that stops the rewriting. The recursive case is the rule that keeps it going. You didn't compute anything. You rewrote symbols until they stopped changing.

There is a puzzle game on Steam called A=B. You are given a set of rewrite rules and a starting string. Your goal: reach a target string by applying the rules.

A level might look like this:

Rules:
  ab → b
  bb → a

Start:  aabb
Goal:   a

Try it:

  aabb
→ abb     [ab → b, applied at position 1]
→ bb      [ab → b, applied at position 1]
→ a       [bb → a]

That's the whole game. Pick a rule, pick where to apply it, watch the string transform. It feels like a word puzzle. It is a word puzzle. It is also a proof.

Each step is a valid deduction. The chain from start to goal is a derivation. You are doing equational reasoning, the same process that drives theorem provers and compilers. Every level is a proof. You just don't notice because it feels like play.

The game gets hard. Some levels require dozens of steps. Some rules interact in unexpected ways. Some strings look close to the goal but are dead ends. This is not an accident. The difficulty comes from a real mathematical property: deciding whether a target is reachable from a source is, in general, undecidable. The game designers are handing you carefully curated instances of an impossible problem.

Rewrite rules can conflict. Given these equations:

x * 1 = x
x * inv(x) = 1
(x * y) * z = x * (y * z)

Turned into left-to-right rewrite rules, they work — sometimes. But what happens when two rules apply to overlapping parts of the same term?

Take inv(x) * (x * y). You could:

• Rewrite inv(x) * x to 1 using rule 2, getting 1 * y, then y.
• Rewrite (inv(x) * x) * y using rule 3 first, associating differently.

If both paths don't reach the same result, the system is broken. This is called a critical pair: two rules claiming the same piece of a term.

    inv(x) * (x * y)
       /           \
      /             \
1 * y            inv(x) * (x * y)
  |              [associativity]
  y          (inv(x) * x) * y
                  |
                1 * y
                  |
                  y

The diamond closes. Both paths reach y. This pair is fine. But when a diamond doesn't close, you need a new rule to force it shut.

The Knuth-Bendix algorithm automates this. It finds all critical pairs, checks if they converge, and when they don't, adds new rules to make them converge. It feeds the new rules back in and repeats.

(defn knuth-bendix [rules]
  (loop [rs rules]
    (let [pairs   (critical-pairs rs)
          failing (remove #(confluent? rs %) pairs)]
      (if (empty? failing)
        rs
        (recur (into rs (map new-rule failing)))))))

The algorithm doesn't always terminate. Some equation systems have no finite confluent rewriting system. But when it works, it produces something remarkable: a decision procedure generated mechanically from raw equations. An algorithm that writes its own rules.

What happens when you take rewriting systems completely seriously and build a programming language around them?

You get Maude.

In Maude, there is no control flow. No loops, no if-else chains, no sequence of statements. A program is a set of equations and rewrite rules. Execution is rewriting. Here is a sorting algorithm:

fmod SORTING is
  sort IntList .
  subsort Int < IntList .
  op nil : -> IntList .
  op _,_ : IntList IntList -> IntList [assoc id: nil] .

  vars X Y : Int .
  var L : IntList .

  eq X, Y, L = Y, X, L [owise] .
  ceq X, Y, L = X, Y, L if X <= Y .
endfm

That's it. Two equations. If X <= Y, leave them alone. Otherwise, swap them. Maude applies these rules everywhere it can, repeatedly, until the list stops changing. The list is sorted.

  3, 1, 4, 1, 5
→ 1, 3, 4, 1, 5
→ 1, 3, 1, 4, 5
→ 1, 1, 3, 4, 5

No loop counter. No index variable. No swap function. The sorted order emerges from the rules the way heat flows from hot to cold: not because anything directs it, but because the rules make every other configuration unstable. No loops. No branches. Just rules firing until nothing matches.

Mathematica's surface looks like a calculator. Underneath, it is a rewriting engine.

Symbolic differentiation in four rules:

D[x_, x_] := 1
D[c_, x_] := 0 /; FreeQ[c, x]
D[f_ + g_, x_] := D[f, x] + D[g, x]
D[f_ * g_, x_] := f * D[g, x] + g * D[f, x]

Feed it D[x^2 + 3*x, x] and watch the rules fire:

  D[x^2 + 3*x, x]
→ D[x^2, x] + D[3*x, x]           [sum rule]
→ (2*x*D[x,x]) + (3*D[x,x])      [product rule]
→ (2*x*1) + (3*1)                  [identity rule]
→ 2*x + 3

No algorithm for differentiation exists in the code. The rules are the algorithm. Each one matches a pattern and emits a replacement. Calculus is string manipulation.

It goes further. A cellular automaton is a rewriting system on a string of bits:

rule110[{1,1,1}] = 0
rule110[{1,1,0}] = 1
rule110[{1,0,1}] = 1
rule110[{1,0,0}] = 0
rule110[{0,1,1}] = 1
rule110[{0,1,0}] = 1
rule110[{0,0,1}] = 1
rule110[{0,0,0}] = 0

Generation 0:  0 0 0 0 0 0 1 0 0 0 0 0 0
Generation 1:  0 0 0 0 0 1 1 0 0 0 0 0 0
Generation 2:  0 0 0 0 1 1 1 0 0 0 0 0 0
Generation 3:  0 0 0 1 1 0 1 0 0 0 0 0 0
Generation 4:  0 0 1 1 1 1 1 0 0 0 0 0 0
Generation 5:  0 1 1 0 0 0 1 0 0 0 0 0 0
Generation 6:  1 1 1 0 0 1 1 0 0 0 0 0 0

Eight rewrite rules on triples of bits. That's all Rule 110 is. It is also Turing-complete — capable of simulating any computation. Mathematica isn't a calculator. It's a rewriting engine with good marketing.

All of this only works cleanly under one condition: confluence.

A rewriting system is confluent if, no matter what order you apply the rules, you always reach the same final result. The Church-Rosser theorem states that the lambda calculus has this property: every term that can be reduced to a normal form will reach the same normal form regardless of reduction strategy.

   a
  / \
 /   \
b     c
 \   /
  \ /
   d

That diamond is the promise. Two different paths from a — maybe you reduced the left subexpression first, maybe the right — and they converge at d. If every divergence closes like this, order is irrelevant. You can be lazy or eager, left-to-right or right-to-left. Same answer.

This is why Haskell can use lazy evaluation. The Church-Rosser property guarantees that delaying a reduction won't change the result (when a result exists). It is why optimizing compilers can reorder operations. It is why parallel reduction works.

But most interesting rewriting systems are not confluent. Add non-determinism, side effects, or rules that overlap without resolution, and the diamond shatters. Order starts to matter. Evaluation strategy becomes a design decision with consequences.

Church-Rosser tells you when you can stop worrying. The catch is, you usually can't.

In 1968, the biologist Aristid Lindenmayer invented a formalism to model plant growth. It was a rewriting system. Two rules:

A → AB
B → A

Start with A. Apply both rules simultaneously to every symbol in the string, each generation:

Gen 0:  A
Gen 1:  AB
Gen 2:  ABA
Gen 3:  ABAAB
Gen 4:  ABAABABA
Gen 5:  ABAABABAABAAB
Gen 6:  ABAABABAABAABABAABABA

Count the lengths: 1, 2, 3, 5, 8, 13, 21. The Fibonacci sequence. Nobody asked for it. Nobody encoded it. Two replacement rules on two symbols, and Fibonacci falls out as a structural inevitability.

Now interpret the symbols as drawing instructions. A: draw forward. B: draw forward. Add a bracket notation: [ saves position and angle, ] restores them. Add + and - for turning. A different L-system:

Axiom:  F
Rule:   F → F[+F]F[-F]F
Angle:  25.7°

After 4 generations:

      |
     /|\
    / | \
   |  |  |
  /|  | /|\
 / | /|/ | \
|  |/ |  |  |
| /|  | /|
|/ |  |/ |
|  |  |  |
|  |  |  |
   |
   |

One rule. A tree. Add more rules, adjust the angle, and you get grasses, ferns, entire forests. Lindenmayer wasn't programming these structures. He was setting initial conditions and letting rewriting do the rest.

def l_system(axiom, rules, n):
    s = axiom
    for _ in range(n):
        s = ''.join(rules.get(c, c) for c in s)
    return s

# Fibonacci system
print(l_system('A', {'A': 'AB', 'B': 'A'}, 6))
# ABAABABAABAABABAABABA

# Tree system
print(l_system('F', {'F': 'F[+F]F[-F]F'}, 3))

The Python is almost embarrassingly simple. The function is seven lines. The output is a forest. One rule. No intelligence. A forest.

Here is where rewriting systems stop being elegant and start being alarming.

The word problem for rewriting systems asks: given a set of rules and two strings, can one be rewritten into the other? In general, this is undecidable. No algorithm can solve it for all cases. This was proven independently by Post and Markov in 1947 — four years before anyone had a programmable computer to worry about.

Knuth-Bendix completion doesn't always terminate. Some equation systems have no finite set of rewrite rules that makes them confluent. You can run the algorithm forever, generating new rules, and it will never finish. Not because the implementation is bad, but because the mathematics doesn't allow it.

Church-Rosser guarantees confluence for the lambda calculus, but not for arbitrary systems. Most rewriting systems in the wild are not confluent, not terminating, or both.

And then there is Rule 110. Eight rules on triples of bits. It is Turing-complete. A one-dimensional rewriting system — the simplest possible kind — can simulate any computation that any computer can perform. This means it also inherits every impossibility: the halting problem, Rice's theorem, Gödel's incompleteness. All of it, from eight pattern-matching rules.

The simplest possible rules. The hardest possible questions. That's the deal.

Your compiler is a rewriting system. Your regex engine is a rewriting system. The spreadsheet formula that computes your quarterly revenue is a rewriting system. The muscle memory you use to type these words was learned through a process that looks, if you squint, like rewriting rules being added and refined until the system converges.

It was rewriting the whole time.