{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T14:29:29Z","timestamp":1754144969317,"version":"3.41.2"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n            Equality saturation has gained significant interest as a powerful optimization and reasoning technique. At its heart is the e-graph data structure, that space-efficiently represents equal sub-terms uniquely.  \nAn important open problem in this context is extending this efficient representation to languages featuring (bound) variables.  \nIndependent of how we represent variables in e-graphs, either as names or nameless (using de Bruijn indices), sharing is broken as sub-terms that differ only in the names of their variables are represented separately.  \nThis results in aggressive e-graph growth, bad performance, as well as reduced expressiveness.  \n  \nIn this paper, we present a novel approach to representing bound variables in e-graphs by making them a first-class built-in feature of the data structure.  \nOur\n            <jats:italic toggle=\"yes\">slotted e-graph<\/jats:italic>\n            represents terms that differ only by (bound or free) variable names uniquely.  \nTo do so, e-classes that represent equivalent terms via e-nodes are parameterized by\n            <jats:italic toggle=\"yes\">slots<\/jats:italic>\n            , abstracting over free variables of the represented terms.  \nReferring to an e-class from an e-node now requires relating the variables from its context to the slots of the e-class.  \n  \nOur evaluation of slotted e-graph uses two case studies from compiler optimization and theorem proving to show that performing equality saturation for languages with bound variables is greatly simplified and that we can solve practically relevant problems that cannot be solved with e-graphs using de Bruijn indices.\n          <\/jats:p>","DOI":"10.1145\/3729326","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"1888-1910","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9151-773X","authenticated-orcid":false,"given":"Rudi","family":"Schneider","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Berlin, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-3567-6890","authenticated-orcid":false,"given":"Marcus","family":"Rossel","sequence":"additional","affiliation":[{"name":"Barkhausen Institut, Dresden, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9062-759X","authenticated-orcid":false,"given":"Amir","family":"Shaikhha","sequence":"additional","affiliation":[{"name":"University of Edinburgh, Edinburgh, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0409-1363","authenticated-orcid":false,"given":"Andr\u00e9s","family":"Goens","sequence":"additional","affiliation":[{"name":"University of Amsterdam, Amsterdam, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8461-8075","authenticated-orcid":false,"given":"Thomas","family":"K\u0153hler","sequence":"additional","affiliation":[{"name":"CNRS - ICube Lab, Strasbourg, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5048-0741","authenticated-orcid":false,"given":"Michel","family":"Steuwer","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t Berlin, Berlin, Germany"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Computational Group Theory: Proceedings of the London Mathematical Society Symposium on Computational Group Theory, Michael D. Atkinson (Ed.).","author":"Butler Gregory","year":"1984","unstructured":"Gregory Butler. 1984. On computing double coset representatives in permutation groups. In Computational Group Theory: Proceedings of the London Mathematical Society Symposium on Computational Group Theory, Michael D. Atkinson (Ed.)."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571207"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2403.14064"},{"key":"e_1_2_2_4_1","volume-title":"SEER: Super-Optimization Explorer for High-Level Synthesis using E-graph Rewriting. In ASPLOS (2). ACM, 1029\u20131044.","author":"Cheng Jianyi","year":"2024","unstructured":"Jianyi Cheng, Samuel Coward, Lorenzo Chelini, Rafael Barbalho, and Theo Drane. 2024. SEER: Super-Optimization Explorer for High-Level Synthesis using E-graph Rewriting. In ASPLOS (2). ACM, 1029\u20131044."},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Nicolaas Govert De Bruijn. 1972. Lambda calculus notation with nameless dummies a tool for automatic formula manipulation with application to the Church-Rosser theorem. In Indagationes mathematicae (proceedings). 75 381\u2013392.","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_2_2_6_1","volume-title":"Germany","author":"Moura Leonardo De","year":"2007","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2007. Efficient E-matching for SMT solvers. In Automated Deduction\u2013CADE-21: 21st International Conference on Automated Deduction Bremen, Germany, July 17-20, 2007 Proceedings 21. 183\u2013198."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2404.08106"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2006.12.002"},{"key":"e_1_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Dan R Ghica. 2021. Operational semantics with hierarchical abstract syntax graphs. arXiv preprint arXiv:2102.02363.","DOI":"10.4204\/EPTCS.334.1"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1134\/S0361768815030056"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218196704001657"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133901"},{"key":"e_1_2_2_14_1","unstructured":"Thomas Koehler. 2022. A domain-extensible compiler with controllable automation of optimisations. Ph. D. Dissertation."},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Dexter Kozen. 1977. Complexity of Finitely Presented Algebras. In STOC. ACM 164\u2013177.","DOI":"10.1145\/800105.803406"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632900"},{"key":"e_1_2_2_17_1","first-page":"19","article-title":"On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic","volume":"53","author":"Lachowski Lukasz","year":"2018","unstructured":"Lukasz Lachowski. 2018. On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic. Reports Math. Log., 53 (2018), 19\u201342. https:\/\/rml.tcs.uj.edu.pl\/rml-53\/02-lachowski.pdf","journal-title":"Reports Math. Log."},{"key":"e_1_2_2_18_1","unstructured":"Serge Lang. 2012. Algebra. 211 Springer Science & Business Media."},{"volume-title":"the Theory of Partial Symmetries","author":"Lawson Mark V","key":"e_1_2_2_19_1","unstructured":"Mark V Lawson. 1998. Inverse Semigroups, the Theory of Partial Symmetries. World Scientific Publishing Co. Pte. Ltd."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Krzysztof Maziarz Tom Ellis Alan Lawrence Andrew W. Fitzgibbon and Simon Peyton Jones. 2021. Hashing modulo alpha-equivalence. In PLDI. ACM 960\u2013973.","DOI":"10.1145\/3453483.3454088"},{"key":"e_1_2_2_22_1","doi-asserted-by":"crossref","unstructured":"Chandrakana Nandi Max Willsey Adam Anderson James R. Wilcox Eva Darulova Dan Grossman and Zachary Tatlock. 2020. Synthesizing structured CAD models with equality saturation and inverse transformations. In PLDI. ACM 31\u201344.","DOI":"10.1145\/3385412.3386012"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_2_24_1","unstructured":"Marcus Rossel. 2024. An Equality Saturation Tactic for Lean. Master\u2019s thesis."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3588717"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","unstructured":"Rudi Schneider Marcus Rossel Amir Shaikhha Andr\u00e9s Goens Thomas Koehler and Michel Steuwer. 2025. Slotted E-Graphs Artifact. https:\/\/doi.org\/10.5281\/zenodo.15237515 10.5281\/zenodo.15237515","DOI":"10.5281\/zenodo.15237515"},{"volume-title":"Permutation group algorithms","author":"Seress \u00c1kos","key":"e_1_2_2_27_1","unstructured":"\u00c1kos Seress. 2003. Permutation group algorithms. Cambridge University Press."},{"volume-title":"A Tensor Algebra Compiler for Sparse Differentiation","author":"Shaikhha Amir","key":"e_1_2_2_28_1","unstructured":"Amir Shaikhha, Mathieu Huot, and Shideh Hashemian. 2024. A Tensor Algebra Compiler for Sparse Differentiation. In CGO. IEEE, 1\u201312."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527333"},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Gus Henry Smith Andrew Liu Steven Lyubomirsky Scott Davidson Joseph McMahan Michael B. Taylor Luis Ceze and Zachary Tatlock. 2021. Pure tensor program rewriting via access patterns (representation pearl). In MAPS@PLDI. ACM 21\u201331.","DOI":"10.1145\/3460945.3464953"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Ross Tate Michael Stepp Zachary Tatlock and Sorin Lerner. 2009. Equality saturation: a new approach to optimization. In POPL. ACM 264\u2013276.","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2004.06.016"},{"key":"e_1_2_2_34_1","volume-title":"Lizy Kurian John, and Tony Nowatzki","author":"Wang Zhengrong","year":"2023","unstructured":"Zhengrong Wang, Christopher Liu, Aman Arora, Lizy Kurian John, and Tony Nowatzki. 2023. Infinity Stream: Portable and Programmer-Friendly In-\/Near-Memory Fusion. In ASPLOS (3). ACM, 359\u2013375."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T06:06:42Z","timestamp":1752646002000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":35,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729326"],"URL":"https:\/\/doi.org\/10.1145\/3729326","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}