一句话：证明嵌套关系隐式定义可有效转换为 NRC 显式查询，并给出模型论与证明论构造。
论文研究如何从逻辑隐式规约得到显式数据集变换。若任何两个满足规约且在源数据 I 上一致的模型也在接口数据 O 上一致，则该规约隐式定义 O。作者证明嵌套关系的 Beth 型结果：用嵌套集合自然逻辑写出的隐式定义可转换为嵌套关系演算 NRC 中的显式查询。方法一是模型论论证，将 NRC 查询、逻辑解释以及“唯一同构意义下”的隐式可定义性联系起来，并借助 Gaifman 相对范畴理论的变体；方法二是证明论构造，引入嵌套集合证明系统及辅助 Beth 型定理，从隐式可定义性证明中有效提取 NRC 定义。由此，在证明查询被视图决定后，可抽取 NRC 查询重写。
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.
@article{paperbot2742,
title = {Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory},
author = {Michael Benedikt and Cécilia Pradic and Christoph Wernhard},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 3},
year = {2024},
doi = {10.46298/lmcs-20(3:7)2024}
}