No Cover Image

Conference Paper/Proceeding/Abstract 536 views

Synthesizing Nested Relational Queries from Implicit Specifications

Michael Benedikt Orcid Logo, Cécilia Pradic Orcid Logo, Christoph Wernhard Orcid Logo

Proceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems

Swansea University Author: Cécilia Pradic Orcid Logo

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...

Full description

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
first_indexed 2023-04-14T14:05:59Z
last_indexed 2024-11-14T12:18:52Z
id cronfa61306
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2023-11-20T15:06:41.3053337</datestamp><bib-version>v2</bib-version><id>61306</id><entry>2022-09-22</entry><title>Synthesizing Nested Relational Queries from Implicit Specifications</title><swanseaauthors><author><sid>3b6e9ebd791c875dac266b3b0b358a58</sid><ORCID>0000-0002-1600-8846</ORCID><firstname>C&#xE9;cilia</firstname><surname>Pradic</surname><name>C&#xE9;cilia Pradic</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2022-09-22</date><deptcode>MACS</deptcode><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&#x2019;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.</abstract><type>Conference Paper/Proceeding/Abstract</type><journal>Proceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems</journal><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher>ACM</publisher><placeOfPublication>New York, NY, USA</placeOfPublication><isbnPrint>979-8-4007-0127-6</isbnPrint><isbnElectronic/><issnPrint/><issnElectronic/><keywords/><publishedDay>18</publishedDay><publishedMonth>6</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-06-18</publishedDate><doi>10.1145/3584372.3588653</doi><url>http://dx.doi.org/10.1145/3584372.3588653</url><notes/><college>COLLEGE NANME</college><department>Mathematics and Computer Science School</department><CollegeCode>COLLEGE CODE</CollegeCode><DepartmentCode>MACS</DepartmentCode><institution>Swansea University</institution><apcterm/><funders>This work was funded by EPSRC grant EP/T022124/1 and by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation)&#x2013; Project-ID 457292495.</funders><projectreference/><lastEdited>2023-11-20T15:06:41.3053337</lastEdited><Created>2022-09-22T16:29:45.2713502</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>Michael</firstname><surname>Benedikt</surname><orcid>0000-0003-2964-0880</orcid><order>1</order></author><author><firstname>C&#xE9;cilia</firstname><surname>Pradic</surname><orcid>0000-0002-1600-8846</orcid><order>2</order></author><author><firstname>Christoph</firstname><surname>Wernhard</surname><orcid>0000-0003-2964-0880</orcid><order>3</order></author></authors><documents/><OutputDurs/></rfc1807>
spelling 2023-11-20T15:06:41.3053337 v2 61306 2022-09-22 Synthesizing Nested Relational Queries from Implicit Specifications 3b6e9ebd791c875dac266b3b0b358a58 0000-0002-1600-8846 Cécilia Pradic Cécilia Pradic true false 2022-09-22 MACS 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. Conference Paper/Proceeding/Abstract Proceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems ACM New York, NY, USA 979-8-4007-0127-6 18 6 2023 2023-06-18 10.1145/3584372.3588653 http://dx.doi.org/10.1145/3584372.3588653 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University This work was funded by EPSRC grant EP/T022124/1 and by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation)– Project-ID 457292495. 2023-11-20T15:06:41.3053337 2022-09-22T16:29:45.2713502 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Michael Benedikt 0000-0003-2964-0880 1 Cécilia Pradic 0000-0002-1600-8846 2 Christoph Wernhard 0000-0003-2964-0880 3
title Synthesizing Nested Relational Queries from Implicit Specifications
spellingShingle Synthesizing Nested Relational Queries from Implicit Specifications
Cécilia Pradic
title_short Synthesizing Nested Relational Queries from Implicit Specifications
title_full Synthesizing Nested Relational Queries from Implicit Specifications
title_fullStr Synthesizing Nested Relational Queries from Implicit Specifications
title_full_unstemmed Synthesizing Nested Relational Queries from Implicit Specifications
title_sort Synthesizing Nested Relational Queries from Implicit Specifications
author_id_str_mv 3b6e9ebd791c875dac266b3b0b358a58
author_id_fullname_str_mv 3b6e9ebd791c875dac266b3b0b358a58_***_Cécilia Pradic
author Cécilia Pradic
author2 Michael Benedikt
Cécilia Pradic
Christoph Wernhard
format Conference Paper/Proceeding/Abstract
container_title Proceedings of the 42nd ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems
publishDate 2023
institution Swansea University
isbn 979-8-4007-0127-6
doi_str_mv 10.1145/3584372.3588653
publisher ACM
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
url http://dx.doi.org/10.1145/3584372.3588653
document_store_str 0
active_str 0
description 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.
published_date 2023-06-18T14:23:44Z
_version_ 1821415754432512000
score 11.543985

Similar Items