Back to Search
Start Over
Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
- Source :
- Logical Methods in Computer Science, Vol Volume 20, Issue 3 (2024)
- Publication Year :
- 2024
- Publisher :
- Logical Methods in Computer Science e.V., 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 "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.
Details
- Language :
- English
- ISSN :
- 18605974
- Volume :
- ume 20, Issue 3
- Database :
- Directory of Open Access Journals
- Journal :
- Logical Methods in Computer Science
- Publication Type :
- Academic Journal
- Accession number :
- edsdoj.3851b818e334c75b0d45ff2ff171f69
- Document Type :
- article
- Full Text :
- https://doi.org/10.46298/lmcs-20(3:7)2024