Diego Figueira
email: diego.figueira@labri.fr

Santiago Figueira
email: santiago@dc.uba.ar

Carlos Areces
email: carlos.areces@gmail.com

Model Theory of XPath on Data Trees. Part I: Bisimulation and Characterization

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.

1. Two pointed data trees are 'equivalent' when they are 'indistinguishable' by the formulas of a given logic.

We adopted the terminology of the literature, and so we used the first word, and not he second. The reader should not confuse this notion with that of 'equivalent' formulas.

Introduction

We study the expressive power and model theory of XPath-arguably 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 reasoning 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 Document Type Definitions (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 the work of [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 the works of [START_REF] Figueira | Reasoning on Words and Trees with Data[END_REF] and [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.

In this article we focus on the basic model theory tool of bisimulations, which defines the structural conditions necessary for ensuring that two models coincide in all the properties expressible by a logic. Whereas the basic notion of bisimulation was introduced for the basic modal logic, one can find adequate notions of bisimulations for different logics, in the sense that they capture the notion of indistiguishability of the logic. The challenge here is to find adequate notions of bisimulation for logics such as XPath, whose navigation is akin to modal logics such as PDL, but which can also test for equality of data values in the data tree.

Contribution: XPath = can navigate the data tree by means of axes like 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 ↓); XPath = (↑↓) (XPath = with ↓ and ↑); XPath = (↓↓ * ) (XPath = with ↓ and ↓ * ); XPath = (↓↑↓ * ↑ * ) (XPath = with ↓, ↑, ↓ * and ↑ * ); and its positive fragments. Our main contributions can be summarized as follows:

• In §3 we introduce bisimulation notions for XPath = (↓), XPath = (↓↓ * ), XPath = (↓ * ), XPath = (↑↓), XPath = (↓↑↓ * ↑ * ) and show that they precisely characterize the logical equivalence relation of the corresponding logic. We also consider fine grained versions of these bisimulations indexed by two measures of formula complexity. The first measure of formula complexity consists on the maximum number of nested axes in a formula, which we call downward depth in the case of XPath = (↓) and vertical depth in the case of XPath = (↑↓). The second one is the number of nested subformulas, called nesting depth.

The notion of bisimulation for XPath = (↑↓) relies on a normal form which we also introduce. Basically, this normal form restricts the navigation of the expressions to be very simple: either going downward or going upward and then downward. Similar normal forms for langauges on trees are folklore, and our work here consists mainly in adapting them to the setup of tests for data values.

We also 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 §4 we characterize XPath = (↓) as the fragment of first-order 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 as we show in a counter-example. However, a weaker result can still be established, namely that if a first-order formula is bisimulation-invariant, for the bisimulation notion corresponding to any fixed number of nested axes, then it is equivalent to an XPath = (↑↓) formula.

• Using bisimulations we show some (non)expressivity results about XPath = in §5. We show, for example, that formulas of XPath = (↓) with nesting depth n+1 and downward depth d have more expressive power than those of nesting and downward depth n and d respectively, as long as n < d.

• 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 [START_REF] Van Benthem | Modal Correspondence Theory[END_REF] in the context of modal correspondence theory, by [START_REF] Milner | A Calculus of Communicating Systems[END_REF] and [START_REF] Park | Concurrency and automata on infinite sequences[END_REF] in concurrency theory, and by [START_REF] Forti | Set theory with free construction principles[END_REF] in non-wellfounded set theory (for a historical outlook see the work of [START_REF] Sangiorgi | On the origins of bisimulation and coinduction[END_REF]. 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. XPath has been known to be closely connected to known modal languages, such as PDL and modal µ-calculus, depending on the fragments taken into account (ten Cate, Fontaine, & Litak, 2010). However, the fragments studied hitherto are "data unaware", that is, allowing to express of the structure of the model as well of the fixed set of labels.

To the best of our knowledge the present is the first work on bisimulations and invariance with logics with data tests.

Bisimulations can also be used to obtain model theoretic characterizations that identifies the expressive power of a logic L 1 in terms of the bisimulation invariant fragment of a logic L 2 which, hopefully, is better understood. The challenge, here, is to pinpoint both the appropriate notion of bisimulation required and the adequate 'framework' logic L 2 . 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 [START_REF] Rosen | Modal logic over finite structures[END_REF]. The proof was then simplified and unified by Otto (2004a[START_REF] Otto | Bisimulation invariance and finite models[END_REF], and later expanded by [START_REF] Dawar | Modal characterisation theorems over special classes of frames[END_REF] to other classes of structures. Other formalisms of different expressive power have also been considered for querying data trees, such as first-order logic with two variables [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF], tree patterns [START_REF] David | Complexity of data tree patterns over XML documents[END_REF][START_REF] Figueira | Pattern logics and auxiliary relations[END_REF], register automata [START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF], µ-calculus with registers [START_REF] Jurdziński | Alternating automata on data trees and xpath satisfiability[END_REF], or datalog programs [START_REF] Abiteboul | Recursive queries on trees and data trees[END_REF]. In the absence of data values, logics for semi-structured databases can often be seen as modal logics. In fact, structural characterizations for XPath without equality test were studied in the work of [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 = .

The first significant result concerning an algorithmic solution to the bisimulation problem for the basic modal logic was given by [START_REF] Hopcroft | An nlog(n) algorithm for minimizing states in a finite automaton[END_REF], with a polynomial time algorithm for state minimization in a deterministic finite automaton. This problem is equivalent to determine a coarsest partition of a set that is stable with respect to a finite set of functions. [START_REF] Paige | Three partition refinement algorithms[END_REF] solved the problem for the more general case, where the restriction of stability concerns a finite set of relations. [START_REF] Kanellakis | CCS expressions, finite state processes, and three problems of equivalence[END_REF] are the first to recognize that the algorithm of Paige and Tarjan can be used to determine the maximum bisimulation for the basic modal logic in an arbitrary graph. Hence it can be decided in polynomial time whether two nodes in finite models are bisimilar for the basic modal logic -though the length of the actual formulas which distinguish two non-bisimilar nodes cannot be polynomially bounded with respect to the size of the models [START_REF] Figueira | On the size of shortest modal descriptions[END_REF]. In our case, deciding whether two nodes in finite data trees are bisimilar can also be solved in polynomial time.

A preliminary version of the present paper appeared in a work of [START_REF] Figueira | Basic model theory of XPath on data trees[END_REF]. Also, there is a continuation (a 'Part II'): a work by [START_REF] Abriola | Model theory of XPath on data trees. Part II: Binary bisimulation and definability[END_REF], after the preliminary version by [START_REF] Abriola | Definability for downward and vertical XPath on data trees[END_REF], where they address further model theoretical questions such as definability and separation, and bisimulation notions for pairs of nodes (instead of single nodes) to capture the idea of "indistinguishability by means of path expressions" (instead of node expressions).

Preliminaries

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 λ for the empty string.

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, Let P be a property on nodes of data trees. When property P is true at node u of data tree T , we say that (T , u) satisfies P . For any binary relation R over nodes 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:

α, β ::= o | αβ | α ∪ β | [ϕ] o ∈ O ∪ {ε} ϕ, ψ ::= a | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | α | α = β | α = β a ∈ A A formula of XPath = (O)
is either a node expression or a path expression. We formally define the semantics of XPath = as follows, for T a data tree:

[[↓]] T = {(x, y) | x→y} [[↓ * ]] T = reflexive transitive closure of [[↓]] T [[↑]] T = {(x, y) | y→x} [[↑ * ]] T = reflexive transitive closure of [[↑]] T [[ε]] T = {(x, x) | x ∈ T } [[αβ]] T = {(x, z) | (∃y ∈ T ) (x, y) ∈ [[α]] T , (y, z) ∈ [[β]] T } [[α ∪ β]] T = [[α]] T ∪ [[β]] T [[[ϕ]]] T = {(x, x) | x ∈ [[ϕ]] T } [[a]] T = {x ∈ T | label (x) = a} [[¬ϕ]] T = T \ [[ϕ]] T [[ϕ ∧ ψ]] T = [[ϕ]] T ∩ [[ψ]] T [[ α ]] T = {x ∈ T | (∃y ∈ T ) (x, y) ∈ [[α]] T } [[ α = β ]] T = {x ∈ T | (∃y,z ∈ T )(x, y) ∈ [[α]] T , (x, z) ∈ [[β]] T , data(y) = data(z)} [[ α = β ]] T = {x ∈ T | (∃y,z ∈ T )(x, y) ∈ [[α]] T , (x, z) ∈ [[β]] T , data(y) = data(z)}
As an example, if T is the data tree shown in Figure 1, then

[[ ↓ * [ b ∧ ↓[b] = ↓[b] ] ]] T = {x, y, z},
and 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 say that T , u is a pointed data tree, we write T , u |= ϕ to denote u ∈ [[ϕ]] T , and we say that T , u satisfies ϕ. We say that the node expressions ϕ, ψ 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 .
The fragment of downward XPath is denoted XPath = (↓) and vertical XPath is denoted XPath = (↑↓).

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 maximum number of nested axes or the maximum 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. In the sequel we will see that in some situations also expressions of the form [ψ] can be sometimes avoided ( §3.2.1), although not when we only have downward axes (Lemma 10).

Translating to First-Order Logic

In this section we show that there is a truth-preserving translation from XPath = (↑↓) to first-order logic over an appropriate signature. To do so, we first must interpret data trees into relational structures, and we do this in the most standard way: using a binary 'child' relation, an equivalence relation for testing data equality, and monadic relations to test for labels. Fix the signature σ with binary relations and ≈, and a unary predicate P a 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 can now give the translation from XPath to first-order logic over σ. The tranlsation function is indexed by the free variables of the formula produced -one for node expressions, and two for path expressions. Proposition 1.

Tr x (a) = P a (x) (a ∈ A) Tr x (ϕ † ψ) = Tr x (ϕ) † Tr x (ψ) ( † ∈ {∧, ∨}) Tr x (¬ϕ) = ¬Tr x (ϕ) Tr x ( α ) = (∃y)Tr x,y (α) (y a new variable) Tr x ( α = β ) = (∃y)(∃z) y ≈ z ∧ Tr x,y (α) ∧ Tr x,z (β) (y, z new variables) Tr x ( α = β ) = (∃y)(∃z) y ≈ z ∧ Tr x,y (α) ∧ Tr x,z (β)
1. If ϕ is an XPath = (↑↓) node expression, then u ∈ [[ϕ]] T iff T |= Tr x (ϕ)(u). 2. If α is an XPath = (↑↓) path expression, then (u, v) ∈ [[α]] T iff T |= Tr x,y (α)(u, v).
Proof. The proof is by structural induction on ϕ and α.

For ϕ ∈ FO(σ), let qr(ϕ) be its quantifier rank, i.e., the depth of nesting of its quantifiers. Observe that for ∈ {=, =} we have

Bisimulation

In this section we define notions of bisimulation for the downward and vertical fragments of XPath, and we show that they coincide with the corresponding logical equivalence relation. For the case of vertical XPath the bisimulation notion relies on a normal form which we introduce for this purpose.

Downward XPath

We write dd(ϕ) to denote the downward depth of ϕ defined as follows:

dd(a) = 0 dd(λ) = 0 dd(ϕ ∧ ψ) = max{dd(ϕ), dd(ψ)} dd(εα) = dd(α) dd(¬ϕ) = dd(ϕ) dd([ϕ]α) = max{dd(ϕ), dd(α)} dd( α ) = dd(α) dd(↓α) = 1 + dd(α) dd( α β ) = max{dd(α), dd(β)}
where a ∈ A, ∈ {=, =}, and α is any path expression or the empty string λ. 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 node expression ϕ ∈ 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 node expression ϕ ∈ -XPath = (↓), we have T , u |= ϕ iff T , u |= ϕ. 1 We will first show that, for every , there are finitely many different formulas ϕ of dd(ϕ) ≤ up to logical equivalence. Formally, this is usually referred by saying that ≡ ↓ has finite index. Proposition 2. ≡ ↓ has finite index.

Proof. It can be easily shown by induction that for any node expression ϕ ∈ -XPath = (↓) with unnecessary uses of ε (recall that αεβ ≡ αβ) we have that qr(Tr x (ϕ)) is bounded. It is a well-known result of first order that there are finitely many nonequivalent formulas of bounded quantifier rank. Hence there are finitely many nonequivalent node expressions of bounded downward depth.

Corollary 3. {T , u | T , u ≡ ↓ T , u } is definable by a node expression χ ,T ,u of - XPath = (↓).
Proof. Consider the conjunction of all -XPath = (↓) formulas ϕ such that T , u |= ϕ. By Proposition 2, 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.

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 ) if there is a relation Z ⊆ T × T such that uZu and for all x ∈ T and x ∈ T we have This bisimulation generalizes the classical bisimulation relation [START_REF] Sangiorgi | On the origins of bisimulation and coinduction[END_REF], in which the Zig is simply: If xZx , x→v, there is v such that x →v and vZv (the Zag being symmetrical). In fact, if we restrict our Zig condition to having n = m = 1 and v = w, and the Zag condition to n = m = 1 and v = w , we obtain a relation that corresponds, precisely, to the classical bisimulation relation. Thus, being bisimilar for the notion we define implies being bisimlar for the classical notion.

For example, the dotted lines in the following two data trees represent a bisimulation for XPath = (↓).

T T 0 $ # x x 0 y 1 y 2 y 0 v v 0 w 0 w
This notion of bisimulation can be seen, as usual, as an Ehrenfeucht-Fraïssé game, where Spoiler tries to find a difference (through the logic's glasses) between nodes u and u , while Duplicator tries to copy him, showing that u and u are indistinguishable. To gain intuition on our notion of bisimulation, we will briefly explain its associated game (without going into the technical details). The board consists of the data trees T and T , and there are two pebbles p and p , so that all along the game, p will always be over a node of T , and p will always be over a node of T . Initially, p is over u, and p is over u . If u and u do not satisfy the same label then Spoiler is declared winner and the game finishes. The game proceeds by rounds. Suppose that at some round, the pebbles p and p are in positions x and x satisfying the same label. A round consists of one move of Spoiler, followed by an answer by Duplicator, and a final decision made by spoiler.

• Step 1. Spoiler's first move: he chooses a pebble, two integers n and m, and two paths, one of length m and the other of length n. These paths start in x if he chose p or in x if he chose p . Suppose the chose p (the case for p is analogous but over data tree T instead of T ). His first path is represented by some w ∈ T such that x m →w, and his second path is represented by some v ∈ T such that x n →v.

• Step 2. Duplicator's answer: he shows two paths in T (or in T in case duplicator had chosen p instead of p), one of length m and the other of length n, both starting on x , such that data(u) = data(v) iff data(u ) = data(v ). If there are no such paths, then Spoiler is declared the winner and the game finishes. If now the pebbles are over two nodes which satisfy the same label, the game proceeds. Else, Spoiler is declared the winner and the game finishes.

Duplicator wins if spoiler is never declared winner in a game at infinitely many rounds. The resemblance of the game rules with Harmony, Zig and Zag is evident. One can see that spoiler has a winning strategy in the game whose initial pebbles are placed over x and x if and only if T , u↔ ↓ T , u .

It is interesting to compare this game to the one for capturing bisimulation for the basic modal logic. In the latter, Spoiler just chooses a successor of x (or x ) following the accessibility relation. This is also the case for Core-XPath or PDL. But in our case, because of adding comparison of data values, Spoiler has to choose a whole path (in fact, two paths), making the game 'less local' that the one for the basic modal logic (or Core-XPath or PDL). An analogous view for the game of XPath = (↓) would be to allow Spoiler to build his paths in a step-by-step fashion, that is, extending the paths constructed so far with a new single node, thus giving Duplicator less certainty. Is it possible to change the rules of the game so that in the second step of the round Spoiler builds his paths in a step-by-step fashion? No. Even if Spoiler has the freedom to extend step-by-step only one of his paths, this would be too unfair for Duplicator. Indeed, consider our last example of bisimilar T , x and T , x . Spoiler would initially declare that his first path will be x of length 0, and so Duplicator can only define his first path to be x of length 0. Then Spoiler will construct, step-by-step, his second path. Initially he shows the path x →y to Duplicator. Duplicator has two possible answers: either the path x→y 1 or x→y 2 . Suppose the chooses x→y 1 (the case for x→y 2 is analogous). Now Spoiler extends his path x →y to x →y →w . Since y 1 has only one child, Spoiler has one possible answer for extending his own path: x→y 1 →v. Next, Spoiler declares that he is done: he has constructed two paths starting in x , one is of length 0 and the other one is x →y →w , of length 2. Duplicator has constructed one path of length 0 and the other as x→y 1 →v. Duplicator looses, as data(x ) = data(w ) but data(x) = data(v). This example shows that the game fairness is established when spoiler tells duplicator in advance which are the two paths he chooses.

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:

Observation 4. T , u ↔ ↓ (T |u), u. Observation 5. If T is a subtree of T and u ∈ T then T , u ↔ ↓ T , u.
We say that u ∈ T and u ∈ T are -bisimilar for XPath = (↓) (notation: T , u ↔ ↓ T , u ) if there is a family of relations (Z j ) j≤ in T × T such that uZ u and for all j ≤ , x ∈ T and x ∈ T we have This notion of -bisimulation corresponds to the game between spoiler and duplicator at rounds.

• Harmony: If xZ j x then label (x) = label (x ).
Clearly if T , u↔ ↓ T , u then T , u↔ ↓ T , u for all .

Observation 6. Suppose T and T have height at most , u ∈ T , and u ∈ T . Then

T , u ↔ ↓ T , u iff T , u ↔ ↓ T , u .
For a data tree T and u ∈ T , let T | u denote the subtree of

T induced by {v ∈ T | (∃n ≤ ) u n →v}. Observation 7. T , u ↔ ↓ (T | u), u.

Equivalence and Bisimulation

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

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 .
The above theorem will be shown as a consequence of Propositions 9 and 11:

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

1. If xZ j x 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 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) Z j-n+i ( i →v ) for all 0 ≤ i ≤ n, ( i →w) Z j-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 .
For the inductive step, let x 0 , . . . , x n ∈ T and x 0 , . . . , x n ∈ T be such that

x = x 0 →x 1 →x 2 → • • • →x n = v in T , x = x 0 →x 1 →x 2 → • • • →x n = v in T ,
and

x i Z j-i x 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 |= ϕ as the next Lemma shows.

Lemma 10. Let α be a path expression of XPath = (↓↓ * ). Let x n →v and

x n →v such that (x, v) ∈ [[α]] T and (x , v ) / ∈ [[α]] T .
Then there is a subformula ϕ of α and k ∈ {0, . . . , n} such that T , (

k →v) |= ϕ and T , ( k →v ) |= ϕ. Proof of Lemma. Let x = v 0 →v 1 → • • • →v n = 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 α.

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.

But this contradicts the inductive hypothesis 1.

Proposition 11. T , u ≡ ↓ T , u implies T , u ↔ ↓ T , u . Proof. Fix u ∈ T and u ∈ T such that T , u ≡ ↓ T , u . Define (Z i ) i≤ by xZ i x 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 = v 0 →v 1 → • • • →v n = v in T , x = w 0 →w 1 → • • • →w m = 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 , v i ≡ ↓ h-i T , v i , and iv. (∀j ∈ {0, . . . , m}) T , w j ≡ ↓ 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 , v i ≡ ↓ h-i T , v i , or (b) (∃j ∈ {0, . . . , m}) T , w j ≡ ↓ h-j T , w j . Figueira, Figueira, & Areces
Fix as any tautology such that dd( ) = 0. For each (v , w ) ∈ P we define two families of node expressions,

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

• Assume (a) and that i is the smallest number such that

T , v i ≡ ↓ h-i T , v i . Let ϕ i v ,w be such that dd(ϕ i v ,w ) ≤ h -i and T , v i |= ϕ 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 (a) does not hold. Then (b) holds. Let j be the smallest number such that T , w j ≡ ↓ h-j T , w j . Let ψ j v ,w be such that dd(ψ j v ,w ) ≤ hj and T , w j |= ψ 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)
However these conjunctions could be potentially infinite the if trees are infinitely branching. Since dd(ϕ i v ,w ) ≤ hi, by Proposition 2 there are finitely many non-equivalent node expressions ϕ i v ,w and 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. It is clear that by construction (x, v) ∈ [[α]] T and (x, w) ∈ [[β]
] T , and therefore T , x |= α = β . We see next that T , x |= α = β . This contradicts T , x ≡ ↓ h T , x , and hence we are done. Suppose that T , x |= α = β . Then there is (v , w

) ∈ P such that (x , v ) ∈ [[α]] T and (x , w ) ∈ [[β]] T .
In particular, i and ii are true, and then either (a) or (b) hold. In the first case, we have, by construction, that (

x , v ) / ∈ [[α]] T , and in the second it is clear that (x , w ) / ∈ [[β]] T .
In either case, we arrive to a contradiction.

Proof of Theorem 8. Item 2 is a direct consequence of Propositions 9 and 11.

The left-to-right argument for item 1 can be seen as a consequence of item 2. Indeed, T , u ↔ ↓ T , u implies T , u ↔ ↓ T , u for all , which by item 2 implies T , u ≡ ↓ T , u for all , which in turn entails T , u ≡ ↓ T , u .

The right-to-left argument for item 1 is similar to that of Proposition 11, but defining 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).

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 (notation: vd(ϕ)). The nesting depth of a formula ϕ (notation: nd(ϕ)) is the maximum number of nested [ ] appearing in ϕ.

vd(a) = (0, 0) vd(λ) = (0, 0) vd(ϕ ∧ ψ) = max{vd(ϕ), vd(ψ)} vd(εα) = vd(α) vd(¬ϕ) = vd(ϕ) vd([ϕ]α) = max{vd(ϕ), vd(α)} vd( α ) = vd(α) vd(↓α) = max{(0, 0), vd(α) + (1, -1)} vd( α β ) = max{vd(α), vd(β)} vd(↑α) = max{(0, 0), vd(α) + (-1, 1)} nd(a) = 0 nd(αβ) = max{nd(α), nd(β)} nd(ϕ ∧ ψ) = max{nd(ϕ), nd(ψ)} nd(ε) = 0 nd(¬ϕ) = nd(ϕ) nd([ϕ]) = 1 + nd(ϕ) nd( α ) = nd(α) nd(↓) = 0 nd( α β ) = max{nd(α), nd(β)} nd(↑) = 0
where, a ∈ A, ∈ {=, =}, '+' and 'max' are performed component-wise, and α is any path expression or the empty string λ. Let (r, s, k)-XPath = (↑↓) be the set of formulas ϕ in XPath = (↑↓) with vd(ϕ) ≤ (r, s) and nd(ϕ) ≤ k. Let T , u and T , u be pointed data trees. 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 = (↑↓) (notation: T , x ≡ ↓↑ r,s T , x [resp. T , x ≡ ↓↑ r,s,k T , x ]) if they satisfy the same node expressions ϕ of XPath = (↑↓) so that vd(ϕ) ≤ (r, s) [resp. vd(ϕ) ≤ (r, s) and nd(ϕ) ≤ k].

Normal Form

We define a normal form for XPath = (↑↓) that will be implicitly used in the definition of bisimulation in this 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. upward] if it is of the form ↓ n [ϕ] [resp. [ϕ]↑ n ]
for some n > 0 with ϕ ∈ XPath = (↑↓). For example, ↓[ ↑ ] is a downward expression 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 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 ∈ {=, =}. Next, we show that for every XPath = (↑↓) formula there is an equivalent one in up-down normal form. Of course, the idea of replacing child axes with parent axes is by no means novel, and there have been a number of works on rewriting expressions into equivalent ones to improve performance or streamability, such as the works of [START_REF] Olteanu | Forward node-selecting queries over trees[END_REF] and [START_REF] Olteanu | XPath: Looking forward[END_REF]. However, these rewrite systems aim at removing backward axes (parent, ancestor, etc) maintaining equivalence at the root, different to our end, which is to maintain equivalence of path expressions over any pair of nodes. Further, we doubt our normal form can be useful in such scenarios since from a computational or streamability perspective the resulting formula in up-down normal from seems more complex. Although being more 'regular', it has more nested modalities and introduces parent axes, as it will be shown later. Our motivation for this normal form is to simplify the defintion of bisimulation by means of rendering the formula as simple as possible in form.

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

(↓[ ↑ ]↓[ ↓ = ↑ ]↑[b]) = ↓↓↑.
Proposition 12. Let ϕ ∈ (r, s, k)-XPath = (↑↓), then there is ϕ ↑↓ ∈ XPath = (↑↓) in up-down normal form such that the following hold

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 test 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 it is 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 (ni)-th test when going up. For example,

↓[¬a]↓[c]↑[¬b]↑ ≡ ↓↑ [ ↓[¬a][¬b]↓[c]
]. 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.

The following lemma treats the case of path expressions:

Lemma 13. Let α be an XPath = (↑↓)-path expression 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 + r + s + 1.
Proof of Lemma. 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 )) = (r 1 , s 1 ). Since nav(α) = nav(γ ↑ α 1 γ ↓ ) contains the pattern ↓↑, we have that r 1 > 0. It can be shown that vd(γ ↑ α 2 γ ↓ ) = (r, s), nd(α 2 ) ≤ nd(α 1 ) + 1, and vd(nav(α 2 )) ≤ (r 1 -1, s 1 ). 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 1. α f ≡ ↓↑ α 1 , 2. vd(γ ↑ α f γ ↓ ) = (r, s), and 3. nd(α f ) ≤ nd(α 1 ) + r 1 .

