Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving the source data I and the interface data O. It 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 query 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 mechanisms for defining structure-to-structure translation in logic, and between interpretations and implicit to definability "up to unique isomorphism". The latter connection makes use of 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.
翻译:隐含的定义( 数据集 O, 数据集 I ) 是包含源数据 I 和界面数据 O 的逻辑性规格。 它是一个对源数据 I 和界面数据 O 的逻辑性定义。 如果两种规格的模型都同意 O 。 相反, 一个明确的定义是产生 O 的查询。 Beth 的变式 指出, 可以将隐含的定义转换为明确定义。 此外, 如果能证明在适当的验证系统中存在隐含的内含定义,这种转换可以有效进行。 我们证明了嵌入关系的类似隐含至解释结果: 嵌入关系的自然逻辑给出的隐含定义, 可以转换为I 的内含定义。 我们首先为这一结果提供一个模型理论性论据, 使一些可能具有独立兴趣的更多关联。 NRC 的查询、 解释、 定义结构对逻辑结构解释的标准机制, 以及解释和隐含的“ 解释性” 至于独特无序的逻辑性解释性解释性结果。