Rerum (Rewriting Expressions via Rules Using Morphisms) is a Python library for pattern matching and term rewriting. It makes symbolic computation accessible through a readable DSL while keeping a clean separation between trusted and untrusted code.

The Problem

Traditional symbolic math systems tend toward two extremes. Monolithic systems like Mathematica bundle everything in. Lighter tools force you to write complex recursive traversals every time you want to transform an expression. I wanted something in between: a simple, extensible system where transformation rules are data that can be loaded, combined, and inspected.

The SICP Connection

This design reflects a core idea from Structure and Interpretation of Computer Programs: when a problem domain is complex enough, the right move is to build a language for it. Rerum’s rule DSL makes transformation logic inspectable, composable, and safe.

The engine composition operators (>> for sequencing, | for union) ensure closure: combining engines yields an engine. Same principle that makes Scheme’s procedures powerful. You can pass them, return them, combine them, no special cases. Transformation strategies are first-class.

A Readable DSL

At the heart of rerum is a domain-specific language for defining rewrite rules:

# Algebraic simplification
@add-zero[100] "x + 0 = x": (+ ?x 0) => :x
@mul-one[100]:  (* ?x 1) => :x
@mul-zero[100]: (* ?x 0) => 0

Each rule has:

• A name: @add-zero for debugging and tracing
• Optional priority: [100] determines firing order when multiple rules match
• Optional description: Human-readable explanation
• A pattern: (+ ?x 0) matches addition with zero
• A skeleton: :x is the replacement

The pattern syntax:

Symbolic Differentiation in 15 Lines

Here’s a calculus ruleset that computes symbolic derivatives:

[basic-derivatives]
@dd-const[100]: (dd ?c:const ?v:var) => 0
@dd-var-same[100]: (dd ?x:var ?x) => 1
@dd-var-diff[90]: (dd ?y:var ?x:var) => 0

[rules]
@dd-sum: (dd (+ ?f ?g) ?v:var) => (+ (dd :f :v) (dd :g :v))
@dd-product: (dd (* ?f ?g) ?v:var) => (+ (* (dd :f :v) :g) (* :f (dd :g :v)))
@dd-power: (dd (^ ?f ?n:const) ?v:var) => (* :n (* (^ :f (- :n 1)) (dd :f :v)))
@dd-exp: (dd (exp ?f) ?v:var) => (* (exp :f) (dd :f :v))
@dd-log: (dd (ln ?f) ?v:var) => (/ (dd :f :v) :f)
@dd-sin: (dd (sin ?f) ?v:var) => (* (cos :f) (dd :f :v))
@dd-cos: (dd (cos ?f) ?v:var) => (* (- (sin :f)) (dd :f :v))

With these rules loaded:

from rerum import RuleEngine, E

engine = RuleEngine.from_file("calculus.rules")

# d/dx(x^2) = 2x
engine(E("(dd (^ x 2) x)"))  # => (* 2 (* (^ x 1) 1))

The result needs simplification (another ruleset), but the differentiation itself is purely declarative.

The Security Model: Rules vs. Preludes

A key architectural decision: the separation between rules (untrusted, serializable) and preludes (trusted Python code). Rules define structural transformations. They can reference operations via the (! op args...) compute form, but those operations must be explicitly provided by the host.

XTK (Expression Toolkit) is a Python library for symbolic computation through rule-based term rewriting. You define pattern-skeleton pairs, and the engine rewrites expressions by matching and substituting until it reaches a normal form.

I built this because I kept wanting a lightweight term rewriting system that wasn’t Mathematica. Something I could embed in other projects, extend with custom rules, and use from the command line.

Quick Start

The fastest way to try it is the interactive REPL:

pip install xpression-tk
python3 -m xtk.cli

xtk> (+ 2 3)
xtk> /rewrite
Rewritten: 5

xtk> (define square (lambda (x) (* x x)))
xtk> (square 4)
xtk> /rewrite
Rewritten: 16

Core Concepts

S-Expressions

XTK uses S-expressions as its primary representation. If you’ve used Lisp, this is familiar:

(+ 1 2)           ; Addition
(* x (+ y 1))     ; Nested expressions
(lambda (x) x)    ; Lambda abstraction

Infix Notation

For people who’d rather not count parentheses, there’s infix support:

xtk> /infix 2 + 3 * 4
S-expr: (+ 2 (* 3 4))

xtk> /infix (x + y) * (x - y)
S-expr: (* (+ x y) (- x y))

Rewrite Rules

Rules are [pattern, skeleton] pairs. Pattern variables bind to subexpressions, and skeleton references substitute them back:

from xtk import rewriter

# Define rules: x + 0 => x, x * 0 => 0
rules = [
    [['+', ['?', 'x'], 0], [':', 'x']],  # x + 0 => x
    [['*', ['?', 'x'], 0], 0],            # x * 0 => 0
]

# Create rewriter and apply
rewrite = rewriter(rules)
result = rewrite(['+', 'a', 0])  # => 'a'
result = rewrite(['*', ['+', 'a', 'b'], 0])  # => 0

Pattern syntax:

• ['?', 'x'] matches any expression, binding it to x
• [':', 'x'] references the matched binding in the skeleton

Built-in Rewrite Rules

XTK ships with standard algebraic simplification rules:

; Arithmetic
(+ x 0) → x
(* x 1) → x
(* x 0) → 0
(- x x) → 0

; Boolean
(and true x) → x
(or false x) → x
(not (not x)) → x

; Lambda calculus
((lambda (x) body) arg) → body[x := arg]

Step-by-Step Tracing

This is where it gets useful for teaching. You can watch the rewriting steps:

xtk> (* (+ 1 2) (- 5 5))
xtk> /trace

Step 1: (* (+ 1 2) (- 5 5))
  Rule: (+ a b) → eval
  Result: (* 3 (- 5 5))

Step 2: (* 3 (- 5 5))
  Rule: (- a a) → 0
  Result: (* 3 0)

Step 3: (* 3 0)
  Rule: (* x 0) → 0
  Result: 0

Final: 0

REPL Commands

/help           Show all commands
/rewrite        Apply rewrite rules
/step           Single rewrite step
/trace          Show rewrite trace
/rules          List active rules
/load file.xtk  Load rule definitions
/infix expr     Parse infix to S-expr
/tree           Show expression tree
/quit           Exit REPL

Python API

from xtk import Expression, RuleSet, Engine

# Create engine with standard rules
engine = Engine.with_standard_rules()

# Parse and rewrite
expr = Expression.parse("(* (+ 1 2) (+ 3 4))")
result = engine.rewrite(expr)
print(result)  # 21

# Custom rules
rules = RuleSet([
    Rule.parse("(square ?x) → (* ?x ?x)"),
    Rule.parse("(cube ?x) → (* ?x ?x ?x)"),
])
engine.add_rules(rules)

expr = Expression.parse("(+ (square 3) (cube 2))")
result = engine.rewrite(expr)
print(result)  # 17

Expression Visualization

The REPL renders expression trees in ASCII: