Diego Figueira

Santiago Figueira

Carlos Areces

Basic Model Theory of XPath on Data Trees *

Keywords: F.4.1 [Mathematical Logic]: Model theory, H.2.3 [Languages]: Query Languages, I.7.2 [Document Preparation]: Markup Languages

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, descendant, parent and ancestor 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 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.

INTRODUCTION

We study the expressive power and model theory of XPatharguably the most widely used XML query language. Indeed, XPath is implemented in XSLT and XQuery and it is used as a constituent part of many specification and update languages. XPath is, fundamentally, a general purpose language for addressing, searching, and matching pieces of an XML document. It is an open standard and constitutes a World Wide Web Consortium (W3C) Recommendation [START_REF] Clark | XML path language (XPath)[END_REF].

Core-XPath (term coined in [START_REF] Gottlob | Efficient algorithms for processing XPath queries[END_REF]) is the fragment of XPath 1.0 containing the navigational behavior of XPath. It can express properties of the underlying tree structure of the XML document, such as the label (tag name) of a node, but it cannot express conditions on the actual data contained in the attributes. In other words, it only allows to reason about trees over a finite alphabet. Core-XPath has been well studied and its satisfiability problem is known to be decidable even in the presence of DTDs [START_REF] Marx | XPath with conditional axis relations[END_REF][START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF]. Moreover, it is known that it is equivalent to FO 2 (first-order logic with two variables over an appropriate signature on trees) in terms of expressive power [START_REF] Marx | Semantic characterizations of navigational XPath[END_REF], and that it is strictly less expressive than PDL with converse over trees [START_REF] Benedikt | XPath leashed[END_REF]. From a database perspective, however, Core-XPath fails to include the single most important construct in a query language: the join. Without the ability to relate nodes based on the actual data values of the attributes, the logic's expressive power is inappropriate for many applications.

The extension of Core-XPath with (in)equality tests between attributes of elements in an XML document is named Core-Data-XPath in [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF]. Here, we will call this logic XPath=. Models of XPath= are data trees which can be seen as XML documents. A data tree is a tree whose nodes contains a label from a finite alphabet and a data value from an infinite domain (see Figure 1 for an example). We will relax the condition on finiteness and consider also infinite data trees, although all our results hold also on finite structures.

The main characteristic of XPath= is to allow formulas of the form α = β , where α, β are path expressions, that navigate the tree using axes: descendant, child, ancestor, next-sibling, etc. and can make tests in intermediate nodes. The formula is true at a node x of a data tree if there are nodes y, z that can be reached by the relations denoted by α, β, respectively, and such that the data value of y is equal to the data value of z.

Recent articles investigate several algorithmic problems of logics evaluated over data trees. For example, satisfiability and evaluation are discussed in [START_REF] Figueira | Reasoning on Words and Trees with Data[END_REF][START_REF] Bojańczyk | XPath evaluation in linear time[END_REF]. In particular, all the logics studied in this article have a decidable satisfiability problem [START_REF] Figueira | Bottom-up automata on data trees and vertical XPath[END_REF][START_REF] Figueira | Decidability of downward XPath[END_REF]; but tools to investigate their expressive power are still lacking. There are good reasons for this: in the presence of joins and data values, classical notions such as Ehrenfeucht-Fraïssé games or structural bisimulations are difficult to handle. In this article we take the first steps towards understanding the expressive power and model theory of XPath= on data trees.

Contribution: XPath= can navigate the data tree by means of its axes: child (that we will note ↓), descendant (↓ * ), parent (↑), ancestor (↑ * ), etc. XPath= can also navigate the data tree horizontally, by going to a next or previous sibling of the current node. However, we focus on the vertical axes that allow downward and upward exploration. In particular, we will discuss the following languages: XPath (XPath= with ↓, ↑, ↓ * and ↑ * ); and its positive fragments. Our main contributions can be summarized as follows:

• In §3 and §5 we introduce bisimulation notions for XPath ↓ = , XPath ↓↓ * = , XPath = , and XPath * = and show that they precisely characterize the logical equivalence relation of the respective logic. We also consider fine grained versions of these bisimulations that take into account the number of nested axes and subformulas. The notion of bisimulation for XPath = relies on a strong normal form which we also introduce.

• In §4 we show that the simulations associated to the defined bisimulations characterize the positive fragments of the logics: a formula is equivalent to a positive formula if and only if it is invariant under simulations.

• In §6 we characterize XPath ↓ = as the fragment of firstorder logic over data trees (over a signature that includes the child relation and an equivalence relation) that is invariant under bisimulations. If we consider XPath = instead the characterization fails, but a weaker result can still be established.

• Using bisimulations we show (non)expressivity results about XPath= in §7. We characterize, for example, in which cases increasing the nesting depth increases the expressive power of XPath ↓ = .

• All results are proved both over the class of arbitrary (possibly infinite) data trees, and over the class of finite data trees. Related work: The notion of bisimulation was introduced independently by Van Benthem [START_REF] Van Benthem | Modal Correspondence Theory[END_REF] in the context of modal correspondence theory, Milner [START_REF] Milner | A Calculus of Communicating Systems[END_REF] and Park [START_REF] Park | Concurrency and automata on infinite sequences[END_REF] in concurrency theory, and Forti and Honsell [START_REF] Forti | Set theory with free construction principles[END_REF] in non-wellfounded set theory (see [START_REF] Sangiorgi | On the origins of bisimulation and coinduction[END_REF] for a historical outlook). This classical work defines a standard notion of bisimulation but this notion has to be suitably adapted for a particular, given logic. The notion of bisimulation for a given logic L defines when two models are indistinguishable for L, that is, when there is no formula of L that is true in one model but false in the other. Bisimulations can also be used to obtain model theoretic characterizations that identifies the expressive power of a logic L1 in terms of the bisimulation invariant fragment of a logic L2 which, hopefully, is better understood. The challenge, here, is to pinpoint both the appropriate notion of bisimulation required and the adequate 'framework' logic L2. The classical example of a result of this kind is Van Benthem's characterization for the basic modal logic as the bisimulation (with the standard notion of bisimulation) invariant fragment of first-order logic [START_REF] Van Benthem | Modal Correspondence Theory[END_REF]. Van Benthem's original result over arbitrary structures was proved to hold for finite structures by Rosen [START_REF] Rosen | Modal logic over finite structures[END_REF]. The proof was then simplified and unified by Otto [START_REF] Otto | Elementary proof of the Van Benthem-Rosen characterisation theorem[END_REF][START_REF] Otto | Bisimulation invariance and finite models[END_REF], and later expanded by Dawar and Otto [START_REF] Dawar | Modal characterisation theorems over special classes of frames[END_REF] to other classes of structures. Logics for semi-structured databases can often be seen as modal logics. In fact, structural characterizations for XPath without equality test were studied in [START_REF] Gyssens | Structural characterizations of the semantics of xpath as navigation tool on a document[END_REF], and XPath is known to be captured by PDL [START_REF] Harel | Dynamic logic[END_REF], whose bisimulation is well-understood [START_REF] Blackburn | Modal Logic[END_REF]. It is then natural to look for an intuitive bisimulation definition for XPath=.

PRELIMINARIES

Notation

Let N = {1, 2, 3, . . . } and let [n] := {1, . . . , n} for n ∈ N. We use the symbol A to denote a finite alphabet, and D to denote an infinite domain (e.g., N) of data values. In our examples we will consider D = N. We write X∼Y to say that X is the result of replacing every data value d ∈ D from Y by f (d) where f : D → D is some arbitrary bijection, for any objects X, Y . We write λ for the empty string.

Data trees

Let Trees(A) be the set of ordered and unranked trees over an arbitrary alphabet A. We say that T is a data tree if it is a tree from Trees(A × D) where A is a finite set of labels and D is an infinite set of data values. Figure 1 shows an example of a (finite) data tree. A data tree is finitely branching if every node has finitely many children. For any given data tree T , we denote by T its set of nodes. We use letters x, y, z, v, w as variables for nodes. Given a node x ∈ T of T , we write label (x) ∈ A to denote the node's label, and data(x) ∈ D to denote the node's data value.

Given two nodes x, y ∈ T we write x→y if y is a child of x, and x n →y if y is a descendant of x at distance n. In particular, For any binary relation R over elements of data trees, we say that a property P is R-invariant whenever the following condition holds: for every data tree T and u ∈ T , if (T , u) satisfies P and (T , u) is R-related to (T , u ) then (T , u ) satisfies P . We introduce the query language XPath adapted to data trees as abstractions of XML documents. We work with a simplification of XPath, stripped of its syntactic sugar. We consider fragments of XPath that correspond 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 fragment XPath=(O), with O ⊆ {↓, ↓ * , ↑, ↑ * }, is defined by mutual recursion as follows: We formally define the semantics of XPath= in Table 1. As an example, if T is the data tree shown in Figure 1 We call downward XPath to XPath ↓ = and vertical XPath to XPath = .

XPath

α, β ::= o | [ϕ] | αβ | α ∪ β o ∈ O ∪ {ε} ϕ, ψ ::= a | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | α | α = β | α = β a ∈ A A formula of XPath=(O)
In terms of expressive power, it is easy to see that ∪ is unessential: every XPath= node expression ϕ has an equivalent ϕ with no ∪ in its path expressions. ϕ can be computed in exponential time without incrementing the number of nested axes or the number of nested subformulas. It is enough to use the following equivalences to eliminate occurrences of ∪

α β ≡ β α β(α ∪ α )β ≡ βαβ ∨ βα β γ β(α ∪ α )β ≡ γ βαβ ∨ γ βα β
where ∈ {=, =}. We will henceforth assume that formulas do not contain union of path expressions.

BISIMULATION

Downward XPath

We write dd (ϕ) to denote the downward depth of ϕ, defined in Table 2. Let -XPath ↓ = be the fragment of XPath ↓

=

consisting of all formulas ϕ with dd(ϕ) ≤ .

Let T and T be data trees, and let u ∈ T , u ∈ T . We say that T , u and T , u are equivalent for XPath ↓ = (notation: T , u ≡ ↓ T , u ) iff for all formulas ϕ ∈ XPath ↓ = , we have T , u |= ϕ iff T , u |= ϕ. We say that T , u and T , u are -equivalent for XPath ↓ = (notation:

T , u ≡ ↓ T , u ) iff for all ϕ ∈ -XPath ↓ = , we have T , u |= ϕ iff T , u |= ϕ.
For every , there are finitely many different formulas ϕ of dd(ϕ) ≤ up to logical equivalence.

Proposition 3.1. ≡ ↓ has finite index. Corollary 3.2. {T , u | T , u ≡ ↓ T , u } is definable by an -XPath ↓ = -formula χ ,T ,u .

Bisimulation and -bisimulation

Let T and T be two data-trees. We say that u ∈ T and u ∈ T are bisimilar for XPath ↓ = (notation: T , u↔ ↓ T , u ) iff there is a relation Z ⊆ T × T such that uZu and for all x ∈ T and x ∈ T we have

