Synthesizing data structure transformations from input-output examples
Top Cited Papers
- 3 June 2015
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
Abstract
We present a method for example-guided synthesis of functional programs over recursive data structures. Given a set of input-output examples, our method synthesizes a program in a functional language with higher-order combinators like map and fold. The synthesized program is guaranteed to be the simplest program in the language to fit the examples. Our approach combines three technical ideas: inductive generalization, deduction, and enumerative search. First, we generalize the input-output examples into hypotheses about the structure of the target program. For each hypothesis, we use deduction to infer new input/output examples for the missing subexpressions. This leads to a new subproblem where the goal is to synthesize expressions within each hypothesis. Since not every hypothesis can be realized into a program that fits the examples, we use a combination of best-first enumeration and deduction to search for a hypothesis that meets our needs. We have implemented our method in a tool called λ2, and we evaluate this tool on a large set of synthesis problems involving lists, trees, and nested data structures. The experiments demonstrate the scalability and broad scope of λ2. A highlight is the synthesis of a program believed to be the world's earliest functional pearl.Keywords
Funding Information
- National Science Foundation (1162076)
- Defense Advanced Research Projects Agency (FA8750-14-2-0270)
This publication has 34 references indexed in Scilit:
- Recursive Program SynthesisLecture Notes in Computer Science, 2013
- Abstraction-guided synthesis of synchronizationInternational Journal on Software Tools for Technology Transfer, 2012
- Template-based program verification and program synthesisInternational Journal on Software Tools for Technology Transfer, 2012
- Automating string processing in spreadsheets using input-output examplesACM SIGPLAN Notices, 2011
- A Combined Analytical and Search-Based Approach for the Inductive Synthesis of Functional ProgramsKI - Künstliche Intelligenz, 2010
- Efficient Exhaustive Generation of Functional Programs Using Monte-Carlo Search with Iterative DeepeningLecture Notes in Computer Science, 2008
- On Barron and Strachey's cartesian product functionACM SIGPLAN Notices, 2007
- Combinatorial sketching for finite programsACM SIGPLAN Notices, 2006
- Jungloid miningACM SIGPLAN Notices, 2005
- Inductive functional programming using incremental program transformationArtificial Intelligence, 1995