Synthesizing Nested Relational Queries from Implicit Specifications
PROCEEDINGS OF THE 42ND ACM SIGMOD-SIGACT-SIGAI SYMPOSIUM ON PRINCIPLES OF DATABASE SYSTEMS, PODS 2023(2023)
Abstract
Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets (I) over right arrow) is a logical specification involving the source data (I) over right arrow and the interface data O. It is a valid definition of O in terms of (I) over right arrow, if two models of the specification agreeing on (I) over right arrow agree on O. In contrast, an explicit definition is a query that produces O from (I) over right arrow. Variants of Beth's theorem [8] state that one can convert implicit definitions to explicit ones. Further, this conversion can be done effectively given a proof witnessing implicit definability in a suitable proof system. We prove the analogous effective implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be effectively converted to explicit definitions in the nested relational calculus (NRC). As a consequence, we can effectively extract rewritings of NRC queries in terms of NRC views, given a proof witnessing that the query is determined by the views.
MoreTranslated text
Key words
Nested Relational Calculus,Views,Beth definability
AI Read Science
Must-Reading Tree
Example
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
Generate MRT to find the research sequence of this paper
Chat Paper
Summary is being generated by the instructions you defined