After applying (ε) and (merge) to γ ↑ α f γ ↓ as many times as possible, we obtain an equivalent α , of the same vertical and nesting depth as γ ↑ α f γ ↓ , of the form

α = χ 1 ↑χ 2 ↑ . . . ↑χ n ↓χ n+1 ↓χ n+2 ↓ . . . ↓χ n+m ,
where χ i is a (possibly empty) string of the form [ϕ

1 i ] . . . [ϕ n i i ].
We apply (shift-l ) and (shift-r ) to α to obtain an equivalent α of the same vertical depth (i.e. vd(α ) = vd(α ) = (r, s)) and of nesting depth equal to nd(α ) + 1 of the form

α ↑↓ = χ ↑ n ↓ m χ ,
where χ and χ are the empty string or of the form [ϕ]. Observe that nd(α ↑↓ ) = nd(α ) + 1 ≤ k + r 1 + 1 ≤ r + s + 1, and so α ↑↓ satisfies all requirements of the lemma. This concludes the proof of Lemma 13.

The following lemma treats the case of data tests: Lemma 14. 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 of Lemma. Let us analyse the case where

α ↑↓ = [ψ α ]↑ nα ↓ mα [τ α ] and β ↑↓ = [ψ β ]↑ n β ↓ m β [τ β ],
where n α + m α > 0, n β + m β > 0, and ψ α , ψ β , τ α , τ β are in up-down normal form (the remaining cases where α ↑↓ = ε or β ↑↓ = ε being simpler). Suppose, without loss of generality, that n α ≤ n β .

