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 + 0tox, for allx. - Rewrite a concrete term using the rules.
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()
endUsing 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.
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
endNaming the rewriting system Prop and using x as a variable, we define many rules. To verbalize a few of them:
- "
xand false" is definitely false. - "not true" is definitely false.
- "not (
xandy)" is equivalent to "(notx) or (noty)". - "not (not
x)" is equivalent to whateverxis.
Under the hood, a custom function called Prop was defined, optimized for rewriting with these specific rules.
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.
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent