{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T17:24:19Z","timestamp":1778520259377,"version":"3.51.4"},"reference-count":62,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1749570"],"award-info":[{"award-number":["1749570"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC0022081"],"award-info":[{"award-number":["DE-SC0022081"]}],"id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8650-20-2-7008"],"award-info":[{"award-number":["FA8650-20-2-7008"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>We present egglog, a fixpoint reasoning system that unifies Datalog and equality saturation (EqSat). Like Datalog, egglog supports efficient incremental execution, cooperating analyses, and lattice-based reasoning. Like EqSat, egglog supports term rewriting, efficient congruence closure, and extraction of optimized terms.<\/jats:p>\n          <jats:p>We identify two recent applications -- a unification-based pointer analysis in Datalog and an EqSat-based floating-point term rewriter -- that have been hampered by features missing from Datalog but found in EqSat or vice-versa. We evaluate our system by reimplementing those projects in egglog. The resulting systems in egglog are faster, simpler, and fix bugs found in the original systems.<\/jats:p>","DOI":"10.1145\/3591239","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"468-492","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Better Together: Unifying Datalog and Equality Saturation"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-5928-4396","authenticated-orcid":false,"given":"Yihong","family":"Zhang","sequence":"first","affiliation":[{"name":"University of Washington, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6887-9395","authenticated-orcid":false,"given":"Yisu Remy","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0656-235X","authenticated-orcid":false,"given":"Oliver","family":"Flatt","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6163-1821","authenticated-orcid":false,"given":"David","family":"Cao","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0244-5962","authenticated-orcid":false,"given":"Philip","family":"Zucker","sequence":"additional","affiliation":[{"name":"Draper Laboratory, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9386-1614","authenticated-orcid":false,"given":"Eli","family":"Rosenthal","sequence":"additional","affiliation":[{"name":"Google, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4731-0124","authenticated-orcid":false,"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8066-4218","authenticated-orcid":false,"given":"Max","family":"Willsey","sequence":"additional","affiliation":[{"name":"University of Washington, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Foundations of Databases","author":"Abiteboul Serge","unstructured":"Serge Abiteboul , Richard Hull , and Victor Vianu . 1995. Foundations of Databases . Addison-Wesley . isbn:0-201-53771-0 http:\/\/webdam.inria.fr\/Alice\/ Serge Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of Databases. Addison-Wesley. isbn:0-201-53771-0 http:\/\/webdam.inria.fr\/Alice\/"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3517804.3524140"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2723372.2742796"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_5"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(87)90004-5"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_2_1_7_1","unstructured":"Langston Barrett and Scott Moore. 2022. cclyzer++: Scalable and Precise Pointer Analysis for LLVM. https:\/\/galois.com\/blog\/2022\/08\/cclyzer-scalable-and-precise-pointer-analysis-for-llvm\/ \t\t\t\t  Langston Barrett and Scott Moore. 2022. cclyzer++: Scalable and Precise Pointer Analysis for LLVM. https:\/\/galois.com\/blog\/2022\/08\/cclyzer-scalable-and-precise-pointer-analysis-for-llvm\/"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.14778\/3213880.3213888"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428209"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3034786.3034796"},{"key":"e_1_2_1_11_1","unstructured":"Martin E. Bidlingmaier. 2023. Algebraic Semantics of Datalog with Equality. arxiv:2302.03167. \t\t\t\t  Martin E. Bidlingmaier. 2023. Algebraic Semantics of Datalog with Equality. arxiv:2302.03167."},{"key":"e_1_2_1_12_1","unstructured":"Martin E. Bidlingmaier. 2023. An Evaluation Algorithm for Datalog with Equality. arxiv:2302.05792. \t\t\t\t  Martin E. Bidlingmaier. 2023. An Evaluation Algorithm for Datalog with Equality. arxiv:2302.05792."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640108"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1559795.1559809"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.21105\/joss.03078"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2391229.2391230"},{"key":"e_1_2_1_17_1","volume-title":"Automated Deduction \u2013 CADE-21","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2007. Efficient E-Matching for SMT Solvers . In Automated Deduction \u2013 CADE-21 , Frank Pfenning (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 183\u2013198. isbn:978-3-540-73595-3 Leonardo de Moura and Nikolaj Bj\u00f8rner. 2007. Efficient E-Matching for SMT Solvers. In Automated Deduction \u2013 CADE-21, Frank Pfenning (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 183\u2013198. isbn:978-3-540-73595-3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1376916.1376938"},{"key":"e_1_2_1_21_1","unstructured":"Rel developers. [n.d.]. Rel reference. https:\/\/docs.relational.ai\/rel\/ref\/overview \t\t\t\t  Rel developers. [n.d.]. Rel reference. https:\/\/docs.relational.ai\/rel\/ref\/overview"},{"key":"e_1_2_1_22_1","unstructured":"Souffl\u00e9 Developers. [n.d.]. Souffl\u00e9 Algebraic Data Types. https:\/\/souffle-lang.github.io\/types#algebraic-data-types-adt Accessed: 2022-11-01. \t\t\t\t  Souffl\u00e9 Developers. [n.d.]. Souffl\u00e9 Algebraic Data Types. https:\/\/souffle-lang.github.io\/types#algebraic-data-types-adt Accessed: 2022-11-01."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322228"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/773153.773163"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of The 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD \u201922)","author":"Flatt Oliver","year":"2022","unstructured":"Oliver Flatt , Samuel Coward , Max Willsey , Zachary Tatlock , and Pavel Panchekha . 2022 . Small Proofs from Congruence Closure . In Proceedings of The 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD \u201922) . 3, 75. https:\/\/doi.org\/20.500.12708\/81325 Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock, and Pavel Panchekha. 2022. Small Proofs from Congruence Closure. In Proceedings of The 22nd Conference on Formal Methods in Computer-Aided Design (FMCAD \u201922). 3, 75. https:\/\/doi.org\/20.500.12708\/81325"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(98)10005-5"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89051-3_10"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_23"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512566"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80018-5"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/308386.308446"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00961871"},{"key":"e_1_2_1_33_1","volume-title":"Naqvi","author":"Krishnamurthy Ravi","year":"1988","unstructured":"Ravi Krishnamurthy and Shamim A . Naqvi . 1988 . Non-Deterministic Choice in Datalog. In JCDKB. Ravi Krishnamurthy and Shamim A. Naqvi. 1988. Non-Deterministic Choice in Datalog. In JCDKB."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908096"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386012"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485496"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2019.00015"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180143"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737959"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2858965.2814310"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/137097.137852"},{"key":"e_1_2_1_45_1","unstructured":"Rust. [n.d.]. Rust programming language. https:\/\/www.rust-lang.org\/ \t\t\t\t  Rust. [n.d.]. Rust programming language. https:\/\/www.rust-lang.org\/"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497776.3517779"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24206-9_14"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276509"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/137097.137854"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3445814.3446707"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158151"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133886"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.14778\/3407790.3407799"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_8"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1025671410623"},{"key":"e_1_2_1_60_1","volume-title":"Proceedings of Machine Learning and Systems. arxiv:2101","author":"Yang Yichen","year":"2021","unstructured":"Yichen Yang , Phitchaya Mangpo Phothilimtha , Yisu Remy Wang , Max Willsey , Sudip Roy , and Jacques Pienaar . 2021 . Equality Saturation for Tensor Graph Superoptimization . In Proceedings of Machine Learning and Systems. arxiv:2101 .01332. Yichen Yang, Phitchaya Mangpo Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy, and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. In Proceedings of Machine Learning and Systems. arxiv:2101.01332."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7709794"},{"key":"e_1_2_1_62_1","volume-title":"Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey.","author":"Zhang Yihong","year":"2023","unstructured":"Yihong Zhang , Yisu Remy Wang , Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023 . Better Together : Unifying Datalog and Equality Saturation . arxiv:2304.04332. Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023. Better Together: Unifying Datalog and Equality Saturation. arxiv:2304.04332."},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498696"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591239","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591239","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:47Z","timestamp":1750178867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591239"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":62,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591239"],"URL":"https:\/\/doi.org\/10.1145\/3591239","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}