NSynC: Normalised Synthesis of Computation
For program synthesis researchers, NSynC offers a principled way to eliminate redundant evaluations, significantly accelerating synthesis for typed functional programs.
NSynC avoids semantic duplication in inductive program synthesis by enumerating programs directly according to their semantics (normal forms), achieving a geometric mean speedup of 8.93x over unrestricted synthesis on a synthetic benchmark suite.
Inductive program synthesis algorithms search a space of programs to find one that meets some specification. Enumerating according to the syntax of a programming language leads to a large search space, and hence slow synthesis, due in large part to semantic duplication. A synthesiser may have to evaluate -- and reject -- multiple semantically identical but syntactically different programs, wasting resources. To avoid this duplication, we present NSynC, a synthesis-by-semantics approach. By enumerating the semantics of the target language directly, we guarantee that each candidate program is semantically unique and that each evaluation of a candidate is meaningful. Specifically, we search the space of normal forms for the simply-typed lambda calculus with sums using a top-down, type-directed synthesis algorithm. Our preliminary results show a geomean speedup of 8.93x on a synthetic benchmark suite over the unrestricted algorithm.