Equality saturation

Equality saturation repeatedly matches and applies rules, rebuilds the e-graph, and stops at an operational fixpoint, a goal, or an iteration bound. This chapter defines that round order, the forms of run, extraction, and run statistics.

A round

Before a run with an :until goal starts, Semper builds the two ground goal terms. Each iteration then performs these operations in order:

1. Rebuild the e-graph, then test the goal against the current union-find. A multiplicity past the configured width stops the run with an error here.
2. Build an immutable full index and its scheduling statistics.
3. Process the selected ordinary rules in declaration order. For each rule, schedule and collect its matches against the index, then apply its actions. The selected sequence rules then run as one batch on the same index.
4. Recycle the index and test whether the action counter is zero.

The index represents the graph immediately after step 1. Nodes and canonical forms produced by rule actions are therefore available to matching in the next iteration, after another rebuild and index construction. A rule’s matches are collected before any of that rule’s actions run.

The first example needs several rounds because each recursive rewrite creates the next dbl application that can match.

(sort N) (function z () N) (function s (N) N) (function dbl (N) N)

(rewrite (dbl (z)) (z)) (rewrite (dbl (s x)) (s (s (dbl x))))

(let two (s (s z))) (let four (s (s (s (s z))))) (let d2 (dbl two))

;; The first iteration exposes another recursive dbl application. (run 1) (check-neq d2 four)

;; Two more iterations finish this input. (run 2) (check-eq d2 four)

;; This run reaches an action-counter fixpoint before its bound. (let d4 (dbl four)) (let eight (s (s (s (s (s (s (s (s z))))))))) (run 10) (check-eq d4 eight) (print-stats)

The first one-round run cannot finish d2. Two more rounds derive d2 = four. The final run requests ten iterations but reaches its operational fixpoint after three.

The complete rule-application procedure is specified in design §7.7.

Saturation

A run reports saturation when an iteration’s action counter is zero. A union counts only when it merges two previously distinct classes. An insert counts whenever its action is applied, even when hash-consing finds an existing node, and a subsume action also counts whenever it is applied. A repeatedly matching insert or subsume rule can therefore keep saturated false without increasing the graph.

This is an operational fixpoint of the selected declared rules and the current driver. It is not a completeness result for an unstated theory. A law that was neither declared as an algebraic property nor encoded by a rule is absent. Likewise, a successful (check-neq a b) says only that a and b currently belong to different classes.

If the iteration bound is reached first, the run stops with saturated: false. The e-graph retains everything derived so far, and subsequent checks inspect that partial result.

The forms of run

The four common forms select a budget, an optional ruleset, and an optional goal:

A named run may also carry either :until goal. Each run selects exactly one ruleset. It does not combine the named ruleset with untagged rules.

(sort E) (constructor a () E) (constructor b () E) (constructor c () E) (constructor f (E) E)

(ruleset selected) (rewrite (f x) (a)) (rewrite (f x) (b) :ruleset selected)

(let term (f (c)))

;; A named run selects only rules tagged with that ruleset. (run selected 2) (check-eq term (b)) (check-neq term (a))

;; A bare run selects only untagged rules. (run 2) (check-eq term (a))

;; Distinct classes satisfy an inequality goal before the first iteration. (run 10 :goal (!= (a) (c))) (check-neq (a) (c))

;; Equal classes cannot become distinct during saturation. (run 1 :goal (!= term (a))) (check-eq term (a))

The goal is tested after rebuild and before matching in the first and every later iteration. It is rebuilt and tested once more after the final permitted round. A goal that already holds still costs zero iterations. An equality goal can become true as classes merge. An inequality goal either succeeds initially or cannot become true during that run: saturation merges classes and never splits them. :goal (!= ...) records no permanent disequality constraint.

Runs that do not saturate

Some rules generate a fresh term at every iteration. The up rewrite below can keep extending its argument, so increasing the iteration bound keeps exposing more work. An equality goal stops this run as soon as the requested depth has joined the starting term.

(function up (N) N) (rewrite (up x) (up (s x)))

;; The rewrite can keep producing larger terms. The equality goal stops this ;; run before the iteration bound. (run 100 :goal (= (up z) (up (s (s (s z)))))) (check-eq (up z) (up (s (s (s z))))) (print-stats)

The practical control is always a finite iteration bound, optionally combined with an equality goal, followed by checks for the facts the program requires. A run that repeatedly reaches its budget should be treated as a property of the rule set, not as evidence that Semper will eventually choose to stop.

Extraction

(extract t) rebuilds the graph and prints a lowest-cost ground term from t’s e-class. It uses the per-operator costs and exclusions introduced in Chapter 3. Costs are additive over the root and children, including each occurrence represented by a multiplicity.

(sort E) (constructor unit () E) (constructor wrap (E) E) (constructor expensive () E :cost 5) (constructor hidden () E :unextractable)

(union (expensive) (wrap (unit))) (union (expensive) (hidden))

;; Prints (wrap (unit)), whose cost is 2. (extract (expensive)) (check-eq (expensive) (wrap (unit)))

The class in this example contains (expensive), (hidden), and (wrap (unit)). Extraction prints (wrap (unit)): its cost is 2, (expensive) costs 5, and (hidden) is not a candidate.

Among nodes of equal cost, extraction takes the one whose term is lowest, and then the one whose content colour (a hash of its structure, the name dump-egraph gives it, Chapter 24) is smallest. The choice therefore depends only on the e-graph’s contents, not on the order nodes were created in: two runs that build the same e-graph extract the same term. Height comes before colour because, with operators of cost 0, a class can reach itself at equal cost, and a choice by colour alone could pick the cycle. An AC, ACI, or commutative node’s operands print sorted by their text.

A cycle is not itself an error when its class also has an extractable grounded member. Extraction fails when no candidate has a fully extractable child set. It reports a more specific error when every node in the requested class is marked :unextractable.

(sort E) (constructor hidden () E :unextractable) (let value (hidden)) (extract value)

A cost that is not additive, or that depends on how an AC operator’s operands are grouped, is a cost model: Chapter 24.

Extraction chooses one representative of one e-class. Anti-unification compares two e-classes and is introduced in Part III. The extraction algorithm and its failure cases are specified in design §11.1.

Statistics

(print-stats) prints the current node and class counts followed by the most recent run’s iteration count, match-step count, wall time, saturation flag, and goal flag. (print-stats :file "path.json") writes the same fields as JSON. The match-step count includes executed lowered matching steps and emitted matches. It is an implementation work measure, not a semantic match count.

print-stats does not rebuild the e-graph. Its node and class fields describe the graph when the command executes, while the remaining fields still describe the last run. The presence of a print-stats command enables match-step counting for that program.

Under the naive strategy selected by the saturation fixture, the first printed reading is 23 nodes, 9 classes, 3 iterations, and 111 match steps, with saturation true. The goal-directed run then reports 30 nodes, 10 classes, 3 iterations, and 144 match steps, with goal-met true and saturation false. Wall time depends on the machine and run.

The interpreter’s command behavior and statistics fields are specified in design §9.1.