Hence, we have α ↑↓ β ↑↓ ≡ ↓↑ γ ↑↓ , where

γ ↑↓ = [ψ α ∧ ψ β ]↑ nα ↓ mα [τ α ∧ ε ↑ mα ↑ n β -nα ↓ m β [τ β ] ].
It is clear that the formulas are equivalent (cf. the picture below).

| { z } | { z } n ↵ n m m ↵ | { z } | { z } [ ↵ ] [ ] [⌧ ] [⌧ ↵ ] | { z } | { z } n ↵ m m ↵ n n ↵ | { z } | { z } [⌧ ] [⌧ ↵ ] [ ↵ ^ ] ↵ "# "# ⌘ l
Moreover, the right-hand formula has at most one more nesting than the lefthand formula, and its vertical depth is at most (r, s). This concludes the proof of Lemma 14.

By induction on ϕ, and using Lemmas 13 and 14, one can show that there is ϕ ↑↓ as desired.

Finite Index

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

Proposition 15. 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 {ψ i r,s } i≥0 of non-equivalent node expressions with 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 2.

In the data tree T n of the figure, we have that T n , x r,s |= ψ n r,s but T n , x r,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).

In the proof of the above proposition 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.

. . .

n times x 1,1 x 2,0 x 0,2
T n : Proof. Same argument as in the proof of Proposition 2.

