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.

Thanks. We have received your report. If we find this content to be in
violation of our guidelines,
we will remove it.

Ok