{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:21Z","timestamp":1751662881349,"version":"3.41.0"},"reference-count":56,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Key Research and Development Program of China","award":["Grant No. 2022YFB450190"],"award-info":[{"award-number":["Grant No. 2022YFB450190"]}]},{"name":"National Natural Science Foundation of China","award":["Grant No. 62161146003"],"award-info":[{"award-number":["Grant No. 62161146003"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,10,16]]},"abstract":"<jats:p>In this paper, we propose an automated approach to finding correct and efficient memoization algorithms from a given declarative specification. This problem has two major challenges: (i) a memoization algorithm is too large to be handled by conventional program synthesizers; (ii) we need to guarantee the efficiency of the memoization algorithm. To address this challenge, we structure the synthesis of memoization algorithms by introducing the local objective function and the memoization partition function and reduce the synthesis task to two smaller independent program synthesis tasks. Moreover, the number of distinct outputs of the function synthesized in the second synthesis task also decides the efficiency of the synthesized memoization algorithm, and we only need to minimize the number of different output values of the synthesized function. However, the generated synthesis task is still too complex for existing synthesizers. Thus, we propose a novel synthesis algorithm that combines the deductive and inductive methods to solve these tasks. To evaluate our algorithm, we collect 42 real-world benchmarks from Leetcode, the National Olympiad in Informatics in Provinces-Junior (a national-wide algorithmic programming contest in China), and previous approaches. Our approach successfully synhesizes 39\/42 problems in a reasonable time, outperforming the baselines.<\/jats:p>","DOI":"10.1145\/3622800","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"89-115","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Synthesizing Efficient Memoization Algorithms"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0370-1676","authenticated-orcid":false,"given":"Yican","family":"Sun","sequence":"first","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8613-3506","authenticated-orcid":false,"given":"Xuanyu","family":"Peng","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8991-747X","authenticated-orcid":false,"given":"Yingfei","family":"Xiong","sequence":"additional","affiliation":[{"name":"Peking University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"[n. d.]. Full version of this paper. https:\/\/boyvolcano.github.io\/publication\/oopsla-23\/oopsla23.pdf \t\t\t\t  [n. d.]. Full version of this paper. https:\/\/boyvolcano.github.io\/publication\/oopsla-23\/oopsla23.pdf"},{"key":"e_1_2_1_2_1","unstructured":"[n. d.]. National Olympiad in Informatics in Provinces-Junior. https:\/\/noi.ccf.org.cn\/zxzy\/lnzl\/index.shtml \t\t\t\t  [n. d.]. National Olympiad in Informatics in Provinces-Junior. https:\/\/noi.ccf.org.cn\/zxzy\/lnzl\/index.shtml"},{"key":"e_1_2_1_3_1","unstructured":"[n. d.]. The world\u2019s leading online programming learning platform. https:\/\/leetcode.com\/ \t\t\t\t  [n. d.]. The world\u2019s leading online programming learning platform. https:\/\/leetcode.com\/"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604133"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/B0-12-227410-5\/00853-X"},{"key":"e_1_2_1_6_1","volume-title":"Hopcroft","author":"Aho Alfred V.","year":"1974","unstructured":"Alfred V. Aho and John E . Hopcroft . 1974 . The Design and Analysis of Computer Algorithms (1st ed.). Addison-Wesley Longman Publishing Co. , Inc., USA. isbn:0201000296 Alfred V. Aho and John E. Hopcroft. 1974. The Design and Analysis of Computer Algorithms (1st ed.). Addison-Wesley Longman Publishing Co., Inc., USA. isbn:0201000296"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208071"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3409757"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of WDS99 (invited lecture), 01","author":"Bart\u00e1k Roman","year":"1999","unstructured":"Roman Bart\u00e1k . 1999 . Constraint programming: In pursuit of the holy grail . Proceedings of WDS99 (invited lecture), 01 . Roman Bart\u00e1k. 1999. Constraint programming: In pursuit of the holy grail. Proceedings of WDS99 (invited lecture), 01."},{"volume-title":"Algebra of Programming","author":"Bird Richard","key":"e_1_2_1_10_1","unstructured":"Richard Bird and Oege de Moor . 1997. Algebra of Programming . Prentice-Hall, Inc. , USA. isbn:013507245X Richard Bird and Oege de Moor. 1997. Algebra of Programming. Prentice-Hall, Inc., USA. isbn:013507245X"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108869041"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611977042.17"},{"key":"e_1_2_1_13_1","volume-title":"Sipma","author":"Bradley Aaron R.","year":"2006","unstructured":"Aaron R. Bradley , Zohar Manna , and Henny B . Sipma . 2006 . What\u2019s Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation, E. Allen Emerson and Kedar S. Namjoshi (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 427\u2013442. isbn:978-3-540-31622-0 Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What\u2019s Decidable About Arrays? In Verification, Model Checking, and Abstract Interpretation, E. Allen Emerson and Kedar S. Namjoshi (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 427\u2013442. isbn:978-3-540-31622-0"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9237-y"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314596"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2166.2167"},{"key":"e_1_2_1_17_1","volume-title":"Introduction to Algorithms","author":"Cormen Thomas H.","year":"2033","unstructured":"Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest , and Clifford Stein . 2009. Introduction to Algorithms , Third Edition (3 rd ed.). The MIT Press . isbn:026 2033 844 Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to Algorithms, Third Edition (3rd ed.). The MIT Press. isbn:0262033844","edition":"3"},{"volume-title":"Programming Languages: Implementations, Logics and Programs, Manuel Hermenegildo and S","author":"de Moor Oege","key":"e_1_2_1_18_1","unstructured":"Oege de Moor . 1995. A generic program for sequential decision processes . In Programming Languages: Implementations, Logics and Programs, Manuel Hermenegildo and S . Doaitse Swierstra (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 1\u201323. isbn:978-3-540-45048-1 Oege de Moor. 1995. A generic program for sequential decision processes. In Programming Languages: Implementations, Logics and Programs, Manuel Hermenegildo and S. Doaitse Swierstra (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1\u201323. isbn:978-3-540-45048-1"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523726"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062355"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454089"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2003.12.005"},{"key":"e_1_2_1_24_1","volume-title":"Nicholson","author":"He Meng","year":"2011","unstructured":"Meng He , J. Ian Munro , and Patrick K . Nicholson . 2011 . Dynamic Range Selection in Linear Space. In Algorithms and Computation, Takao Asano, Shin-ichi Nakano, Yoshio Okamoto, and Osamu Watanabe (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg. 160\u2013169. isbn:978-3-642-25591-5 Meng He, J. Ian Munro, and Patrick K. Nicholson. 2011. Dynamic Range Selection in Linear Space. In Algorithms and Computation, Takao Asano, Shin-ichi Nakano, Yoshio Okamoto, and Osamu Watanabe (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 160\u2013169. isbn:978-3-642-25591-5"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_37"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485544"},{"volume-title":"Knapsack problems","author":"Kellerer Hans","key":"e_1_2_1_28_1","unstructured":"Hans Kellerer , Ulrich Pferschy , and David Pisinger . 2004. Knapsack problems .. Springer . isbn:978-3-540-40286-2 Hans Kellerer, Ulrich Pferschy, and David Pisinger. 2004. Knapsack problems.. Springer. isbn:978-3-540-40286-2"},{"key":"e_1_2_1_29_1","volume-title":"Inductive Synthesis of Functional Programs: An Explanation Based Generalization Approach. J. Mach. Learn. Res., 7","author":"Kitzelmann Emanuel","year":"2006","unstructured":"Emanuel Kitzelmann and Ute Schmid . 2006. Inductive Synthesis of Functional Programs: An Explanation Based Generalization Approach. J. Mach. Learn. Res., 7 ( 2006 ), dec, 429\u2013454. issn:1532-4435 Emanuel Kitzelmann and Ute Schmid. 2006. Inductive Synthesis of Functional Programs: An Explanation Based Generalization Approach. J. Mach. Learn. Res., 7 (2006), dec, 429\u2013454. issn:1532-4435"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314602"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571263"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468566"},{"key":"e_1_2_1_34_1","volume-title":"Stoller","author":"Liu Yanhong A.","year":"1999","unstructured":"Yanhong A. Liu and Scott D . Stoller . 1999 . Dynamic Programming via Static Incrementalization. In Programming Languages and Systems, S. Doaitse Swierstra (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg. 288\u2013305. isbn:978-3-540-49099-9 Yanhong A. Liu and Scott D. Stoller. 1999. Dynamic Programming via Static Incrementalization. In Programming Languages and Systems, S. Doaitse Swierstra (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 288\u2013305. isbn:978-3-540-49099-9"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408991"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/322063.322075"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0011"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/647197.720999"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498682"},{"volume-title":"Dynamic Programming via Thinning and Incrementalization","author":"Morihata Akimasa","key":"e_1_2_1_40_1","unstructured":"Akimasa Morihata , Masato Koishi , and Atsushi Ohori . 2014. Dynamic Programming via Thinning and Incrementalization . In Functional and Logic Programming, Michael Codish and Eijiro Sumii (Eds.). Springer International Publishing , Cham . 186\u2013202. isbn:978-3-319-07151-0 Akimasa Morihata, Masato Koishi, and Atsushi Ohori. 2014. Dynamic Programming via Thinning and Incrementalization. In Functional and Logic Programming, Michael Codish and Eijiro Sumii (Eds.). Springer International Publishing, Cham. 186\u2013202. isbn:978-3-319-07151-0"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273442.1250752"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328408.1328414"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/1771668.1771709"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234529"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_2_1_46_1","unstructured":"M. Presburger. 1931. \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchem die Addition als einzige Operation hervortritt. https:\/\/books.google.com.sg\/books?id=7agKHQAACAAJ \t\t\t\t  M. Presburger. 1931. \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchem die Addition als einzige Operation hervortritt. https:\/\/books.google.com.sg\/books?id=7agKHQAACAAJ"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076021.2048076"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2003476.2003484"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.4153\/CJM-1961-015-3"},{"key":"e_1_2_1_50_1","volume-title":"Combinatorial Optimization: Polyhedra and Efficiency. B.","author":"Schrijver Alexander","year":"2003","unstructured":"Alexander Schrijver . 2003 . Combinatorial Optimization: Polyhedra and Efficiency. B. Alexander Schrijver. 2003. Combinatorial Optimization: Polyhedra and Efficiency. B."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/322123.322137"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908102"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168919.1168907"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8325410"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276525"},{"key":"e_1_2_1_56_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\/10.1145\/3622800","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622800","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622800"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":56,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622800"],"URL":"https:\/\/doi.org\/10.1145\/3622800","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}