Journal article 434 views 66 downloads
Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
,
Christoph Wernhard
Logical Methods in Computer Science, Volume: 20, Issue: 3
Swansea University Author:
Cécilia Pradic
-
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)
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...
| 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 |
| 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. |
|---|---|
| Keywords: |
Computer Science; Logic in Computer Science |
| College: |
Faculty of Science and Engineering |
| Issue: |
3 |