Skip to main content

XTK: Expression Toolkit for Symbolic Computation

3 min read Updated:
Python symbolic-computation term-rewriting pattern-matching REPL mathematics

XTK (Expression Toolkit) is a Python library for symbolic computation through rule-based term rewriting. It provides pattern matching, expression transformation, and an interactive REPL with rich visualizations.

Quick Start

The fastest way to explore XTK is through 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 (like Lisp) as its primary representation:

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

Infix Notation

For convenience, XTK also supports infix notation:

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 defined as [pattern, skeleton] pairs using pattern variables:

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'] — Variable matching any expression
  • [':', 'x'] — Skeleton reference to matched variable

Built-in Rewrite Rules

XTK includes 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]

Interactive 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

Step-by-Step Tracing

Watch how expressions simplify:

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

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

Use Cases

  • Computer Algebra: Symbolic differentiation, integration
  • Compiler Optimization: Peephole optimization rules
  • Theorem Proving: Automated reasoning
  • DSL Implementation: Custom language semantics
  • Education: Teaching term rewriting and lambda calculus

Expression Visualization

The REPL can display expression trees:

xtk> (* (+ a b) (- c d))
xtk> /tree

        *
       / \
      +   -
     / \ / \
    a  b c  d

Installation

pip install xpression-tk

Resources

XTK: Where pattern matching meets symbolic computation. Define the rules, let the engine do the rest.

Related Posts

Discussion