从隐式规范合成嵌套关系查询：基于模型论与证明论
Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
AI总结：
本文研究如何将嵌套关系上的隐式逻辑规范有效转换为嵌套关系演算（NRC）中的显式查询，分别通过模型论和证明论两种途径给出转换结果，并应用于从视图证明中提取NRC查询重写。
摘要：
派生数据集可以被隐式或显式地定义。数据集O关于数据集I的隐式定义是一个涉及两组不同关系符号的逻辑规范：一组关系用于“源数据”I，另一组用于“接口数据”O。如果该规范的任意两个在I上一致的模型也在O上一致，则该规范就是O关于I的有效定义。相比之下，显式定义是从I产生O的变换（下文称为“查询”）。Beth定理的若干变体表明，可以将隐式定义转换为显式定义。此外，如果在一个合适的证明系统中存在一个见证隐式可定义性的证明，那么这种转换可以被有效地完成。我们证明了嵌套关系上的类似隐式到显式的结果：在嵌套关系的自然逻辑中给出的隐式定义，可以转换为嵌套关系演算（NRC）中的显式定义。我们首先为该结果提供一个模型论论证，该论证建立了NRC查询、解释（逻辑中定义结构到结构翻译的标准机制）以及解释与“唯一同构意义下”的隐式可定义性之间的一些额外联系，这些联系可能具有独立的研究价值。后一个联系使用了Gaifman关于“相对范畴”理论的一个结果的变体。我们还提供了一个证明论结果，它给出了一个有效论证：从一个见证隐式可定义性的证明出发，我们可以高效地产生一个NRC定义。这将涉及引入用于嵌套集合推理的适当证明系统，以及该系统的一些辅助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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
