论文标题
从隐式规格中合成嵌套的关系查询
Synthesizing Nested Relational Queries from Implicit Specifications
论文作者
论文摘要
派生的数据集可以隐式或明确定义。隐式定义（数据集$ $的数据集$ \ vec {i} $）是逻辑规范，涉及源数据$ \ vec {i} $和接口数据$ o $。如果在$ \ vec {i} $上同意$ o $ $ o $的任何两个模型，则在$ \ vec {i} $方面，这是$ o $的有效定义。相比之下，明确的定义是从$ \ 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.