• Harmony: If xZx then label (x) = label (x ).
• Zig (Figure 2 We say that u ∈ T and u ∈ T are -bisimilar for XPath ↓ = (notation: T , u ↔ ↓ T , u ) if there is a family of relations (Zj) j≤ in T × T such that uZ u and for all j ≤ , x ∈ T and x ∈ T we have Vertical depth

nd(a) = 0 nd(ϕ ∧ ψ) = max{nd(ϕ), nd(ψ)} nd(¬ϕ) = nd(ϕ) nd( α ) = nd(α) nd( α β ) = max{nd(α), nd(β)} nd(αβ) = max{nd(α), nd(β)} nd(ε) = 0 nd([ϕ]) = 1 + nd(ϕ) nd(↓) = 0 nd(↑) = 0
Nesting depth

= ( 6 = ) 8v 9v 0 8w 9w 0 T T 0 n m x x 0 Z = ( 6 =

Equivalence and bisimulation

We now show that↔ ↓ coincides with ≡ ↓ on finitely branching data trees, and that ↔ ↓ coincides with ≡ ↓ . Theorem 3.7.

1. T , u ↔ ↓ T , u implies T , u ≡ ↓ T , u . The converse also holds when T and T are finitely branching.

2. T , u ↔ ↓ T , u iff T , u ≡ ↓ T , u .
The Theorem above (see Appendix for details) is a consequence of the next two propositions:

Proposition 3.8. T , u ↔ ↓ T , u implies T , u ≡ ↓ T , u .
Proof. We actually show that if T , u↔ ↓ T , u via (Zi) i≤ then for all 0 ≤ n ≤ j ≤ , for all ϕ with dd(ϕ) ≤ j, and for all α with dd(α) ≤ j:

1. If xZjx then T , x |= ϕ iff T , x |= ϕ; 2. If x n →v, x n →v and ( i →v) Z (j-n)+i ( i →v ) for all 0 ≤ i ≤ n, then (x, v) ∈ [[α]] T iff (x , v ) ∈ [[α]] T .
We For the inductive step, let x0, . . . , xn ∈ T and x 0 , . . . , x n ∈ T be such that

x = x0→x1→x2→ • • • →xn = v in T , x = x 0 →x 1 →x 2 → • • • →x n = v in T ,
and xiZj-ix i for all 0 ≤ i ≤ n. Assume, for contradiction, that (x , v ) / ∈ [[α]] T . Then, there is a subformula ϕ of α and k ∈ {0, . . . , n} such that T , x k |= ϕ and T , x k |= ϕ(this is shown in Lemma A.1 in the Appendix). This contradicts the inductive hypothesis 1. Proposition 3.9. T , u ≡ ↓ T , u implies T , u ↔ ↓ T , u .

Proof. Fix u ∈ T and u ∈ T such that T , u ≡ ↓ T , u . Define (Zi) i≤ by xZix iff T , x ≡ ↓ i T , x . We show that Z is an -bisimulation between T , u and T , u . By hypothesis, uZ u . Fix h ≤ , by construction, Z h satisfies Harmony. Let us see that Z h satisfies Zig (the case for Zag is analogous). Suppose xZ h x ,

x = v0→v1→ • • • →vn = v in T , x = w0→w1→ • • • →wm = w in T ,
and data(v) = data(w) (the case data(v) = data(w) is shown in a similar way), where m, n ≤ h. Let P ⊆ T 2 be defined by

P = {(v , w ) | x n →v ∧ x m →w ∧ data(v ) = data(w )}. Since T , x ≡ ↓ h T , x , dd( ↓ n =↓ m ) ≤ h and T , x |= ↓ n =↓ m , we conclude that P = ∅. We next show that there exists (v , w ) ∈ P such that i. x = v 0 →v 1 → • • • →v n = v in T , ii. x = w 0 →w 1 → • • • →w m = w in T ,
iii. (∀i ∈ {0, . . . , n}) T , vi ≡ ↓ h-i T , v i , and iv. (∀j ∈ {0, . . . , m}) T , wj ≡ ↓ h-j T , w j , and hence Zig is satisfied by Z h . By way of contradiction, assume that for all (v , w ) ∈ P satisfying i and ii we have either

(a) (∃i ∈ {0, . . . , n}) T , vi ≡ ↓ h-i T , v i , or (b) (∃j ∈ {0, . . . , m}) T , wj ≡ ↓ h-j T , w j .
Fix as any tautology such that dd( ) = 0. For each (v , w ) ∈ P we define two families of formulas,

ϕ 0 v ,w , . . . , ϕ n v ,w
and ψ 0 v ,w , . . . , ψ m v ,w , satisfying that dd(ϕ i v ,w ) ≤ h -i for all i ∈ {0, . . . , n} and dd(ψ j v ,w ) ≤ h -j for all j ∈ {0, . . . , m} as follows:

• Suppose that (a) holds and that i is the smallest number such that T , vi

≡ ↓ h-i T , v i . Let ϕ i v ,w be such that dd(ϕ i v ,w ) ≤ h-i and T , vi |= ϕ i v ,w but T , v i |= ϕ i v ,w . For k ∈ {0, . . . , n} \ {i}, let ϕ k v ,w = , and for k ∈ {0, . . . , m}, let ψ k v ,w = .
• Suppose that (a) does not hold. Then (b) holds. Let j be the smallest number such that T , wj ≡ ↓ h-j T , w j . Let ψ j v ,w be such that dd(ψ j v ,w ) ≤ h-j and T , wj |= ψ j v ,w but T , w j |= ψ j v ,w . For k ∈ {0, . . . , m} \ {j}, let ψ k v ,w = , and for k ∈ {0, . . . , n}, let ϕ k v ,w = .

For each i ∈ {0, . . . , n} and j ∈ {0, . . . , m}, let

Φ i = (v ,w )∈P ϕ i v ,w and Ψ j = (v ,w )∈P ψ j v ,w . (1)
Since dd(ϕ i v ,w ) ≤ h -i, by Proposition 3.1, there are finitely many non-equivalent formulas ϕ i v ,w ; the same applies to ψ j v ,w . Hence, both infinite conjunctions in (1) are equivalent to finite ones, and we may assume that Φ i and Ψ j are well-formed formulas. Finally, let

α = [Φ 0 ]↓[Φ 1 ]↓ • • • ↓[Φ n ] and β = [Ψ 0 ]↓[Ψ 1 ]↓ • • • ↓[Ψ m ].
By construction, dd(α), dd(β) ≤ h and so dd(

α = β ) ≤ h. Furthermore, T , x |= α = β and T , x |= α = β . This contradicts T , x ≡ ↓ h T , x .

Vertical XPath

We now study bisimulation for XPath = . Interestingly, the notion we give is simpler than the one for XPath ↓ = due to a normal form enjoyed by the logic.

In the downward fragment of XPath= we used dd(ϕ) to measure the maximum depth from the current point of evaluation that the formula can access. For the vertical fragment of XPath=, we need to define both the maximum distance r going downward and the maximum distance s going upward that the formula can reach. We call the pair (r, s) the vertical depth of a formula. Formally, the vertical depth of a formula ϕ (notation: vd(ϕ)) is the pair vd(ϕ) ∈ Z 2 ≥0 defined in Table 2.

The nesting depth of a formula ϕ (notation: nd(ϕ)) is the maximum number of nested [ ] appearing in ϕ. See Table 2 for the formal definition.

Let (r, s, k)-XPath = be the set of all formulas ϕ in XPath = with vd(ϕ) ≤ (r, s) and nd(ϕ) ≤ k.

Let T and T be data trees, let u ∈ T and u ∈ T . We say that T , u and T , u are equivalent for XPath = (notation: T , u ≡ T , u ) iff for all ϕ ∈ XPath = , we have T , u |= ϕ iff T , u |= ϕ. T , x and T , x are (r, s)-equivalent [resp. (r, s, k)-equivalent] for XPath = , and we note it T , x ≡ r,s T , x [resp. T , x ≡ r,s,k T , x ] if they satisfy the same XPath = formulas ϕ so that vd(ϕ) ≤ (r, s) [resp. vd(ϕ) ≤ (r, s) and nd(ϕ) ≤ k].

Normal form

We define a useful normal form for XPath = that will be implicitly used in the definition of bisimulation in the section. For n ≥ 0, let ↓ n denote the concatenation of n symbols ↓. I.e., ↓ 0 is the empty string λ, ↓ 1 = ↓, and

↓ n+1 = ↓↓ n (similarly for ↑ n ). A path expression α of XPath = is downward [resp. up- ward] if it is of the form ↓ n [ϕ] [resp. [ϕ]↑ n ] for some n ≥ 0 with ϕ ∈ XPath = . For example, ↓[ ↑ ] is a downward expres- sion whereas ↓[ ↓ ]↓ is not. An up-down expression is any expression of the form ε, α ↑ , α ↓ or α ↑ α ↓
where α ↑ is upward and α ↓ is downward. Henceforth we will use α ↑ , β ↑ , γ ↑ to denote upward expressions and α ↓ , β ↓ , γ ↓ to denote downward expressions and α ↑↓ , β ↑↓ , γ ↑↓ to denote up-down expressions. Note that in particular any downward or upward expression is an up-down expression. An XPath = formula or expression is in up-down normal form if every path expression contained in it is up-down and every data test is of the form ε α ↑↓ with ∈ {=, =}.

Proposition 3.10. Let ϕ ∈ (r, s, k)-XPath = . There is ϕ ↑↓ ∈ XPath = in up-down normal form such that 1. ϕ ↑↓ ≡ ϕ; 2. vd(ϕ ↑↓ ) = (r, s); and 3. nd(ϕ ↑↓ ) ≤ k • (r + s + 2).

Finite index

Contrary to the case of XPath ↓ = (cf., Proposition 3.1), the logical equivalence relation restricted to XPath = -formulas of bounded vertical depth has infinitely many equivalence classes.

Proposition 3.11. If r + s ≥ 2 then ≡ r,s has infinite index.

In the proof of the above proposition (see Appendix)we need to use formulas with unbounded nesting depth. In fact, when restricted to bounded nesting depth there are only finitely many formulas up to logical equivalence, as stated next.

Proposition 3.12. ≡ r,s,k has finite index.

Corollary 3.13. {T , u | T , u ≡ r,s,k T , u } is definable by an (r, s, k)-XPath = -formula.

Bisimulation and (r, s, k)-bisimulation

The advantage of the normal form presented in Section 3.2.1, is that it makes it possible to use a very simple notion of bisimulation. The disadvantage is that, since it does not preserve nesting depth, ↔ r,s,k does not correspond precisely to ≡ r,s,k , although ↔ corresponds precisely to ≡ . Nonetheless, we obtain, for all r, s, k,

↔ r,s,k ⊆ ≡ r,s,k ⊆ ↔ r,s,k•(r+s+2) .
Let T and T be two data-trees. We say that u ∈ T and u ∈ T are bisimilar for XPath = (notation: T , u↔ T , u ) iff there is a relation Z ⊆ T × T such that uZu and for all x ∈ T and x ∈ T we have

• Harmony: If xZx then label (x) = label (x ),
• Zig (Figure 3 Observe that contrary to the definition of ↔ ↓ , the conditions above do not require intermediate nodes to be related by Z. This is a direct consequence of the up-down normal form (Proposition 3.10).

We say that u ∈ T and u ∈ T are (r, s, k)-bisimilar for XPath = (notation: T , u↔ r,s,k T , u ) if there is a family of relations (Z k r,ŝ ) r+ŝ≤r+s, k≤k in T × T such that uZ k r,s u and for all r + ŝ ≤ r + s, k ≤ k, x ∈ T and x ∈ T we have that the following conditions hold.

Equivalence and bisimulation

The next result says that ↔ coincides with ≡ on finitely branching data trees, and states precisely in what way↔ r,s,k is related to ≡ r,s,k . Theorem 3.16.

1. T , u ↔ T , u implies T , u ≡ T , u . The converse also holds when T and T are finitely branching.

2. T , u ↔ r,s,k•(r+s+2) T , u implies T , u ≡ r,s,k T , u . 3. T , u ≡ r,s,k T , u implies T , u ↔ r,s,k T , u .
Corollary 3.17. ↔ r,s,k has finite index.

SIMULATION

In this section we define notions of directed (non-symmetric) simulations for XPath ↓ = and XPath = , as it is done, e.g., in [START_REF] Kurtonina | Simulating without negation[END_REF] for some modal logics. We obtain results similar to Theorems 3.7 and 3.16 but relating each simulation notion with the corresponding logical implication.

We say that an XPath= formula is positive if it contains no negation ¬ and no inequality data tests α = β . For L one of XPath ↓ = , XPath = , XPath ↓↓ * = , or XPath * = , we write L + for the positive fragment of L.

A simulation for XPath ↓ = [resp. for XPath = ] is simply a bisimulation from which the Zag clause and half of the first condition in the Zig clause have been omitted. Observe that simulations need not be symmetric.

Formally, we say that u ∈ T is similar to u ∈ T for XPath ↓ = (notation: T , u → ↓ T , u ) iff there is a relation Z ⊆ T × T such that uZu and for all x ∈ T and x ∈ T we have Relations → ↓ and → r,s,k are defined accordingly. We define one-way (non-symmetric) logical implication between models as follows. We write T , u ↓ T , u for

• Harmony: If xZx then label (x) = label (x ). • Zig: If xZx , x
(∀ϕ ∈ XPath ↓+ = ) [T , u |= ϕ ⇒ T , u |= ϕ].
Define ↓ , , and r,s,k in an analogous way for -XPath ↓+ = , XPath + = , (r, s, k)-XPath + = , respectively. As for bisimulation, we have that → coincides with . Theorem 4.1.

1. Let † ∈ {↓, }. T , u → † T , u implies T , u † T , u .
The converse holds when T is finitely branching.

2. T , u → ↓ T , u iff T , u ↓ T , u . 3. T , u → r,s,k•(r+s+2) T , u implies T , u r,s,k T , u . 4. T , u r,s,k T , u implies T , u → r,s,k T , u .
We say that T is a substructure of T if T is a data tree which results from removing some nodes of T , i.e., T ⊆ T and for all u, v ∈ T we have: 1) u→v on T iff u→v on T ; 2) label (u) on T equals label (u) on T ; and 3) data(u) on T equals data(u) on T . Equivalently, seen as σ-structures, T is the σ-substructure of T induced by T ⊆ T . One can verify that the identity on T is a simulation for XPath = from T to T . Lemma 4.2. If T is a substructure of T and u ∈ T then T , u → T , u .

