← All reference docs

Semantic canonicalization (the e-graph) — design note

Status: shipped (2026-07) — commutativity + type-directed associativity; extended (2026-08, "rung 1a") with identity elements, Bool idempotence, neg involution, and the control-flow and binding rules; extended again (2026-08, "rung 1b") with a REAL E-GRAPH — hash-consed e-nodes, union-find e-classes, congruence closure, bidirectional distributivity over Int/Rat saturated to a fixpoint under explicit budgets, and cost-based extraction. The last rung of the discovery ladder (docs/discovery.md): find definitions that are the SAME FUNCTION even when their bodies differ — body-equivalence, not just same-property (rung 2) or provably-satisfies-my-spec (proof-implication).

What it is, and the honest ceiling

Two definitions can compute the same function with different bodies: (+ a b) and (+ b a); a def and its eta-expansion; two different sorts. We'd like the commons to treat these as one — so a fresh implementation dedups onto an existing proven one, and discovery finds it.

The honest ceiling: full extensional equivalence is undecidable. No engine collapses all equal functions. What an e-graph does is collapse things equal under a rewrite rule set — congruence closure over the rules, saturated to a fixpoint. A useful, bounded class, and the standard tool (egg). Anything outside the rules stays distinct; that's a soundness feature, not a gap to apologize for.

There are two complementary mechanisms for body-equivalence, and we already have one:

The e-graph is the rewriting mechanism, and its payoff for the commons is the canonical form, not a pairwise oracle.

The load-bearing invariant (unchanged from discovery.md)

Canonicalization never touches identity. A definition's identity stays the O1 hash of its actual canonical AST (SPEC §1). The e-graph computes a SEPARATE key — call it the eHash — over a rewritten form, used only to draw equivalence edges between existing objects. (+ a b) and (+ b a) remain two distinct objects with two distinct identities; the e-graph just records that they land in the same equivalence class. Semantics is a view over the hash graph, never a redefinition of it. This is what keeps the e-graph from destabilizing the foundation everything else stands on — and why it can be built additively.

The first slice: AC-normalization

The first, soundest rules are the algebraic ones for the built-in operators:

Rung 1a: the structure-removing rules

Commutativity and associativity REORDER a chain. These REMOVE structure from it, so a body carrying an identity element, a duplicated Bool operand, or a doubled neg lands in the same class as the body it equals. Each rule is stated with the types it fires on and the types it is EXCLUDED from, because the exclusions are where the soundness lives:

rulefires onexcluded from, and why
x + 0 ≡ xInt, RatFloat — -0.0 + 0.0 is +0.0, a distinct value under the kernel's Leibniz ==, so this would merge definitions that disagree on an input
x * 1 ≡ xInt, Rat, Floatnothing — x * 1.0 is x for every IEEE value: ±0.0 keeps its sign, ±inf is unchanged, and NaN stays NaN, which is an identity rather than a near-miss only because the kernel canonicalizes every NaN to one bit pattern
x and true ≡ x, x or false ≡ xBool—
x and x ≡ x, x or x ≡ xBool+ and * — they are not idempotent (a + a is 2a), so a rule keyed on "the same operand twice" rather than on which operators are idempotent would be unsound
neg (neg x) ≡ xInt, Rat, Floatnothing — neg's typing rule admits exactly those three, and flipping a sign twice restores the exact value, including ±0.0, ±inf and (canonical) NaN

Type direction is carried by the leaf's own kind, and that is exact rather than a shortcut: the checker refuses operands of mixed numeric type and the language has no numeric coercion, so an int-kinded literal inside a + proves the whole chain is Int-typed. A Float chain cannot smuggle an int 0 past the test, because such a term does not typecheck.

The unit and idempotence rules are applied where a whole chain is visible — once per maximal associative-commutative chain, not per level — so they compose with the flattening rather than fighting it.

Rung 1a: control flow and binding

These are restricted by Oath's strict evaluation order and by binding structure, not by any type's algebra. So unlike the table above they carry no Float carve-out and hold at every well-formed type.

The admitted eta heads are var and ref, and that boundary is a COST one as much as a semantic one.