Corollary 17. {T , u | T , u ≡ ↓↑ r,s,k T , u } is definable by a node expression of (r, s, k)- XPath = (↑↓).
Proof. Similar to the proof of Corollary 3.

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 The above definitions heavily rely on the normal form of Proposition 12. In fact, the normal form is not strictly necessary for giving a notion of bisimulation for the vertical fragment. For the case of the downward fragment, no normal form was used, as every path expression is essentially a repetition of node test and 'child' relation. On the contrary, for the case of the vertical fragment, the use of a normal form would be very beneficial. A notion of bisimulation not taking into account the existence of normal form would have a rule Zig of the form: If If xZx and n 1 , . . . , n k , m 1 , . . . , m k , ñ1 , . . . , ñk and m1 , . . . , mk are such that

• v i 1 → . . . →v i n i in T and w i 1 → . . . →w i m i in T for i ∈ {1, . . . , k},
• ṽi 1 → . . . →ṽ i ñi in T and wi 1 → . . . → wi mi in T for i ∈ {1, . . . , k},

• v i 1 = w i 1 and ṽi 1 = wi 1 • w i m i = v i+1 n i+1 and wi mi = ṽi+1 ñi+1 • x = v 1 n 1 and x = ṽ1 ñ1
then there are v i 1 , . . . , v i n i in T , w i 1 , . . . , w i m i for i ∈ {1, . . . , k}, and ṽ i 1 , . . . , ṽ i ñi , w i 1 , . . . , w i mi in T for i ∈ {1, . . . , k} such that

• v i 1 → . . . →v i n i in T and w i 1 → . . . →w i m i in T , • ṽ i 1 → . . . →ṽ i ñi in T and w i 1 → . . . → w i mi in T , • v i 1 = w i 1 and ṽ i 1 = w i 1 • w i m i = v i+1 n i+1 and w i mi = ṽ i+1 ñi+1 • x = v 1 n 1 and x = ṽ 1 ñ1 • v i j Zv i j , w i j Zw i j , ṽi j Z ṽ i j , wi j Z w i j and • data(w k n k ) = data( wk n k ) iff data(w k n k ) = data( w k n k )
Intuitively, this definition establishes that for every paths p and p going up and down, many times in T , there has to be a similar paths p and p in T , going up and down many times, and respecting the 'shape' of p and p respectively such that the j-th node of p is connected to the j-the node of p via Z, and the same for the nodes along p, and such that the data values of the last node of p and p in T are equal if and only if the data values of the last nodes of p and p are so. This definition is the 'natural' extension of the downward bisimulation, but of considering downward paths, it considers more general ones. As it happens with the downward bisimulation, every intermediate node of T in both paths have to be related with the corresponding node in T . As one can immediately see, this definition is quite long and checks too many conditions. Working with normal forms allow us to get a much simpler definition of bisimulation, which has two main advantages: a) there is only one path in each data tree, and b) we do not require intermediate nodes to be related by Z. These two features are direct consequences of the up-down normal form, as the normal form a) only compares values against the root (so there is only one non-empty path expression in each 'diamond' node expression) and b) it only make tests at the beginning and at the end of each path expressions (but not in intermediate nodes). However, notice that due to the normal form both definitions denote the same bisimulation relation.

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. Observation 19. T , u ↔ ↓↑ r,s,k (T | s r u), u.

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 20.

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

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 .
The above theorem will be shown as a consequence of the following Propositions 21 and 22.

