Recursive Program Synthesis using Paramorphisms
Authors: 
Qiantan Hong, 
Alex AikenAuthors Info & Claims
Article No.: 151, Pages 102 - 125
Abstract
We show that synthesizing recursive functional programs using a class of primitive recursive combinators is both simpler and solves more benchmarks from the literature than previously proposed approaches. Our method synthesizes paramorphisms, a class of programs that includes the most common recursive programming patterns on algebraic data types. The crux of our approach is to split the synthesis problem into two parts: a multi-hole template that fixes the recursive structure, and a search for non-recursive program fragments to fill the template holes.
References
[1]
Alexandros Agapitos and Simon M Lucas. 2006. Learning recursive functions with object oriented genetic programming. In European Conference on Genetic Programming. Springer, 166-177.
[2]
Alexandros Agapitos, Michael O'Neill, Ahmed Kattan, and Simon M Lucas. 2017. Recursion in tree-based genetic programming. Genetic programming and evolvable machines 18, 2 ( 2017 ), 149-183.
[3]
Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive program synthesis. In International conference on computer aided verification. Springer, 934-950.
[4]
Brad Alexander and Brad Zacher. 2014. Boosting search for recursive functions using partial call-trees. In International Conference on Parallel Problem Solving from Nature. Springer, 384-393.
[5]
Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo MK Martin, Mukund Raghothaman, Sanjit A Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. 2013. Syntax-guided synthesis. IEEE.
[6]
Sorav Bansal and Alex Aiken. 2006. Automatic generation of peephole superoptimizers. In Proceedings of the Conference on Architectural Support for Programming Languages and Operating Systems. 394-403.
[7]
Franck Binard and Amy Felty. 2008. Genetic programming with polymorphic types and higher-order functions. In Proceedings of the 10th annual conference on Genetic and evolutionary computation. 1187-1194.
[8]
Taylor L Booth and Richard A Thompson. 1973. Applying probability measures to abstract languages. IEEE transactions on Computers 100, 5 ( 1973 ), 442-450.
[9]
James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. 2016. Optimizing synthesis with metasketches. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 775-788.
[10]
Sarah E Chasins, Maria Mueller, and Rastislav Bodik. 2018. Rousillon: Scraping distributed hierarchical web data. In Proceedings of the 31st Annual ACM Symposium on User Interface Software and Technology. 963-975.
[11]
Shingo Eguchi, Naoki Kobayashi, and Takeshi Tsukada. 2018. Automated synthesis of functional programs with auxiliary functions. In Asian Symposium on Programming Languages and Systems. Springer, 223-241.
[12]
Yu Feng, Ruben Martins, Osbert Bastani, and Isil Dillig. 2018. Program synthesis using conflict-driven learning. ACM SIGPLAN Notices 53, 4 ( 2018 ), 420-435.
[13]
Yu Feng, Ruben Martins, Jacob Van Gefen, Isil Dillig, and Swarat Chaudhuri. 2017. Component-based synthesis of table consolidation and transformation tasks from examples. ACM SIGPLAN Notices 52, 6 ( 2017 ), 422-436.
[14]
John K Feser, Swarat Chaudhuri, and Isil Dillig. 2015. Synthesizing data structure transformations from input-output examples. ACM SIGPLAN Notices 50, 6 ( 2015 ), 229-239.
[15]
Jean-Yves Girard. 1971. Une extension de L' interpretation de gödel a L'analyse, et son application a L'elimination des coupures dans L'analyse et la theorie des types. In Studies in Logic and the Foundations of Mathematics. Vol. 63. Elsevier, 63-92.
[16]
Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. Ph. D. Dissertation. Éditeur inconnu.
[17]
Sumit Gulwani. 2011. Automating string processing in spreadsheets using input-output examples. ACM Sigplan Notices 46, 1 ( 2011 ), 317-330.
[18]
W Keith Hastings. 1970. Monte Carlo sampling methods using Markov chains and their applications. ( 1970 ).
[19]
Brian Hempel, Justin Lubin, and Ravi Chugh. 2019. Sketch-n-sketch: Output-directed programming for SVG. In Proceedings of the 32nd Annual ACM Symposium on User Interface Software and Technology. 281-292.
[20]
Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Benjamin S Lerner, and Armando Solar-Lezama. 2017. Synthesis of recursive ADT transformations from reusable templates. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 247-263.
[21]
Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben NS Rowe, and Ilya Sergey. 2021. Cyclic program synthesis. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 944-959.
[22]
Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. 2013. Synthesis modulo recursive functions. In Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications. 407-426.
[23]
Jason R Koenig, Oded Padon, and Alex Aiken. 2021. Adaptive restarts for stochastic synthesis. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 696-709.
[24]
John R Koza. 1994. Genetic programming as a means for programming computers by natural selection. Statistics and computing 4, 2 ( 1994 ), 87-112.
[25]
Woosuk Lee and Hangyeol Cho. 2023. Inductive synthesis of structurally recursive functional programs from non-recursive expressions. Proceedings of the ACM on Programming Languages 7, POPL ( 2023 ), 2048-2078.
[26]
Justin Lubin, Nick Collins, Cyrus Omar, and Ravi Chugh. 2020. Program sketching with live bidirectional evaluation. Proceedings of the ACM on Programming Languages 4, ICFP ( 2020 ), 1-29.
[27]
Simon Marlow et al. 2010. Haskell 2010 language report. Available online http://www. haskell. org/(May 2011 ) ( 2010 ).
[28]
Henry Massalin. 1987. Superoptimizer: A look at the smallest program. ACM SIGARCH Computer Architecture News 15, 5 ( 1987 ), 122-126.
[29]
Lambert Meertens. 1992. Paramorphisms. Formal aspects of computing 4 ( 1992 ), 413-424.
[30]
Erik Meijer, Maarten Fokkinga, and Ross Paterson. 1991. Functional programming with bananas, lenses, envelopes and barbed wire. In Conference on functional programming languages and computer architecture. Springer, 124-144.
[31]
Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. 1997. The definition of standard ML: revised. MIT press.
[32]
Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, and Isil Dillig. 2022. Bottom-up synthesis of recursive functional programs using angelic execution. Proceedings of the ACM on Programming Languages 6, POPL ( 2022 ), 1-29.
[33]
Alberto Moraglio, Fernando EB Otero, Colin G Johnson, Simon Thompson, and Alex A Freitas. 2012. Evolving recursive programs using non-recursive scafolding. In 2012 IEEE Congress on Evolutionary Computation. IEEE, 1-8.
[34]
Masato Nishiguchi and Yoshiji Fujimoto. 1998. Evolution of recursive programs with multi-niche genetic programming (mnGP). In 1998 IEEE International Conference on Evolutionary Computation Proceedings. IEEE World Congress on Computational Intelligence (Cat. No. 98TH8360). IEEE, 247-252.
[35]
Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed program synthesis. ACM SIGPLAN Notices 50, 6 ( 2015 ), 619-630.
[36]
Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. ACM SIGPLAN Notices 51, 6 ( 2016 ), 522-538.
[37]
John C Reynolds. 1974. Towards a theory of type structure. In Programming Symposium. Springer, 408-425.
[38]
Christophe Rhodes. 2008. Sbcl: A sanely-bootstrappable common lisp. In Workshop on Self-sustaining Systems. Springer, 74-86.
[39]
Eric Schkufza, Rahul Sharma, and Alex Aiken. 2013. Stochastic superoptimization. ACM SIGARCH Computer Architecture News 41, 1 ( 2013 ), 305-316.
[40]
Rishabh Singh and Sumit Gulwani. 2016. Transforming spreadsheet data types using examples. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 343-356.
[41]
Armando Solar-Lezama. 2013. Program sketching. International Journal on Software Tools for Technology Transfer 15, 5 ( 2013 ), 475-495.
[42]
Jerry Swan, Krzysztof Krawiec, and Zoltan A Kocsis. 2019. Stochastic synthesis of recursive functions made easy with bananas, lenses, envelopes and barbed wire. Genetic Programming and Evolvable Machines 20, 3 ( 2019 ), 327-350.
[43]
Emina Torlak and Rastislav Bodik. 2013. Growing solver-aided languages with Rosette. In Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software. 135-152.
[44]
Chenglong Wang, Alvin Cheung, and Rastislav Bodik. 2017. Synthesizing highly expressive SQL queries from input-output examples. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 452-466.
[45]
Chenglong Wang, Yu Feng, Rastislav Bodik, Alvin Cheung, and Isil Dillig. 2019. Visualization by example. Proceedings of the ACM on Programming Languages 4, POPL ( 2019 ), 1-28.
[46]
Man Leung Wong and Kwong Sak Leung. 1996. Evolving recursive functions for the even-parity problem using genetic programming. In Advances in genetic programming. MIT press, 221-240.
[47]
Navid Yaghmazadeh, Christian Klinger, Isil Dillig, and Swarat Chaudhuri. 2016. Synthesizing transformations on hierarchically structured data. ACM SIGPLAN Notices 51, 6 ( 2016 ), 508-521.
[48]
Tina Yu. 2001. Hierarchical processing for evolving recursive and modular programs using higher-order functions and lambda abstraction. Genetic Programming and Evolvable Machines 2, 4 ( 2001 ), 345-380.
[49]
Tina Yu and Chris Clack. 1998. Recursion, lambda abstraction and genetic programming. Morgan Kaufman.
[50]
Yongwei Yuan, Arjun Radhakrishna, and Roopsha Samanta. 2023. Trace-Guided Inductive Synthesis of Recursive Functional Programs. Proceedings of the ACM on Programming Languages 7, PLDI ( 2023 ), 860-883.
Index Terms
- Recursive Program Synthesis using Paramorphisms
Recommendations
Stochastic program synthesis via recursion schemes
GECCO '19: Proceedings of the Genetic and Evolutionary Computation Conference CompanionStochastic synthesis of recursive functions has historically proved difficult, not least due to issues of non-termination and the often ad hoc methods for addressing this. We propose a general method of implicit recursion which operates via an ...
Partial bounding for recursive function synthesis
AbstractQuantifier bounding is a standard approach in inductive program synthesis to deal with unbounded domains. In this paper, we propose one such bounding method for the synthesis of recursive functions over recursive input data types. The synthesis ...
Stochastic synthesis of recursive functions made easy with bananas, lenses, envelopes and barbed wire
AbstractStochastic synthesis of recursive functions has historically proved difficult, not least due to issues of non-termination and the often ad hoc methods for addressing this. This article presents a general method of implicit recursion which operates ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 20 June 2024
Published in PACMPL Volume 8, Issue PLDI
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 518Total Downloads
- Downloads (Last 12 months)518
- Downloads (Last 6 weeks)94
Reflects downloads up to 10 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in