[madPL] SemGuS Reading Group 9/24

[Wiley Corning <wcorning@xxxxxxxx>]

Hi everyone,

I'm pleased to announce that we are resuming the SemGuS reading group this week! We will now be meeting on Fridays at 1pm Central Time in this Zoom room.

To get us started, this week I will discuss Synthesizing highly expressive SQL queries from input-output examples (PLDI 2017). The synthesis system presented in this paper, Scythe, incorporates many of the techniques we've been working with lately: it is enumerative, performs reduction by observational equivalence, and uses syntactic restrictions (akin to rewrite rules) to avoid redundancy. In particular, the authors propose an abstract semantics for SQL queries that overapproximates the concrete semantics, and use this abstraction to construct an efficient two-phase synthesis method. We'll be diving into this design and considering ways in which it could be generalized for SemGuS.

"Homework" question: the second phase of Scythe generates predicates which are used to fill holes in filter clauses (e.g., Select * From t Where ___ -> Select * From t Where (t.index < 10)). As an optimization, Scythe represents each predicate as a bit vector whose k'th bit corresponds to whether it accepts or rejects the k'th row in a given input table; these bit vectors can then be quickly checked for observational equivalence. How could you extend this concept to efficiently encode a more general mapping operation (e.g., vector.map(x => ___) -> vector.map(x => f(x)))?

Best,
Wiley Corning