We obtain that the formulas of XPath= invariant under simulations are, precisely, the positive ones.

1. ϕ ∈ XPath ↓ = is → ↓ -invariant [resp. → ↓ ] iff it is equivalent to a formula of XPath ↓+ = [resp. -XPath ↓+ = ]. 2. ϕ ∈ XPath = is → -invariant iff it is equivalent to a for- mula of XPath + = .
3. If ϕ ∈ XPath = is → r,s,k -invariant then it is equivalent to a formula of (r, s, k)-XPath + = .

4. If ϕ ∈ XPath = is equivalent to a formula of (r, s, k)-

XPath + = then ϕ is → r,s,k -invariant, for k = k•(r+s+2).

ADDING TRANSITIVITY

As it happens, for example, with the basic modal logic and propositional dynamic logic, the same notion of bisimulation [resp. simulation] of each logic captures the logical equivalence [resp. logical implication] for the corresponding fragments including the reflexive-transitive closure of the axes which are present. Intuitively, this occurs because ↓ * is an infinite union of compositions of ↓, and similarly for ↑.

Let ≡ ↓↓ * and ≡ * be the logical equivalence relation for XPath ↓↓ *

1. T , u ↔ † T , u implies T , u ≡ † T , u .
The converse also holds when T is finitely branching.

2. T , u → † T , u implies T , u † T , u . The converse also holds when T is finitely branching.

CHARACTERIZATION

In §6.1 we show that there is a truth-preserving translation from XPath = to first-order logic over an appropriate signature. In §6.2 we characterize XPath ↓ = as the fragment of first-order logic ↔ ↓ -invariant over data trees. In §6.3 we show that this result fails for XPath = in general, but a weaker result can still be proved.

Translating to first-order logic

We say that an XPath = -path expression α is in simple normal form if it is of the form

[ϕ0]o1[ϕ1]o2 • • • on[ϕn],
for n ≥ 0, ϕi ∈ XPath = , and oi ∈ {↓, ↑}. Proposition 6.1. For any XPath = -[resp. XPath ↓ = -] path expression α there is an equivalent XPath = -[resp. XPath ↓ = -] path expression α in simple normal form. Further, α can be computed in polynomial time from α. 1We say that an XPath = -formula ϕ is in simple normal form if each path expression α occurring in ϕ is in simple normal form.

Fix the signature σ with binary relations and ≈, and a unary predicate Pa for each a ∈ A. Any data tree T can be seen as a first-order σ-structure such that

T = {(x, y) ∈ T 2 | y is a child of x}; ≈ T = {(x, y) ∈ T 2 | data(x) = data(y)}; P T a = {x ∈ T | label (x) = a}.
We define the following translation Tr mapping XPath = formulas in simple normal form to first-order σ-formulas:

Trx(a) = Pa(x) (a ∈ A) Trx(ϕ † ψ) = Trx(ϕ) † Trx(ψ) ( † ∈ {∧, ∨}) Trx(¬ϕ) = ¬Trx(ϕ) Trx( α ) = (∃ȳ) x = y0 ∧ Trȳ(α) Trx( α = β ) = (∃ȳ)(∃z) x = y0 ∧ x = z0 ∧ yn ≈ zm∧ Trȳ(α) ∧ Trz(β) Trx( α = β ) = (∃ȳ)(∃z) x = y0 ∧ x = z0 ∧ yn ≈ zm∧ Trȳ(α) ∧ Trz(β) Trȳ(α) = n-1 i=0 oi+1(yi, yi+1) ∧ n i=0
Try i (ϕi), where ȳ = y0, . . . , yn and z = z0, . . . , zm, and are fresh when quantified in the fourth and fifth definition;

α = [ϕ0]o1[ϕ1]o2[ϕ2]o3 • • • on[ϕn]; β = [ψ0]o 1 [ψ1]o 2 [ψ2]o 3 • • • o m [ψm]; oi, o i ∈ {↓, ↑}; oj(u, v) represents u v if oj = ↓, and v u otherwise. Proposition 6.2. For ϕ ∈ XPath = we have T , u |= ϕ iff T |= Trx(ϕ)(u).

Downward XPath

Let FO(σ) be the set of first-order formulas over a given signature σ, and let C be a class of σ-models. An FO(σ)formula ϕ(x) is -local if for all data trees T and u ∈ T , we have T |= ϕ(u) ⇔ T | u |= ϕ(u). Finally, for ϕ ∈ FO(σ) let qr(ϕ) be its quantifier rank, i.e., the depth of nesting of its quantifiers.

Observe that the following result has two readings: one classical, and one restricted to finite models.

Theorem 6.3 (Characterization). Let ϕ(x) ∈ FO(σ).

The following are equivalent:

(i) ϕ is ↔ ↓ -invariant over [finite] data-trees;
(ii) ϕ is logically equivalent over [finite] data-trees to an -XPath ↓ = -formula, where = 2 qr(ϕ) -1. Proof. The implication (ii) ⇒ (i) follows straightforwardly from Theorem 3.7. The proof of (i) ⇒ (ii) goes as follows: First, we show that any ↔ ↓ -invariant ϕ(x) ∈ FO(σ) is -local for = 2 qr(ϕ) -1 (Proposition 6.4). Then, we prove that any

↔ ↓ -invariant ϕ(x) ∈ FO(σ) that is -local is ↔ ↓ -invariant(Proposition B.2 in the Appendix). Finally, we show that any FO(σ)-definable property which is ↔ ↓ - invariant is definable in -XPath ↓ = (Proposition B.3 in the Appendix). Proposition 6.4. Any ↔ ↓ -invariant ϕ(x) ∈ FO(σ) over [finite] data-trees is -local for = 2 qr(ϕ) -1.
Proof. We follow Otto's proof [START_REF] Otto | Elementary proof of the Van Benthem-Rosen characterisation theorem[END_REF]. Assume that ϕ(x) ∈ FO(σ) is ↔ ↓ -invariant, let q = qr(ϕ), and put = 2 q -1. Given a data tree T and u ∈ T it suffices to show the existence of data trees T and T , with corresponding elements u ∈ T and u ∈ T such that Indeed, from the above conditions it follows that

| {z } q copies ⌘ q u 0 u 00 | {z } q copies | {z } q copies | {z } q copies
T |= ϕ(u) iff T |= ϕ(u ) ((a) and ↔ ↓ -inv. of ϕ) iff T |= ϕ(u ) (c) iff (T | u) |= ϕ(u), ((b) and ↔ ↓ -inv. of ϕ)
and hence ϕ is -local. By Proposition 3.3 one may assume that u ∈ T is the root of T . We define T and T , as structures that are disjoint copies of sufficiently many isomorphic copies of T and T | u, respectively, all tied together by some common root. Both structures have q isomorphic copies of both T and T | u, and only distinguish themselves by the nature of the one extra subtree, in which u and u live, respectively: u is the root of one of the copies of T and u is the root of one of the copies of T | u. We indicate the two structures in the diagram of Figure 4, with distinguished elements u and u marked by •; the open cones stand for copies of T , the closed cones for copies of T | u. The new isomorphic copies have the same data values as the original one. The new root has an arbitrary, fixed, data value and label.

By Proposition 3.4, it is straightforward that conditions (a) and (b) are satisfied. Condition (c) is true because one can exhibit a strategy for player II in the q-round Ehrenfeucht-Fraïssé game on structures T and T . The strategy is exactly the same used in [START_REF] Otto | Elementary proof of the Van Benthem-Rosen characterisation theorem[END_REF].

Vertical XPath

The analog of Theorem 6.3 fails for XPath = : Lemma 6.5. The FO(σ)-formula

(∃x) Pa(x)
is ↔ -invariant though not logically equivalent over [finite] data-trees to any XPath = -formula.

Hence XPath = is not the fragment of FO(σ) which is ↔invariant over [finite] data-trees. However, the following analog of Proposition B.3 (needed for the proof of Theorem 6.3) still holds for the case of XPath = :

Proposition 6.6. Let k = k•(r+s+2). If ϕ(x) ∈ FO(σ) is ↔ r,s,k -invariant over [finite] data-trees, then there is ψ ∈ (r, s, k)-XPath = such that Trx(ψ) is logically equivalent to ϕ over [finite] data-trees.
Notice that the counterexample in Lemma 6.5 is an unrestricted, existential formula. One may wonder if it might be possible to extend the expressive power of XPath = to accout for unrestricted quantification. The natural candidate would be the modal operator E (usually known as the existential modality) which, intuitively, let us express that there is some node in the model where a formula holds. But even with the additional expressive power provided by E the analog of Theorem 6.3 fails. Formally, consider the logic XPath E = , which results from adding the operator E to XPath = with the following semantics:

