research-article

Open access

Trace-Guided Inductive Synthesis of Recursive Functional Programs

Authors:

Arjun Radhakrishna,

Roopsha SamantaAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue PLDI

Article No.: 141, Pages 860 - 883

https://doi.org/10.1145/3591255

Published: 06 June 2023 Publication History

Abstract

We propose a novel trace-guided approach to tackle the challenges of ambiguity and generalization in synthesis of recursive functional programs from input-output examples. Our approach augments the search space of programs with recursion traces consisting of recursive subcalls of the programs. Our method is based on a new version space algebra (VSA) for succinct representation and efficient manipulation of pairs of recursion traces and programs that are consistent with each other. We have implemented this approach in a tool called SyRup and evaluated it on benchmarks from prior work. Our evaluation demonstrates that SyRup not only requires fewer examples to achieve a certain success rate than existing synthesizers, but is also less sensitive to the quality of the examples.

References

[1]

Aws Albarghouthi, Sumit Gulwani, and Zachary Kincaid. 2013. Recursive Program Synthesis. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.) (Lecture Notes in Computer Science). Springer, Berlin, Heidelberg. 934–950. isbn:978-3-642-39799-8 https://doi.org/10.1007/978-3-642-39799-8_67

[2]

Rajeev Alur, Pavol Černý, and Arjun Radhakrishna. 2015. Synthesis Through Unification. In Computer Aided Verification, Daniel Kroening and Corina S. Păsăreanu (Eds.) (Lecture Notes in Computer Science). Springer International Publishing, Cham. 163–179. isbn:978-3-319-21668-3 https://doi.org/10.1007/978-3-319-21668-3_10

[3]

Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. 2017. Scaling Enumerative Program Synthesis via Divide and Conquer. In Tools and Algorithms for the Construction and Analysis of Systems, Axel Legay and Tiziana Margaria (Eds.). 10205, Springer Berlin Heidelberg, Berlin, Heidelberg. 319–336. isbn:978-3-662-54576-8 978-3-662-54577-5 https://doi.org/10.1007/978-3-662-54577-5_18

[4]

Shraddha Barke, Hila Peleg, and Nadia Polikarpova. 2020. Just-in-Time Learning for Bottom-up Enumerative Synthesis. Proceedings of the ACM on Programming Languages, 4, OOPSLA (2020), Nov., 1–29. issn:2475-1421, 2475-1421 https://doi.org/10.1145/3428295

Digital Library

[5]

Daniel W. Barowy, Sumit Gulwani, Ted Hart, and Benjamin Zorn. 2015. FlashRelate: Extracting Relational Data from Semi-Structured Spreadsheets Using Examples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). Association for Computing Machinery, New York, NY, USA. 218–228. isbn:978-1-4503-3468-6 https://doi.org/10.1145/2737924.2737952

Digital Library

[6]

Rastislav Bodik, Satish Chandra, Joel Galenson, Doug Kimelman, Nicholas Tung, Shaon Barman, and Casey Rodarmor. 2010. Programming with Angelic Nondeterminism. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’10). Association for Computing Machinery, New York, NY, USA. 339–352. isbn:978-1-60558-479-9 https://doi.org/10.1145/1706299.1706339

Digital Library

[7]

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 (POPL ’16). Association for Computing Machinery, New York, NY, USA. 775–788. isbn:978-1-4503-3549-2 https://doi.org/10.1145/2837614.2837666

Digital Library

[8]

Ravi Chugh, Brian Hempel, Mitchell Spradlin, and Jacob Albers. 2016. Programmatic and Direct Manipulation, Together at Last. ACM SIGPLAN Notices, 51, 6 (2016), June, 341–354. issn:0362-1340 https://doi.org/10.1145/2980983.2908103

Digital Library

[9]

Thierry Coquand. 1994. Infinite Objects in Type Theory. In Types for Proofs and Programs, Henk Barendregt and Tobias Nipkow (Eds.) (Lecture Notes in Computer Science). Springer, Berlin, Heidelberg. 62–78. isbn:978-3-540-48440-0 https://doi.org/10.1007/3-540-58085-9_72

[10]

