# Term Rewriting Systems

Dec 12, 2023I’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
```