{"id":"ab8e8fde-1c34-4763-a8bc-0e4465018bf2","arxiv_id":"2504.14340","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":4.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper proposes bottom-up e-matching plus semantic e-ids as a pragmatic way to make e-graphs work modulo mathematical theories.","lead":"This paper argues that e-graphs, a tool for reasoning about equal terms in computer programs, can work with specialized mathematical data like numbers, sets, and polynomials by matching rules from the bottom up and by using structured values instead of plain names. The proposal is a conceptual case with no running code or benchmarks yet.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Semantic e-ids as canonical values lack a stable key for e-node hash-consing; Section 3 never shows how congruence closure survives canonizer updates, so the 'nearly free' EMT claim is unproven.","rationale":"The reader's weakest_assumption points directly at the sufficiency of the generic union-find interface for congruence closure, matching, and extraction when e-ids are structured values. My concern sharpens one specific mechanism: canonical representatives of semantic e-ids can change when new equations are asserted, and the paper does not explain how e-node tables keyed by such e-ids remain consistent. This is load-bearing because the bottom-up lookup idiom in Section 2 and the 'nearly free' claim in Section 3 both rely on deterministic hash-consing of canonical semantic values. If a later assertion changes a child's canonical form, an existing e-node may be unfindable or duplicated, breaking both matching and congruence. The paper is a position paper with no implementation, so this is not an internal contradiction that is already disproven; it is an unverified design assumption. A small prototype could plausibly resolve it by showing that e-ids are in fact stable handles, or that a cheap re-keying pass restores soundness. Therefore I keep the reader's CONDITIONAL verdict rather than escalating to REJECT: the conceptual case is attractive, but the central mechanism is not yet demonstrated. I agree with the reader that this is the weakest assumption; among the two candidate weaknesses, the semantic-e-id/congruence issue is more fundamental than the complexity heuristic, since even a perfect complexity story would not help if the data structure cannot maintain sound equality.","tokens_in":11830,"tokens_out":10814,"duration_ms":108129,"concrete_test":"Implement a minimal prototype (about 100 lines) with e-ids as rational vectors and exactly the five-function union-find interface of Section 3. Create eids a, b, c; insert the e-node f(a+b); assert_eq(a+b, c); then check (1) whether the lookup f[canon(c)] returns the same e-id as f[canon(a+b)], and (2) whether the bottom-up loop from Section 2 fires the same rule for X=c as it did for X=a+b. If the e-node table retains an entry under the old canonical vector and returns a different e-id, the nearly-free integration fails and the paper needs an explicit re-canonicalization strategy.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central promise is that EMT comes 'nearly for free' by reusing lookups and canonizers (Section 2) through the generalized union-find interface of Section 3 (create, eq, fresh, canon, assert_eq). The weak point is that this interface is supposed to support semantic e-ids that are themselves values, e.g. vectors for linear arithmetic. In any such theory, adding an equation can change the canonical representative of an e-class: if x+y and z are asserted equal, the canonical vector for that class may become a new value that neither x+y nor z had before. Ordinary e-graphs avoid this by using stable integer e-class ids and only changing union-find parent pointers; e-node tables are keyed by the stable ids, so congruence is preserved. If e-ids are semantic values, however, an e-node stored under the old canonical child (f(x+y) keyed by vector v1) will not be found by a later lookup with the new canonical child (f(z) keyed by v2), or it will be duplicated. The paper gives no invariant specifying whether eids are stable handles or values, and no re-keying/rebuilding procedure for e-node tables when canon changes. Its bottom-up loop 'lhs = foo[bar[X],Y]' assumes that such a lookup is a single deterministic hash-cons; if canon can change between iterations, that assumption fails. This is not a question of performance tuning or missing benchmarks; it is the one mechanism that makes the title's claim true, and the paper does not establish that it is sound.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper proposes a pragmatic recipe for e-graphs modulo theories (EMT) based on two ideas: bottom-up e-matching and semantic e-ids. In bottom-up e-matching, one scans all e-classes or variables, constructs a fully ground pattern by hash-cons lookups, and asserts equality with the right-hand side, rather than expanding patterns top-down from e-class roots. Semantic e-ids replace integer e-class identifiers with theory-specific structured values (vectors, polynomials, multisets, etc.), and the union-find is replaced by a generic canonizer supporting create, eq, fresh, canon, and assert_eq. The paper argues that this combination gives EMT 'nearly for free' because it reuses existing lookups and canonizers, and that bottom-up e-matching is more powerful than top-down in the presence of theories. The manuscript is a short position/tool paper: it contains code sketches and a catalogue of candidate theory-specific union-finds, but no implementation, no benchmarks, and no formal proofs.","tokens_in":12120,"tokens_out":5150,"duration_ms":52298,"significance":"If the central claims are correct, this would be a valuable and inexpensive recipe for users of e-graphs who need built-in theories such as linear arithmetic, polynomials, multisets, or group actions. The paper is explicit about the proposed five-method interface and gives concrete examples, which makes the intended design easy to reproduce. It also states clearly that the asymptotic comparison in Section 2 is rough, which is appropriate. The main contribution, however, is not yet established: the soundness of using semantic e-ids as keys in e-node tables is not proved, and the complexity argument omits match enumeration and canonization costs. The manuscript relies heavily on the author's unpublished blog posts for several load-bearing claims, which limits verifiability. The ideas are plausible and worth pursuing, but the paper does not yet provide enough formal or experimental support for its 'nearly for free' assertion.","major_comments":[{"comment":"The manuscript uses semantic e-ids both as values and as keys for e-node tables, but it never states an invariant separating stable handles from canonical values. In an ordinary e-graph, e-class ids are stable handles and e-node tables are keyed by those ids, so congruence is preserved after unions. If an e-id is a semantic value, then a new ground equation can change the canonical representative of a class (for example, asserting x+y = z may change the canonical vector for that class to a new vector that neither original term had). In that case, an e-node stored under the old canonical child is no longer found by the Section 2 lookup `lhs = foo[bar[X],Y]`, or it is duplicated. The paper gives no re-keying or rebuilding procedure, and no theorem stating whether the e-node table and congruence closure remain sound and complete. This is load-bearing for the 'nearly for free' claim; the manuscript's own 'self-healing character' comment in Section 3.2 suggests the author is aware of incompleteness but does not formalize what invariant is preserved.","section":"Section 3 (Generalized Union Finds and Semantic E-ids)"},{"comment":"The asymptotic comparison O(E (N/E)^d) for top-down versus O(E^V d ln N) for bottom-up is marked as rough, but it omits two quantities that are essential to the matching problem: the number of matches produced and the cost of theory-specific canonization during the hash-cons lookup. Bottom-up scans a Cartesian product of variable assignments and is exponential in the number of pattern variables (E^V), while top-down's depth factor d depends on the branching structure of the e-graph; both are also at least linear in the output size. Consequently, the examples of 'bad' patterns do not by themselves establish the claim that 'bottom-up e-matching is more powerful than top-down e-matching' in the presence of theories. A precise problem statement (what counts as one match, whether all matches or only witnesses are required) and a comparison that includes match enumeration and canonizer cost are needed.","section":"Section 2 (Bottom Up E-Matching Plays Nicer With Theories)"},{"comment":"Several load-bearing claims are supported mainly by the author's own unpublished blog posts. In particular, the characterization of union-find as ground completion is credited to [32], the multiset canonizer to [36], and the linear/Gröbner canonizers to [34]. The text states that various theories 'are guaranteed to be completable to canonizers,' but it does not give proofs or cite peer-reviewed sources for termination and confluence of the relevant completion procedures. Because the entire EMT scheme presupposes that the canonizer is a well-defined function that respects the asserted equalities, the manuscript should either provide proofs, point to published treatments, or explicitly present these cases as conjectured. As written, a reader cannot verify the central claim from the manuscript alone.","section":"Section 3.2 and references [27]–[36]"}],"minor_comments":[{"comment":"In the arXiv text, the title appears as 'via Bo/t_tom-up E-Matching'; this looks like a typo for 'Bottom-up' and should be corrected.","section":"Title"},{"comment":"The phrase 'might reaosnably go' contains a typo; it should be 'might reasonably go'.","section":"Section 4"},{"comment":"The Python snippets use comments and indentation in a way that is hard to parse in the rendered text. Providing a single runnable listing with explicit `continue` statements would make the idiom clearer.","section":"Section 2"},{"comment":"The paper uses 'union find' both for the standard integer parent-pointer data structure and for the generalized theory-specific canonizer; a short table or glossary distinguishing the two would reduce confusion.","section":"Section 3"}],"recommendation":"major_revision","confidential_remarks":"The manuscript is a short position paper with no implementation or formal development. The absence of benchmarks is not by itself disqualifying if the conceptual contribution is clear, but the missing invariant for semantic e-ids is a genuine soundness gap that blocks the central 'nearly for free' claim. I would ask the authors to either provide a precise invariant and a rebuilding argument, or recast the paper as a proposal with clear open questions. The heavy reliance on self-citations is also worth addressing during revision."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This is a position paper by Philip Zucker arguing that two ingredients—bottom-up e-matching and semantic e-ids—make e-graphs modulo theories (EMT) nearly free. The conceptual case is plausible and the writing is refreshingly clear, but the central mechanism has a real gap the author doesn't confront.\n\nWhat's good: the paper crystallizes a nice observation. Bottom-up e-matching proceeds in the same direction as term insertion, so it reuses existing lookup and canonization infrastructure, whereas top-down matching requires expanding e-classes to e-nodes, which is awkward or impossible once e-ids are semantic values. The examples of theory-specific union-finds (linear arithmetic, Gröbner bases, multisets, group actions) are useful and the limitations (e.g., non-terminating completion) are acknowledged honestly. For a paper with no implementation, it does a good job of explaining why the approach should be practical.\n\nWhere it's soft: the stress-test concern is real and lands. Section 3 presents a generalized union-find API (create, eq, fresh, canon, assert_eq) and says e-ids are structured values, but it never specifies whether e-node tables are keyed by stable handles or by mutable canonical values. If x+y and z are asserted equal, the canonical representative of that class can become a new value that neither x+y nor z had. An e-node stored under the old canonical child (e.g., f(x+y) keyed by vector v1) won't be found by a later lookup with the new canonical child (f(z) keyed by v2)—or it will be duplicated, breaking congruence. The paper's claim that EMT comes \"nearly for free\" depends exactly on this. No invariant or re-keying procedure is given. This isn't a performance issue; it's a correctness question about the title claim.\n\nAlso, the paper leans heavily on the author's own blog posts for load-bearing claims (ground completion as union-find, semantic e-ids). Those are unpublished and not peer-reviewed, which is fine for intuition but not enough for verification. A prototype or a formal treatment of congruence closure over structured e-ids would address both gaps.\n\nBottom line: it's a good design argument worth engaging with. A serious referee should see it, but the referee should push hard on the re-keying question and request either a prototype or a formal invariant. If that can be fixed, this could become a useful reference for practitioners.","headline":"A readable, honest synthesis arguing bottom-up e-matching plus semantic e-ids can make e-graphs modulo theories nearly free—but the key soundness question (what happens when a canonizer changes an e-class's canonical value) is left unaddressed.","tokens_in":12658,"tokens_out":2747,"would_cite":true,"duration_ms":23409,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Bottom-up e-matching with semantic e-ids makes e-graphs modulo theories a practical, nearly free extension of the standard equality-saturation engine.","keywords":["e-graphs","e-matching","equality saturation","term rewriting modulo theories","semantic e-ids","union-find canonizer","congruence closure","SMT"],"falsifier":"Build an e-graph with a linear-arithmetic canonizer in the proposed interface and run a saturation where an asserted equality like $4x+5y=13z+2w$ is followed by a rewrite whose pattern has a variable occurring under a non-canonical subterm; if the e-node table misses a congruence that the unspecialized e-graph would find, or if canonization changes a key during rebuilding and loses a match, the nearly-free claim fails. More directly, exhibit a finite ground theory and a pattern where seeding the term bank with all subterms still leaves bottom-up matching unable to find a substitution that top-down matching finds.","tokens_in":11572,"feed_emoji":"🧅","tokens_out":6119,"duration_ms":53157,"temperature":0.7,"pith_summary":"This paper argues that two ingredients—bottom-up e-matching and semantic e-ids—turn e-graphs modulo theories into a pragmatic technique rather than a research project. Bottom-up e-matching scans the pool of already-known e-classes, grounding pattern variables through ordinary hash-cons lookups, so it needs no ability to enumerate subterms of a term. Semantic e-ids replace plain integer class identifiers with structured values from a theory-specific domain, such as linear combinations, polynomials quotiented by an ideal, multisets, or group orbits. If the recipe works, an existing e-graph engine can gain specialized theories by supplying a small canonizer interface, and equality saturation can reason about arithmetic and algebraic identities with the same generic machinery.","feed_headline":"Bottom-up e-matching makes theory-aware e-graphs nearly free","feed_subtitle":"Swap plain e-class ids for theory-specific values and one engine handles linear algebra, polynomials, and AC rewriting.","key_machinery":"The two load-bearing mechanisms are bottom-up e-matching and semantic e-ids. Bottom-up e-matching is a query strategy that iterates over e-classes in the term bank to ground pattern variables, replacing each variable by a candidate e-id and constructing the instantiated pattern by a lookup; its complexity is roughly $O(E^v d \\log N)$ in e-class count $E$, variables $v$, pattern depth $d$, and nodes $N$, versus top-down's exponential-in-depth cost. Semantic e-ids are structured values—vectors, polynomials, multisets, group elements, primitive constants, or even terms—used directly as e-class identifiers, with a theory-specific canonizer supplying the union-find interface. The e-node tables and congruence closure remain the generic glue that relates different sorts and theories.","core_discovery":"The discovery the paper is trying to establish is that the standard e-graph, viewed as a model of a set of ground equalities, can have its uninterpreted value domain replaced by a structured semantic domain without abandoning congruence closure. Each theory contributes a canonizer—a generalized union-find that implements create, eq, fresh, canon, and assert_eq—and the canonizer's output serves as the e-id. Bottom-up e-matching then proceeds in the same direction as term insertion, reusing the e-node tables and canonizers that already exist, and it can find matches even for theories where top-down e-matching would need to enumerate infinitely many or unrepresentable subterms. The paper claims that in this setting bottom-up e-matching is strictly more powerful than top-down e-matching, because seeding the term bank with subterms lets bottom-up matching reproduce every top-down match while remaining meaningful when top-down is not.","pith_inferences":["If the central claim holds, the practical bottleneck of e-graph rewriting shifts from matching algorithms to the quality of the term bank and the cost of canonization, which the paper's complexity sketch leaves out.","A natural testable extension is to combine several semantic domains at once—say multisets for AC symbols and polynomials for arithmetic—and check whether cross-theory equalities still propagate correctly through the e-node tables.","The semantic-e-id view may also change extraction: if an e-class is a canonical vector or polynomial, extracting a readable term requires a theory-specific inverse translation, which the paper does not address."],"forward_implications":["An equality-saturation engine can be extended to linear arithmetic by plugging in a Gaussian-elimination canonizer, without changing the rewriting loop.","Polynomial identities such as $\\sin(x)^2 + \\cos(x)^2 = 1$ become usable as matching facts when e-ids are elements of a polynomial quotient ring modulo a Gröbner basis.","For deep patterns with few variables, bottom-up matching avoids the exponential factor top-down pays per pattern depth.","Theories whose completion does not terminate, such as string rewriting, can still be used by stopping completion early and relying on the e-graph's self-healing behavior."],"supporting_citations":[{"why":"Defines e-graphs and the equality-saturation setting this paper extends.","marker":"[25]"},{"why":"Provides the top-down e-matching algorithm whose complexity and limitations are compared.","marker":"[5]"},{"why":"Supplies the abstract theory-combination interface that motivates the generalized union-find API.","marker":"[10]"},{"why":"Offers the closest prior framework for rewriting modulo theories, which the semantic-e-id approach builds on.","marker":"[17]"},{"why":"Supplies the general query-plan perspective in which bottom-up matching is one admissible plan.","marker":"[26]"},{"why":"Ground completion view of e-graphs that turns the union-find into a theory-specific canonizer.","marker":"[32]"}],"fun_headline_variants":["E-graphs get theory-aware with bottom-up matching","One engine for AC, linear, and polynomials via e-id semantics","Bottom-up e-matching unlocks modular theories for e-graphs","Swap e-class ids for semantic values: theory-aware e-graphs","Bottom-up e-matching beats top-down for theory-heavy e-graphs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole approach rests on the assumption that any theory-specific canonizer can be dropped into the generic union-find interface without breaking congruence closure, matching, or extraction—specifically, that canonical structured values remain usable as hash-consed e-node keys.","fun_headline_variants_meta":{"raw":{"variants":["E-graphs get theory-aware with bottom-up matching","One engine for AC, linear, and polynomials via e-id semantics","Bottom-up e-matching unlocks modular theories for e-graphs","Swap e-class ids for semantic values: theory-aware e-graphs","Bottom-up e-matching beats top-down for theory-heavy e-graphs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000841,"raw_usage":{"total_tokens":3617,"prompt_tokens":853,"completion_tokens":2764,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":469,"completion_tokens_details":{"reasoning_tokens":2672}},"tokens_in":469,"tokens_out":2764,"duration_ms":17579,"temperature":1.0,"reasoning_tokens":2672,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T11:51:22.179937+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build an e-graph with a linear-arithmetic canonizer in the proposed interface and run a saturation where an asserted equality like $4x+5y=13z+2w$ is followed by a rewrite whose pattern has a variable occurring under a non-canonical subterm; if the e-node table misses a congruence that the unspecialized e-graph would find, or if canonization changes a key during rebuilding and loses a match, the nearly-free claim fails. More directly, exhibit a finite ground theory and a pattern where seeding the term bank with all subterms still leaves bottom-up matching unable to find a substitution that top-down matching finds.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the top-down e-matching algorithm whose complexity and limitations are compared."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the abstract theory-combination interface that motivates the generalized union-find API."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Offers the closest prior framework for rewriting modulo theories, which the semantic-e-id approach builds on."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Ground completion view of e-graphs that turns the union-find into a theory-specific canonizer."}],"review_version":1}