[[Eϕ]] T = T if [[ϕ]] T = ∅, and [[Eϕ]] T = ∅ otherwise.
The following lemma shows a counterexample to the analog of Theorem 6.3, showing that XPath E = is not the fragment of FO(σ) ↔ -invariant over [finite] data-trees.

APPLICATIONS

We devote this section to exemplify how the model theoretic tools we developed can be used to show expressiveness results for XPath=. We do not intend to be comprehensive; rather we will exhibit a number of different results that show possible uses of the notions of bisimulation we introduced. Following the same ideas used in Propositions 3.8 and 3.9, it is easy to show that ( , k)-bisimulations characterize ( , k)equivalence. ↔ Figure 6: Closure subtree replication.

Expressiveness hierarchies

(v) = data(w) ⇔ data(v ) = data(w ), 2. if t > 0, ( i →v) Zj-n+i,t-1 ( i →v ) for all 0 ≤ i < n, and
3. if t > 0, ( i →w) Zj-m+i,t-1 ( i →w ) for all 0 ≤ i < m. • Zag: If xZj,tx , x
Proposition 7.1. T , u ↔ ↓ ,k T , u iff T , u ≡ ↓ ,k T , u . ≡ ↓ 0,0 ≡ ↓ 0,1 ≡ ↓ 0,2 ≡ ↓ 0,3 ≡ ↓ 0,4 ≡ ↓ 1,0 ≡ ↓ 1,1 ≡ ↓ 1,2 ≡ ↓ 1,3 ≡ ↓ 1,4 ≡ ↓ 2,1 ≡ ↓ 2,0 ≡ ↓ 2,2 ≡ ↓ 2,3 ≡ ↓ 2,4 ≡ ↓ 3,0 ≡ ↓ 3,1 ≡ ↓ 3,2 ≡ ↓
• • • • • • • • • • • •
The following theorem -proved in the Appendix using the bisimulation notion introduced above-characterizes when an increase in nesting depth results in an increase in expressive power (see Figure 5). We conjecture that a similar hierarchy holds in the absence of data values, but is not a direct consequence of our result. Theorem 7.2. For all , k ≥ 0, i ≥ 1,

≡ ↓ ,0 ≡ ↓ ,1 • • • ≡ ↓ , = ≡ ↓ , +i , and ≡ ↓ ,k ≡ ↓ +i,k

Safe operations on models

Bisimulations can also be used to that certain operations on models preserve truth. Such operations are usually called safe for given logic, as they can be applied to a model without changing the truth values of any formula in the language. Proposition 3.3, for example, is already an example of this kind of results showing that the class of models of a formula is closed under sub-model generation. We will now show a more elaborate example.

We say that T is a subtree replication of T , if T is the result of inserting T |x into T as a sibling of x, where x is any node of T different from the root. Figure 6 gives a schematic representation of this operation. Proof. Suppose that x ∈ T is not the root of T , and that T is the result of inserting T |x into T as a sibling of x. Let us call Tx to the new copy of T |x inserted into T , and let X be the set of nodes of T |x. Furthermore, if v ∈ X then vx is the corresponding node of Tx. Nodes v and vx have the same label and data value, and the position of v in T |x coincides with the position of vx in Tx.

By Theorem 5.1, it suffices to verify that T , u ↔ T , u via Z ⊆ T × T defined by:

Z = {(y, y) | y ∈ T } ∪ {(v, vx) | v ∈ X}
(Z is depicted as dotted lines in Figure 6). .

Non-expressivity results

Proof. The first item follows from Proposition 7.3. Since the logic is closed under subtree replication, the trees of Figure 7 are equivalent. As key(a) holds in one and not in the other, the statement follows.

For the second item, it is easy to see that fk

dist3 is expressible in XPath

= ; 2. dist3 is not expressible in XPath ↓↓ * = ;
3. neither dist3 nor its complement can be expressed in XPath * + =

.

Proof. For 1, one can check that

T , x |= ϕ iff T , x sat- isfies dist3, for ϕ = ε = ↓↓[ ε = ↑ ] .
Let us see 2. Consider the data trees T , x and T , x depicted in Figure 9. It is straightforward that T , x satisfies dist3 and T , x does not.

Let v 1 and v 2 be the leaves of T and let v be the only node of T with data value 3. One can check that T , x ↔ ↓ T , x via Z ⊆ T × T defined by

Z = { u, u | h(u) = h(u ) ∧ data(u) = data(u )} ∪ { v, v 1 , v, v 2 },
where h(y) denotes the height of y, i.e., the distance from y to the root of the corresponding tree (Z is depicted as dotted lines in Figure 9). Since T , x satisfies dist3 but T , x does not, from Theorem 5.1 it follows that dist3 is not expressible in XPath ↓↓ * = . For 3, one can verify that T , x → T , x via Z as defined above. If dist3 were definable in XPath * + = via ψ and the fact that T , x |= ψ, by Theorem 5.1(2) we would have T , x |= ψ, and this is a contradiction.

Let dist3 denote the complement of dist3, i.e., dist3(x) iff for all y, z so that x→y→z, we have that x, y, z do not have pairwise distinct data values. Now T , x satisfies dist3 and T , x does not. Since T is a substructure of T , by an argument analog to the one used in the proof of Proposition 7.4-2, we conclude that dist3 is not expressible in XPath * + = .

DISCUSSION

In this article we studied model theoretic properties of XPath over both finite and arbitrary data trees using bisimulations. One of the main results we discuss is the characterization of the downward and vertical fragments of XPath as the fragments of first-order logic which are invariant under suitable notions of bisimulation. This can be seen as a first step in the larger program of studying the model theory and expressiveness of XPath with data values and, more generally, of logics on data trees. It would be interesting to study notions of bisimulation with only descendant; or characterizations of XPath with child and descendant, as a fragment of FO with the descendant relation on data trees. We did not considered XPath with horizontal navigation between siblings, such as the axes next-sibling and previous-sibling. In fact, adding these axes results in a fragment that is somewhat less interesting since the adequate bisimulation notion on finite data trees corresponds precisely to data tree isomorphism modulo renaming of data values.

In Section 7 we show a number of concrete application of the model theoretic tools we developed, discussing both expressivity and non-expressivity results. We also show examples of operations which are safe for a given XPath fragment. It would be worthwhile to devise other model operations that preserve truth of XPath formulas as we show is the case for subtree replication.

An important application of bisimulation is as a minimization method: given a data tree T1 we want to find a data tree T2, as small as possible, so that T1 and T2 are bisimilar for some fragment L of XPath. Since L cannot distinguish between T1 and T2, we can use T2 as representative of T1 while the expressive power of L is all that is required by a given application. The complexity of several inference tasks (e.g., model checking) depends directly on the model size. This is why in some cases it may be profitable to first apply a minimization step. The existence of efficient minimization algorithms is intimately related to bisimulations: we can minimize a data tree T by partitioning it in terms of its coarsest auto-bisimulation. We plan to design and implement algorithms for data tree minimization using bisimulation and investigate their computational complexity. a, 1

