{"id":"87e7f3d8-5496-4873-a000-9990762dfeb7","arxiv_id":"2505.00807","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper defines e-graphs with bindings as morphisms of closed semilattice-enriched monoidal categories and represents them as hierarchical hypergraphs with double-pushout rewriting.","lead":"Equality graphs let a compiler keep many equivalent versions of a program while optimizing it. This paper gives a new graphical and categorical representation that also handles variable binding, a step toward faster optimization of functional programming languages.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Proposition VI.7 rests on an unproved assertion that the structural rewrite set S induces a congruence on MEHypI(Σ), so MEHypI(Σ)/S is a well-defined closed SLat-SMC; without context closure of ⇛_S the main iff has no well-defined codomain.","rationale":"The reader's weakest_assumption identifies precisely the point I find most load-bearing: the unproved assertion that the rules S make MEHypI(Σ)/S a well-defined closed SLat-enriched SMC. Proposition VI.7 is the paper's central soundness-and-completeness result, and its proof is only a sketch that does not address the quotient construction. The concern is not that the result is false, but that the main equivalence is not established by the text. This matches the reader's CONDITIONAL verdict, so no change to the verdict is needed. I also note Lemma VI.3 is unproved, but it is secondary to the congruence problem because even if every term decomposes as a join of join-free summands, the correspondence still requires the quotient relation on e-hypergraphs to be a congruence.","tokens_in":24793,"tokens_out":4110,"duration_ms":46103,"concrete_test":"Prove or mechanically check context closure of the structural rewrite set S: for each schema rule L ⇛ R in S, especially the distributivity rule displayed after Fig. 8, and for every compatible discrete interface K, verify that L ⊗ K ⇛*_S R ⊗ K and L; K ⇛*_S R; K (and symmetrically K; L ⇛*_S K; R). A single failure of context closure would show MEHypI(Σ)/S is not a well-defined category, invalidating Proposition VI.7. As a secondary check, attempt to prove Lemma VI.3 by exhibiting a terminating rewrite strategy that pushes every + to the top level; if no such strategy exists, the decomposition step in the proof of Proposition VI.7 fails.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim, Proposition VI.7, depends on the assertion immediately after Definition VI.5 that 'MEHypI(Σ)/S is a closed SLat SMC'. This is not proved. For a quotient of a category by a relation to be a category, the relation must be a congruence: if G ⇛*_S H then C[G] ⇛*_S C[H] for every context C, including composition on either side and tensoring with an arbitrary cospan. Without this, the hom-set structure, composition, and tensor of MEHypI(Σ)/S are not well-defined, and the equivalence stated in Proposition VI.7 has no well-defined graph-rewriting side. The one-paragraph proof of Proposition VI.7 invokes Lemma VI.3 and Proposition VI.6 only; it never shows that rewriting closed Σ+-terms modulo SMC laws, SLat equations, and the distributivity law corresponds exactly to quotienting by S, nor that the representative chosen for [[f]] or [[g]] is immaterial for the subsequent DPOI rewrite by ⟨[[l]],[[r]]⟩. Lemma VI.3, also unproved, is needed to decompose every f into a join of join-free summands; if the distributivity rewrite rules are not terminating or confluent, that normalization may fail. These gaps are internal incompleteness, not a demonstrated falsehood, but they are exactly the load-bearing link between term rewriting and e-hypergraph rewriting.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a categorical semantics for e-graphs with bindings, extending the semilattice-enriched symmetric monoidal category framework of [14] to closed symmetric monoidal categories. It defines e-hypergraphs with extended interfaces and a DPOI-style rewriting relation (EDPOI), and claims in Proposition VI.7 that term rewriting of closed Σ+-terms modulo SMC laws, SLat equations, and the distributivity law is equivalent to convex EDPOI rewriting in the quotient MEHypI(Σ)/S. The proof of this central equivalence is sketched in one paragraph and relies on unproved structural assertions about the quotient and on Lemma VI.3, which is also stated without proof.","tokens_in":25128,"tokens_out":8187,"duration_ms":72881,"significance":"The paper addresses a real and current problem: equality saturation for lambda calculi. The proposed representation via hierarchical hypergraphs with internal interfaces is a natural extension of prior work and, if the main theorem is established, would provide a principled way to absorb symmetric monoidal equations into the graph representation. The explicit definitions of extended cospans, boundary complements, and EDPOI rewriting are substantial pieces of work, and the paper builds openly on the soundness/completeness theorems of [2], [5], and [14]. The verification, however, is currently incomplete at exactly the load-bearing points.","major_comments":[{"comment":"The sentence 'We collect all such rewrite schemas into a set S and then a category MEHypI(Σ)/S is a closed SLat SMC' is the load-bearing step of the whole paper and is not proved. A quotient of a category by a relation is a category only if the relation is a congruence: from G ⇛*_S H one must have C[G] ⇛*_S C[H] for every context C, in particular for composition with any cospan on either side and for tensoring with an arbitrary cospan. The paper does not show that ⇛*_S is compatible with the composition of extended cospans (Definition IV.4) or with the join operation of Fig. 8. Without this, the hom-sets of MEHypI(Σ)/S are not well-defined and the right-hand side of Proposition VI.7 has no mathematical content.","section":"§VI, after Definition VI.5"},{"comment":"Lemma VI.3 is stated without proof. It asserts that every closed Σ+-term is equivalent, modulo SMC laws, SLat-equations, and the distributivity law, to a join of join-free terms. This lemma is used in Definition VI.4 to define the term-side rewrite relation and again in the proof of Proposition VI.7. Because the rewrite set S is intended to enforce exactly these equations, the lemma is essentially a normalization claim about S; it requires either a termination/confluence argument for S or a separate proof. As it stands, the main theorem depends on an unproved normalization statement.","section":"Lemma VI.3"},{"comment":"The proof of Proposition VI.7 reduces the claim to Proposition VI.6, but the reduction is not valid as written. Proposition VI.6 is stated for a subcategory of MEHypI(Σ) whose carriers contain only edges from E ∪ E, i.e., before quotienting by S, whereas Proposition VI.7 concerns rewriting in MEHypI(Σ)/S. The proof notes that each fi is a Σ-term and its carrier has no E-edges, but it does not show that the equivalence class of [[f]] in MEHypI(Σ)/S is independent of the choice of decomposition f = f1 + ... + fn, nor that the S-rewrites (which implement the SLat equations and distributivity) commute with the rule rewrite ⟨[[l]],[[r]]⟩. The gap between the two propositions is exactly the quotient structure S that the new theorem claims to handle.","section":"Proposition VI.7"},{"comment":"The statement of Proposition VI.7 is ambiguous regarding the role of S. It reads 'f↝⟨l,r⟩ g if and only if [[f]]⇛⟨[[l]],[[r]]⟩ [[g]] in MEHypI(Σ)/S'. If rewriting on the graph side is performed in the quotient (i.e., modulo S), the rule subscript should be 'S ∪ {⟨[[l]],[[r]]⟩}' or the notation should be explained, since ⇛ is defined on objects of MEHypI(Σ), not on equivalence classes. If instead the graph side is meant to use only the single rule, then the phrase 'in MEHypI(Σ)/S' is a statement about the ambient category and the proof must show that the rewrite relation on representatives is well-defined. Neither reading is supported by the current text.","section":"Proposition VI.7, statement"},{"comment":"The composition of extended cospans is defined via a pushout H, with the assertion that 'a pushout for the composition of two cospans with discrete feet always exists'. Appendix B proves pushout existence only under hypotheses (2)–(4) of Theorem A.10. The paper does not verify these hypotheses for the composition diagram of Definition IV.4, nor does it prove that composition is well-defined on the isomorphism classes of Definition IV.5. Since MEHypI(Σ)/S is constructed from this category, this is another unproved structural requirement for the statement of Proposition VI.7.","section":"Definition IV.4"}],"minor_comments":[{"comment":"The sentence 'a more detailed comparison with the work of remains a future work' is incomplete; the reference to [28]'s authors or title is missing.","section":"§I.C"},{"comment":"The statement of the soundness/completeness theorem imported from [5] is garbled: '/llbracketf /rrbracket⇛ /llbracketE/rrbracket/llbracketg/rrbracket' should be written as something like '[[f]] ⇛*_{[[E]]} [[g]]'.","section":"§III.9"},{"comment":"The phrase 'including the distributivity law II' refers to an unlabeled displayed equation (1); the equation should be numbered and referenced consistently.","section":"§II after Definition II.12"},{"comment":"In the displayed definition of E, the third set in the union is not rendered (the line 'E = E ∪ E∪ E' appears to lose a symbol), and the overloaded use of E for both the edge set and one of its components makes the definition hard to read.","section":"Definition IV.1"},{"comment":"In the proof, the verification that f+g is a semilattice homomorphism ends with 'f(x)+g(x)+f(y)+g(y) = f(x+y)+g(x+y)', which is a typo; the final expression should be '(f+g)(x)+(f+g)(y)'.","section":"Proposition A.4"},{"comment":"The proof contains corrupted typesetting, e.g., '|B× . . .× B/bracehtipupleft /bracehtipdownright/bracehtipdownleft/bracehtipupright |A| |', and 'the fist isomorphism' should be 'the first isomorphism'.","section":"Proposition A.6"},{"comment":"The notation n\\m for the discrete e-hypergraph with vertices of m removed from n is only explained for the case when 'vertices of m is a sub-e-hypergraph of n'; the general case is ambiguous.","section":"Definition IV.4"},{"comment":"Condition (4) contains a duplicated word: 'or or v⌣w'.","section":"Definition V.2"}],"recommendation":"major_revision","confidential_remarks":"The paper is a preprint with many typographical errors and incomplete sentences, which suggest it was submitted in a preliminary state. The main theorem's proof is a sketch, and the structural well-definedness claims need to be proved. The heavy reliance on prior work by the same group ([2], [13], [14]) is not by itself a problem, but the manuscript should make explicit exactly which results are imported and which are new. I would encourage the authors to prove the congruence property for S and Lemma VI.3, and to clarify the statement of Proposition VI.7."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The main theorem, Proposition VI.7, is not actually proved in the paper. The proof is a one-paragraph reduction to Proposition VI.6, and it never addresses the new quotient structure S. The assertion right after the rewrite schemas are collected that MEHypI(Σ)/S is a closed SLat-SMC is load-bearing, and it is asserted rather than proved. Without a proof that ⇛*_S is a congruence for composition and tensor, the graph-rewriting side of the iff has no well-defined category to live in.\n\nWhat the paper does well: it gives a concrete combinatorial representation for closed semilattice-enriched SMCs using hierarchical hypergraphs, introduces extended cospans with internal interfaces, and defines convex EDPOI rewriting tailored to those cospans. The high-level idea—that the closed structure lets you absorb binding and substitution into the graph syntax, and that the SMC equations are absorbed by the combinatorial representation—is genuinely new and worth taking seriously. The paper is also honest about its place in the literature: it builds directly on [2] and [14], and the self-citation is appropriate given the subject.\n\nThe soft spots are exactly where the stress-test note lands. Lemma VI.3, the decomposition of every closed Σ+-term into a join of join-free terms, is stated without proof and is needed for the normalization step. Proposition VI.7's proof assumes that quotienting by S corresponds to rewriting modulo SLat equations and distributivity, and that the representative chosen for [[f]] is immaterial for subsequent DPOI rewriting. Neither is shown. These are gaps in the proof, not evidence of falsehood; the construction is plausible and probably repairable. But the central equivalence is not established as written.\n\nThe paper has no implementation, so the significance is conditional. That is fine for a theory paper, but it means the proof gaps are the whole ballgame.\n\nThis paper deserves a serious referee: the framework is novel and the gaps are specific enough that an expert can tell whether they close. I would send it to peer review, with the expectation of major revision—ask for a real proof of the quotient congruence and for Lemma VI.3. The reader's verdict of 'conditional' is the right one.","headline":"The paper has a plausible and well-designed framework, but the main soundness/completeness theorem is not proved: the quotient by the structural rewrite rules is asserted, not shown to be a congruence.","tokens_in":25632,"tokens_out":3264,"would_cite":false,"duration_ms":33230,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["18M05","68Q42","03B40"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper claims that equality saturation for lambda calculi can be carried out directly on hierarchical e-hypergraphs, where binding boxes and equivalence boxes are native and the symmetric monoidal equations are absorbed by the graph…","keywords":["equality saturation","e-graphs","lambda calculus","hierarchical hypergraphs","string diagrams","double-pushout rewriting","closed symmetric monoidal categories","variable binding"],"falsifier":"One concrete test is to search for a counterexample to the unproved congruence property: find e-hypergraphs $G$, $H$, and $K$ such that $G$ rewrites to $H$ via schema $S$ but $G$ followed by, or tensored with, $K$ does not rewrite to $H$ followed by, or tensored with, $K$ by the same rule system. Such a pair would show that $\\mathrm{MEHypI}(\\Sigma)/S$ is not a category and that Proposition VI.7 fails. A smaller-scale check is to enumerate all closed $\\Sigma^+$-terms of small depth over a one-object signature, test term equality in the theory, and verify that their e-hypergraph interpretations land in the same rewrite-connected component exactly when term equality holds.","tokens_in":24600,"feed_emoji":"🧩","tokens_out":9997,"duration_ms":100738,"temperature":0.7,"pith_summary":"Equality saturation is a rewriting technique that keeps all equivalent versions of a term around instead of destroying alternatives, but it has never sat comfortably with variable binding because alpha-equivalent terms do not share syntax. This paper tries to remove that obstacle by moving the whole construction one level up: e-graphs become morphisms of a free semilattice-enriched closed symmetric monoidal category, and lambda abstraction is represented by an explicit hierarchical box rather than by names or de Bruijn indices. The central claim is an if-and-only-if theorem: two closed terms are equal modulo the symmetric monoidal laws, the semilattice equations, and distributivity exactly when their renderings as hierarchical e-hypergraphs rewrite to one another through a concrete double-pushout rule system. A sympathetic reader would care because, if the theorem holds, equality saturation for functional programs no longer needs explicit substitutions and shifting operations as add-on bookkeeping; the categorical representation itself absorbs those equations.","feed_headline":"Nested boxes let e-graphs handle lambda bindings","feed_subtitle":"Term rewriting and e-hypergraph rewriting coincide, so equality saturation can target lambda calculus directly.","key_machinery":"The central object is the hierarchical e-hypergraph: a monogamous directed acyclic hypergraph with ordered external and internal interfaces, whose edges are layered by two kinds of hierarchical boxes—e-boxes, which mark equivalence classes of subdiagrams, and $\\lambda$-boxes, which mark abstractions with a dangling wire for the bound variable—together with predecessor relations that record nesting and a consistency relation that records which ports of a box belong to the same equivalence class. The rewrite mechanism is convex extended DPOI rewriting, whose boundary complements and convexity conditions ensure that deleting and inserting a rule occurrence keeps the graph monogamous, directed, acyclic, and well-typed. The machinery's job is absorption: the symmetric monoidal equations are baked into hypergraph isomorphism, while the rule schema $S$, quotiented into $\\mathrm{MEHypI}(\\Sigma)/S$, absorbs semilattice and distributivity equations, so the only rewrites left are user equations such as $\\beta$-like rules.","core_discovery":"The paper's central discovery is that a free closed symmetric monoidal category enriched in semilattices has exactly the structure needed to make e-graphs with bindings. Writing terms as string diagrams of this category, $\\lambda$ abstraction becomes a box with a dangling bound wire, and an equivalence class of subterms becomes another kind of box; both are layered into a single hierarchical hypergraph. The paper then proves, as Proposition VI.7, that for closed $\\Sigma^+$-terms $f$ and $g$, $f$ rewrites to $g$ modulo SMC laws, semilattice equations, and the distributivity law if and only if their interpretations as morphisms of $\\mathrm{MEHypI}(\\Sigma)/S$ rewrite to each other under convex extended double-pushout rewriting with interfaces. In other words, the graph representation does not just approximate the term theory; it is the term theory, with the symmetric monoidal equations absorbed by graph isomorphism and the semilattice and distributivity equations absorbed by the quotient rewrite rules.","pith_inferences":["Editorial inference: if the congruence gap in the proof of Proposition VI.7 is repaired, the same recipe—closed semilattice-enriched symmetric monoidal categories plus hierarchical hypergraphs—should transfer to linear, ordered, or dependent binding disciplines by changing the ambient closed category.","Editorial inference: the paper leaves algorithmics untouched; a natural next test is whether convexity and boundary-complement conditions can be checked and repaired efficiently during saturation, because those conditions govern whether each rewrite is admissible.","Editorial inference: idempotent join and absorbed distributivity suggest a normal form for e-hypergraph states as sums of join-free diagrams, which could serve as a canonical size measure and termination heuristic, although the paper does not develop one."],"forward_implications":["Equality saturation for a lambda calculus can be implemented by rewriting hierarchical e-hypergraphs directly, without explicit-substitution nodes or de Bruijn shifting; beta-reduction becomes a local rewiring when an application node meets a lambda-box.","The quotient by $S$ means all semilattice and distributivity equivalences are handled by the graph structure rather than by search, so the saturation engine only needs to fire user equations plus the structural schema rules.","Because the theorem is an if-and-only-if, unreachable graph pairs correspond exactly to non-equal terms; a saturation run that reaches a fixpoint has already closed the theory under the given equations.","The representation makes alpha-equivalence disappear: occurrences of the same bound variable share one wire, so e-graph sharing applies to bound variables as well."],"supporting_citations":[{"why":"It establishes the semilattice-enriched categorical account of e-graphs and the e-hypergraph DPOI design for monoidal theories without bindings, which this paper extends to closed categories.","marker":"[14]"},{"why":"It supplies the string-diagrammatic syntax for lambda abstraction boxes and the diagrammatic beta-rule that the paper makes combinatorial.","marker":"[13]"},{"why":"It proves that free symmetric monoidal categories are equivalent to monogamous directed acyclic hypergraphs with interfaces and that convex DPOI rewriting is sound and complete, the base theorem for the modulo-SMC-laws part.","marker":"[5]"},{"why":"It gives rewriting for monoidal closed categories and the closed-term interpretation of evaluation and abstraction that the paper reuses as Proposition VI.6.","marker":"[2]"},{"why":"It introduces hypergraph cospans and DPO rewriting of string diagrams, from which the paper's DPOI-with-interfaces formalism is derived.","marker":"[3]"},{"why":"It introduces functorial boxes in string diagrams, the hierarchical-box idea behind the e-boxes and lambda-boxes of e-hypergraphs.","marker":"[21]"}],"fun_headline_variants":["E-graphs crack lambda bindings with categorical boxes","Lambda calculus joins equality saturation via nested hypergraphs","Proof: e-hypergraph rewriting matches lambda term rewriting","Binding-aware e-graphs from closed monoidal categories"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The equivalence depends on an unproved assumption: the rewrite rules that impose semilattice and distributivity laws are compatible with composing and tensoring e-hypergraphs, so that quotienting by rewrites gives a genuine category; if that fails, the main if-and-only-if does not follow.","fun_headline_variants_meta":{"raw":{"variants":["E-graphs crack lambda bindings with categorical boxes","Lambda calculus joins equality saturation via nested hypergraphs","Proof: e-hypergraph rewriting matches lambda term rewriting","Binding-aware e-graphs from closed monoidal categories"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000745,"raw_usage":{"total_tokens":3297,"prompt_tokens":894,"completion_tokens":2403,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":510,"completion_tokens_details":{"reasoning_tokens":2338}},"tokens_in":510,"tokens_out":2403,"duration_ms":18492,"temperature":1.0,"reasoning_tokens":2338,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-16T04:34:40.827357+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"One concrete test is to search for a counterexample to the unproved congruence property: find e-hypergraphs $G$, $H$, and $K$ such that $G$ rewrites to $H$ via schema $S$ but $G$ followed by, or tensored with, $K$ does not rewrite to $H$ followed by, or tensored with, $K$ by the same rule system. Such a pair would show that $\\mathrm{MEHypI}(\\Sigma)/S$ is not a category and that Proposition VI.7 fails. A smaller-scale check is to enumerate all closed $\\Sigma^+$-terms of small depth over a one-object signature, test term equality in the theory, and verify that their e-hypergraph interpretations land in the same rewrite-connected component exactly when term equality holds.","supporting_citations":[{"cited_title":"R., B ARRETT , C., AND TIURIN , A","cited_arxiv_id":null,"evidence_quote":"It establishes the semilattice-enriched categorical account of e-graphs and the e-hypergraph DPOI design for monoidal theories without bindings, which this paper extends to closed categories."},{"cited_title":"String diagrams for λ -calculi and functional computation, 2024","cited_arxiv_id":null,"evidence_quote":"It supplies the string-diagrammatic syntax for lambda abstraction boxes and the diagrammatic beta-rule that the paper makes combinatorial."},{"cited_title":"String diagram rewrite theory ii: Rewriting with symmet ric monoidal structure","cited_arxiv_id":null,"evidence_quote":"It proves that free symmetric monoidal categories are equivalent to monogamous directed acyclic hypergraphs with interfaces and that convex DPOI rewriting is sound and complete, the base theorem for the modulo-SMC-laws part."},{"cited_title":"R., S PRUNGER , D., AND ZANASI , F","cited_arxiv_id":null,"evidence_quote":"It gives rewriting for monoidal closed categories and the closed-term interpretation of evaluation and abstraction that the paper reuses as Proposition VI.6."},{"cited_title":"String diagram rewrite theory i: Rewriting with frobeni us structure","cited_arxiv_id":null,"evidence_quote":"It introduces hypergraph cospans and DPO rewriting of string diagrams, from which the paper's DPOI-with-interfaces formalism is derived."},{"cited_title":"Functorial boxes in string diagrams","cited_arxiv_id":null,"evidence_quote":"It introduces functorial boxes in string diagrams, the hierarchical-box idea behind the e-boxes and lambda-boxes of e-hypergraphs."}],"review_version":1}