We study the expressive power of some fragments of XPath equipped with (in)equality tests over data trees. Our main results are the de nability theorems, which give necessary and su cient conditions under which a class of data trees can be de ned by a node expression or set of node expressions, and our separation theorems, which give su cient conditions under which two disjoint classes of data trees can be separated by a class of data trees de nable in XPath.
de nability
rst-order logic
The abstraction of an XML document is a data tree, i.e. a tree whose every
node contains a tag or label (such as LastName) from a nite domain, and a
data value (such as Smith) from an in nite domain. XPath is the most widely
used query language for XML documents; it is an open standard and
constitutes a World Wide Web Consortium (W3C) Recommendation [
First, we provide notions of saturation and ultraproducts that are adequate for XPath=, and show that bisimulation coincides with logical equivalence over saturated data trees. Using these tools, we show de nability theorems, giving necessary and su cient conditions under which a class of data trees can be de ned by a node expression or set of node expressions of XPath=. Finally we give separation results, providing su cient conditions under which two disjoint classes of data trees can be separated by a class of data trees de nable in XPath=.
While on this work we will only show results for the fragment of XPath that can only navigate via the `child' accessibility relation, similar results hold for the vertical fragment having both the `child' and `parent' navigational operators.
The results on de nability of this paper appeared originally in [
Data trees. We say that T is a data tree if it is a tree from Trees(A D), where A is a nite set of labels and D is an in nite set of data values. The data of a node x is denoted data(x), and its label is label (x). The set of nodes of a data tree T is denoted T .
Downward XPath with data tests. We consider a fragment of XPath that corresponds to the navigational part of XPath 1.0 with data equality and inequality. XPath= is a two-sorted language, with path expressions (that we write ; ; ) and node expressions (that we write '; ; ). The downward XPath, notated XPath#= is de ned by mutual recursion as follows:
; '; ::= o j ['] j ::= a j :' j ' ^ j [ j ' _ j h i j h = i j h 6= i o 2 f"; #g a 2 A
Node expressions represent properties on nodes. They are evaluated in nodes, and, intuitively, h = i is true at x if there are two paths starting in x, one satisfying the property , and the other satisfying the property , which end in nodes with equal data value. On the other hand, path expressions represent properties on paths. They are evaluated in pairs of nodes. For instance # is true at (x; y) if y is a child of x, and ['] is true at x; y if x = y and x satis es '.
Let T and T 0 be data trees, and let u 2 T , u0 2 T 0. We say that T ; u and T 0; u0 are logically equivalent for XPath#= if no XPath#= can distinguish node u from u0.
Bisimulations. Notions of bisimulation present a way to determine whether two pointed data trees can be distinguished by a series of moves in XPath. We do not reproduce them here, but it is worth mentioning that they are forms of back-and-forth conditions over two data trees.
The main previous result in the literature establishing the connection between
bisimulation and equivalence is the following:
Theorem 1. [
We introduce a notion of saturation for the downward fragment of XPath, and show that the reverse implication of Theorem 1 is true over saturated data trees. Saturation is the key ingredient to show the De nability theorems, but their use lays hidden in the proof.
Saturation. Let h 1; : : : ; ni and h 1; : : : ; mi be tuples of sets of XPath#=formulas. Given a data tree T and u 2 T , we say that h 1; : : : ; ni and h 1; : : : ; mi are =#n;m-satis able [resp. 6=#n;m-satis able] at T ; u if there exist v0 ! v1 ! ! vn 2 T and w0 ! w1 ! ! wm 2 T such that u = v0 = w0 and 1. for all i 2 f1; : : : ; ng, T ; vi j= i; 2. for all j 2 f1; : : : ; mg, T ; wj j= j ; and 3. data(vn) = data(wm) [resp. data(vn) 6= data(wm)].
We say that h 1; : : : ; ni and h 1; : : : ; mi are =#n;m- nitely satis able [resp. 6=#n;m- nitely satis able] at T ; u if for every nite i0 i and nite j0 j , we have that h 10; : : : ; n0i and h 10; : : : ; m0i are =#n;m-satis able [resp. 6=#n;msatis able] at T ; u.
De nition 2. We say that a data tree T is #-saturated if for every n; m 2 N, every pair of tuples h 1; : : : ; ni and h 1; : : : ; mi of sets of XPath#=-formulas, every u 2 T , and ? 2 f=; 6=g, the following is true: if h 1; : : : ; ni and h 1; : : : ; mi are ?#n;m- nitely satis able at T ; u then h 1; : : : ; ni and h 1; : : : ; mi are ?#n;m-satis able at T ; u.
Proposition 3. For #-saturated data trees, bisimulation coincides with logical equivalence.
Quasi-ultraproducts We introduce the notion of quasi-ultraproduct, a variant of the usual notion of rst-order model theory, which will be needed for the de nability theorems. Some of our results for quasi-ultraproducts make use of the fundamental theorem of ultraproducts (see e.g. [2, Thm. 4.1.9]). De nition 4. Suppose (Ti; ui)i2I is a family of pointed data trees, U is an ultra lter over I, T is the ultraproduct of (Ti; ui)i2I , and u is the ultralimit of (ui)i2I . The #-quasi ultraproduct of (Ti; ui)i2I modulo U is the pointed data tree (T ju ; u ), where T ju denotes the subtree of T induced by al the descendants of u . As a particular case one has the notion of #-quasi ultrapower. 4
De nability theorems address the question of which properties of models can be de ned via formulas of the logic. If K is a class of pointed data trees, we denote its complement by K.
Theorem 5. Let K be a class of pointed data trees. Then K is de nable by a set of XPath#=-formulas i K is closed under #-bisimulations and #-quasi ultraproducts, and K is closed under #-quasi ultrapowers.
Theorem 6. Let K be a class of pointed data trees. Then K is de nable by an XPath#=-formula i both K and K are closed under #-bisimulations and #-quasi ultraproducts.
The notion of `-bisimulation is a restricted version of #-bisimulations. It has been shown to coincide with the notion of `-equivalence, which informally means indistinguishable by XPath#= formulas that cannot \see" beyond ` `child'-steps from the current point of evaluation.
Theorem 7. Let K be a class of pointed data trees. Then K is de nable by a formula of XPath#= i K is closed by `-bisimulations for XPath#= for some `.
Separation theorem provide conditions under which two disjoint classes of pointed models can be separated by a class de nable in the logic.
Theorem 8. Let K1 and K2 be two disjoint classes of pointed data trees such that K1 is closed under #-bisimulations and #-quasi ultraproducts and K2 is closed under #-bisimulations and #-quasi ultrapowers. Then there exists a third class K which is de nable by a set of XPath#=-formulas, contains K1 and is disjoint from K2.
Theorem 9. Let K1 and K2 be two disjoint classes of pointed data trees closed under #-bisimulations and #-quasi ultraproducts. Then there exists a third class K which is de nable by an XPath#=-formula, contains K1 and is disjoint from K2.