Proposition 21. 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 ) ∈ [[α ↓ ]] T .
Hence, by Proposition 12, 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 T , z , where r = r + nm, ŝ = ŝ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 ≡ ↓↑ k-1 T , x ; or (b) T , z ≡ ↓↑ r ,ŝ , k-1 T , z for r = r + n -m, ŝ = ŝ -n + m.

Fix

as any tautology such that vd( ) = (0, 0), nd( ) = 0. For each (y , z ) ∈ P we define node expressions, ϕ 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 (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 . (2)
Since vd(ϕ y ,z ) ≤ (r, ŝ), nd(ϕ y ,z ) < k, by Proposition 16, there are finitely many nonequivalent 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. Furthermore, T , x |= ε = α ↑ α ↓ and T , x |= ε = α ↑ α ↓ , but this contradicts the fact that T , x ≡ ↓↑ r,ŝ, k T , x .
Proof of Theorem 20. Items 2 and 3 are shown in Propositions 21 and 22.

The left-to-right argument for item 1 can be seen as a consequence of item 2. Indeed, T , u↔ ↓↑ T , u implies T , u↔ ↓↑ (r,s) T , u for all r, s, which by item 2 implies T , u ≡ ↓↑ (r,s) T , u for all r, s, which in turn entalis T , u ≡ ↓↑ T , u .

The right-to-left argument for item 1 is similar to that of Proposition 22, 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).

Corollary 23. ↔ ↓↑ r,s,k has finite index. Proof. Immediate from Theorem 20 and Proposition 16.

Simulation

In this section we define notions of directed (non-symmetric) simulations for XPath = (↓) and XPath = (↑↓), as it is done, e.g., in the works of [START_REF] Kurtonina | Simulating without negation[END_REF] or [START_REF] Lutz | Description logic tboxes: Model-theoretic characterizations and rewritability[END_REF] for some modal logics. We obtain results similar to Theorems 8 and 20 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 ).
(∀ϕ ∈ 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 24.

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 9 and 11 and Propositions 21 and 22 respectively, and are ommitted here. In particular, for the 'if' part, in the adaptation of the proofs of Propositions 11 and 22, the simulations are defined by

xZ i x 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 13 become now

(a) [∃i ∈ {0, . . . , n} ∃ϕ ∈ XPath = (↓) + ] dd(ϕ) ≤ h -i ∧ T , v i |= ϕ ∧ T , v i |= ϕ; or (b) [∃j ∈ {0, . . . , m} ∃ϕ ∈ XPath = (↓) + ] dd(ϕ) ≤ h -j ∧ T , w j |= ϕ ∧ T , w j |= ϕ, and
(a) [∃i ∈ {0, . . . n} ∃ϕ ∈ XPath = (↓↑) + ] vd(ϕ) ≤ (r + i, ŝ -i) ∧ nd(ϕ) ≤ k -1 ∧ T , v i |= ϕ ∧ T , v i |= ϕ; or (b) [∃j ∈ {0, . . . m} ∃ϕ ∈ XPath = (↓↑) + ] vd(ϕ) ≤ (r + j , ŝ -j ) for j = n -m + j ∧nd(ϕ) ≤ k -1 ∧ T , w j |= ϕ ∧ T , w j |= ϕ respectively.
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 25. If T is a substructure of T and u ∈ T then T , u → ↓↑ T , u .

Lemma 26.

(1) {T , u | T , u → ↓ T , u } is definable by a node expression χ + ,u,T of XPath = (↓) + with downward depth ≤ .

(2) {T , u | T , u → ↓↑ r,s,k T , u } is definable by a node expression χ + r,s,k,u,T of XPath = (↓↑) + with 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 node expressions ϕ ∈ 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 .

Transitive Axes

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 also the reflexivetransitive closure of the axes which are present. Intuitively, this occurs because ↓ * is an infinite union of compositions of ↓, and similarly for ↑. Hence the notions of bisimulations for XPath = (↓↓ * ) and XPath = (↓↑↓ * ↑ * ) (denoted ↔ ↓↓ * and ↔ ↓↑↓ * ↑ * respectively) coincide with ↔ ↓ and ↔ ↓↑ , respectively. Let ≡ ↓↓ * and ≡ ↓↑↓ * ↑ * be the logical equivalence relation for the fragments XPath = (↓↓ * ) and XPath = (↓↑↓ * ↑ * ) respectively, and let ↓↓ * and ↓↑↓ * ↑ * be the logical implication for XPath = (↓↓ * ) + and XPath = (↓↑↓ * ↑ * ) + respectively.

Theorem 28. Let † ∈ {↓↓ * , ↓↑↓ * ↑ * }.
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.

Proof. The proof that T , u↔ ↓ T , u ⇒ T , u ≡ ↓↓ * T , u follows from a simple adaptation of Proposition 9 to the logic XPath = (↓↓ * ) and Lemma 10. The fact that for finitely branching,

T , u ≡ ↓↓ * T , u ⇒ T , u ↔ ↓ T , u is straightforward from Theorem 8-1 since ≡ ↓↓ * ⊆ ≡ ↓ .
The cases for XPath = (↓↑↓ * ↑ * ), XPath = (↓↓ * ) and XPath = (↓↑↓ * ↑ * ) + are analogous.

It is not hard to see that the adequate notion of (bi)simulation of any other 'intermediate' fragment between XPath = (↑↓) and XPath = (↓↑↓ * ↑ * ) -such as XPath = (↓↑↓ * ) and XPath = (↓↑↑ * )-also corresponds to that of XPath = (↑↓) in the sense of the statement above.

On the other hand, if we restrict formulas to have only transitive axes, we obtain that the notion of bisimulation for XPath = (↓ * ) has a coarser bisimulation notion, as we define next.

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 As before, one can define -bisimilarity for XPath = (↓ * ), notated T , u ↔ ↓ * T , u , and also the notions of equivalence ≡ ↓ * and ≡ ↓ * as expected.

• Harmony: If xZx then label (x) = label (x ). • Zig: If xZx and there are x * →v 1 * → • • • * →v n , and x * →w 1 * → • • • * →w m in T then there are x * →v 1 * → • • • * →v n , and x * →w 1 * → • • • * →w m in T such that 1. data(v n ) = data(w m ) ⇔ data(v n ) = data(w m ), 2. v i Z v i for all 1 ≤ i ≤ n,
These notions of bisimulation coincide with the corresponding logical equivalences:

Theorem 29.

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

T , u ↔

↓ * T , u iff T , u ≡ ↓ * T , u .
For the case of XPath = (↓ * ↑ * ) it is not obvious how to adapt the bisimulation of vertical XPath, since the normal form results does not hold for XPath = (↓ * ↑ * ).

Characterization

In Section 4.1 we characterize XPath = (↓) as the fragment of first-order logic ↔ ↓ -invariant over data trees. In Section 4.2 we show that this result fails for XPath = (↑↓) in general, but a weaker result holds: Any first-order formula ↔ ↓↑ r,s,k -invariant for some r, s, k is equivalent to a XPath = (↑↓) formula.

Downward XPath

Recall that a data tree T and u ∈ T , let T | u denote the subtree of T induced by {v ∈ T | (∃n ≤ ) u n →v}. Any data tree can be regarded as a σ-structure, as explained in §2.1. An FO(σ)-formula ϕ(x) is -local if for all data trees T and u ∈ T , we have T |= ϕ(u) ⇔ T | u |= ϕ(u). Recall that ϕ ∈ FO(σ), qr(ϕ) is the quantifier rank of ϕ.

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

Theorem 30 (Characterization). Let ϕ(x) ∈ FO(σ). The following are equivalent:

1. ϕ is ↔ ↓ -invariant over [finite] data-trees;
2. ϕ is logically equivalent over [finite] data-trees to a node expression of -XPath = (↓), where = 2 qr(ϕ) -1.

The proof of this theorem, whose proof is afterwards, will be a consequence of the following three propositions:

Proposition 31. Any ↔ ↓ -invariant ϕ(x) ∈ FO(σ) over [finite] data-trees is -local for = 2 qr(ϕ) -1.
Proof. We follow the proof by Otto (2004a). 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 (a) T , u ↔ ↓ T , u, (b) T , u ↔ ↓ (T | u), u, and (c) T , u ≡ q T , u . Indeed, from the above conditions it follows that

T |= ϕ(u) iff T |= ϕ(u ) ((a) and ↔ ↓ -invariance of ϕ) iff T |= ϕ(u ) (c) iff (T | u) |= ϕ(u), ( (b
) and ↔ ↓ -invariance of ϕ)

and hence ϕ is -local. By Observation 4 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. Consider the structures T and T in the diagram below,

| {z } q copies ⌘ q u 0 u 00 | {z } q copies | {z } q copies | {z } q copies
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 Observation 5, 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 as the one used in the paper by Otto (2004a).

Proposition 32. Any ↔ ↓ -invariant ϕ(x) ∈ FO(σ) over [finite] data-trees that is -local, is ↔ ↓ -invariant. Proof. Let ϕ(x) be -local and ↔ ↓ -invariant. Suppose T , u ↔ ↓ T , u and T |= ϕ(u). By -locality, T | u |= ϕ(u). Now T , u↔ ↓ T , u iff (T | u), u↔ ↓ (T | u ), u (Obs. 7) iff (T | u), u↔ ↓ (T | u ), u . (Obs. 6) By ↔ ↓ -invariance, T | u |= ϕ(u )
and by -locality again, T |= ϕ(u ).

Proposition 33. If ϕ(x) ∈ FO(σ) is ↔ ↓ -invariant over [finite] data-trees, then there is ψ ∈ -XPath = (↓) such that Tr x (ψ) is logically equivalent to ϕ over [finite] data-trees.
Proof. By Corollary 3, for every data tree T and u ∈ T there is a node expression χ ,T ,u of -XPath = (↓) such that T , u ≡ ↓ T , u iff T , u |= χ ,T ,u . Let

ψ = T |=ϕ(u) χ ,T ,u .
Since χ ,T ,u ∈ -XPath = (↓) and, by Proposition 2, ≡ ↓ has finite index, it follows that ψ is equivalent to a finite disjunction. We now show that ϕ ≡ Tr x (ψ). Let us see that ϕ |= Tr x (ψ). Suppose T |= ϕ(u). Since T , u |= χ ,T ,u , we have T , u |= ψ and so T |= Tr x (ψ)(u). Let us now see that Tr x (ψ) |= ϕ. Assume T |= Tr x (ψ)(u), and so T , u |= ψ. Then there exists T , u such that T |= ϕ(u ) and T , u |= χ ,T ,u . By the property of χ ,T ,u , we have T , u ≡ ↓ T , u and since ϕ is ↔ ↓ -invariant (and hence ≡ ↓ -invariant by Theorem 8-2) we conclude T |= ϕ(u).

Proof of theorem 30. The implication 2 ⇒ 1 follows straightforwardly from Theorem 8. The proof of 1 ⇒ 2 is as follows: First, we show that any ↔ ↓ -invariant ϕ(x) ∈ FO(σ) is -local for = 2 qr(ϕ) -1 (Proposition 31). Then, we prove that any ↔ ↓ -invariant ϕ(x) ∈ FO(σ) that is -local is ↔ ↓ -invariant (see Proposition 32 below). Finally, we show that any FO(σ)definable property which is ↔ ↓ -invariant is definable in -XPath = (↓) (see Proposition 33 below).

Vertical XPath

The analog of Theorem 30 fails for XPath = (↑↓).

This basically because the property p(x) ="the tree where x belongs contains a label a" is ↔ ↓↑ -invariant while it is not expressible in XPath = (↑↓). Notice that, however, p is not ↔ ↓ -invariant. This is as expected, since otherwise p would be expressed by a XPath = (↓) formula. Indeed, consider two data trees with only two nodes, the root and a leaf, labeled respectively a, b in one tree, and b, b in the other tree. Note that the leafs of these trees are ↔ ↓ -bisimilar although they don't coincide in the property p.

Lemma 34. The FO(σ)-formula (∃x) P a (x) is ↔ ↓↑ -invariant though not logically equivalent over [finite] data-trees to any node expression of XPath = (↑↓).

Proof. Let ϕ(x) be the FO(σ)-formula for there is a node labeled a in the tree, i.e., ϕ(x) = (∃y) P a (y). We prove that ϕ is↔ ↓↑ -invariant over [finite] data-trees, though it is not logically equivalent over [finite] data-trees to any node expression of XPath = (↑↓).

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 20, 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 Observation 19 we have T , u ↔ ↓↑ r,s,k (T | s r u), u. Since T , u |= ψ, by Theorem 20, 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.

Hence XPath = (↑↓) is not the fragment of FO(σ) which is↔ ↓↑ -invariant over [finite] datatrees. However, the following analog of Proposition 33 (needed for the proof of Theorem 30) still holds for the case of XPath = (↑↓): For any r, s, k, every first-order formula ↔ ↓↑ r,s,kinvariant is equivalent to a XPath = (↑↓) formula. Notice that the counterexample in Lemma 34 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 30 fails. Formally, consider the logic XPath = ( E), which results from adding the operator E to XPath = (↑↓) with the following semantics:

Proposition 35. Let k = k • (r + s + 2). If ϕ(x) ∈ FO(σ) is ↔ ↓↑ r,
[[Eϕ]] T = T if [[ϕ]] T = ∅, and [[Eϕ]] T = ∅ otherwise.
The following lemma shows a counterexample to the analog of Theorem 30, showing that XPath = ( E) is not the fragment of FO(σ) ↔ ↓↑ -invariant over [finite] data-trees.

Lemma 36. The FO(σ)-formula (∃y, z) [y ≈ z ∧ P a (y) ∧ P b (z)] is ↔ ↓↑ -invariant though not logically equivalent over [finite] data-trees to any node expression of XPath = ( E).

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 ∧P a (y)∧P b (z)]. We show that ϕ cannot be expressed in XPath = (↓, ↑, E). Suppose, by means of contradiction, that there is a node expression ψ ∈ XPath = (↓, ↑, E) expressing ϕ, with vd(ψ) = (r, s) (vd(•) for XPath = (↓, ↑, E) is defined as before together with the clause vd(Eϕ) = vd(ϕ)). Let n = r + s, and let T be the chain-like data-tree

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

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.

