How big must complete XML query languages be?
How big must complete XML query languages be?
复制标题
完整的 XML 查询语言必须有多大？
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
Michael Benedikt
中科院分区：
文献类型：
--
作者：
Clemens Ley;Michael Benedikt
马克思和de rijke表明，W3C XML查询语言XPath的导航核心不是一阶完成 - 也就是说，它不能在导航谓词上表达一阶逻辑中可定义的每个查询。如何扩展XPath以获得一阶完整语言？马克思已经表明，有条件的XPath - XPath的扩展名为“直到”操作员 - 一阶完成。完整性参数使有条件XPath中向上轴的存在的存在必不可少。我们检查是否有可能获得XML布尔查询一阶完整的“仅远期”语言。很容易看出，时间逻辑CTL*的变体是一阶完成。该变体具有向下，向左和向右路径的路径量词，而沿路径可以检查线性时间逻辑（LTL）的任意公式。该语言具有两个主要缺点：它需要在两个水平方向上进行路径定量（特别是，它需要向后看节点的先前兄弟姐妹），并且需要考虑垂直路径上任意复杂性的LTL公式。最后一个与马克思的有条件XPath形成鲜明对比，后者只需要检查单个直到操作员在路径上。我们研究是否可以消除这两种限制。我们的主要结果是负面结果。我们表明，如果我们通过仅朝着一个水平方向限制直到操作员来限制我们的CTL*语言，那么我们就会失去完整性。我们还表明，沿垂直路径的LTL的“小”子集无限制足以达到一级完整性。这里的狭小手段是“直到深度”的界限，这是Etessami和Wilke定义的LTL公式复杂性的度量。特别是，从我们的工作中遵循的是，只有向前轴的条件XPath并未表现出来。这扩展了Rabinovich和Maoz在无限的无序树的背景下证明的结果。
Marx and de Rijke have shown that the navigational core of the w3c XML query language XPath is not first-order complete -- that is it cannot express every query definable in firstorder logic over the navigational predicates. How can one extend XPath to get a first-order complete language? Marx has shown that Conditional XPath -- an extension of XPath with an "Until" operator -- is first order complete. The completeness argument makes essential use of the presence of upward axes in Conditional XPath. We examine whether it is possible to get "forward-only" languages that are first-order complete for XML Boolean queries. It is easy to see that a variant of the temporal logic CTL* is first-order complete; the variant has path quantifiers for downward, leftward and rightward paths, while along a path one can check arbitrary formulas of linear temporal logic (LTL). This language has two major disadvantages: it requires path quantification in both horizontal directions (in particular, it requires looking backward at the prior siblings of a node), and it requires the consideration of formulas of LTL of arbitrary complexity on vertical paths. This last is in contrast with Marx's Conditional XPath, which requires only the checking of a single Until operator on a path. We investigate whether either of these restrictions can be eliminated. Our main results are negative ones. We show that if we restrict our CTL* language by having an until operator in only one horizontal direction, then we lose completeness. We also show that no restriction to a "small" subset of LTL along vertical paths is sufficient for first order completeness. Smallness here means of bounded "Until Depth", a measure of complexity of LTL formulas defined by Etessami and Wilke. In particular, it follows from our work that Conditional XPath with only forward axes is not expressively complete; this extends results proved by Rabinovich and Maoz in the context of infinite unordered trees.