Model Theory of XPath on Data Trees. Part I: Bisimulation and Characterization
Model Theory of XPath on Data Trees. Part I: Bisimulation and Characterization
复制标题
DOI：
10.1613/jair.4658
复制
发表时间：
2015-01-01
影响因子：
5
通讯作者：
Areces, Carlos
中科院分区：
文献类型：
--
作者：
Figueira, Diego;Figueira, Santiago;Areces, Carlos
我们通过数据树类上的数据（中）相等性测试来研究XPath的模型理论属性，即，树的类，其中每个节点包含来自有限字母表的标签和来自无限域的数据值。我们提供了包含子，父，祖先和后代轴的可编程逻辑的（bi）模拟概念来导航树。我们表明，这些概念准确地描述了与每个逻辑相关的等价关系。我们研究公式复杂性的措施，包括嵌套轴和嵌套的子公式在一个公式中的数量，这些概念是类似于一阶逻辑中的量词排名的概念。我们展示了细粒度的等价概念和（双）模拟，考虑到这些复杂性措施的表征结果。我们还证明了这些逻辑的积极片段对应于（非对称）模拟下保存的公式。我们证明了包含子轴的逻辑在相应的互模拟概念下等价于一阶逻辑不变量的片段。如果允许向上导航，则表征失败，但仍可以建立较弱的结果。这些结果保持在类的可能无限的数据trees.Father类的有限的数据trees.Father其内在的理论价值，我们认为，互模拟是有用的工具来证明（非）表达性的结果，这里研究的逻辑，我们证实了这一说法的例子。
We investigate model theoretic properties of XPath with data (in)equality tests over the class of data trees, i.e., the class of trees where each node contains a label from a finite alphabet and a data value from an infinite domain.We provide notions of (bi)simulations for XPath logics containing the child, parent, ancestor and descendant axes to navigate the tree. We show that these notions precisely characterize the equivalence relation associated with each logic. We study formula complexity measures consisting of the number of nested axes and nested subformulas in a formula; these notions are akin to the notion of quantifier rank in first-order logic. We show characterization results for fine grained notions of equivalence and (bi)simulation that take into account these complexity measures. We also prove that positive fragments of these logics correspond to the formulas preserved under (non-symmetric) simulations. We show that the logic including the child axis is equivalent to the fragment of first-order logic invariant under the corresponding notion of bisimulation. If upward navigation is allowed the characterization fails but a weaker result can still be established. These results hold both over the class of possibly infinite data trees and over the class of finite data trees.Besides their intrinsic theoretical value, we argue that bisimulations are useful tools to prove (non)expressivity results for the logics studied here, and we substantiate this claim with examples.