Synthesis of Recursive ADT Transformations from Reusable Templates
Recent work has proposed a promising approach to improving scalability of program synthesis by allowing the user to supply a syntactic template that constrains the space of potential programs. Unfortunately, creating templates often requires nontrivial effort from the user, which impedes the usabili...
| Main Authors: | , , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Springer-Verlag
2017
|
| Online Access: | http://hdl.handle.net/1721.1/111015 https://orcid.org/0000-0001-5571-173X https://orcid.org/0000-0001-7604-8252 |
| _version_ | 1811081409600684032 |
|---|---|
| author | Qiu, Xiaokang Lerner, Benjamin S. Inala, Jeevana Priya Polikarpova, Nadezhda Solar Lezama, Armando |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Qiu, Xiaokang Lerner, Benjamin S. Inala, Jeevana Priya Polikarpova, Nadezhda Solar Lezama, Armando |
| author_sort | Qiu, Xiaokang |
| collection | MIT |
| description | Recent work has proposed a promising approach to improving scalability of program synthesis by allowing the user to supply a syntactic template that constrains the space of potential programs. Unfortunately, creating templates often requires nontrivial effort from the user, which impedes the usability of the synthesizer. We present a solution to this problem in the context of recursive transformations on algebraic data-types. Our approach relies on polymorphic synthesis constructs: a small but powerful extension to the language of syntactic templates, which makes it possible to define a program space in a concise and highly reusable manner, while at the same time retains the scalability benefits of conventional templates. This approach enables end-users to reuse predefined templates from a library for a wide variety of problems with little effort. The paper also describes a novel optimization that further improves the performance and the scalability of the system. We evaluated the approach on a set of benchmarks that most notably includes desugaring functions for lambda calculus, which force the synthesizer to discover Church encodings for pairs and boolean operations. |
| first_indexed | 2024-09-23T11:46:13Z |
| format | Article |
| id | mit-1721.1/111015 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T11:46:13Z |
| publishDate | 2017 |
| publisher | Springer-Verlag |
| record_format | dspace |
| spelling | mit-1721.1/1110152022-10-01T05:54:02Z Synthesis of Recursive ADT Transformations from Reusable Templates Qiu, Xiaokang Lerner, Benjamin S. Inala, Jeevana Priya Polikarpova, Nadezhda Solar Lezama, Armando Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Inala, Jeevana Priya Polikarpova, Nadezhda Solar Lezama, Armando Recent work has proposed a promising approach to improving scalability of program synthesis by allowing the user to supply a syntactic template that constrains the space of potential programs. Unfortunately, creating templates often requires nontrivial effort from the user, which impedes the usability of the synthesizer. We present a solution to this problem in the context of recursive transformations on algebraic data-types. Our approach relies on polymorphic synthesis constructs: a small but powerful extension to the language of syntactic templates, which makes it possible to define a program space in a concise and highly reusable manner, while at the same time retains the scalability benefits of conventional templates. This approach enables end-users to reuse predefined templates from a library for a wide variety of problems with little effort. The paper also describes a novel optimization that further improves the performance and the scalability of the system. We evaluated the approach on a set of benchmarks that most notably includes desugaring functions for lambda calculus, which force the synthesizer to discover Church encodings for pairs and boolean operations. National Science Foundation (U.S.) (Award 1139056) 2017-08-24T19:36:27Z 2017-08-24T19:36:27Z 2017-03 Article http://purl.org/eprint/type/ConferencePaper 978-3-662-54576-8 978-3-662-54577-5 0302-9743 1611-3349 http://hdl.handle.net/1721.1/111015 Inala, Jeevana Priya et al. “Synthesis of Recursive ADT Transformations from Reusable Templates.” A. Legay and T. Margaria, editors. Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2017. Lecture Notes in Computer Science, 10205 (2017): 247–263 © 2017 Springer-Verlag GmbH Germany https://orcid.org/0000-0001-5571-173X https://orcid.org/0000-0001-7604-8252 en_US http://dx.doi.org/10.1007/978-3-662-54577-5_14 Tools and Algorithms for the Construction and Analysis of Systems Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Springer-Verlag MIT Web Domain |
| spellingShingle | Qiu, Xiaokang Lerner, Benjamin S. Inala, Jeevana Priya Polikarpova, Nadezhda Solar Lezama, Armando Synthesis of Recursive ADT Transformations from Reusable Templates |
| title | Synthesis of Recursive ADT Transformations from Reusable Templates |
| title_full | Synthesis of Recursive ADT Transformations from Reusable Templates |
| title_fullStr | Synthesis of Recursive ADT Transformations from Reusable Templates |
| title_full_unstemmed | Synthesis of Recursive ADT Transformations from Reusable Templates |
| title_short | Synthesis of Recursive ADT Transformations from Reusable Templates |
| title_sort | synthesis of recursive adt transformations from reusable templates |
| url | http://hdl.handle.net/1721.1/111015 https://orcid.org/0000-0001-5571-173X https://orcid.org/0000-0001-7604-8252 |
| work_keys_str_mv | AT qiuxiaokang synthesisofrecursiveadttransformationsfromreusabletemplates AT lernerbenjamins synthesisofrecursiveadttransformationsfromreusabletemplates AT inalajeevanapriya synthesisofrecursiveadttransformationsfromreusabletemplates AT polikarpovanadezhda synthesisofrecursiveadttransformationsfromreusabletemplates AT solarlezamaarmando synthesisofrecursiveadttransformationsfromreusabletemplates |