a, 2 a, 3 a, 1 a, 1 a, 2 a, 2 T T 0 a, 1 a, 2 a, 1 a, 1 a, 2 x 0 x $ # Figure 9: dist3 not in XPath ↓↓ * = .
Then there is a subformula ϕ of α and k ∈ {0, . . . , n} such that T , ( Suppose α = βγ. Then there is

k such that (x, v k ) ∈ [[β]] T and (v k , v) ∈ [[γ]] T . Since (x , v ) / ∈ [[α]] T , we have (x , v k ) / ∈ [[β]] T or (v k , v ) / ∈ [[γ]] T .
In either case, apply inductive hypothesis straightforwardly. Proposition 3.1. ≡ ↓ has finite index.

Proof. We show by induction on that there are finitely many non-equivalent formulas of downward depth at most , and finitely many non-equivalent path expressions of downward depth at most .

For the base case, any formula of downward depth 0 is a Boolean combination of labels, and hence there are finitely many non-equivalent of them. Any path expression of downward depth 0 is equivalent to [ϕ] for dd(ϕ) = 0, and hence there are finitely many non-equivalent of them.

For the induction, any formula of downward depth + 1 is a boolean combination of labels or formulas of the form α , α = β or α = β , where dd(α), dd(β) ≤ + 1, so it suffices to show that there are finitely many non-equivalent path expressions of downward depth at most + 1. Let α be such that dd(α) ≤ + 1. By Proposition 6.1, α is either equivalent to a path expression of the form [ψ] or of the form [ψ] ↓ β, where dd(ψ), dd(β) ≤ . By inductive hypothesis there are finitely many non-equivalent ψ's and βi's, and hence finitely many non-equivalent α's.

Corollary 3.2. {T , u | T , u ≡ ↓ T , u } is definable by an -XPath ↓ = -formula χ ,T ,u .
Proof. Consider the conjunction of all -XPath ↓ = formulas ϕ such that T , u |= ϕ. By Proposition 3.1, up to logical equivalence, there are finitely many such ϕ's, and hence the conjunction is equivalent to a finite one. Define χ ,T ,u as this finite conjunction. Theorem 3.7.

1. T , u ↔ ↓ T , u implies T , u ≡ ↓ T , u . The converse also holds when T and T are finitely branching.

T , u ↔

↓ T , u iff T , u ≡ ↓ T , u .
Proof. Item 2 is a direct consequence of Propositions 3.8 and 3.9. The argument for item 1 is similar to the one of the aforementioned propositions, but working with a single Z instead of (Zi) i≤ . For the converse implication, define Z by xZx iff T , x ≡ ↓ T , x . The conjunctions in (1) are then finite because T is finitely branching, and so P is finite (the fact that T is finitely branching is used to show that Zag is satisfied). Proposition 3.10.Let ϕ ∈ (r, s, k)-XPath = . There is ϕ ↑↓ ∈ XPath = in up-down normal form such that 1. ϕ ↑↓ ≡ ϕ;

2. vd(ϕ ↑↓ ) = (r, s); and

3. nd(ϕ ↑↓ ) ≤ k • (r + s + 2).
Proof. The idea is that we can factorize any path in the tree going down and up as a node tests in the expression. Consider for instance the expression α = ↑↓[a]↑↑↓. It is immediate that α is equivalent to the up-down expression [ ↑[ ↓ [a] ] ]↑↑↓, which is in up-down normal form.

We use the following directed equivalences to translate any path expression into an equivalent up-down expression.

εγ ≡ γ (ε) α[ψ1][ψ2]β ≡ α[ψ1 ∧ ψ2]β (merge) α ξ-n↓ • • • ↓ξ-1↓ξ0↑ξ1↑ • • • ↑ξn β ≡ α[ ξ-nξn↓ • • • ↓ξ-1ξ1↓ξ0 ]β (factor ) α ξn↓ξn-1↓ • • • ↓ξ0 ≡ α ↓ n [ ξ0↑ξ1↑ . . . ↑ξn ] (shift-r ) ξ0↑ξ1↑ • • • ↑ξn β ≡ [ ξ0↑ξ1↑ • • • ↑ξn ]↑ n β (shift-l )
In the expressions above, each ξi is the empty string, or of the form ε or [ϕ1][ϕ2] . . . [ϕn], α and β can be any path expression, or the empty string, and γ is any path expression. The idea is that (factor ) converts an expression that goes down n times and then up n times into a node expression, and when doing this, any test done in the i-th node when going down is merged with the (n -i)-th test when going up. For example, Lemma A.2. Let α be an XPath = -path expression with vd(α) = (r, s) and nd(α) = k, Then there is an up-down path expression α ↑↓ such that:

↓[¬a]↓[c]↑[¬b]↑ ≡ [ ↓[¬a][¬b]↓[c] ].
1. α ↑↓ ≡ α 2. vd(α ↑↓ ) = (r, s), and 3. nd(α ↑↓ ) ≤ k + r + s + 1.
Proof. We first apply rule (factor ) as many times as possible. It is clear that if nav(α) is of the form ↑ n ↓ m for some n, m ≥ 0 then rule (factor ) cannot be applied and we are done. Hence, suppose nav(α) contains the pattern ↓↑. Let

α = γ ↑ α1γ ↓ α1 = γ1 ξ 1 -n 1 ↓ . . . ↓ξ 1 0 ↑ . . . ↑ξ 1 n 1 matches (factor ) γ2 ξ 2 -n 2 ↓ . . . ↓ξ 2 0 ↑ . . . ↑ξ 2 n 2 matches (factor ) . . . γm-1 ξ m -nm ↓ . . . ↓ξ m 0 ↑ . . . ↑ξ m nm matches (factor ) γm,
where nav(γ ↑ ), nav(γm) ∈ ↑ * , nav(γ ↓ ), nav(γ1) ∈ ↓ * , and ξ i j are the empty string, ε or [ϕ

i,j 1 ][ϕ i,j 2 ] . . . [ϕ i,j h i,j ]
. Furthermore, assume that m is maximal (i.e., it is impossible to apply (factor ) in any of the γi's) and that the length of each γi is minimal (i.e., it is not the case that nav(γi) ends with ↓ and that nav(γi+1) begins with ↑). Observe that nav(γi) ∈ ↑ * ↓ * . We apply rule (factor ) in the m-1 marked places and obtain

α2 = γ1 [ ξ 1 -n 1 ξ 1 n 1 ↓ • • • ↓ξ 1 -1 ξ 1 1 ↓ξ 1 0 ] (factor ) applied γ2 [ ξ 2 -n 2 ξ 2 n 2 ↓ • • • ↓ξ 2 -1 ξ 2 1 ↓ξ 2 0 ] (factor ) applied
. . .

γm-1 [ ξ m -nm ξ m nm ↓ • • • ↓ξ m -1 ξ m 1 ↓ξ m 0 ] (factor ) applied γm,
Let vd(nav(α1)) = (r1, s1). Since nav(α) = nav(γ ↑ α1γ ↓ ) contains the pattern ↓↑, we have that r1 > 0. It can be shown that vd(γ ↑ α2γ ↑ ) = (r, s), nd(α2) ≤ nd(α1) + 1, and vd(nav(α2)) ≤ (r1 -1, s1). If we repeat this procedure with α2 and so on until we can no longer apply rule (factor ), we end up with an up-down path expression α f so that We can now apply (shift-r ), (shift-l ), (ε) and (merge) to γ ↑ α f γ ↓ in order to obtain an up-down path expression α ↑↓ satisfying the desired conditions:

1. α f ≡ α1, 2. vd(γ ↑ α f γ ↓ ) = (r, s),
1. α ↑↓ ≡ α 2. vd(α ↑↓ ) = (r, s), and

3. nd(α ↑↓ ) ≤ k + r1 + 1 ≤ r + s + 1.
This concludes the proof of Lemma A.2.

Lemma A.3. Let α ↑↓ , β ↑↓ be up-down path expressions and let ϕ = α ↑↓ β ↑↓ (for ∈ {=, =}) with vd(ϕ) = (r, s) and nd(ϕ) = k. Then there is an up-down path expression γ such that:

1. ε γ ↑↓ ≡ ϕ, 2. vd(γ ↑↓ ) = (r, s), and 3. nd(γ ↑↓ ) ≤ k + 1.
Proof. Let us analyse the case where

α ↑↓ = [ψα]↑ nα ↓ mα [τα] β ↑↓ = [ψ β ]↑ n β ↓ m β [τ β ]
(the remaining cases being only simpler), where ψα, ψ β , τα, τ β are in up-down normal form. Suppose, without loss of generality, that nα ≤ n β . Hence, we have . . .

α ↑↓ β ↑↓ ≡ | { z } | { z } n ↵ n m m ↵ | { z } | { z } [ ↵ ] [ ] [⌧ ] [⌧ ↵ ] | { z } | { z } n ↵ m m ↵ n n ↵ | { z } | { z } [⌧ ] [⌧ ↵ ] [ ↵ ^ ] ↵ "# "# ⌘ l
n times x 1,1
x 2,0

x 0,2

T n :

γ ↑↓ = [ψα ∧ ψ β ]↑ nα ↓ mα [τα ∧ ε ↑ mα ↑ n β -nα ↓ m β [τ β ] ].
It is clear that the formulas are equivalent (cf. Figure 10). Moreover, the right-hand formula has at most one more nesting than the left-hand formula, and its vertical depth is at most (r, s). This concludes the proof of Lemma A.3.

By induction on ϕ, and using lemmas A.2 and A.3, one can show that there is ϕ ↑↓ as desired. Proposition 3.11. If r + s ≥ 2 then ≡ r,s has infinite index.

Proof. We show that for every r, s so that r + s = 2 there is an infinite set of non-equivalent formulas {ψ i r,s } i≥0 of vertical depth (r, s). It thus follows that for every r, s so that r + s ≥ 2, ≡ r,s has infinite index.

Consider the following formulas.

ψ 0 1,1 = ε = ↑↓↓ ψ i+1 1,1 = ε = ↑↓[ψ i 1,1 ]↓ ψ 0 0,2 = ↑ = ↑↑↓↓ ψ i+1 0,2 = ↑ = ↑↑↓[ψ i 1,1 ]↓ ψ 0 2,0 = ↓ = ↓↓ ψ i+1 2,0 = ↓ = ↓[ψ i 1,1 ]↓ Note that vd(ψ n
r,s ) = (r, s) and nd(ψ n r,s ) = n for every n. The formula ψ n r,s intuitively says that there is a chain of length n as depicted in Figure 11.

In the data tree Tn of the figure, we have that Tn, xr,s |= ψ n r,s but Tn, xr,s |= ψ n r,s for any n > n. Therefore, {ψ i r,s } i≥0 is an infinite set of non-equivalent formulas of vertical depth (r, s). Proposition 3.12.≡ r,s,k has finite index.

Proof. For any ϕ with nd(ϕ) = k and vd(ϕ) = (r, s), let F (ϕ) = (k, r + s). Define F in a similar way for path expressions α. In this proof "finite" means finite up to logical equivalence. By Proposition 3.10 we can consider only formulas in up-down normal form.

We show that there are finitely many formulas ϕ in updown normal form such that F (ϕ) ≤ (k, t), and that there are finitely many path expressions α in up-down normal form such that F (α) ≤ (k, t). We use induction on the lexicographic ordering of (k, t). Observe that if F (ϕ) = (k, t) then ϕ is a boolean combination of labels and formulas of the form ε = α , ε = α or α , where F (α) ≤ (k, t). Hence it suffices to show the statement for path expressions. If F (α) = (0, t) then α is either ε or ↑ n ↓ m , where n, m ≤ 2t, so there are finitely many of them. If

F (α) = (k + 1, t), then α is [ϕ1]↑ n ↓ m [ϕ2],
where n, m ≤ 2t and nd(ϕi) ≤ k for i = 1, 2. Since F (ϕi) < lex (k + 1, t), by inductive hypothesis there are finitely many such ϕi's, and therefore α's. The argument for item 1 is similar to the one of the aforementioned propositions, but working with a single Z instead of (Z k r,ŝ ) r,ŝ, k . For the converse implication, define Z by xZx iff T , x ≡ T , x . The conjunctions in (2) are then finite because T is finitely branching, and so P is finite (the fact that T is finitely branching is used for showing that Zag is satisfied).

Proposition A.4. T , u ↔ r,s,k•(r+s+2) T , u implies T , u ≡ r,s,k T , u .

Proof. We show that if T , u↔ r,s,k T , u via (Z k r,ŝ ) r+ŝ≤r+s, k≤k then for all n ≤ ŝ and m ≤ r+n, for all ϕ in up-down normal form with vd(ϕ) ≤ (r, ŝ), nd(ϕ) ≤ k, for all upward expression α ↑ in up-down normal form, and for all downward expression α ↓ in up-down normal form with vd(α ↑ ), vd(α ↓ ) ≤ (r, ŝ), nd(α ↑ ), nd(α ↓ ) ≤ k:

1. If xZ k r,ŝ x then T , x |= ϕ iff T , x |= ϕ. 2. If y n →x, y n →x , x Z k-1 r,ŝ x , then (x, y) ∈ [[α ↑ ]] T iff (x , y ) ∈ [[α ↑ ]] T . 3. If y m →z, y m →z , z Z k-1 r ,ŝ z for r = r + n -m, ŝ = ŝ -n + m, then (y, z) ∈ [[α ↓ ]] T iff (y , z ) ∈ [[α ↓ ]]

Fix

as any tautology such that vd( ) = (0, 0), nd( ) = 0. For each (y , z ) ∈ P we define formulas, ϕ y ,z and ψ y ,z , satisfying that vd(ϕ y ,z ) ≤ (r, ŝ), nd(ϕ y ,z ) < k and vd(ψ y ,z ) ≤ (r , ŝ ), nd(ψ y ,z ) < k as follows:

• Suppose (a) holds. Let ϕ y ,z be such that vd(ϕ v ,w ) ≤ (r, ŝ), nd(ϕ v ,w ) < k, and such that T , x |= ϕ y ,z but T , x |= ϕ y ,z ; and let ψ v ,w = .

• Suppose

Since vd(ϕ y ,z ) ≤ (r, ŝ), nd(ϕ y ,z ) < k, by Proposition 3.12, there are finitely many non-equivalent formulas ϕ y ,z . The same applies to formulas ψ y ,z . Hence both infinite conjunctions in (2) are equivalent to finite ones, and therefore without loss of generality we may assume that Φ and Ψ are well-formed formulas. Finally, let

α ↑ = [Φ]↑ n and α ↓ = ↓ m [Ψ]. By construction, vd(α ↑ α ↓ ) ≤ (r, ŝ), nd(α ↑ α ↓ ) ≤ k. Further- more, T , x |= ε = α ↑ α ↓ and T , x |= ε = α ↑ α ↓ , but this contradicts the fact that T , x ≡ r,ŝ, k T , x .
Corollary 3.17. ↔ r,s,k has finite index.

Proof. Immediate from Theorem 3.16 and Proposition 3.12.

B. PROOFS OF SECTION 4

Theorem 4.1.

1. Let † ∈ {↓, }. T , u → † T , u implies T , u † T , u . The converse holds when T is finitely branching.

T , u →

↓ T , u iff T , u ↓ T , u . 3. T , u → r,s,k•(r+s+2) T , u implies T , u r,s,k T , u . 4. T , u r,s,k T , u implies T , u → r,s,k T , u .
Proof. The proofs are straightforward adaptations of the proofs of Propositions 3.8 and 3.9 and Propositions A.4 and A.5 respectively, and are ommitted here. In particular, for the 'if' part, in the adaptation of the proofs of Propositions 3.9 and A.5, the simulations are defined by

xZix iff T , x ↓ i T , x xZ k r,ŝ x iff T , x r,ŝ, k T , x
respectively, and the conditions (a) and (b) on page 5 become now Since every Φ T ,u is finite up to logical equivalence by Proposition 3.12, it follows that Ψ is a valid formula. We show that it defines sim r,s,k (T , u). We prove that ϕ is↔ -invariant over [finite] data-trees, though it is not logically equivalent over [finite] data-trees to any XPath = -formula.

(a) [∃i ∈ {0, . . . , n} ∃ϕ ∈ XPath ↓+ = ] dd(ϕ) ≤ h -i ∧ T , vi |= ϕ ∧ T , v i |= ϕ; or (b) [∃j ∈ {0, . . . , m} ∃ϕ ∈ XPath ↓+ = ] dd(ϕ) ≤ h-j∧T , wj |= ϕ ∧ T , w j |= ϕ, and (a) [∃i ∈ {0, . . . n} ∃ϕ ∈ XPath + = ] vd(ϕ) ≤ (r + i, ŝ -i) ∧ nd(ϕ) ≤ k -1 ∧ T , vi |= ϕ ∧ T , v i
To see that ϕ is ↔ -invariant over [finite] data-trees, take T , u and T , u such that T , u ↔ T , u and T |= ϕ(u). Furthermore, suppose that T , u |= ↑ m ↓ n a for adequate n and m. By Theorem 3.16, T , u |= ↑ n ↓ m a and so T |= ϕ(u ).

Assume by contradiction that there is ψ ∈ XPath = such that T , u |= ψ iff T |= ϕ(u) for all data-tree T and u ∈ T . Suppose vd(ψ) = (r, s) and nd(ψ) = k. Let T be a data tree formed by a chain of length r + 1 starting from the root u with all its nodes containing a label b except the leave, which has label a (the data values are irrelevant). By Proposition 3. We show that ϕ cannot be expressed in XPath ↓,↑,E = . Suppose, by means of contradition, that there is a formula ψ ∈ XPath ↓,↑,E = expressing ϕ, with vd(ψ) = (r, s) (vd(•) for XPath ↓,↑,E = is defined as in Table 2 plus the clause vd(Eϕ) = vd(ϕ)). Let n = r + s, and let T be the chain-like data-tree u0 → u1 → • • • → un such that label (u0) = a, label (un) = b, label (ui) = c for i ∈ {1, . . . n -1} and data(ui) = i for i ∈ {0, . . . , n}. Let T be the chain-like data-tree

u 0 → u 1 → • • • → u n
such that label (u i ) = label (ui) for i ∈ {0, . . . n}, data(u i ) = data(ui) for i ∈ {0, . . . , n -1} and data(u n ) = 0. Note that T |= ϕ(u0) and T |= ϕ(u 0 ). However, one can show that for all i ∈ {0, . . . , n} we have T , ui |= ψ iff T , u i |= ψ. Hence, ψ does not express ϕ and thus ϕ is not expressible in XPath ↓,↑,E = .

E. PROOFS OF SECTION 7

Theorem 7.2. For all , k ≥ 0, i ≥ 1,

≡ ↓ ,0 ≡ ↓ ,1 • • • ≡ ↓ , = ≡ ↓ , +i , and ≡ ↓ ,k ≡ ↓ +i,k .
Proof. Consider the data trees defined in Figure 12 for every k. Note that ≡ ↓ ,k+1 ⊆ ≡ ↓ ,k and ≡ ↓ +1,k ⊆ ≡ ↓ ,k by definition. We show that ≡ ↓ ,k = ≡ ↓ ,k+1 for all ≥ k + 1. For this purpose, we show that

T 1 k , x 1 k ≡ ↓ k+1,k T 1 k , x 1 k but T 1 k , x 1 k ≡ ↓ k+1,k+1 T 1 k , x 1 k . The fact that T 1 k , x 1 k ≡ ↓ k+1,k+1 T 1 k , x 1
k comes from the fact that the property "there is a path of length k + 1 ending with a label a whose every pair of consecutive nodes have distinct data value" is definable with the following formula ϕ k+1 of depth k + 1 and nesting depth k + 1, We now show

ϕ1 = ε = ↓[a] ϕi+1 = ε = ↓[ϕi] for i > 0. Since T 1 k , x
T 1 k , x 1 k ↔ ↓ k+1,k T 1 k , x 1
k . For every j ≤ k + 1, t ≤ k, let Zj,t be the set of all pairs (x, y) ∈ T 1 k × T 1 k so that x and y are some x i k or x i k for i ∈ {1, 2} and k ≥ t.2 Observe that Zj+1,t ⊆ Zj,t for all j, t ≤ k.

(

) 4
We show that (Zj,t) j≤k+1,t≤k verify the bisimulation conditions. We proceed by induction on j + t. The base case, j = t = 0, is trivial. The case l > 0, t = 0 is also straightforward. Suppose then that t > 0. Let (u, u ) ∈ Zj,t. Again, Harmony is met since Z l,t relates only nodes with label a. Let us suppose that u is some x 1 t and u is x 1 t for some t ≤ t, the other cases being similar or simpler. Let us now show Zig. Let v, w be so that x 1 t n →v and x 1 t m →w with n, m ≤ j.

• If v is inside the subtree T 2 t -1 of T 1 t , but it is not x 2 t -1 , then we choose v as the corresponding 3 node inside the subtree T 1 t -1 of T 1 t . Note that data(v) = data(v ) by Observation E.1. Further, since every node of T 1 t -1 is in a Zj,t-1-relation with the corresponding node in T 2 t -1 by construction of Zj,t-1, it follows that ( i →v)Zj,t-1( i →v ) for all i ≤ n. Thus, by (4), ( i →v)Zj-n+i,t-1( i →v ) for all i ≤ n.

• If, on the other hand, v is x 2 t -1 , we choose v as the root of T 2 t -1 , x 2 t -1 . Again, we have that data(v ) = data(v) and by construction that vZj,t-1v . Thus, by (4), vZj-1,t-1v .

• Finally, if v falls outside T 2 t -1 , we choose v as the same node in T 1 t , where of course we will have that data(v) = data(v ) and that ( i →v)Zj,t-1( i →v ) for all i ≤ n. Thus, by ( 4), ( i →v)Zj-n+i,t-1( i →v ) for all i ≤ n.

We do the same with w and w . Since in every case we can reach a node with the same data value and so that the corresponding nodes in the path are Zj,t-1-related, it follows that the Zig condition is satisfied. The Zag condition is only easier, and hence we conclude that T 1 k , x ↔ ↓ k+1,k T k 1 , x for every k.

We therefore have that ≡ ↓ ,k+1

≡ ↓ ,k for all ≥ k + 1. The fact that ≡ ↓ +1,k

≡ ↓

,k is of course trivial, formulas of depth + 1 can express "the tree has at least depth + 1", which cannot be expressed by formulas of depth .

3 Remember that T 1 t -1 and T 2 t -1 are isomorphic modulo a renaming of data values, so by corresponding we mean the node in the same position in the tree It remains to show that ≡ ↓ ,k = ≡ ↓ ,k+1 for all ≤ k. To show this, we prove T , x ↔ ↓ ,k+1 T , x for every T , T so that T , x ↔ ↓ ,k T , x . We prove it by induction on + k. The base case is easy.

For the inductive case, let Zj,t = ↔ ↓ j,t for all j ≤ , t ≤ k. Hence, (Zj,t) j≤ ,t≤k verify the bisimulation conditions. Let Z ,k+1 = {(x, x )}. We show that Z ,k+1 together with (Zj,t) j≤ ,t≤k verifies the bisimulation conditions. Harmony follows from xZ ,k x . We show Zig since Zag is equivalent. With respect to vertical XPath, note that since ≡ r,s,k ⊆ ≡ r ,s ,k for all (r, s, k) ≤ (r , s , k ), as a consequence of Proposition 3.11 we obtain that for every r, s, k with r+s ≥ 2 there is some k > k so that ≡ r,s,k ≡ r,s,k . In fact, we conjecture that ≡ r,s,k ≡ r,s,k+1 for every k. We argue that this can be proven through the models (Tn)n in the proof of Proposition 3.11, by showing that T k , x r ,s ≡ r,s,k T k+1 , x r ,s but T k , x r ,s ≡ r,s,k+1 T k+1 , , x r ,s for every (r, s) ≥ (r , s ). The fact that ≡ r,s,k ≡ r+1,s,k and ≡ r,s,k ≡ r,s+1,k are straightforward. We then obtain the following.

↓ =((

 ↓ XPath= with ↓); XPath = (XPath= with ↓ and ↑); XPath ↓↓ * = XPath= with ↓ and ↓ * ); XPath * =

2 Figure 1 :

 21 Figure 1: A data tree of Trees(A×D) with A = {a, b} and D = N.

1 →→

 1 is the same as →, and 0 is the identity relation. (x n →) denotes the set of all descendants of x at distance n, and ( n →y) denotes the sole ancestor of y at distance n (assuming it has one).

  is either a node expression or a path expression. To save space, we use XPath ↓ = for XPath=(↓); XPath = for XPath=(↓, ↑); XPath ↓↓ * = for XPath=(↓, ↓ * ); and XPath * = for XPath=(↓, ↑, ↓ * , ↑ * ).

  , then [[ ↓ * [ b ∧ ↓[b] = ↓[b] ] ]] T = {x, y, z}, where the formula reads: "there is a descendant node labeled b, with two children labeled b with different data values." For a data tree T and u ∈ T , we write T , u |= ϕ to denote u ∈ [[ϕ]] T , and we say that T , u satisfies ϕ. We say that the formulas ϕ, ψ of XPath= are equivalent (notation: ϕ ≡ ψ) iff [[ϕ]] T = [[ψ]] T for all data trees T . Similarly, path expressions α, β of XPath= are equivalent (notation: α ≡ β) iff [[α]] T = [[β]] T for all data trees T .

  ): If xZx , x n →v and x m →w then there are v , w ∈ T such that x n →v , x m →w and 1. data(v) = data(w) ⇔ data(v ) = data(w ), 2. ( i →v) Z ( i →v ) for all 0 ≤ i < n, and 3. ( i →w) Z ( i →w ) for all 0 ≤ i < m. • Zag: If xZx , x n →v and x m →w then there are v, w ∈ T such that x n →v, x m →w and items 1, 2 and 3 above are verified. For a data tree T and u ∈ T , let T |u denote the subtree of T induced by {v ∈ T | (∃n) u n →v}. Observe that the root of T |u is u. The following results are straightforward consequences of the definition of bisimulation: Proposition 3.3. T , u ↔ ↓ (T |u), u. Proposition 3.4. If T is a subtree of T and u ∈ T then T , u ↔ ↓ T , u.

  ∧ ψ) = max{dd(ϕ), dd(ψ)} dd(¬ϕ) = dd(ϕ) dd( α ) = dd(α) dd( α β ) = max{dd(α), dd(β)} dd(λ) = 0 dd(εα) = dd(α) dd([ϕ]α) = max{dd(ϕ), dd(α)} dd(↓α) = 1 + dd(α) Downward depth vd(a) = (0, 0) vd(ϕ ∧ ψ) = max{vd(ϕ), vd(ψ)} vd(¬ϕ) = vd(ϕ) vd( α ) = vd(α) vd( α β ) = max{vd(α), vd(β)} vd(λ) = (0, 0) vd(εα) = vd(α) vd([ϕ]α) = max{vd(ϕ), vd(α)} vd(↓α) = max{(0, 0), vd(α) + (1, -1)} vd(↑α) = max{(0, 0), vd(α) + (-1, 1)}

)