Peter J. Downey, Ravi Sethi, and Robert Endre Tarjan. 1980. Variations on the Common Subexpression Problem. J. ACM, 27, 4 (1980), Oct., 758–771. issn:0004-5411, 1557-735X https://doi.org/10.1145/322217.322228

Digital Library

[11]

Kevin Ellis and Sumit Gulwani. 2017. Learning to Learn Programs from Examples: Going Beyond Program Structure. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization, Melbourne, Australia. 1638–1645. isbn:978-0-9992411-0-3 https://doi.org/10.24963/ijcai.2017/227

[12]

Azadeh Farzan, Danya Lette, and Victor Nicolet. 2022. Recursion Synthesis with Unrealizability Witnesses. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022). Association for Computing Machinery, New York, NY, USA. 244–259. isbn:978-1-4503-9265-5 https://doi.org/10.1145/3519939.3523726

Digital Library

[13]

Azadeh Farzan and Victor Nicolet. 2021. Counterexample-Guided Partial Bounding for Recursive Function Synthesis. In Computer Aided Verification, Alexandra Silva and K. Rustan M. Leino (Eds.) (Lecture Notes in Computer Science). Springer International Publishing, Cham. 832–855. isbn:978-3-030-81685-8 https://doi.org/10.1007/978-3-030-81685-8_39

Digital Library

[14]

John K. Feser, Swarat Chaudhuri, and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-Output Examples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). Association for Computing Machinery, New York, NY, USA. 229–239. isbn:978-1-4503-3468-6 https://doi.org/10.1145/2737924.2737977

Digital Library

[15]

Robert W. Floyd. 1967. Nondeterministic Algorithms. J. ACM, 14, 4 (1967), Oct., 636–644. issn:0004-5411 https://doi.org/10.1145/321420.321422

Digital Library

[16]

Sumit Gulwani. 2011. Automating String Processing in Spreadsheets Using Input-Output Examples. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). Association for Computing Machinery, New York, NY, USA. 317–330. isbn:978-1-4503-0490-0 https://doi.org/10.1145/1926385.1926423

Digital Library

[17]

Martin Hofmann. 2010. IGOR2 - an Analytical Inductive Functional Programming System: Tool Demo. In Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM ’10). Association for Computing Machinery, New York, NY, USA. 29–32. isbn:978-1-60558-727-1 https://doi.org/10.1145/1706356.1706364

Digital Library

[18]

Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, and Ilya Sergey. 2021. Cyclic Program Synthesis. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). Association for Computing Machinery, New York, NY, USA. 944–959. isbn:978-1-4503-8391-2 https://doi.org/10.1145/3453483.3454087

Digital Library

[19]

Ruyi Ji, Jingtao Xia, Yingfei Xiong, and Zhenjiang Hu. 2021. Generalizable Synthesis through Unification. Proceedings of the ACM on Programming Languages, 5, OOPSLA (2021), Oct., 1–28. issn:2475-1421 https://doi.org/10.1145/3485544

Digital Library

[20]

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. ACM, Indianapolis Indiana USA. 407–426. isbn:978-1-4503-2374-1 https://doi.org/10.1145/2509136.2509555

Digital Library

[21]

James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, and Nadia Polikarpova. 2022. Searching Entangled Program Spaces. Proceedings of the ACM on Programming Languages, 6, ICFP (2022), Aug., 91:23–91:51. https://doi.org/10.1145/3547622

Digital Library

[22]

Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. 2010. Complete Functional Synthesis. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’10). Association for Computing Machinery, New York, NY, USA. 316–329. isbn:978-1-4503-0019-3 https://doi.org/10.1145/1806596.1806632

Digital Library

[23]

Tessa Lau, Steven A. Wolfman, Pedro Domingos, and Daniel S. Weld. 2003. Programming by Demonstration Using Version Space Algebra. Machine Learning, 53, 1 (2003), Oct., 111–156. issn:1573-0565 https://doi.org/10.1023/A:1025671410623

Digital Library

[24]

Vu Le and Sumit Gulwani. 2014. FlashExtract: A Framework for Data Extraction by Examples. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’14). Association for Computing Machinery, New York, NY, USA. 542–553. isbn:978-1-4503-2784-8 https://doi.org/10.1145/2594291.2594333

Digital Library

[25]

