Term Rewriting

Taylor Hogge

Dec 12, 2023

A Term Rewriting System (TRS) is a set of rewrite rules that express transformations from one mathematical expression into another.

Rewrite rules are defined using the arrow -> symbol. The left side of the arrow is a pattern, which matches an incoming expression, and the right side of the arrow produces the rewritten expression <pattern> -> <rewritten>. For example, a rule could specify that not true should be rewritten as false: not true -> false

Rewrite rules can also include variables that will match any subexpression. Variables are marked using $ as a prefix. For example, we could write a rule that rewrites any expression plus zero to remove the addition: $x + 0 -> $x. This rule would apply to (2 * x) + 0 to produce 2 * x

Rewriting systems can be a useful way to define formal systems. Here is a TRS that can reduce a statement in propositional logic into its conjunctive normal form. We can use this system to reason about the mortality of Socrates.

not true -> false
not false -> true

true or $x -> true
false or $x -> $x

true and $x -> $x
false and $x -> false

if true then $x -> $x
if false then $x -> false
if true then $x else $y -> $x
if false then $x else $y -> $y

not (not $x) -> $x
not ($x and $y) -> (not $x) or (not $y)
not ($x or $y) -> (not $x) and (not $y)
($x and $y) or $z -> ($x or $z) and ($y or $z)
$x or ($y and $z) -> ($x or $y) and ($x or $z)

$x mortal? -> if ($x man?) then true
socrates man? -> true

()

Tip: Use the button to apply a rewrite to the expression above

Here's another TRS that implements basic Peano arithmetic. We can use this to demonstrate that x * 2 is equivalent to x + x

1 -> S 0
2 -> S (S 0)
3 -> S (S (S 0))
4 -> S (S (S (S 0)))
5 -> S (S (S (S (S 0))))

$x + 0 -> $x
$x + (S $y) -> S ($x + $y)

$x * 0 -> 0
$x * (S $y) -> $x + ($x * $y)

$x = $x -> true
$x = $$y -> false

()

Term Rewriting Systems let us define new logical operators and reason about their behavior in a formal manner. We can think of a rewrite rule that has no variables socrates man? -> true as a fact; a single piece of knowledge. Rewrite rules with variables $x mortal? -> if ($x man?) then true let us deduce new facts from the existing ones.

To demonstrate that term rewriting systems are turing complete, here's one that uses a turing machine to write "abc" to its tape $n + 1 times.

new_tape -> TAPE (() 0 ())

write $x (TAPE ($l $h $r)) -> TAPE ($l $x $r)

left (TAPE (() $h $r)) -> TAPE (() 0 ($h $r))
left (TAPE (($n $l) $h $r)) -> TAPE ($l $n ($h $r))

right (TAPE ($l $h ())) -> TAPE (($h $l) 0 ())
right (TAPE ($l $h ($n $r))) -> TAPE (($h $l) $n $r)

(TAPE $t) (A $n) -> (right (write a (TAPE $t))) (B $n)
(TAPE $t) (B $n) -> (right (write b (TAPE $t))) (C $n)
(TAPE $t) (C (S $n)) -> (right (write c (TAPE $t))) (A $n)
(TAPE $t) (C 0) -> (right (write c (TAPE $t))) DONE
(TAPE $t) DONE -> $t

1 -> S 0
2 -> S (S 0)
3 -> S (S (S 0))
4 -> S (S (S (S 0)))

abcs $n -> new_tape (A $n)

()

The Rust source code that power these WASM demos can be found on Github at irreducible-io/term-rewriting

Additional Reading