从隐式规格说明合成嵌套的关系数据库
Synthesizing Nested Relational Queries from Implicit Specifications
摘要：
派生数据集可以隐式或显式定义。（数据集$\vec{I}$方面的数据集$O$的）隐式定义是涉及源数据$\vec{I}$和接口数据$O$的逻辑规范。如果规范的任何两个模型在$\vec{I}$上达成一致，则它是$O$在$\vec{I}$方面的有效定义。相反，显式定义是从$\vec{I}$生成$O$的查询。贝丝定理的变体指出，可以将隐式定义转换为显式定义。此外，这种转换可以有效地完成，在一个合适的证明系统中证明隐含的可定义性。我们证明了嵌套关系的类似的有效的隐式到显式的结果：隐式定义，在嵌套关系的自然逻辑，可以有效地转换为显式定义的嵌套关系演算NRC。因此，我们可以有效地提取重写的NRC查询的NRC意见方面，证明了该查询是由意见。
英文摘要：
Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset $O$ in terms of datasets $\vec{I}$) is a logical specification involving the source data $\vec{I}$ and the interface data $O$. It is a valid definition of $O$ in terms of $\vec{I}$, if any two models of the specification agreeing on $\vec{I}$ agree on $O$. In contrast, an explicit definition is a query that produces $O$ from $\vec{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 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