Woosuk Lee. 2021. Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis. Proceedings of the ACM on Programming Languages, 5, POPL (2021), Jan., 1–28. issn:2475-1421 https://doi.org/10.1145/3434335

Digital Library

[26]

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), Jan., 70:2048–70:2078. https://doi.org/10.1145/3571263

Digital Library

[27]

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), Aug., 109:1–109:29. https://doi.org/10.1145/3408991

Digital Library

[28]

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), Jan., 21:1–21:29. https://doi.org/10.1145/3498682

Digital Library

[29]

Tom M. Mitchell. 1982. Generalization as Search. Artificial Intelligence, 18, 2 (1982), March, 203–226. issn:0004-3702 https://doi.org/10.1016/0004-3702(82)90040-6

[30]

Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer. 2019. Live Functional Programming with Typed Holes. Proceedings of the ACM on Programming Languages, 3, POPL (2019), Jan., 1–32. issn:2475-1421, 2475-1421 https://doi.org/10.1145/3290327

Digital Library

[31]

Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-Example-Directed Program Synthesis. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). Association for Computing Machinery, New York, NY, USA. 619–630. isbn:978-1-4503-3468-6 https://doi.org/10.1145/2737924.2738007

Digital Library

[32]

Saswat Padhi, Todd Millstein, Aditya Nori, and Rahul Sharma. 2019. Overfitting in Synthesis: Theory and Practice. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.) (Lecture Notes in Computer Science). Springer International Publishing, Cham. 315–334. isbn:978-3-030-25540-4 https://doi.org/10.1007/978-3-030-25540-4_17

[33]

Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). Association for Computing Machinery, New York, NY, USA. 522–538. isbn:978-1-4503-4261-2 https://doi.org/10.1145/2908080.2908093

Digital Library

[34]

Oleksandr Polozov and Sumit Gulwani. 2015. FlashMeta: A Framework for Inductive Program Synthesis. In Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications. ACM, Pittsburgh PA USA. 107–126. isbn:978-1-4503-3689-5 https://doi.org/10.1145/2814270.2814310

Digital Library

[35]

Reudismam Rolim, Gustavo Soares, Loris D’Antoni, Oleksandr Polozov, Sumit Gulwani, Rohit Gheyi, Ryo Suzuki, and Björn Hartmann. 2017. Learning Syntactic Program Transformations from Examples. In 2017 IEEE/ACM 39th International Conference on Software Engineering (ICSE). 404–415. issn:1558-1225 https://doi.org/10.1109/ICSE.2017.44

Digital Library

[36]

Kensen Shi, Jacob Steinhardt, and Percy Liang. 2019. FrAngel: Component-Based Synthesis with Control Structures. Proceedings of the ACM on Programming Languages, 3, POPL (2019), Jan., 1–29. issn:2475-1421 https://doi.org/10.1145/3290386

Digital Library

[37]

Calvin Smith and Aws Albarghouthi. 2016. MapReduce Program Synthesis. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). Association for Computing Machinery, New York, NY, USA. 326–340. isbn:978-1-4503-4261-2 https://doi.org/10.1145/2908080.2908102

Digital Library

[38]

Phillip D. Summers. 1977. A Methodology for LISP Program Construction from Examples. J. ACM, 24, 1 (1977), Jan., 161–175. issn:0004-5411 https://doi.org/10.1145/321992.322002

Digital Library

[39]

Xinyu Wang, Isil Dillig, and Rishabh Singh. 2017. Synthesis of Data Completion Scripts Using Finite Tree Automata. Proceedings of the ACM on Programming Languages, 1, OOPSLA (2017), Oct., 1–26. issn:2475-1421 https://doi.org/10.1145/3133886

Digital Library

[40]

Xinyu Wang, Isil Dillig, and Rishabh Singh. 2018. Program Synthesis Using Abstraction Refinement. Proceedings of the ACM on Programming Languages, 2, POPL (2018), Jan., 1–30. issn:2475-1421 https://doi.org/10.1145/3158151

Digital Library

[41]

Xinyu Wang, Sumit Gulwani, and Rishabh Singh. 2016. FIDEX: Filtering Spreadsheet Data Using Examples. In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016). Association for Computing Machinery, New York, NY, USA. 195–213. isbn:978-1-4503-4444-9 https://doi.org/10.1145/2983990.2984030

