Program Synthesis with Live Bidirectional Evaluation
share
We present an algorithm for completing program sketches (partial programs, with holes), in which evaluation and example-based synthesis are interleaved until the program is complete and produces a value. Our approach combines and extends recent advances in live programming with holes and type-and-example-directed synthesis of recursive functions over algebraic data types. Novel to our formulation is the ability to simultaneously solve interdependent synthesis goals — the key technique, called live bidirectional evaluation, iteratively solves constraints that arise during "forward" evaluation of candidate completions and propagates examples "backward" through partial results. We implement our approach in a prototype system, called Sketch-n-Myth, and develop several examples that demonstrate how live bidirectional evaluation enables a novel workflow for programming with synthesis. On benchmarks used to evaluate a state-of-the-art example-based synthesis technique, Sketch-n-Myth requires on average 55 overcoming the example trace-completeness requirement of previous work. Our techniques thus contribute to ongoing efforts to develop synthesis algorithms that can be deployed in future programming environments.
READ FULL TEXT