Safe Operations on Models

Bisimulations can also be used to show that certain operations on models preserve truth. Such operations are usually called safe for a given logic, as they can be applied to a model without changing the truth values of any formula in the language. Observation 4, 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 3 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 T x 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 v x is the corresponding node of T x . Nodes v and v x have the same label and data value, and the position of v in T |x coincides with the position of v x in T x .

↔

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

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

Non-expressivity Results

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)[P a (x) ⇒ (∃y)[P b (y) ∧ x ≈ y]].

Proposition 38.

1. key(a) is not expressible in XPath = (↓↑↓ * ↑ * ).

fk(a, b) is expressible in XPath

= (↓↑↓ * ↑ * ) but it is not expressible in XPath = (↓↓ * ) or XPath = (↓↑↓ * ↑ * ) + .
Proof. The first item follows from Proposition 37. Since the logic is closed under subtree replication, the trees below are equivalent.

a, 1 a, 2 a, 2 a, 2 a, 1 x x 0 $ l
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(a, b) is expressible with the formula

¬ ↑ * ↓ * [a ∧ ¬ ε = ↑ * ↓ * [b]
] . However, this property cannot be expressed in XPath = (↓↓ * ) because the models T and T below are bisimilar for XPath = (↓) via Z, depicted as dotted lines.

↔ ↓ a, 1 a, 2 b, 1 b, 2 x x T T c, 0 a, 1 a, 2 b, 1 b, 2 c, 0 a, 3
Since T , x satisfies fk(a, b) but T x does not, from Theorem 28 it follows that fk(a, b) is not expressible in XPath = (↓↓ * ).

suppose there exists ψ ∈ XPath = (↓↑↓ * ↑ * ) + expressing fk(a, b). Since T is a substructure of T we have T , x → ↓↑ T , x by Lemma 25. By Theorem 28(2) and the fact that T , x |= ψ, we have T , x |= ψ, which is a contradiction.

