# Synthesizing Nested Relational Queries from Implicit Specifications

arXiv: https://arxiv.org/abs/2209.08299 · HTML: https://mlsanity.com/paper/2209.08299/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Sep 2022.

## Built on by (most cited first, 1 of 1)

- [Range-Restricted Interpolation through Clausal Tableaux](https://mlsanity.com/paper/2306.03572/) (2023)

## Abstract (arXiv)

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