Michael Benedikt ; Cécilia Pradic ; Christoph Wernhard - Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory

lmcs:10495 - Logical Methods in Computer Science, July 22, 2024, Volume 20, Issue 3 - https://doi.org/10.46298/lmcs-20(3:7)2024
Synthesizing nested relational queries from implicit specifications: via model theory and via proof theoryArticle

Authors: Michael Benedikt ; Pierre Pradic ; Christoph Wernhard

    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.


    Volume: Volume 20, Issue 3
    Published on: July 22, 2024
    Accepted on: May 21, 2024
    Submitted on: December 16, 2022
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 973 times.
    This article's PDF has been downloaded 424 times.