Let dist 3 (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 39.

1. dist 3 is expressible in XPath = (↑↓); 2. dist 3 is not expressible in XPath = (↓↓ * ); 3. neither dist 3 nor its complement can be expressed in XPath = (↓↑↓ * ↑ * ) + . Proof. For 1, one can check that T , x |= ϕ iff T , x satisfies dist 3 , for

ϕ = ε = ↓↓[ ε = ↑[ ε = ↑ ] ] .
Let us see 2. Consider the data trees T , x and T , x depicted below. It is straightforward that T , x satisfies dist 3 and T , x does not.

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 $ #
Let v 1 and v 2 be the leaves of T and let v be the only node of T 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) is the height of y, i.e., the distance from y to the root of the corresponding (Z is depicted as dotted lines in picture above). Since T , x satisfies dist 3 but T , x does not, from Theorem 28 it follows that dist 3 is not expressible in XPath = (↓↓ * ).

For 3, one can verify that T , x → ↓↑ T , x via Z as defined above. If dist 3 were definable in XPath = (↓↑↓ * ↑ * ) + via ψ and the fact that T , x |= ψ, by Theorem 28(2) we would have T , x |= ψ, and this is a contradiction.

Let dist 3 denote the complement of dist 3 , i.e., dist 3 (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 dist 3 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 38-2, dist 3 is not expressible in XPath = (↓↑↓ * ↑ * ) + .

Expressiveness Hierarchies

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 (Z j,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 Following the same ideas used in Propositions 9 and 11, it is easy to show that ( , k)bisimulations characterize ( , k)-equivalence.

≡ ↓ 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 ≡ ↓ 3,3 ≡ ↓ 3,4 = = = = = = = = = = . . . . . . . . . . . . . . . . . . • • • • • • • • • • • •
Proposition 40. T , u ↔ ↓ ,k T , u iff T , u ≡ ↓ ,k T , u .
The following theorem characterizes when an increase in nesting depth results in an increase in expressive power (see Figure 4). We speculate that a similar hierarchy holds in the absence of data values, but this is not a direct consequence of our result.

Theorem 41. For all , k ≥ 0

, i ≥ 1, ≡ ↓ ,0 ≡ ↓ ,1 • • • ≡ ↓ , = ≡ ↓ , +i , and ≡ ↓ ,k ≡ ↓ +i,k .
Proof. Consider the data trees T i n , T i n (n ≥ 0, i ∈ {1, 2}) defined for every k.

Figueira, Figueira, & Areces

↔ ↓ 0,0 ↔ ↓ 0,0 a, 2 a, 1 b, 1 b, 2 a, 1 a, 1 b, 1 b, 2 a, 1 T 1 0 T 1 0 ↔ ↓ 1,0 T 2 n T 1 n T 2 n T 1 n T 2 n T 1 n T 1 n ↔ ↓ n+2,n+1 ↔ ↓ n+1,n T 1 n+1 T 1 n+1 a, 1 a, 1 1 T 2 n T 1 n T 2 n T 1 n 1 T 2 n T 1 n ↔ ↓ n+2,n+1 ↔ ↓ n+1,n T 2 n+1 T 2 n+1 T 2 n a, 2 a, 2 a, 2 a, 2 a, 1 b, 1 b, 2 b, 1 b, 2 a, 2 a, 2 T 2 0 T 2 0 ↔ ↓ 1,0 ↔ ↓ 0,0 ↔ ↓ 0,0 x 1 0 x 1 0 x 2 0 x 2 0 x 1 n x 1 n x 2 n x 2 n 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 ≡ ↓ T 1 k x 1 but T 1 k , 1 k ≡ k+1,k+1 T 1 k , x 1 . That T 1 k x 1 k ↓ k+1,k+1 T 1 k , x 1
k results 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,

ϕ 1 = ε = ↓[a] ϕ i+1 = ε = ↓[ϕ i ] for i > 0. Since T 1 k , x 1 k |= ϕ k+1 but T 1 k , x 1 k |= ϕ k+1 , it follows that 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 use Proposition 40 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 (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 42. 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. We show T 1 k , x 1 k ↔ ↓ k+1,k T 1 k , x 1 k . For every j ≤ k + 1, t ≤ k, let Z j,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 (the notation x i k and x i k does not necessarily identify a unique node but, possibly, many; the intended meaning is that they can refer to any of them). Observe that Z j+1,t ⊆ Z j,t for all j, t ≤ k.

(4)

We show that (Z j,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 ) ∈ Z j,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 node inside the subtree T 1 t -1 of T 1 t . 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. data(v) = data(v ) by Observation 42. Furthermore, since every node of T 1 t -1 is in a Z j,t-1 -relation with the corresponding node in T 2 t -1 by construction of j,t-1 , it follows that ( i →v)Z j,t-1 ( i →v for all ≤ n. Thus, by (4), i →v)Z j-n+i,t-1 →v for all i ≤ n.

If, 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 vZ j,t-1 v . Thus, by (4), vZ j-1,t-1 v .

• 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)Z j,t-1 ( i →v ) for all i ≤ n. Thus, by ( 4), ( i →v)Z j-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 Z j,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 .

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 Z j,t = ↔ ↓ j,t for all j ≤ , t ≤ k. Hence, (Z j,t ) j≤ ,t≤k verify the bisimulation conditions. Let Z ,k+1 = {(x, x )}. We show that Z ,k+1 together with (Z j,t ) j≤ ,t≤k verifies the bisimulation conditions. Harmony follows from xZ ,k x . We show Zig since Zag is equivalent. Suppose x 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 15 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 (T n ) n in the proof of Proposition 15, by showing that T k , x r ,s ≡ ↓↑ 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 for all (r, s, k) < (r , s , k ), r + s ≥ 2.

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. Next we explain why this is so. Consider the following notation for denoting positions of nodes in a tree. Positions are elements of (N × N) * , where the root's position is the empty string , and the position of any other node in the tree is the concatenation of the position of its parent and the pair (l, r), where l is the number of siblings to the left of the node and r the number of siblings to its right. For every position p ∈ (N × N) * of a tree, there is a path expression α p of XPath = (↓→) that can access the node in this position (and only this position) from the root. The α p 's are defined as α = ε for the root; α (l,r) = ↓→ l+1 [ → k ∧ ¬ → k+1 ] for (l, r) ∈ N × N; and α p•(l,r) = α p α (l,r) for p ∈ (N × N) * , (l, r) ∈ N × N. It is easy to check that testing p α p [¬ ↓ ] where p ranges over all leaf positions of a given tree T tests the property that the subtree hanging from the node where the formula is evaluated is structurally isomorphic to T . Further, by also adding the tests α p [a] = α p [a ] for every pair of positions p, p with label a, a of T having the same data value, as well as α p [a] = α p [a ] for those having different data value, yields the property of being equal to T , up to isomorphism of data values.

In Section 5 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 T 1 we want to find a data tree T 2 , as small as possible, so that T 1 and T 2 are bisimilar for some fragment L of XPath. Since L cannot distinguish between T 1 and T 2 , we can use T 2 as representative of T 1 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 maximum auto-bisimulation (observe that the identity is always an auto-bisimulation, and that the union of two bisimulations is a bisimulation; therefore there is a 'maximum', often called 'coarsest', bisimulation).

The idea is to find the coarsest auto-bisimulation Z over a given data-tree T . One cannot simply make the quotient of T over Z, as the result is not necessarily a tree and it is not clear how to assign data values to each class in the quotient. However, one can make a quotient of T over the equivalence relation 'Z and same data value'. If we do so, we obtain a smaller structure, and then evaluate all queries here.

Determining the maximum auto-(bi)simulation, either downward or vertical, of a finite data T tree can be done in polynomial time. A naive algorithm starts by defining Z as the set of all nodes which satisfy Harmony. Each time Zig or Zag is not satisfied, it removes from Z the pair responsible for Zig or Zag not being true. It repeats this until a fixed point of Z is found; this is the maximum auto-bisimulation in T . If one is interested in deciding if two nodes of different finite data trees are bisimilar, one can use the same idea: the answer is 'yes' if and only if the fixed point is not the empty set. Since checking the validity of Zig or Zag is polynomial time computable (because there are linearly many paths in a tree), and at each step the algorithm decreases the size of Z, the whole process has polynomial time. Better implementations, based on more sophisticated ideas, such as the works of [START_REF] Henzinger | Computing simulations on finite and infinite graphs[END_REF] or [START_REF] Dovier | An efficient algorithm for computing bisimulation equivalence[END_REF], can lead to more efficient polynomial time algorithms. We plan to design and implement algorithms for data tree minimization using bisimulation and investigate their computational complexity.

Figure 1 :

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

1→

  is the same as →, and 0 → is the identity relation. We write x * →y to denote that (x, y) is in the reflexive transitive closure of →. (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).

  Tr x,y (αβ) = (∃z) Tr x,z (α) ∧ Tr z,y (β) (z a new variable) Tr x,y (α ∪ β) = Tr x,y (α) ∨ Tr x,y (β) Tr x,y ([ϕ]) = Tr x (ϕ) ∧ (x = y).

  qr(Tr x ( α )) = 1 + qr(Tr x (α)) qr(Tr x ( α β )) = 2 + max(qr(Tr x (α)), qr(Tr x (β))) qr(Tr x,y (αβ)) = 1 + max(qr(Tr x,y (α)), qr(Tr x,y (β))) qr(Tr x,y ([φ])) = qr(Tr x (ϕ)).

Figueira

  Figueira, Figueira, & Areces

•

  Harmony: If xZx then label (x) = label (x ). • Zig: 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 ),

•

  Step 3. Final move by Spoiler: he chooses either i ∈ {0 . . . n -1}, and places pebble p over ( i →v) and pebble p over ( i →v ) -or i ∈ {0 . . . m -1}, and places pebble p on ( i →w) and pebble p over ( i →w )

•

  Zig: If xZ j x , x n →v and x m →w with n, m ≤ j 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 j-n+i ( i →v ) for all 0 ≤ i < n, and 3. ( i →w) Z j-m+i ( i →w ) for all 0 ≤ i < m. • Zag: If xZ j x , x n →v and x m →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 2 :

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

•

  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 , data(z) = data(x) ⇔ data(z ) = data(x ), and zZz . The following picture illustrates the intended requirements are y, z ∈ T such that y n →x, y m →z, data(z) = data(x) ⇔ data(z ) = data(x ), and zZz .

•

  Harmony: If xZ k r,ŝ x then label (x) = label (x ). • Zig: If xZ k r,ŝ x , y n →x and y m →z with n ≤ ŝ and m ≤ r + n then there are y , z ∈ T such that y n →x , y m →z , and the following hold1. data(z) = data(x) ⇔ data(z ) = data(x ), 2. if k > 0, zZ k-1 r ,ŝ z for r = r + nm, ŝ = ŝn + m. • Zag: If xZ k r,ŝ x , y n →x and y m →z with n ≤ ŝ and m ≤ r + n then there are y, z ∈ T follows that yZ k-1 r ,ŝ y , for r = r + n, ŝ = ŝn. The same occurs with Z instead of Z k r,ŝ for the case of bisimilarity. For a data tree T and u ∈ T , let T | s r u denote the subtree of T induced by {v ∈ T | (∃m ≤ s) (∃n ≤ r + m) (∃w ∈ T ) w m →u ∧ w n →v}.

  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 + nm, ŝ = ŝ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. iii. T , x ≡ ↓↑ r,ŝ, k-1 T , x , and iv. T , z ≡ ↓↑ r ,ŝ , k-1

Figueira

  Figueira, Figueira, & Areces

•

  Zig: 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 ), 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 ).

  and 3. w i Z w i for all 1 ≤ i ≤ m. • Zag: If xZx and there are x * →v 1 * → • • • * →v n , and x * →w 1 * → • • • * →w m in T then there are x * →v 1 * → • • • * →v n , and x * →w 1 * → • • • * →w m in T such that items 1, 2 and 3 above are verified.

  s,k -invariant over [finite] data-trees, then there is ψ ∈ (r, s, k)-XPath = (↑↓) such that Tr x (ψ) is logically equivalent to ϕ over [finite] data-trees.Proof. By Corollary 17, for every data tree T and u ∈ T there is a node expression χ r,s,k,T ,u of (r, s, k)-XPath = (↑↓) 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 16, ≡ ↓↑ r,s,k has finite index, it follows that ψ is equivalent to a finite disjunction. The proof that ϕ(x) ≡ Tr x (ψ) is similar to Proposition 33, as we show next. Let us see that ϕ |= Tr x (ψ). Suppose T |= ϕ(u). Since T , u |= χ r,s,k,T ,a , we have T , u |= ψ and so T |= Tr x (ψ)(u). Let us see that Tr x (ψ) |= ϕ. Assume T |= Tr x (ψ)(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 20-2) we conclude T |= ϕ(u).

