PL Seminar: Term-rewriting techniques for improving program synthesis

Tuesday, March 1, 2016 -
12:00pm to 1:00pm

Speaker Name: 

Calvin Smith




Program synthesis, as a field, consists of a number of techniques for turning specifications into executable programs and has applications ranging from spreadsheet manipulations to superoptimization. Excepting a few restricted cases, these techniques widely reduce to search, either directly, stochastically, or through an SMT solver. This dependence on enumeration serves as a bottleneck for many tools. In this talk we’ll explore methods for guiding enumeration and reducing the space of candidate solutions by encoding partial semantics of the domain in equations. By using one of several completion algorithms, we turn our set of equations into a decision procedure for equational equality in the form of a term-rewriting system. We’ll introduce several important properties of term-rewriting systems and detail how they can be exploited in a variety of synthesis frameworks to improve efficiency. Preliminary application of these rewrite systems towards improving enumeration show promising reductions in search time required, and there is promising work in using these rewrite rules to break symmetries in SMT-solver based solutions.