Synthesizing Nested Relational Queries from Implicit Specifications

TL;DR

This paper proves that implicit definitions of nested relational datasets can be effectively transformed into explicit queries, enabling automatic rewriting of queries based on proof of data determination.

Contribution

It extends Beth's theorem to nested relations, providing an effective method to convert implicit definitions into explicit NRC queries using proof systems.

Findings

Effective conversion from implicit to explicit definitions for nested relations.

Automatic extraction of query rewritings from proofs of data determination.

Formalization of the implicit-to-explicit transformation in nested relational logic.

Abstract

Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset $O$ in terms of datasets $\vec{I}$) is a logical specification involving the source data $\vec{I}$ and the interface data $O$. It is a valid definition of $O$ in terms of $\vec{I}$, if any two models of the specification agreeing on $\vec{I}$ agree on $O$. In contrast, an explicit definition is a query that produces $O$ from $\vec{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 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 a proof witnessing that the query is determined by the views.