Document Open Access Logo

Semantic Foundations of Equality Saturation

Authors Dan Suciu , Yisu Remy Wang , Yihong Zhang

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICDT.2025.11.pdf
  • Filesize: 1.02 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Rewrite systems
Keywords
  • the chase
  • equality saturation
  • term rewriting
  • tree automata
  • query optimization

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Equality saturation is an emerging technique for program and query optimization developed in the programming language community. It performs term rewriting over an E-graph, a data structure that compactly represents a program space. Despite its popularity, the theory of equality saturation lags behind the practice. In this paper, we define a fixpoint semantics of equality saturation based on tree automata and uncover deep connections between equality saturation and the chase. We characterize the class of chase sequences that correspond to equality saturation. We study the complexities of terminations of equality saturation in three cases: single-instance, all-term-instance, and all-E-graph-instance. Finally, we define a syntactic criterion based on acyclicity that implies equality saturation termination.

Cite As Get BibTex

Dan Suciu, Yisu Remy Wang, and Yihong Zhang. Semantic Foundations of Equality Saturation. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ICDT.2025.11

Author Details

Dan Suciu
  • University of Washington, Seattle, WA, USA
Yisu Remy Wang
  • University of California Los Angeles, CA, USA
Yihong Zhang
  • University of Washington, Seattle, WA, USA

Funding

This work is supported by NSF IIS 2314527 and NSF SHF 2312195, and is conducted while some of the authors participated in the Simons Program on Logic and Algorithms in Databases and AI.

