Synthesizing Data Structure Transformations from Input-Output Examples
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 Lambda^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 Lambda^2. A highlight is the synthesis of a program believed to be the world’s earliest functional pearl.
Tue 16 JunDisplayed time zone: Tijuana, Baja California change
09:15 - 10:55
|Efficient Synthesis of Network Updates|
Jedidiah McClurg University of Colorado Boulder, Hossein Hojjat Cornell University, Pavol Cerny University of Colorado Boulder, Nate Foster Cornell UniversityPre-print Media Attached
|Efficient Synthesis of Probabilistic Programs|
Aditya Nori Microsoft Research, UK, Sherjil Ozair IIT Delhi, Sriram Rajamani Microsoft Research, Deepak Vijaykeerthy Microsoft ResearchMedia Attached
|FlashRelate: Extracting Relational Data from Semi-Structured Spreadsheets Using Examples|
Dan Barowy University of Massachusetts Amherst, Sumit Gulwani Microsoft Research, Ted Hart Microsoft Research, Benjamin Zorn Microsoft ResearchMedia Attached
|Synthesizing Data Structure Transformations from Input-Output Examples|
John Feser Rice University, Swarat Chaudhuri Rice University, Işil Dillig University of Texas, AustinMedia Attached