{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:13:56Z","timestamp":1781892836369,"version":"3.54.5"},"reference-count":60,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,3,28]],"date-time":"2011-03-28T00:00:00Z","timestamp":1301270400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"National Science Foundation","award":["0644306"],"award-info":[{"award-number":["0644306"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Optimizations in a traditional compiler are applied sequentially, with each\noptimization destructively modifying the program to produce a transformed\nprogram that is then passed to the next optimization. We present a new approach\nfor structuring the optimization phase of a compiler. In our approach,\noptimizations take the form of equality analyses that add equality information\nto a common intermediate representation. The optimizer works by repeatedly\napplying these analyses to infer equivalences between program fragments, thus\nsaturating the intermediate representation with equalities. Once saturated, the\nintermediate representation encodes multiple optimized versions of the input\nprogram. At this point, a profitability heuristic picks the final optimized\nprogram from the various programs represented in the saturated representation.\nOur proposed way of structuring optimizers has a variety of benefits over\nprevious approaches: our approach obviates the need to worry about optimization\nordering, enables the use of a global optimization heuristic that selects among\nfully optimized programs, and can be used to perform translation validation,\neven on compilers other than our own. We present our approach, formalize it,\nand describe our choice of intermediate representation. We also present\nexperimental results showing that our approach is practical in terms of time\nand space overhead, is effective at discovering intricate optimization\nopportunities, and is effective at performing translation validation for a\nrealistic optimizer.<\/jats:p>","DOI":"10.2168\/lmcs-7(1:10)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:18:47Z","timestamp":1316780327000},"source":"Crossref","is-referenced-by-count":21,"title":["Equality Saturation: A New Approach to Optimization"],"prefix":"10.46298","volume":"Volume 7, Issue 1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7608-4605","authenticated-orcid":false,"given":"Ross","family":"Tate","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Stepp","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4731-0124","authenticated-orcid":false,"given":"Zachary","family":"Tatlock","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sorin","family":"Lerner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2011,3,28]]},"reference":[{"key":"10.2168\/LMCS-7(1:10)2011_sat4j","unstructured":"SAT4J. \\texttthttp:\/\/www.sat4j.org\/. C++0x draft standard, 2010. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2010\/n3126.pdf, page 130."},{"key":"10.2168\/LMCS-7(1:10)2011_terminate-blog","unstructured":"Embedded in Academia, 2010. http:\/\/blog.regehr.org\/archives\/140. L. Almagor, K. D. Cooper, A. Grosul, T. J. Harvey, S. W. Reeves, D. Subramanian, L. Torczon, and T. Waterman. Finding effective compilation sequences. InLCTES, 2004."},{"key":"10.2168\/LMCS-7(1:10)2011_ZadeckVariableEquality","doi-asserted-by":"crossref","unstructured":"B. Alpern, M. Wegman, and F. Zadeck. Detecting equality of variables in programs. InPOPL, January 1988.","DOI":"10.1145\/73560.73561"},{"key":"10.2168\/LMCS-7(1:10)2011_AppelBookContinuations1991","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609619"},{"key":"10.2168\/LMCS-7(1:10)2011_AppelBook","doi-asserted-by":"crossref","unstructured":"A. Appel and J. Palsberg.Modern Compiler Implementation in Java. Cambridge University Press, 2002.","DOI":"10.1017\/CBO9780511811432"},{"issue":"5","key":"10.2168\/LMCS-7(1:10)2011_AppelShrinkingLambda1997","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1017\/S0956796897002839","volume":"7","author":"Andrew W. Appel and Trevor Jim","year":"1997","journal-title":"Journal of Functional Programming"},{"issue":"7","key":"10.2168\/LMCS-7(1:10)2011_lucid","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1145\/359636.359715","volume":"20","author":"E. A. Ashcroft and W. W. Wadge","year":"1977","journal-title":"Communications of the ACM"},{"key":"10.2168\/LMCS-7(1:10)2011_citeulike:4121553","unstructured":"John C. Baez and Mike Stay. Physics, topology, logic and computation: A rosetta stone. http:\/\/arxiv.org\/abs\/0903.0340. Mar 2009."},{"key":"10.2168\/LMCS-7(1:10)2011_AikenSuperOpt","doi-asserted-by":"crossref","unstructured":"S. Bansal and A. Aiken. Automatic generation of peephole superoptimizers. InASPLOS, 2006.","DOI":"10.1145\/1168857.1168906"},{"key":"10.2168\/LMCS-7(1:10)2011_CoqArt","doi-asserted-by":"crossref","unstructured":"Yves Bertot and Pierre Cast\u00e9ran.Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer Verlag, 2004.","DOI":"10.1007\/978-3-662-07964-5"},{"key":"10.2168\/LMCS-7(1:10)2011_tampr","doi-asserted-by":"crossref","unstructured":"James M. Boyle, Terence J. Harmer, and Victor L. Winter. The TAMPR program transformation system: simplifying the development of numerical software.Modern software tools for scientific computing, pages 353-372, 1997.","DOI":"10.1007\/978-1-4612-1986-6_17"},{"issue":"1-2","key":"10.2168\/LMCS-7(1:10)2011_stratego","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1016\/j.scico.2007.11.003","volume":"72","author":"M. Bravenboer, K. T. Kalleberg, R. Verma","year":"2008","journal-title":"Science of Computer Programming"},{"issue":"2","key":"10.2168\/LMCS-7(1:10)2011_click-cooper","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/201059.201061","volume":"17","author":"K. D. Cooper C. Click","year":"1995","journal-title":"Transactions on Programming Languages and Systems 17(2):181-196, 1995"},{"key":"10.2168\/LMCS-7(1:10)2011_GlobalCodeMotionValueNumbering","doi-asserted-by":"crossref","unstructured":"C. Click. Global code motion\/global value numbering. InPLDI, June 1995.","DOI":"10.1145\/207110.207154"},{"key":"10.2168\/LMCS-7(1:10)2011_lctes99","doi-asserted-by":"crossref","unstructured":"K. D. Cooper, P. J. Schielke, and Subramanian D. Optimizing for reduced code space using genetic algorithms. InLCTES, 1999.","DOI":"10.1145\/314403.314414"},{"key":"10.2168\/LMCS-7(1:10)2011_1432053","doi-asserted-by":"crossref","unstructured":"Pierre-Louis Curien. The joy of string diagrams. InCSL '08: Proceedings of the 22nd international workshop on Computer Science Logic, pages 15-22, Berlin, Heidelberg, 2008. Springer-Verlag.","DOI":"10.1007\/978-3-540-87531-4_2"},{"key":"10.2168\/LMCS-7(1:10)2011_ssa","doi-asserted-by":"crossref","unstructured":"R. Cytron, J. Ferrante, B. Rosen, M. Wegman, and K. Zadeck. An efficient method for computing static single assignment form. InPOPL, January 1989.","DOI":"10.1145\/75277.75280"},{"key":"10.2168\/LMCS-7(1:10)2011_inlining-trials","doi-asserted-by":"crossref","unstructured":"Jeffrey Dean and Craig Chambers. Towards better inlining decisions using inlining trials. InConference on LISP and Functional Programming, 1994.","DOI":"10.1145\/182409.182489"},{"issue":"3","key":"10.2168\/LMCS-7(1:10)2011_simplify","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs, G. Nelson, and J. Saxe","year":"2005","journal-title":"Journal of the Association for Computing Machinery 52(3):365-473, May 2005"},{"issue":"3","key":"10.2168\/LMCS-7(1:10)2011_gotoharmful","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1145\/362929.362947","volume":"11","author":"E. Dijkstra","year":"1968","journal-title":"Communications of the ACM"},{"key":"10.2168\/LMCS-7(1:10)2011_minisat","unstructured":"Niklas E\u00e9n and Niklas S\u00f6rensson. MiniSat: A SAT solver with conflict-clause minimization. In8th International Conference on Theory and Application of Satisfiability Testing (SAT), 2005."},{"issue":"3","key":"10.2168\/LMCS-7(1:10)2011_PDG","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1145\/24039.24041","volume":"9","author":"J. Ferrante, K. Ottenstein, and J. Warre","year":"1987","journal-title":"Transactions on Programming Languages and Systems 9(3):319-349, July 1987"},{"key":"10.2168\/LMCS-7(1:10)2011_FlanaganContinuations1993","doi-asserted-by":"crossref","unstructured":"Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of compiling with continuations. InPLDI '93: Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, pages 237-247, New York, NY, USA, 1993. ACM.","DOI":"10.1145\/155090.155113"},{"issue":"4","key":"10.2168\/LMCS-7(1:10)2011_burg","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/131080.131089","volume":"27","author":"Christopher W. Fraser, Robert R. Henry,","year":"1992","journal-title":"SIGPLAN Notices"},{"key":"10.2168\/LMCS-7(1:10)2011_tarjan_union_find","doi-asserted-by":"crossref","unstructured":"Harold N. Gabow and Robert Endre Tarjan. A linear-time algorithm for a special case of disjoint set union. InSTOC '83: Proceedings of the fifteenth annual ACM symposium on Theory of computing, pages 246-251, New York, NY, USA, 1983. ACM.","DOI":"10.1145\/800061.808753"},{"key":"10.2168\/LMCS-7(1:10)2011_ExpertSystemsBook","unstructured":"J. Giarratano and G. Riley.Expert Systems - Principles and Programming. PWS Publishing Company, 1993."},{"key":"10.2168\/LMCS-7(1:10)2011_gcc-super-opt","doi-asserted-by":"crossref","unstructured":"Torbjorn Granlund and Richard Kenner. Eliminating branches using a superoptimizer and the GNU C compiler. InPLDI, 1992.","DOI":"10.1145\/143095.143146"},{"key":"10.2168\/LMCS-7(1:10)2011_HatcliffContinuations1994","doi-asserted-by":"crossref","unstructured":"John Hatcliff and Olivier Danvy. A generic account of continuation-passing styles. InPOPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 458-471, New York, NY, USA, 1994. ACM.","DOI":"10.1145\/174675.178053"},{"key":"10.2168\/LMCS-7(1:10)2011_ThinGSSA","doi-asserted-by":"crossref","unstructured":"P. Havlak. Construction of thinned gated single-assignment form. InWorkshop on Languages and Compilers for Parallel Computing, 1993.","DOI":"10.1007\/3-540-57659-2_28"},{"issue":"1","key":"10.2168\/LMCS-7(1:10)2011_dataflowlangs","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1013208.1013209","volume":"36","author":"W. M. Johnston, J. R. P. Hanna, and R. J","year":"2004","journal-title":"ACM Computing Surveys"},{"key":"10.2168\/LMCS-7(1:10)2011_Denali","doi-asserted-by":"crossref","unstructured":"R. Joshi, G. Nelson, and K. Randall. Denali: a goal-directed superoptimizer. InPLDI, June 2002.","DOI":"10.1145\/512565.512566"},{"key":"10.2168\/LMCS-7(1:10)2011_comp-for-21st-century","unstructured":"L. Torczon K. D. Cooper, D. Subramanian. Adaptive optimizing compilers for the 21st century.The Journal of Supercomputing, pages 7-22, 2002."},{"key":"10.2168\/LMCS-7(1:10)2011_KennedyContinuations2007","doi-asserted-by":"crossref","unstructured":"Andrew Kennedy. Compiling with continuations, continued. InICFP '07: Proceedings of the 12th ACM SIGPLAN international conference on Functional programming, pages 177-190, New York, NY, USA, 2007. ACM.","DOI":"10.1145\/1291151.1291179"},{"issue":"4","key":"10.2168\/LMCS-7(1:10)2011_landin_ref_trans","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"P. J. Landin","year":"1963","journal-title":"Computer Journal"},{"key":"10.2168\/LMCS-7(1:10)2011_Leijen:mlftof","doi-asserted-by":"crossref","unstructured":"Daan Leijen. A type directed translation of MLF to System F. InThe International Conference on Functional Programming (ICFP'07). ACM Press, October 2007.","DOI":"10.1145\/1291151.1291169"},{"key":"10.2168\/LMCS-7(1:10)2011_Lerner-etal-02","doi-asserted-by":"crossref","unstructured":"S. Lerner, D. Grove, and C. Chambers. Composing dataflow analyses and transformations. InPOPL, January 2002.","DOI":"10.1145\/503272.503298"},{"key":"10.2168\/LMCS-7(1:10)2011_massalini","doi-asserted-by":"crossref","unstructured":"Henry Massalin. Superoptimizer: a look at the smallest program. InASPLOS, 1987.","DOI":"10.1145\/36204.36194"},{"key":"10.2168\/LMCS-7(1:10)2011_necula:00:trans-valid","doi-asserted-by":"crossref","unstructured":"G. Necula. Translation validation for an optimizing compiler. InPLDI, June 2000.","DOI":"10.1145\/349299.349314"},{"issue":"2","key":"10.2168\/LMCS-7(1:10)2011_Nelson:1979:SCD","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson and D. Oppen","year":"1979","journal-title":"Transactions on Programming Languages and Systems 1(2):245-257, October 1979"},{"issue":"2","key":"10.2168\/LMCS-7(1:10)2011_NelsonOpenCongruence80","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson and D. Oppen","year":"1980","journal-title":"Journal of the Association for Computing Machinery 27(2):356-364, April 1980"},{"key":"10.2168\/LMCS-7(1:10)2011_PDW","doi-asserted-by":"crossref","unstructured":"K. Ottenstein, R. Ballance, and A. MacCabe. The program dependence web: a representation supporting control-, data-, and demand-driven interpretation of imperative languages. InPLDI, June 1990.","DOI":"10.1145\/93542.93578"},{"key":"10.2168\/LMCS-7(1:10)2011_DFG","doi-asserted-by":"crossref","unstructured":"K. Pengali, M. Beck, and R. Johson. Dependence flow graphs: an algebraic approach to program dependencies. InPOPL, January 1991.","DOI":"10.1145\/99583.99595"},{"key":"10.2168\/LMCS-7(1:10)2011_pnueli98translation","doi-asserted-by":"crossref","unstructured":"A. Pnueli, M. Siegel, and E. Singerman. Translation validation. InTACAS, 1998.","DOI":"10.1007\/BFb0054170"},{"key":"10.2168\/LMCS-7(1:10)2011_quine_ref_trans","unstructured":"W. Quine.Word and Object. Simon and Schuster, New York, 1964."},{"key":"10.2168\/LMCS-7(1:10)2011_pueblo","doi-asserted-by":"crossref","first-page":"61","DOI":"10.3233\/SAT190017","volume":"2","author":"H. Sheini and K. Sakallah","year":"2006","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation 2:61-96, 2006"},{"key":"10.2168\/LMCS-7(1:10)2011_VFG","doi-asserted-by":"crossref","unstructured":"B. Steffen, J. Knoop, and O. Ruthing. The value flow graph: A program representation for optimal program transformations. InEuropean Symposium on Programming, 1990.","DOI":"10.1007\/3-540-52592-0_76"},{"issue":"1-2","key":"10.2168\/LMCS-7(1:10)2011_strachey_ref_trans","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1023\/A:1010000313106","volume":"13","author":"Christopher Strachey","year":"2000","journal-title":"Higher Order Symbol. Comput."},{"key":"10.2168\/LMCS-7(1:10)2011_peg2cfg","unstructured":"Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. Translating between PEGs and CFGs. Technical report, University of California, San Diego, October 2010."},{"key":"10.2168\/LMCS-7(1:10)2011_GSSA","doi-asserted-by":"crossref","unstructured":"P. Tu and D. Padua. Efficient building and placing of gating functions. InPLDI, June 1995.","DOI":"10.1145\/207110.207115"},{"key":"10.2168\/LMCS-7(1:10)2011_vall99soot","unstructured":"R. Vall\u00e9e-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot - a Java optimization framework. InCASCON, 1999."},{"key":"10.2168\/LMCS-7(1:10)2011_ASF-SDF","doi-asserted-by":"crossref","unstructured":"M. G. J. van den Brand, J. Heering, P. Klint, and P. A. Olivier. Compiling language definitions: the ASF+SDF compiler.Transactions on Programming Languages and Systems, 24(4), 2002.","DOI":"10.1145\/567097.567099"},{"key":"10.2168\/LMCS-7(1:10)2011_visseretal98","doi-asserted-by":"crossref","unstructured":"E. Visser, Z. Benaissa, and A Tolmach. Building program optimizers with rewriting strategies. InICFP, 1998.","DOI":"10.1145\/289423.289425"},{"key":"10.2168\/LMCS-7(1:10)2011_WadlerMonads1990","doi-asserted-by":"crossref","unstructured":"Philip Wadler. Comprehending monads. InLFP '90: Proceedings of the 1990 ACM conference on LISP and functional programming, pages 61-78, New York, NY, USA, 1990. ACM.","DOI":"10.1145\/91556.91592"},{"key":"10.2168\/LMCS-7(1:10)2011_WadlerMonads1995","doi-asserted-by":"crossref","unstructured":"Philip Wadler. Monads for functional programming. InAdvanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, pages 24-52, London, UK, 1995. Springer-Verlag.","DOI":"10.1007\/3-540-59451-5_2"},{"key":"10.2168\/LMCS-7(1:10)2011_WadlerMonads1998","doi-asserted-by":"crossref","unstructured":"Philip Wadler. The marriage of effects and monads. InICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming, pages 63-74, New York, NY, USA, 1998. ACM.","DOI":"10.1145\/289423.289429"},{"key":"10.2168\/LMCS-7(1:10)2011_VDG","doi-asserted-by":"crossref","unstructured":"D. Weise, R. Crew, M. Ernst, and B. Steensgaard. Value dependence graphs: Representation without taxation. InPOPL, 1994.","DOI":"10.1145\/174675.177907"},{"key":"10.2168\/LMCS-7(1:10)2011_Whitfield90","doi-asserted-by":"crossref","unstructured":"Debbie Whitfield and Mary Lou Soffa. An approach to ordering optimizing transformations. InPPOPP, 1990.","DOI":"10.1145\/99163.99179"},{"issue":"6","key":"10.2168\/LMCS-7(1:10)2011_WhitfieldSoffa97","doi-asserted-by":"crossref","first-page":"1053","DOI":"10.1145\/267959.267960","volume":"19","author":"Deborah L. Whitfield and Mary Lou Soffa","year":"1997","journal-title":"Transactions on Programming Languages and Systems 19(6):1053-1084, November 1997"},{"key":"10.2168\/LMCS-7(1:10)2011_execindex","doi-asserted-by":"crossref","unstructured":"B. Xin, W. N. Sumner, and X. Zhang. Efficient program execution indexing. InPLDI, June 2008.","DOI":"10.1145\/1375581.1375611"},{"issue":"3","key":"10.2168\/LMCS-7(1:10)2011_voc:jucs","first-page":"223","volume":"9","author":"Lenore Zuck, Amir Pnueli, Yi Fang, and B","year":"2003","journal-title":"Journal of Universal Computer Science 2003"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1016\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1016\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:01:19Z","timestamp":1681243279000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1016"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3,28]]},"references-count":60,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(1:10)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1012.1802","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1012.1802","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,3,28]]},"article-number":"1016"}}