References

  1. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, USA, 1999. Google Scholar
  2. Leo Bachmair, Ashish Tiwari, and Laurent Vigneron. Abstract congruence closure. J. Autom. Reason., 31(2):129-168, 2003. URL: https://doi.org/10.1023/B:JARS.0000009518.26415.49.
  3. Michael Benedikt, George Konstantinidis, Giansalvatore Mecca, Boris Motik, Paolo Papotti, Donatello Santoro, and Efthymia Tsamoura. Benchmarking the chase. In Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS '17, pages 37-52, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3034786.3034796.
  4. Samuel Coward, George A. Constantinides, and Theo Drane. Automating constraint-aware datapath optimization using e-graphs. 2023 60th ACM/IEEE Design Automation Conference (DAC), pages 1-6, 2023. URL: https://api.semanticscholar.org/CorpusID:257353847.
  5. Alin Deutsch, Alan Nash, and Jeff Remmel. The chase revisited. In Proceedings of the Twenty-Seventh ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS '08, pages 149-158, New York, NY, USA, 2008. Association for Computing Machinery. URL: https://doi.org/10.1145/1376916.1376938.
  6. RisingLight developers. RisingLight: An Educational OLAP Database System, December 2022. URL: https://github.com/risinglightdb/risinglight.
  7. Peter J. Downey, Ravi Sethi, and Robert Endre Tarjan. Variations on the common subexpression problem. Journal of the ACM, 27(4):758-771, October 1980. URL: https://doi.org/10.1145/322217.322228.
  8. Ronald Fagin, Phokion G. Kolaitis, Renée J. Miller, and Lucian Popa. Data exchange: semantics and query answering. Theoretical Computer Science, 336(1):89-124, 2005. Database Theory. URL: https://doi.org/10.1016/j.tcs.2004.10.033.
  9. Thomas Genet. Termination criteria for tree automata completion. Journal of Logical and Algebraic Methods in Programming, 85(1, Part 1):3-33, 2016. Rewriting Logic and its Applications. URL: https://doi.org/10.1016/j.jlamp.2015.05.003.
  10. Tomasz Gogacz and Jerzy Marcinkowski. All-instances termination of chase is undecidable. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming, pages 293-304, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-43951-7_25.
  11. Gösta Grahne and Adrian Onet. Anatomy of the chase. Fundam. Informaticae, 157(3):221-270, 2018. URL: https://doi.org/10.3233/FI-2018-1627.
  12. Sumit Gulwani, Ashish Tiwari, and George C. Necula. Join algorithms for the theory of uninterpreted functions. In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, pages 311-323, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  13. Pavol Hell and Jaroslav Nesetril. Images of rigid digraphs. Eur. J. Comb., 12(1):33-42, 1991. URL: https://doi.org/10.1016/S0195-6698(13)80005-4.
  14. Rajeev Joshi, Greg Nelson, and Keith Randall. Denali: A goal-directed superoptimizer. SIGPLAN Not., 37(5):304-314, May 2002. URL: https://doi.org/10.1145/543552.512566.
  15. Donald E. Knuth. A generalization of dijkstra’s algorithm. Inf. Process. Lett., 6(1):1-5, 1977. URL: https://doi.org/10.1016/0020-0190(77)90002-3.
  16. Dexter Kozen. On the myhill-nerode theorem for trees. Bulletin of the EATCS, 47:170-173, 1992. Google Scholar
  17. Dexter Kozen. Partial Automata and Finitely Generated Congruences: An Extension of Nerode’s Theorem, pages 490-511. Birkhäuser Boston, Boston, MA, 1993. URL: https://doi.org/10.1007/978-1-4612-0325-4_16.
  18. Bruno Marnette. Generalized schema-mappings: From termination to tractability. In Proceedings of the Twenty-Eighth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS '09, pages 13-22, New York, NY, USA, 2009. Association for Computing Machinery. URL: https://doi.org/10.1145/1559795.1559799.
  19. Leonardo Moura and Nikolaj Bjørner. Efficient e-matching for smt solvers. In Proceedings of the 21st International Conference on Automated Deduction: Automated Deduction, CADE-21, pages 183-198, Berlin, Heidelberg, 2007. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-73595-3_13.
  20. Chandrakana Nandi, Max Willsey, Adam Anderson, James R. Wilcox, Eva Darulova, Dan Grossman, and Zachary Tatlock. Synthesizing structured CAD models with equality saturation and inverse transformations. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020, pages 31-44, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3385412.3386012.
  21. Paliath Narendran, Colm Ó'Dúnlaing, and Heinrich Rolletschek. Complexity of certain decision problems about congruential languages. Journal of Computer and System Sciences, 30(3):343-358, 1985. URL: https://doi.org/10.1016/0022-0000(85)90051-0.
  22. Charles Gregory Nelson. Techniques for Program Verification. PhD thesis, Stanford University, Stanford, CA, USA, 1980. AAI8011683. Google Scholar
  23. Hung Q. Ngo, Christopher Ré, and Atri Rudra. Skew strikes back: new developments in the theory of join algorithms. SIGMOD Rec., 42(4):5-16, 2013. URL: https://doi.org/10.1145/2590989.2590991.
  24. Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock. Automatically improving accuracy for floating point expressions. SIGPLAN Not., 50(6):1-11, June 2015. URL: https://doi.org/10.1145/2813885.2737959.
  25. Maximilian Schleich, Amir Shaikhha, and Dan Suciu. Optimizing tensor programs on flexible storage, 2022. URL: https://doi.org/10.48550/arXiv.2210.06267.
  26. Wayne Snyder. A fast algorithm for generating reduced ground rewriting systems from a set of ground equations. J. Symb. Comput., 15(4):415-450, April 1993. URL: https://doi.org/10.1006/jsco.1993.1029.
  27. Dan Suciu, Yisu Remy Wang, and Yihong Zhang. Semantic foundations of equality saturation, 2025. URL: https://arxiv.org/abs/2501.02413.
  28. Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. Equality saturation: A new approach to optimization. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '09, pages 264-276, New York, NY, USA, 2009. ACM. URL: https://doi.org/10.1145/1480881.1480915.
  29. Alexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt, and Adrian Sampson. Vectorization for Digital Signal Processors via Equality Saturation, pages 874-886. Association for Computing Machinery, New York, NY, USA, 2021. URL: https://doi.org/10.1145/3445814.3446707.
  30. Yisu Remy Wang, Shana Hutchison, Jonathan Leang, Bill Howe, and Dan Suciu. SPORES: Sum-product optimization via relational equality saturation for large scale linear algebra. Proceedings of the VLDB Endowment, 2020. Google Scholar
  31. Yisu Remy Wang, Mahmoud Abo Khamis, Hung Q Ngo, Reinhard Pichler, and Dan Suciu. Optimizing recursive queries with program synthesis. arXiv preprint arXiv:2202.10390, 2022. URL: https://arxiv.org/abs/2202.10390.
  32. Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. Egg: Fast and extensible equality saturation. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434304.
  33. Yichen Yang, Phitchaya Mangpo Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy, and Jacques Pienaar. Equality saturation for tensor graph superoptimization. In Proceedings of Machine Learning and Systems, 2021. URL: https://arxiv.org/abs/2101.01332.
  34. Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. Better together: Unifying datalog and equality saturation. Proc. ACM Program. Lang., 7(PLDI), June 2023. URL: https://doi.org/10.1145/3591239.
  35. Yihong Zhang, Yisu Remy Wang, Max Willsey, and Zachary Tatlock. Relational e-matching. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498696.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact