# Rewrite.jl

**Rewrite.jl** is an efficient symbolic term rewriting engine.

There are three primary steps in the development and use of a rewriting program:

- Map each relevant function symbol to an equational theory. For example, we might specify that
`+`

is associative and commutative. - Define a system of rules to rewrite with respect to. For example, we might describe a desired rewrite from
`x + 0`

to`x`

, for all`x`

. - Rewrite a concrete term using the rules.

## Example

### Theory Definition

In this example, we'll simplify boolean propositions.

First, we'll define the theories which each function symbol belongs to. "Free" symbols follow no special axioms during matching, whereas AC symbols will match under associativity and commutativity.

```
@theory! begin
F => FreeTheory()
T => FreeTheory()
(&) => ACTheory()
(|) => ACTheory()
(!) => FreeTheory()
end
```

Using the `@theory!`

macro, we associate each of our symbols with a theory. Note that `F`

and `T`

will be a nullary (zero-argument) function, so we assign it the `FreeTheory`

.

### Rules Definition

Given the defined theory, we now want to describe the rules which govern boolean logic. We include a handful of cases:

```
@rules Prop [x, y] begin
x & F := F
x & T := x
x | F := x
x | T := T
!T := F
!F := T
!(x & y) := !x | !y
!(x | y) := !x & !y
!(!x) := x
end
```

Naming the rewriting system `Prop`

and using `x`

as a variable, we define many rules. To verbalize a few of them:

- "
`x`

and false" is definitely false. - "not true" is definitely false.
- "not (
`x`

and`y`

)" is equivalent to "(not`x`

) or (not`y`

)". - "not (not
`x`

)" is equivalent to whatever`x`

is.

Under the hood, a custom function called `Prop`

was defined, optimized for rewriting with these specific rules.

### Rewriting

Let's test it out on some concrete terms. First, we can evaluate some expressions which are based on constants:

```
julia> @rewrite(Prop, !(T & F) | !(!F))
@term(T())
julia> @rewrite(Prop, !(T & T) | !(!F | F))
@term(F())
```

We can also bring in our own custom symbols, which the system knows nothing about:

```
julia> @rewrite(Prop, a & (T & b) & (c & !F))
@term(&(a(), b(), c()))
julia> @rewrite(Prop, F | f(!(b & T)))
@term(f(!(b())))
```

Success! We've rewritten some boolean terms.