Digital Library

[42]

Yuepeng Wang, Xinyu Wang, and Isil Dillig. 2018. Relational Program Synthesis. Proceedings of the ACM on Programming Languages, 2, OOPSLA (2018), Oct., 1–27. issn:2475-1421 https://doi.org/10.1145/3276525

Digital Library

[43]

Yongwei Yuan, Arjun Radhakrishna, and Roopsha Samanta. 2023. Artifact for "Trace-Guided Inductive Synthesis of Recursive Functional Programs". https://doi.org/10.5281/zenodo.7812616

Digital Library

Cited By

Mariano BWang ZPailoor SCollberg CDillig I(2024)Control-Flow Deobfuscation using Trace-Informed Compositional Program SynthesisProceedings of the ACM on Programming Languages10.1145/36897898:OOPSLA2(2211-2241)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689789
Lubin JFerguson JYe KYim JChasins S(2024)Equivalence by Canonicalization for Synthesis-Backed RefactoringProceedings of the ACM on Programming Languages10.1145/36564538:PLDI(1879-1904)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656453
Wang ZPailoor SPrakash AWang YDillig I(2024)From Batch to Stream: Automatic Generation of Online AlgorithmsProceedings of the ACM on Programming Languages10.1145/36564188:PLDI(1014-1039)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656418
Show More Cited By

Index Terms

Trace-Guided Inductive Synthesis of Recursive Functional Programs
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
      1. Automatic programming
  2. Software notations and tools
    1. Context specific languages
      1. Programming by example
    2. General programming languages
      1. Language features
        Recursion
      2. Language types
        Functional languages

Recommendations

Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions

We present a novel approach to synthesizing recursive functional programs from input-output examples. Synthesizing a recursive function is challenging because recursive subexpressions should be constructed while the target function has not been fully ...
Automatic synthesis of recursive programs: the proof-planning paradigm
ASE '97: Proceedings of the 12th international conference on Automated software engineering (formerly: KBSE)

We describe a proof plan that characterises a family of proofs corresponding to the synthesis of recursive functional programs. This plan provides a significant degree of automation in the construction of recursive programs from specifications, together ...
Can reactive synthesis and syntax-guided synthesis be friends?
SPLASH Companion 2021: Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity

While reactive synthesis and syntax-guided synthesis (SyGuS) have seen enormous progress in recent years, combining the two approaches has remained a challenge. In this work, we present the synthesis of reactive programs from Temporal Stream Logic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue PLDI

June 2023

2020 pages

EISSN:2475-1421

DOI:10.1145/3554310

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 June 2023

Published in PACMPL Volume 7, Issue PLDI

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
709
Total Downloads

Downloads (Last 12 months)441
Downloads (Last 6 weeks)87

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Mariano BWang ZPailoor SCollberg CDillig I(2024)Control-Flow Deobfuscation using Trace-Informed Compositional Program SynthesisProceedings of the ACM on Programming Languages10.1145/36897898:OOPSLA2(2211-2241)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689789
Lubin JFerguson JYe KYim JChasins S(2024)Equivalence by Canonicalization for Synthesis-Backed RefactoringProceedings of the ACM on Programming Languages10.1145/36564538:PLDI(1879-1904)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656453
Wang ZPailoor SPrakash AWang YDillig I(2024)From Batch to Stream: Automatic Generation of Online AlgorithmsProceedings of the ACM on Programming Languages10.1145/36564188:PLDI(1014-1039)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656418
Hong QAiken A(2024)Recursive Program Synthesis using ParamorphismsProceedings of the ACM on Programming Languages10.1145/36563818:PLDI(102-125)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656381
Ji RZhao YXiong YWang DZhang LHu Z(2024)Decomposition-based Synthesis for Applying Divide-and-Conquer-like Algorithmic ParadigmsACM Transactions on Programming Languages and Systems10.1145/364844046:2(1-59)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1145/3648440
Miltner AWang ZChaudhuri SDillig I(2024)Relational Synthesis of Recursive Programs via Constraint Annotated Tree AutomataComputer Aided Verification10.1007/978-3-031-65633-0_3(41-63)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_3

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents