No Cover Image

Journal article 434 views 66 downloads

Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory

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

Logical Methods in Computer Science, Volume: 20, Issue: 3

Swansea University Author: Cécilia Pradic Orcid Logo

  • 69247.VoR.pdf

    PDF | Version of Record

    © M.Benedikt, C. Pradic, and C. Wernhard. Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license.

    Download (809.64KB)

Check full text

DOI (Published version): 10.46298/lmcs-20(3:7)2024

Abstract

Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving two distinguished sets of relational symbols. One set of relations is for the "source data" I, and the other is for the "interfac...

Full description

Published in: Logical Methods in Computer Science
ISSN: 1860-5974
Published: Centre pour la Communication Scientifique Directe (CCSD) 2024
Online Access: Check full text

URI: https://cronfa.swan.ac.uk/Record/cronfa69247
first_indexed 2025-04-09T17:47:38Z
last_indexed 2025-05-02T04:24:51Z
id cronfa69247
recordtype SURis
fullrecord <?xml version="1.0"?><rfc1807><datestamp>2025-05-01T12:20:42.5532616</datestamp><bib-version>v2</bib-version><id>69247</id><entry>2025-04-09</entry><title>Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory</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>2025-04-09</date><deptcode>MACS</deptcode><abstract>Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving two distinguished sets of relational symbols. One set of relations is for the "source data" I, and the other is for the "interface data" O. Such a specification is a valid definition of O in terms of I, if any two models of the specification agreeing on I agree on O. In contrast, an explicit definition is a transformation (or "query" below) that produces O from I. 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 implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be converted to explicit definitions in the nested relational calculus (NRC). We first provide a model-theoretic argument for this result, which makes some additional connections that may be of independent interest, between NRC queries, interpretations, a standard mechanism for defining structure-to-structure translation in logic, and between interpretations and implicit to definability "up to unique isomorphism". The latter connection uses a variation of a result of Gaifman concerning "relatively categorical" theories. We also provide a proof-theoretic result that provides an effective argument: from a proof witnessing implicit definability, we can efficiently produce an NRC definition. This will involve introducing the appropriate proof system for reasoning with nested sets, along with some auxiliary Beth-type results for this system. 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.</abstract><type>Journal Article</type><journal>Logical Methods in Computer Science</journal><volume>20</volume><journalNumber>3</journalNumber><paginationStart/><paginationEnd/><publisher>Centre pour la Communication Scientifique Directe (CCSD)</publisher><placeOfPublication/><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic>1860-5974</issnElectronic><keywords>Computer Science; Logic in Computer Science</keywords><publishedDay>22</publishedDay><publishedMonth>7</publishedMonth><publishedYear>2024</publishedYear><publishedDate>2024-07-22</publishedDate><doi>10.46298/lmcs-20(3:7)2024</doi><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>Not Required</apcterm><funders/><projectreference/><lastEdited>2025-05-01T12:20:42.5532616</lastEdited><Created>2025-04-09T18:45:20.9409615</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><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><order>3</order></author></authors><documents><document><filename>69247__34152__262897c1bc9f4489bbb618e808d7144e.pdf</filename><originalFilename>69247.VoR.pdf</originalFilename><uploaded>2025-05-01T12:17:59.6129791</uploaded><type>Output</type><contentLength>829075</contentLength><contentType>application/pdf</contentType><version>Version of Record</version><cronfaStatus>true</cronfaStatus><documentNotes>&#xA9; M.Benedikt, C. Pradic, and C. Wernhard. Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language><licence>https://creativecommons.org/licenses/by/4.0</licence></document></documents><OutputDurs/></rfc1807>
spelling 2025-05-01T12:20:42.5532616 v2 69247 2025-04-09 Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory 3b6e9ebd791c875dac266b3b0b358a58 0000-0002-1600-8846 Cécilia Pradic Cécilia Pradic true false 2025-04-09 MACS Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving two distinguished sets of relational symbols. One set of relations is for the "source data" I, and the other is for the "interface data" O. Such a specification is a valid definition of O in terms of I, if any two models of the specification agreeing on I agree on O. In contrast, an explicit definition is a transformation (or "query" below) that produces O from I. 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 implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be converted to explicit definitions in the nested relational calculus (NRC). We first provide a model-theoretic argument for this result, which makes some additional connections that may be of independent interest, between NRC queries, interpretations, a standard mechanism for defining structure-to-structure translation in logic, and between interpretations and implicit to definability "up to unique isomorphism". The latter connection uses a variation of a result of Gaifman concerning "relatively categorical" theories. We also provide a proof-theoretic result that provides an effective argument: from a proof witnessing implicit definability, we can efficiently produce an NRC definition. This will involve introducing the appropriate proof system for reasoning with nested sets, along with some auxiliary Beth-type results for this system. 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. Journal Article Logical Methods in Computer Science 20 3 Centre pour la Communication Scientifique Directe (CCSD) 1860-5974 Computer Science; Logic in Computer Science 22 7 2024 2024-07-22 10.46298/lmcs-20(3:7)2024 COLLEGE NANME Mathematics and Computer Science School COLLEGE CODE MACS Swansea University Not Required 2025-05-01T12:20:42.5532616 2025-04-09T18:45:20.9409615 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science Michael Benedikt 1 Cécilia Pradic 0000-0002-1600-8846 2 Christoph Wernhard 3 69247__34152__262897c1bc9f4489bbb618e808d7144e.pdf 69247.VoR.pdf 2025-05-01T12:17:59.6129791 Output 829075 application/pdf Version of Record true © M.Benedikt, C. Pradic, and C. Wernhard. Released under the terms of a Creative Commons Attribution 4.0 International (CC BY 4.0) license. true eng https://creativecommons.org/licenses/by/4.0
title Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
spellingShingle Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
Cécilia Pradic
title_short Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
title_full Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
title_fullStr Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
title_full_unstemmed Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
title_sort Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
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 Journal article
container_title Logical Methods in Computer Science
container_volume 20
container_issue 3
publishDate 2024
institution Swansea University
issn 1860-5974
doi_str_mv 10.46298/lmcs-20(3:7)2024
publisher Centre pour la Communication Scientifique Directe (CCSD)
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
document_store_str 1
active_str 0
description Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving two distinguished sets of relational symbols. One set of relations is for the "source data" I, and the other is for the "interface data" O. Such a specification is a valid definition of O in terms of I, if any two models of the specification agreeing on I agree on O. In contrast, an explicit definition is a transformation (or "query" below) that produces O from I. 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 implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be converted to explicit definitions in the nested relational calculus (NRC). We first provide a model-theoretic argument for this result, which makes some additional connections that may be of independent interest, between NRC queries, interpretations, a standard mechanism for defining structure-to-structure translation in logic, and between interpretations and implicit to definability "up to unique isomorphism". The latter connection uses a variation of a result of Gaifman concerning "relatively categorical" theories. We also provide a proof-theoretic result that provides an effective argument: from a proof witnessing implicit definability, we can efficiently produce an NRC definition. This will involve introducing the appropriate proof system for reasoning with nested sets, along with some auxiliary Beth-type results for this system. 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.
published_date 2024-07-22T17:53:18Z
_version_ 1850691759975170048
score 11.08899

Similar Items