Figure 2 :•, x m →w and 1 .

 21 Figure 2: Zig clause of bisimulation for XPath ↓ = .

For a data

  tree T and u ∈ T , let T | u denote the subtree of T induced by {v ∈ T | (∃n ≤ ) u n →v}. Proposition 3.6. T , u ↔ ↓ (T | u), u.

  show 1 and 2 by induction on |ϕ| + |α|. Let us see item 1. The base case is ϕ = a for some a ∈ A. By Harmony, label (x) = label (x ) and then T , x |= ϕ iff T , x |= ϕ. The Boolean cases for ϕ are straightforward. Suppose ϕ = α = β . We show T , x |= ϕ ⇒ T , x |= ϕ, so assume T , x |= ϕ. Suppose there are v, w ∈ T and n, m ≤ j such that x n →v, x m →w, (x, v) ∈ [[α]] T , (x, w) ∈ [[β]] T and data(v) = data(w). By Zig, there are v , w ∈ T such that x n →v , x m →w , ( i →v) Zj-n+i ( i →v ) for all 0 ≤ i ≤ n, ( i →w) Zj-m+i ( i →w ) for all 0 ≤ i ≤ m, and data(v ) = data(w ). By inductive hypothesis 2 (twice), (x , v ) ∈ [[α]] T and (x , w ) ∈ [[β]] T . Hence T , x |= ϕ. The implication T , x |= ϕ ⇒ T , x |= ϕ is analogous. The case ϕ = α = β is shown similarly. The case ϕ = α is similar (and simpler) to the previous case. Let us now analyze item 2. We only show the 'only if' direction. The base case is when α ∈ {ε, ↓}. If α = ε then v = x and so n = 0. Since v = x , we conclude (x , v ) ∈ [[α]] T . If α =↓ then x→v in T , and so n = 1. Since x →v , we have (x , v ) ∈ [[α]] T .

  ): If xZx , y n →x and y m →z then there are y , z ∈ T such that y n →x , y m →z , data(z) = data(x) ⇔ data(z ) = data(x ), and zZz . • Zag: If xZx , y n →x and y m →z then there are y, z ∈ T such that y n →x, y m →z, data(z) = data(x) ⇔ data(z ) = data(x ), and zZz .