The lam-head refusal, measured (#155)

The falsifier came back ZERO: admitting lam heads discovers nothing on the committed corpus. The sound rule — freeness and shifting decided by traversal, which is what the deferred attribute would make O(1) — moves no definition's normal form and creates no new equivalence:

committed corpus, codebase/ at 9f7cbf3 (2026-08-07) — a ONE-SHOT
experiment, like the tower timings above: the lam-head normalizer exists
only in the harness, so nothing in the tree regenerates these.

unique function digests                194   210 live names, 15 non-function,
                                             deduped by hash
pairs compared                      18,721
definitions whose eHash MOVED             0
NEWLY equivalent pairs                    0
equivalent pairs at baseline              0   nothing was equivalent before,
                                              either

The census says why, and says it more strongly than the pair count can: those 194 bodies normalize to 322 lam nodes, of which 3 are eta-shaped fn x. (H x) — and their heads are app (2) and self (1). Bodies only, because eHash is signature plus normalized BODY and nothing else; the corpus's property bodies carry 2 further lam nodes and no eta shapes at all. Not one lam-headed redex exists in the corpus, and none of the three that do exist is excluded by the cost boundary:

Method, and the two controls the zero rests on. The universe is apiFindEquiv's own — every live name resolved, kept when K == "func", deduped by hash — because a walk of meta/ would answer a question about the store's HISTORY while looking like a question about the corpus. eHash was then computed for every definition twice, once under the shipped rule and once under the lam-head rule, and the two partitions compared pairwise. An instrument that measures nothing also reports zero, and the baseline row above shows this corpus offers no positive instance of its own, so the discrimination was established synthetically first: the rule fires on fn x. ((fn y. y) x), refuses when the binder occurs free in the head, decrements outer free indices — and end-to-end, a definition whose body is a lam-head redex takes the same eHash as its already-reduced twin only when the rule is on. The corpus zero is therefore a fact about the corpus rather than about the harness.

What it does not say. It is a statement about THIS corpus, not about Oath programs in general: examples/ and apps/ are the exhibits this project chose, and the eta tower is a term the portable profile admits whether or not anyone here has written one. It also does not make the rewrite unsound — it is sound and unadmitted, which was already the position. What it removes is the reason to PAY for it. On this evidence the recommendation is that #155 closes DECLINED: the admitted-head boundary stands, now on measurement rather than on caution.

What witnesses the normal form, and what does not (#152)

eNormalize's output IS discovery: eHash is signature plus normalized body, and find --equiv groups by it. A change to the normal form does not degrade performance or break a proof — it may silently redefine equivalence classes, and the two ways it can go are worth separating. A RULE change moves only definitions containing an applicable redex, so it repartitions some classes and leaves the rest alone. A change to canonical BYTES can move every eHash while leaving the partition identical. Neither is visible as a failure anywhere obvious, which is why it is worth stating plainly what would notice.

Measured, by mutating SIX of rung 1a's rules, one at a time. Not all of them: eta reduction, the Boolean unit rules, and idempotence and several type variants were not mutated, so no witness is claimed or denied for those.

rule mutated                    goldens      caught by
---------------------------------------------------------------
`+ 0` Int/Rat                   SURVIVED     find_test.go
`* 1.0` Float                   SURVIVED     find_test.go
`or` idempotence                SURVIVED     find_test.go
`negInvolution`                 SURVIVED     find_test.go x3
`ifSelect` const-cond           SURVIVED     find_test.go x4
`ifSelect` identical-branches   SURVIVED     find_test.go x5

Six of six survived the recorded digests. Six of six were caught by the discovery-behaviour tests.

THE WITNESS FOR THESE SIX IS find_test.go, AND IT WORKS ON eHash. The relevant cases compare equivalence keys directly; they do not call apiFindEquiv or assert its printed output. That is the right level — eHash is exactly what find --equiv groups by — but it is a claim about the KEY, not about the command's returned text, and nothing here covers the latter.

THE RECORDED GOLDENS ARE NOT A SYSTEMATIC WITNESS, WHICH IS NARROWER THAN SAYING THEY WITNESS NOTHING. They do catch some rules: disabling Int * 1 moves the int-times-duplicates digest, and the Boolean unit rules moved bool-and-duplicates and bool-or-duplicates when rung 1a landed. What the measurement establishes is that they catch none of the six mutated above — + 0 Int/Rat, Float * 1, or idempotence, negInvolution, and both ifSelect forms. So they cover part of the rule set by accident of which shapes were chosen, and no argument says which part. Do not call them the witness, and do not call them useless.

A GOLDEN CASE CAN BE TOPICALLY EXACT AND STILL INCAPABLE OF WITNESSING ITS RULE, which is the finding worth carrying past this issue. bool-or-duplicates looks like it covers or idempotence and does not: the unit pass consumes the duplicates before idempotence can act. int-plus-* and + 0 are the same shape. Coverage cannot be read off case names — it has to be measured by mutation, which is why this was settled that way rather than by inspection, and why any future fixture needs its own coverage argument rather than a plausible-looking list.

THE ACCEPTED RESIDUAL GAP, stated so nobody has to rediscover it. These tests compare INLINE SYNTHETIC PAIRS, not equivalence matches among the committed corpus. So the gap is not "a change that leaves corpus matches identical" — it is narrower and differently shaped: a normal-form change that does not alter the eHash relation between any of the specific pairs those tests construct would pass, whatever it does to the corpus. Conversely, a change that repartitions real corpus definitions is not guaranteed to fail them. That is accepted deliberately, not overlooked:

Rung 1b did not close it either, and chose a different witness. Equality saturation and extraction moved the normal form far more than rung 1a did, so the gap above would have widened. What was added instead of a golden is a CORPUS-WIDE INERTNESS check (TestEgraphIsInertWithoutArithRulesOnTheCorpus): the e-graph is forced to run on every committed body, and wherever no rule fires its extraction must reproduce the e-normalized bytes exactly. That witnesses the extractor against the real population rather than against synthetic pairs — but it is silent about bodies where a rule DOES fire, and on this corpus none does.

Rung 1b: the real e-graph

Rung 1a's four bullets — no distributivity, no e-classes, no saturation, no extraction — described exactly what a CONFLUENT rule set does not need. All four are now present, because distributivity is the rule that ends confluence: a*(b+c) and a*b + a*c are equal, neither is canonically smaller in the sense a rewriter needs, and expanding one can enable a factoring that re-creates the other. There is no orientation to pick, so the class cannot be decided by rewriting a term in place.

eHash therefore runs TWO passes, and they are different kinds of thing:

eNormalize        the confluent rules, applied directly to a normal form
                  (everything above; unchanged)
eCanonicalArith   the non-confluent rules, run through an e-graph and
                  resolved by extraction (oath/egraph.go)

The structure

The rules, and where they are allowed to fire

All three are confined to + and * over Int and Rat. Both types are EXACT — Int is ℤ and Rat is ℚ — so there is no overflow and no rounding for a re-association or a re-distribution to expose.

rulefires onnote
x*(y+z) ≡ x*y + x*zInt, Ratproducts and sums of ANY arity, since both are flattened
x*y + x*z + w ≡ x*(y+z) + wInt, Ratthe inverse direction; the factor comes out of every addend that can supply it
op(x, op(y, z)) ≡ op(x, y, z)Int, Ratassociativity ACROSS A MERGED CLASS — see below

Float is excluded, and it is the same exclusion associativity already carries. a*(b+c) and a*b + a*c differ in binary64 for real inputs, so distributing over Float would merge definitions that disagree on an input. The type direction is read from isACPrim — the existing authority for "may this operator be re-associated at this operand type" — narrowed to the two exact numeric kinds, rather than from a second list that could drift from it. Operand types are synthesized against a THROWAWAY COPY of the body, because the checker publishes inferred type arguments into the term it is given and eHash must not move as a side effect of type inference.

Why associativity is a RULE here when the representation is already flat. Flattening happens at INSERTION, on syntax. Once a rewrite has merged classes, a child class can come to CONTAIN a same-operator node without any term ever having been written that way, and the flattened form of that is a node nothing else would create. It takes TWO nested sums to observe: with one, the nested chain sorts last and right-nesting reproduces the flat chain by accident.

Extraction: which term becomes the eHash

Saturation produces a set of equal terms; extraction picks one.

Budgets, and what happens at the cap

Equality saturation is unbounded in general — a product of n sums expands exponentially — so three explicit limits apply, all in oath/egraph.go:

limitvaluewhat happens when it is reached
term size2048 nodesthe e-graph is not built; the e-normalized term is hashed exactly as before
e-nodes8192saturation stops; extraction runs on the graph as it stands
saturation rounds12the same

Exceeding a limit is not an error and never produces a wrong answer. Every node in a class is equal to every other, so any representative is a correct one: what a budget costs is COMPLETENESS — two definitions that would have been found equivalent under a larger budget may not be. Stopping is also DETERMINISTIC: rule application, unions and extraction ties are all decided without reading a Go map's iteration order, so the same input under the same budget produces the same bytes every time.

The bound is regression-tested by NODE COUNT, not by timing or by scaling. TestEgraphEngineCostIsBoundedBelowTheCap runs a term dense with distributivity redexes and asserts the graph never exceeds the declared node budget — and that some row actually REACHES it, so the assertion is satisfied by the guard rather than by arithmetic. A scaling ratio was tried first and does not witness this: re-run under a 25x budget the cost-per-doubling ratios stay in the same band while absolute cost goes from 60 MB to 2.7 GB, so a missing bound is invisible to a scaling test and obvious to a node count.

A syntactic pre-check runs first and skips the whole machine for a body with no distributivity or factoring match. It is conservative, and only one direction of that matters: it has no FALSE NEGATIVES — it never skips a term a rule could fire on, because at insertion every class is a singleton, so a rule can only match a shape the term already has, and only a rule firing creates new matches.

It does admit FALSE POSITIVES, deliberately. The factoring test asks whether a sum has two PRODUCTS under it, not whether those products share a factor — deciding that here would be a second copy of the factoring rule's own matching, free to drift from it — and operand types are not consulted, so a Float chain passes the pre-check and is stopped later by the annotation. Measured on the committed corpus: 34 bodies are admitted and 0 fire a rule.

It sizes the term BEFORE it matches, and each maximal AC chain is flattened once. Both are load-bearing rather than tidy: matching walks chains, so a survey that flattened at every level was quadratic in chain depth, and running it before consulting the node cap meant the cap could not protect the case it exists for — a 65,536-node arithmetic chain that the portable profile admits and find --equiv reaches. Measured at 4 GB allocated for a 16,000-node chain before the split, 47 MB after; TestEgraphSurveyScalesOnDeepChainsAboveTheCap holds the line by scaling rather than by a wall-clock bound. A body with no arithmetic redex therefore hashes precisely the bytes it hashed before rung 1b — measured over the committed corpus, where the pass fires on nothing and moves no eHash.

Completeness limits, stated so nobody re-derives them

The invariant, now regression-tested rather than argued

oath/discovery_identity_test.go snapshots the canonical ENCODING, the IDENTITY, every property's propHash and propHashGeneral, and the store's name resolution — over the committed corpus and over a constructed store carrying the polymorphic and arithmetic shapes the corpus lacks — and re-checks them after EVERY eHash and find --equiv call, then again through a freshly opened store.

Per-call rather than end-to-end for a measured reason: an endpoint comparison cannot see a write that undoes itself over an even number of calls, and a mutant that swapped a commutative primitive's operands on every eHash passed the endpoint form of that test.

The hazard it guards is real, not decorative. Store.GetDef CACHES, so every call for one hash returns the same *Def pointer — a mutation made while hashing would be published to every later consumer in the process — and eNormalize calls chk.synth on the original subterm, which is a live write path into the structure whose bytes ARE the identity.

Why this is the right shape

Everything here draws edges over the hash graph and leaves identity alone; the rule set is a knob that only ever adds recognized equivalences; and each rule is sound by construction (we apply a law only where it holds — hence the type-direction for associativity, learned straight from the numeric tower). The commons gets a canonical-form dedup key that started modest (AC), reached the saturating engine, and never forked reality on the way.

Rendered verbatim from docs/egraph.md in the repository. The markdown is the single source; this page is a copy checked for drift in CI, so what you read here is what an implementer reads.