Conference Paper/Proceeding/Abstract 531 views
Synthesizing Nested Relational Queries from Implicit Specifications
,
Cécilia Pradic ,
Christoph Wernhard
Proceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems
Swansea University Author:
Cécilia Pradic
Full text not available from this repository: check for access using links below.
DOI (Published version): 10.1145/3584372.3588653
Abstract
Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset in terms of datasets ) is a logical specification involving the source data and the interface data . It is a valid definition of in terms of , if any two models of the specification agreeing on agree on . In...
| Published in: | Proceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems |
|---|---|
| ISBN: | 979-8-4007-0127-6 |
| Published: |
New York, NY, USA
ACM
2023
|
| Online Access: |
http://dx.doi.org/10.1145/3584372.3588653 |
| URI: | https://cronfa.swan.ac.uk/Record/cronfa61306 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Abstract: |
Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset in terms of datasets ) is a logical specification involving the source data and the interface data . It is a valid definition of in terms of , if any two models of the specification agreeing on agree on . In contrast, an explicit definition is a query that produces from . Variants of Beth’s theorem 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 aproof witnessing that the query is determined by the views. |
|---|---|
| College: |
Faculty of Science and Engineering |
| Funders: |
This work was funded by EPSRC grant EP/T022124/1 and by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation)– Project-ID 457292495. |