Term Rewriting Systems

Dec 12, 2023

I’m going to begin by defining a simple language that can be used to specify term rewriting systems. We’ll start with the syntax and semantics of the language, and then move on to some interesting examples. An implementation of this language can be found on Github.

Syntax

The atomic unit of our language is a symbol — which is a utf8 string of any characters except whitespace, parentheses, or dollar signs. mySymbol, +, and 82 are all symbols.

<symbol> ::= <schar>*
<schar> ::= [^\s\(\)\$]

In addition to symbols, variables are expressed with a dollar sign prefix followed by a label which can be any valid symbol. $x, $0 are variables.

<variable> ::= $ <symbol>

symbols and variables can be composed into a tree of parenthetical expressions. For example, both x + 4 and ($n + x) == ($n + 1) are expressions.

<expression> ::= ( <term> <ws>* )*
<term> ::= <symbol> | <variable> | <subexpr>
<subexpr> ::= \( <expression> \)
<ws> ::= [\s]

Now we introduce the first and only keyword: -> (pronounced “rewrite”). Using the -> keyword, we define rewrite rules that map an input expression to an output expression. Both $x + $x -> $x * 2 and not true -> false are examples of rewrite rules.

<rule> ::= <expression> <rewrite> <expression>
<rewrite> ::= ->

A term rewriting system is a newline separated list of rewrite rules.

<trs> ::= ( <rule> \n* )*

For demonstration purposes we allow a single line of dashes to append an expression as an input for the term rewriting system.

<demo> ::= <trs> ( \n <fence> \n <expression> )?
<fence> ::= --*-

Semantics

Here is a very simple system that rewrites a to b, b to c, and so on. You can use the button below to run a single reduction step (apply one rewrite rule) to the text field.

a -> b
b -> c
c -> d
d -> e
e -> f
---
a

Our rewrite rules can use variables to match any symbol or subexpression.

quad $x -> $x $x $x $x
---
quad (quad hello)

Rewrite rules can reference each other recursively.

count $n -> count (S $n)
---
count 0

If multiple rules match the expression, the rule specified first takes precedence.

count (S (S (S $n))) -> DONE
count $n -> count (S $n)
---
count 0

Examples

Here is a system that introduces logical operators like not, and, or, and if along with De Morgan’s Laws. 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
---
socrates mortal?

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

1 -> S 0
2 -> S 1

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

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

$x = $x -> true
$x = $$y -> false
---
(x + x) = (x * 2)

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 1
3 -> S 2

abcs $n -> new_tape (A $n)
---
abcs 3

Additional Reading