Design Datalog Templates for Synthesizing Bidirectional Programs from Tabular E...
summary
Designs Datalog templates that let ProIn plus Z3 synthesize paired get/put programs from one tabular example and a supplied schema with functional dependencies, by forward-propagating functional dependencies through atomic query fragments and emitting candidate view-update rules encoding minimal-effect VI strategies and dependency-induced effects. A Python prototype called CBP generates candidate rules for ProIn, evaluates them, and successfully synthesizes 31 of 32 VDB-style benchmarks (aggregation unsupported).
AI-written summary · about
chapters (17)
- 0:00Datalog templates for bidirectional programs
- 1:07Bidirectional transformation programs
- 3:36Bidirectional transformation in databases
- 7:10Challenges in manual bidirectional programs
- 8:15Proven synthesizer overview
- 9:24Template design in Proven
- 11:13Template design observations
- 13:21Input requirements for synthesis
- 14:04Query synthesis with Proven
- 16:54Core contributions
- 17:14Forward propagation of dependencies
- 18:58View update strategies
- 23:00Dependency constraints in templates
- 24:27Dependency effect handling templates
- 25:52Prototype benchmark results
- 27:57Summary and future work
- 29:44Q&A
related talks
18mMobius: Synthesizing Relational Queries with Recursive and Invented Predicates
47mLogic Programming à la Carte
34mA Taste of Prolog
40mProduction Prolog
31mLetting users do the undecidable: lessons from program synthesis
32mSatisfiability Modulo Custom Theories in Z3 (Tool Paper)
30mProof Logging for Constraint Programming
26mProgram Synthesis Using Example Propagation