Figure 3 :

 3 Figure 3: Zig clause of bisimulation for XPath =

n →v and x m

 x →w then there are v , w ∈ T such that x n →v , x m →w and 1. data(v) = data(w) ⇒ data(v ) = data(w ), 2. ( i →v) Z ( i →v ) for all 0 ≤ i < n, and 3. ( i →w) Z ( i →w ) for all 0 ≤ i < m. u ∈ T is similar to u ∈ T for XPath = (notation: T , u → T , u ) iff there is a relation Z ⊆ T × T such that uZu and for all x ∈ T and x ∈ T we have • Harmony: If xZx then label (x) = label (x ). • Zig: If xZx , y n →x and y m →z then there are y , z ∈ T such that y n →x , y m →z , zZz , and if data(z) = data(x) then data(z ) = data(x ).

Theorem 4

 4

=

  and XPath * = respectively, and let ↓↓ * and * be the logical implication for XPath ↓↓ * + = and XPath * + = respectively. Theorem 5.1. Let † ∈ {↓↓ * , * }.

Figure 4 :

 4 Figure 4: Definition of T , u and T , u .

( a )

 a T , u ↔ ↓ T , u, (b) T , u ↔ ↓ (T | u), u, and (c) T , u ≡q T , u .

Lemma 6 . 7 .

 67 The FO(σ)-formula(∃y, z) [y ≈ z ∧ Pa(y) ∧ P b (z)]is ↔ -invariant though not logically equivalent over [finite] data-trees to any XPath E = -formula.

  Define ≡ ↓,k as the equivalence ≡ ↓ restricted to formulas of nesting depth at most k, that is, T , u ≡ ↓ ,k T , u iff for all ϕ ∈ XPath↓ = such that dd(ϕ) ≤ and nd(ϕ) ≤ k we have T , u |= ϕ iff T , u |= ϕ. Define a more fine-grained notion of bisimulation in a similar way. We say that u ∈ T and u ∈ T are ( , k)-bisimilar for XPath↓ = (notation: T , u↔ ↓ ,k T , u ) if there is a family of relations (Zj,t) j≤ ,t≤k in T × T such that uZ ,k u and for all j ≤ , t ≤ k, x ∈ T and x T we have • Harmony: If xZj,tx then label (x) = label (x ). • Zig: If xZj,tx , x n →v and x m →w with n, m ≤ j then there are v , w ∈ T such that x n

n →v and x m

 x →w with n, m ≤ j then there are v, w ∈ T such that x n →v, x m →w and items 1, 2 and 3 above are verified.

Figure 5 :

 5 Figure 5: Hierarchy of XPath ↓ = .

Proposition 7 . 3 .

 73 XPath * = is closed under subtree replication, i.e. if T is a subtree replication of T , and u ∈ T then T , u ≡ * T , u.

Finally, we will

  use bisimulation to show the expressivity limits of different fragments of XPath. Let key(a) be the property stating that every node with label a has a different data value. Let fk(a, b) (for foreign key) be the property (∀x)[Pa(x) ⇒ (∃y)[P b (y) ∧ x ∼ y]]. Proposition 7.4. 1. key(a) is not expressible in XPath * = . 2. fk(a, b) is expressible in XPath * = but it is not expressible in XPath ↓↓ * = or XPath * + =

  (a, b) is expressible with the formula ¬ ↑ * ↓ * [a ∧ ¬ ε = ↑ * ↓ * [b] ] . However, this property cannot be expressed in XPath ↓↓ * = because models T and T in Figure 8 are bisimilar for XPath ↓ = via Z, depicted as dotted lines. Since T , x satisfies fk(a, b) but T , x does not, from Theorem 5.1 it follows that fk(a, b) is not expressible in XPath ↓↓ * = . Finally, suppose there exists ψ ∈ XPath * + = expressing fk(a, b). Since T is a substructure of T we have T , x → T , x by Lemma 4.2. By Theorem 5.1(2) and the fact that T , x |= ψ, we have T , x |= ψ, which is a contradiction. Let dist3(x) be the property stating that there are nodes y, z so that x→y→z and x, y, z have pairwise distinct data values. Proposition 7.5.

Figure 7 :

 7 Figure 7: key(a) not in XPath * = .

Figure 8 :

 8 Figure 8: fk(a, b) not in XPath ↓↓ * = .

k

  →v) |= ϕ and T , ( k →v ) |= ϕ. Proof. Let x = v0→v1→ • • • →vn = v and x = v 0 →v 1 → • • • →v n = v . We proceed by induction on |α|. If α = ε then x = v and so n = 0. Hence x = v and (x , v ) ∈ [[α]] T , which contradicts the hypothesis, and thus the statement is trivially true. If α =↓ then x→v and so n = 1. Hence x →v and (x , v ) ∈ [[α]] T . This case is also trivial. The case α = ↓ * is similar. Suppose α = [ψ]. Since (x , v ) / ∈ [[α]] T , we have x = v and T , v |= ψ. Taking k = 0 and ϕ = ψ the statement holds. Observe that ψ is a subformula of α.

  On the other hand, (shift-r ) and (shift-l ) group all the node tests in the lowest node in the expression, making use of the fact that the parent relation is functional. Thus, for example [a]↓[b]↓ ≡ ↓↓[ ↑[b]↑[a] ] and ↑[a]↑[b] ≡ [ ↑[a]↑[b] ]↑↑. It is thus clear that the left and right expressions above are semantically equivalent.

and 3 .

 3 nd(α f ) ≤ nd(α1) + r1.

Figure 10 :

 10 Figure 10: Normal form for data tests.

Figure 11 :

 11 Figure 11: Model verifying ψ jfor all i ≥ n and not verifying ϕ l for no l < n. Dotted lines represent equal data values.