Figure 3 :

 3 Figure 3: Closure under subtree replication.

Figure 4 :

 4 Figure 4: Hierarchy of XPath = (↓).

n

  →v, x m →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 , ( -n+i,k ( i →v ). By an indentical reasoning, T , ( i →w)↔ ↓ -n+i,k T , ( i →w ) and thus ( i →w)Z -n+i,k ( i →w ). Thus, the Zig condition for ↔ ↓ ,k+1 is verified. The Zag condition holds by symmetry.

a, 2 a, 1 a, 3 a, 1 a, 1 a, 1 a, 2 a, 2 a, 3

Acknowledgements

This work was partially supported by grant ANPCyT-PICT-2013-2011, 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".

Let us now analyze item 2. Let α ↑ = [ψ]↑ n (n ≥ 0), and let x 0 , . . . , x n ∈ T and x 0 , . . . , x n ∈ T be such that

and xZ k-1 r,ŝ x . By 18, we have x 0 Z k-1 r ,ŝ x 0 , for r = r + n, ŝ = ŝn. Assume by contradiction that (x , y ) / ∈ [[α ↑ ]] T . This necessarily means that T , x 0 |= ψ but T , x 0 |= ψ. But ψ is a subformula of α ↑ , nd(ψ) ≤ k -1 and nd(ψ) ≤ (r , ŝ ) and this contradicts inductive hypothesis 1.

Item 3 is shown in a similar way. Let α ↓ = ↓ m [ψ] (m ≥ 0), and let z 0 , . . . , z m ∈ T and z 0 , . . . , z m ∈ T be such that

and zZ k-1 r ,ŝ z . Assume by contradiction that (y , z

and this contradicts inductive hypothesis 1.

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 .

satisfies Zig (the case for Zag is analogous). Suppose xZ k r,ŝ x ,

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 by

we conclude that P = ∅. We next show that there exists (y , z

Since every Φ T ,u is finite up to logical equivalence by Proposition 16, it follows that Ψ is a valid node expression. We show that it defines sim ↓↑ r,s,k (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 20-3 we then have that T , u ↔ ↓↑ r,s,k T , u , and in particular T , u → ↓↑ r,s,k T , u . Since T , u → ↓↑ r,s,k T , u and T , u → ↓↑ r,s,k T , u , then T , u → ↓↑ r,s,k T , u (by transitivity of → ↓↑ r,s,k ) and thus T , u ∈ sim ↓↑ r,s,k (T , u). Item ( 1) is shown in a similar way, using Proposition 2 and Theorem 8-2.

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

Theorem 27.

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

On the one hand, if T , u |= ϕ then there is i ≤ n such that T i , u i ↔ ↓ T , u, and so T i , u i → ↓ T , u. On the other hand, suppose T i , u i → ↓ T , u for some i. Since ϕ is preserved under → ↓ and T i , u i |= ϕ, we conclude T , u |= ϕ.

Let χ ,u i ,T i ∈ XPath = (↓) + , dd(ψ i ) ≤ , be as in Lemma 26-(1). Using (3) one shows that i≤n χ ,u i ,T i ≡ ϕ.

For the case of → ↓ of item (1), the 'if' direction follows from Theorem 24-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 23 and Lemma 26-(2).

Item (4) is straightforward from Theorem 24-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(ϕ) = k.