论文标题
从隐性规范中综合嵌套的关系查询：通过模型理论和证明理论
Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
论文作者
论文摘要
派生的数据集可以隐式或明确定义。隐式定义（数据集i的数据集i）是逻辑规范，涉及两套杰出的关系符号集。一组关系是针对“源数据” i的，而另一个关系是针对“接口数据”O。这样的规范是i的有效定义，如果规范的两个模型同意i同意i。相反，明确的定义是下面的转换（或“ query”），可以从beth theorem theorem senere的变体中产生o o cortsits convertits convertits convertits convertiss convertiss convertits。此外，可以有效地进行这种转换，鉴于在合适的证明系统中证明了隐式确定性的证明。我们证明了嵌套关系的类似的隐式对解释结果：嵌套关系的自然逻辑中给出的隐式定义可以转换为嵌套的关系计算（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.