Corollary 3 .

 3 [START_REF] Gottlob | Efficient algorithms for processing XPath queries[END_REF]. {T , u | T , u ≡ r,s,k T , u } is definable by an (r, s, k)-XPath = -formula.Proof. Similar to the proof of Corollary 3.2. Theorem 3.16. 1. T , u ↔ T , u implies T , u ≡ T , u . The converse also holds when T and T are finitely branching. 2. T , u ↔ r,s,k•(r+s+2) T , u implies T , u ≡ r,s,k T , u . 3. T , u ≡ r,s,k T , u implies T , u ↔ r,s,k T , u . Proof. Items 2 and 3 are shown in Propositions A.4 and A.5.

  T .Hence, by Proposition 3.10, the main statement follows. We simultaneously show 1, 2 and 3 by induction on |ϕ| + |α ↑ | + |α ↓ |. Let us see item 1. The base case is ϕ = a for some a ∈ A. By Harmony, label (x) = label (x ) and then T , x |= ϕ iff T , x |= ϕ. The boolean cases for ϕ are straightforward. Suppose ϕ = ε = α ↑ α ↓ . We show T , x |= ϕ ⇒ T , x |= ϕ, so assume T , x |= ϕ. Suppose there are y, z ∈ T and n ≤ ŝ, m ≤ r + n such that y n →x, y m →z, (x, y) ∈ [[α ↑ ]] T , (y, z) ∈ [[α ↓ ]] T and data(x) = data(z). By Zig, there are y , z ∈ T such that zZ k-1 r ,ŝ z for r = r + n -m, ŝ = ŝ -n + m, and data(x ) = data(z ). By inductive hypothesis 2 and 3, (x , y ) ∈ [[α ↑ ]] T and (y , z ) ∈ [[α ↓ ]] T . Hence T , x |= ϕ. The implication T , x |= ϕ ⇒ T , x |= ϕ is analogous. The cases ϕ = ε = α ↑↓ , and ϕ = ε α ↑ , ϕ = ε α ↓ ( ∈ {=, =}) and ϕ = α (for α in up-down normal form) are shown in a similar way. The cases ϕ = ε ε ( ∈ {=, =}) are trivial. Let us now analyze item 2. Let α ↑ = [ψ]↑ n (n ≥ 0), and let x0, . . . , xn ∈ T and x 0 , . . . , x n ∈ T be such thaty = x0→x1→ • • • →xn = x in T , y = x 0 →x 1 → • • • →x n = x in T ,and xZ k-1 r,ŝ x . By Observation 3.14, we have x0Z k-1 r ,ŝ x 0 , for r = r+n, ŝ = ŝ-n. Assume by contradiction that (x , y) / ∈ [[α ↑ ]] T . This necessarily means that T , x0 |= ψ but T , x 0 |= ψ. But ψ is a subformula of α ↑ , nd(ψ) ≤ k -1and nd(ψ) ≤ (r , ŝ ) and this contradicts inductive hypothesis 1. Item 3 is shown in a similar way. Let α ↓ = ↓ m [ψ] (m ≥ 0), and let z0, . . . , zm ∈ T and z 0 , . . . , z m ∈ T be such thaty = z0→z1→ • • • →zm = z in T , y = z 0 →z 1 → • • • →z m = z in T ,and zZ k-1 r ,ŝ z . Assume by contradiction that (y , z) / ∈ [[α ↓ ]] T . This necessarily means that T , xm |= ψ but T , x m |= ψ.But ψ is a subformula of α ↓ , nd(ψ) ≤ k -1 and nd(ψ) ≤ (r , ŝ ) and this contradicts inductive hypothesis 1.Proposition A.5. T , u ≡ r,s,k T , u implies T , u ↔ r,s,k T , u . Proof. Fix u ∈ T and u ∈ T such that T , u ≡ r,s,k T , u . Define (Z k r,ŝ ) r+ŝ≤r+s, k≤k by xZ k r,ŝ x iff T , x ≡ r,ŝ, k T , x .We show that Z k r,s is a (r, s, k)-bisimulation between T , u and T , u . By hypothesis, uZ k r,s u . Now fix r + ŝ ≤ r + s, k ≤ k. By construction, Z k r,ŝ satisfies Harmony. Let us see that Z k r,ŝ satisfies Zig (the case for Zag is analogous). Suppose xZ k r,ŝ x ,y = x0→x1→ • • • →vn = x in T , y = z0→z1→ • • • →zm = z in T ,and data(x) = data(z) (the case data(x) = data(z) is shown in a similar way), where m ≤ r + n. Let P ⊆ T 2 be defined byP = {(y , z ) | y n →x ∧ y m →z ∧ data(x ) = data(z )}. Since T , x ≡ r,s,k T , x , vd( ε = ↑ n ↓ m ) ≤ (r, s), nd( ε = ↑ n ↓ m ) = 0, and T , x |= ε = ↑ n ↓ m, we conclude that P = ∅. We next show that there exists (y , z ) ∈ P such that i.y = x 0 →x 1 → • • • →x n = x in T ii. y = z 0 →z 1 → • • • →z m = z in T , iii. T , x ≡ r,ŝ, k-1 T , x, and iv. T , z ≡ r ,ŝ , k-1 T , z , where r = r + n -m, ŝ = ŝ -n + m, and hence, by inductive hypothesis, Zig is satisfied by Z k r,ŝ . By way of contradiction, assume that for all (y , z ) ∈ P satisfying i and ii we have either (a) T , x ≡ r,ŝ, k-1 T , x ; or (b) T , z ≡ r ,ŝ , k-1 T , z for r = r + n -m, ŝ = ŝ -n + m.

  (a) does not hold. Then (b) holds. Let ψ y ,z be such that vd(ψ y ,z ) ≤ (r , ŝ ), nd(ψ y ,z ) < k and such that T , z |= ψ y ,z but T , z |= ψ y ,z ; and let ϕ y ,z = . Let Φ = (y ,z )∈P ϕ y ,z and Ψ = (y ,z )∈P ψ y ,z .

  |= ϕ; or (b) [∃j ∈ {0, . . . m} ∃ϕ ∈ XPath + = ] vd(ϕ) ≤ (r + j , ŝ -j ) for j = n-m+j ∧nd(ϕ) ≤ k-1∧T , wj |= ϕ∧T , w j |= ϕ respectively. Lemma B.1.(1) {T , u | T , u → ↓ T , u } is definable by an XPath ↓+ =formula χ +,u,T of downward depth ≤ .(2) {T , u | T , u → r,s,k T , u } is definable by an XPath + =formula χ + r,s,k,u,T of vertical depth ≤ (r, s) and nesting depth ≤ k.Proof. For item (2), let sim r,s,k (T , u) = {T , u | T , u → r,s,k T , u }. Let Φ T ,u be the set of all positive formulas ϕ ∈ XPath + = of vertical depth at most (r, s) and nesting depth at most k so that T , u |= ϕ. Let Ψ be Ψ = T ,u ∈sim r,s,k (T ,u) Φ T ,u .

  Let T , u ∈ sim r,s,k(T , u). Then, T , u |= Φ T ,u and thus T , u |= Ψ. If on the other hand T , u |= Ψ we have that T , u |= Φ T ,u for some T , u ∈ sim r,s,k (T , u) and then T , u ≡ r,s,k T , u . By Theorem 3.16-3 we then have that T , u ↔ r,s,k T , u , and in particular T , u → r,s,k

  15 we have T , u ↔ r,s,k (T | s r u), u. Since T , u |= ψ, by Theorem 3.16, we have (T | s r u), u |= ψ, and so T | s r u |= ϕ(u). This last fact is a contradiction because no node of T | s r u is labeled with a.Proposition 6.6.Let k = k •(r +s+2). If ϕ(x) ∈ FO(σ) is ↔ r,s,k -invariant over [finite] data-trees, then there is ψ ∈ (r, s, k)-XPath = such that Trx(ψ) is logically equivalent to ϕ over [finite] data-trees.Proof. By Corollary 3.13, for every data tree T and u ∈ T there is an (r, s, k)-XPath = formula χ r,s,k,T ,u such that T , u ≡ r,s,k T , u iff T , u |= χ r,s,k,T ,u . Let ψ = T |=ϕ(u) χ r,s,k,T ,u .As χ r,s,k,T ,u ∈ (r, s, k)-XPath = and, by Proposition 3.12, ≡ r,s,k has finite index, it follows that ψ is equivalent to a finite disjunction. The proof that ϕ(x) ≡ Trx(ψ) is similar to Proposition B.3, as we show next. Let us see that ϕ |= Trx(ψ). Suppose T |= ϕ(u). Since T , u |= χ r,s,k,T ,a , we have T , u |= ψ and so T |= Trx(ψ)(u). Let us see that Trx(ψ) |= ϕ. Assume T |= Trx(ψ)(u), and so T , u |= ψ. Then there exists T , u such that T |= ϕ(u ) and T , u |= χ r,s,k,T ,u . By the property of χ r,s,k,T ,u , we have T , u ≡ r,s,k T , u and since ϕ is↔ ↓ r,s,k•(r+s+2) -invariant (and hence ≡ ↓ r,s,k -invariant by Theorem 3.16-2) we conclude T |= ϕ(u). Lemma 6.7.The FO(σ)-formula (∃y, z) [y ≈ z ∧ Pa(y) ∧ P b (z)] is ↔ -invariant though not logically equivalent over [finite] data-trees to any XPath E = -formula. Proof. Let ϕ(x) be the FO(σ)-formula for there are two nodes with same data value and labels a and b respectively, i.e., ϕ(x) = (∃y, z) [y ≈ z ∧ Pa(y) ∧ P b (z)].

2 nFigure 12 :

 212 Figure 12: Definition of data trees T i n , T i n (n ≥ 0, i ∈ {1, 2}) for proof of Theorem 7.2.

Suppose x n →v, x m

 x →w with n, m ≤ . Then, since Z ,k verifies Zig, there are x n →v , x m →w where (1) data(v) = data(w ) iff data(v ) = data(w ),(2)( i →v)Z -n+i,k-1 ( i →v ) for all i ∈ {0, . . . , n -1}, and(3)( i →w)Z -m+i,k-1 ( i →w ) for all i ∈ {0, . . . , m -1}.Since ≤ k, then -n+i ≤ k-1. Further, -n+i+k < +k, which means that we can apply the inductive hypothesis. Hence, by inductive hypothesis, T , ( i →v)↔ ↓ -n+i,k T , ( Zig condition for ↔ ↓ ,k+1 is verified. The Zag condition holds by symmetry.

Table 1 :

 1 Semantics of XPath= for a data tree T .

Table 2 :

 2 Definitions of downward depth, vertical depth and nesting depth. (a ∈ A, ∈ {=, =}, '+' and 'max' are performed component-wise, α is any path expression or the empty string λ.)

  1 k |= ϕ k+1 but T 1 k , x 1 k |= ϕ k+1 , it follows that (resp. T 1 k and T 2 k ) are equal modulo renaming of data values, so we are also showing that the roots of any two data trees with subindex k are (k + 1, k)-bisimilar. Observation E.1. Note that the set of immediate subtrees of the roots of T 1 k , T 1 k , T 2 k , T 2 k are the same as those of T 1 k , T 2 k , T 2 k (and of T 1 k , T 1 k , T 2 k ) by construction.

	T 1 k , x 1 k ≡ ↓ k+1,k+1 T 1 k , x 1 k .
	To show T 1 k , x 1 k ≡ ↓ k+1,k T 1 k , x 1 k we actually use Proposi-
	tion 7.1 and show T 1 k , x 1 k ↔ ↓ k+1,k T 1 k , x 1 k . Note that T 1 k and
	T 2 k

Note that this proposition holds only for paths expressions without union.

Note that x i k or x i k do not necessarily uniquely identify one node, but many possible. The intended meaning is that x, y can be any of them.

* This work was partially supported by grant ANPCyT-PICT-2010-688, ANPCyT-PICT-2011-0365, UBACyT 20020110100025 and the FP7-PEOPLE-2011-IRSES Project "Mobility between Europe and Argentina applying Logics to Systems" (MEALS) and the Laboratoire International Associé "INFINIS".

APPENDIX A. PROOFS OF SECTION 3

Given a path expression α, the navigation of α (notation: nav(α)) is the string of {↑, ↓} * that results from removing all node expressions [ψ] and ε from α. For example, nav (

3. If ϕ ∈ XPath = is → r,s,k -invariant then it is equivalent to a formula of (r, s, k)-XPath + = .

4. If ϕ ∈ XPath = is equivalent to a formula of (r, s, k)-

Proof. We start with item (1), for the case of → ↓ . The 'if' part is straightforward from Theorem 4.1-2, and here we focus on the 'only if' part. Let ϕ be preserved under → ↓ . Let {(Ti, ui)} i≤n be the set of all pointed models of ϕ modulo ↔ ↓ (which is finite due to Theorem 3.7-2 together with Proposition 3.1). We claim that

On the one hand, if T , u |= ϕ then there is i ≤ n such that Ti, ui ↔ ↓ T , u, and so Ti, ui → ↓ T , u. On the other hand, suppose Ti, ui

For the case of → ↓ of item (1), the 'if' direction follows from Theorem 4.1-1. For the 'only if' direction, let ϕ be preserved under → ↓ . It is easy to see that ϕ is preserved under → ↓ iff it is preserved under → ↓ dd (ϕ) . We can then apply the same reasoning as before and the statement follows.

Item (3) follows the same argument as item (1) but this time using Corollary 3.17 and Lemma B.1-(2).

Item (4) is straightforward from Theorem 4.1-3. Item (2) follows from items (3) and ( 4) and the observation that ϕ is preserved under → iff it is preserved under → r,s,k•(r+s+2) for vd(ϕ) = (r, s) and nd(ϕ

D. PROOFS OF SECTION 6

Proposition 6.1.For any XPath = -[resp. XPath ↓ = -] path expression α there is an equivalent XPath = -[resp. XPath ↓ = -] path expression α in simple normal form. Further, α can be computed in polynomial time from α.

Proof. The translation is straightforward, given the following equivalences:

where denotes any fixed tautology, for example a ∨ ¬a, for some a ∈ A. Proof. Let ϕ(x) be the FO(σ)-formula for there is a node labeled a in the tree, i.e., ϕ(x) = (∃y) Pa (y).

Claim E.2. ≡ r,s,k ≡ r ,s ,k for all (r, s, k) < (r , s , k ), r + s ≥ 2.