Introduction

What this is

Semper is a term rewriting and equality saturation engine. Programs can snapshot and restore its state with semi-persistent (push) and (pop), and can issue anti-unification queries over e-classes. Semper is a command-line program that reads a text file of S-expression commands in order. Every program in this book is one such file.

Semper lets a program tag operators with algebraic properties such as associativity, commutativity, idempotence, an identity element, or a declared nilpotence order. The engine enforces those properties through automatic term canonization instead of rewrite rules. For an associative and commutative operator, children are represented as a sorted multiset. One e-node therefore represents every reassociation and permutation of that multiset, compressing a whole family of AC-equivalent terms without enumerating its members.

The engine also answers more than equality questions. An anti-unification query returns a term that preserves shared structure and marks the remaining disagreements with Variants nodes.

The five parts

In Part I, we build the binary, write and run a program, declare operators with algebraic properties, and write rules over ordinary, sequence, multiset, and set operators.

In Part II, we explain what the e-graph stores, how saturation runs, how canonization implements declared algebraic properties, and how the three congruence modes differ.

In Part III, we explain what anti-unification computes, how exact search, graph search, and their hybrid work, and what an optimal result is optimal over.

In Part IV, we apply the engine to autoformalization. We sample a formalizer several times, cluster the samples by equality saturation, and anti-unify across clusters to explain the remaining differences.

In Part V, we extract terms under cost models: costs written as scripts, in Rust, as answer-set programs, or in MiniZinc, solved by an internal or an external solver. Chapter 24 opens the part.

What you need to know already

We assume that you are familiar with first-order terms and rewrite rules. We do not assume any experience with Semper or with e-graphs, equality saturation, AC canonization, or anti-unification; we introduce each of them from scratch.

The examples

Every program shown in this book lives in doc/book/examples/ and is included in its chapter directly from that file. The book_examples test executes every .egg file at the top level of that directory. The book_cost_model_examples test runs the Part V programs in examples/cost-models/ and compares each output with its .out file. It skips a program whose external solver is not installed.

Each example states the behavior the chapter relies on, either with check or checkau assertions or, for a program the book shows being rejected, with an EXPECT directive naming the failure. A change in engine behavior therefore fails a test instead of silently invalidating the book. Every number, size, ratio, and error message quoted in the book was captured by running the corresponding file.

What this book is not

This book is not the design documentation. It states what a user needs to run and understand the engine. The design chapters are the source of truth for storage, algorithms, and implementation invariants. When more detail is needed, this book links to the relevant design chapter instead of restating its specification.

This book is also not a paper. It proves no theorems. When an implementation claim rests on a prose argument rather than a machine-checked proof, the book states that boundary and links to the design chapter containing the argument.