Serge Abiteboul
email: serge.abiteboul@inria.fr

Pierre Bourhis
email: bourhis@comlab.ox.ac.uk

Anca Muscholl

Zhilin Wu

Recursive queries on trees and data trees *

The analysis of datalog programs over relational structures has been studied in depth, most notably the problem of containment. The analysis problems that have been considered were shown to be undecidable with the exception of (i) containment of arbitrary programs in nonrecursive ones, (ii) containment of monadic programs, and (iii) emptiness. In this paper, we are concerned with a much less studied problem, the analysis of datalog programs over data trees. We show that the analysis of datalog programs is more complex for data trees than for arbitrary structures. In particular, we prove that the three aforementioned problems are undecidable for data trees. But in practice, data trees (e.g., XML trees) are often of bounded depth. We prove that all three problems are decidable over bounded depth data trees.

Another contribution of the paper is the study of a new form of automata called pattern automata, that are essentially equivalent to linear datalog programs. We use pattern automata to show that the emptiness problem for linear monadic datalog programs with data value inequalities is decidable over arbitrary data trees.

INTRODUCTION

In this paper, we study recursive queries over data trees. The trees we consider are unordered, unranked, labelled trees with data from an infinite domain. For specifying recursive queries, we use datalog on a relational representation of the trees. We show that the analysis of datalog programs is more complex for data trees than for arbitrary structures. We show that for bounded depth data trees, one can solve analysis problems that are undecidable for data trees in general. In our study, we introduce and use pattern automata, that correspond to linear datalog programs.

Following [START_REF] Björklund | Optimizing conjunctive queries over trees using schema information[END_REF][START_REF] David | Complexity of data tree patterns over XML documents[END_REF], we describe a data tree by a relational structure as follows. A tree is described by relations child and desc (for descendant) between nodes. Each node has a label from a finite fixed alphabet of labels and a value from an infinite set of data values. For each label α, a unary relation gives all the nodes with that particular label. The "data" is captured by a relation ∼, with n1 ∼ n2 if the two nodes n1, n2 have the same data value.

The analysis of datalog programs has been studied in depth, most notably the problem of containment. The problems that have been considered were shown to be undecidable with the exception of (i) containment of arbitrary programs in nonrecursive ones, (ii) containment of monadic programs, and (iii) emptiness. We show that the analysis of datalog programs is more complex for data trees than for arbitrary structures. In particular, we prove that the three aforementioned problems are undecidable for data trees.

We show that emptiness of a datalog program over trees is undecidable even for trees without data, and even for words. This illustrates the complexity introduced by the constraints of the tree structure. On the positive side, emptiness over trees becomes decidable for linear monadic programs for trees with data, and even for queries with inequalities. This shows notably the power of arity 2 that allows keeping track simultaneously of two computations. Whether decidability also holds for non-linear monadic programs remains open.

In practice, data trees (like in XML) are often of bounded depth. We prove that (i), (ii) and (iii) are decidable over bounded depth data trees. From a practical viewpoint, these are probably the most meaningful results of the paper, in spite of the double exponential lower bounds. This shows that, when attempting to analyse datalog programs over trees (e.g. for optimization), assuming the boundedness of trees may greatly simplify the problem.

Another contribution of the paper is the study of a new form of automata called pattern automata, that are essentially equivalent to linear datalog programs. We use pattern automata to show that the emptiness problem for linear monadic datalog programs with data value inequalities is decidable over arbitrary data trees.

DEFINITIONS

Consider a finite alphabet Σ of labels and an infinite set N of nodes. The structures we consider here are finite, labeled, unranked and unordered trees. To represent trees, we use the relational schema S = {child , desc} ∪ Σ. The representation I of a tree t is defined by the following (with n, n1, n2 ∈ N):

• child (n1, n2) if n2 is a child of n1;

• desc(n1, n2) if n2 is a strict descendant of n1;

• For each σ in Σ, σ(n) if the label of n is σ.

Observe that the instances satisfy some particular constraints because they represent trees. For instance,

• The second attribute of the relation child is a primary key (each node has at most one parent)

• There exists a single value n that occurs in the first column of child and not the second (the unique root).

• desc is the (nonreflexive) transitive closure of child .

• The relations σ ∈ Σ partition the set of nodes.

Data trees. In this paper, the focus is on queries over data trees defined as follows.

Consider an infinite set D of data values. A data tree t is a tree such that to each of its nodes is also associated some value of D. To represent data trees, we use the relational schema S ∼ = {child , desc, ∼} ∪ Σ.

The representation I of a data tree t is defined by

• child , desc and each σ in Σ are as in the definition of trees, and

• n1 ∼ n2 if the nodes n1, n2 in t have the same data value.

Note that ∼ is an equivalence relation. Data words can be defined as the special case of data trees where each non-leaf node has exactly one child.

Datalog and UCQs. We assume that the reader is familiar with datalog. We recall briefly some definitions next. A datalog program consists of a finite set of rules of the form: R(x) :-R1(x1), . . . , R k (x k ) such that k ≥ 0, x and each xi are vectors of variables and constants and each variable occurring in the head R of the rule also occurs in the body. A datalog program is defined over a database schema Sch and predicates from Sch are called extensional, the other predicates are called intensional. Only intensional predicates can occur in rule heads. A distinguished intensional predicate is called the goal. A datalog program defines a mapping from database instances over Sch to relational instances over goal.

We also consider some restrictions. A datalog program is:

• linear if each rule body includes at most one intensional atom;

• k-datalog if the arity of each intensional predicate is at most k, and monadic if it is at most one, i.e., it is 1-datalog (k is also called the arity of the datalog program); and

• Boolean if the arity of the goal predicate is zero.

The answer of a datalog program P over an instance I, denoted by P (I), is the set of tuples appearing in the goal predicate after having filled the intensional predicates by using recursively the rules of the datalog program until a fixpoint is reached.

In this paper, we consider datalog programs over the schema S, S ∼ and S ∼, , where S ∼, = S ∼ ∪ { =, } is the extended schema for data trees, with = and interpreted respectively as node inequality and data value inequality. We use the notation datalog ∼, to denote the datalog programs over the schema S ∼, .

A conjunctive query (CQ) is an existential formula of the form ∃x1 • • • ∃x k ϕ, where ϕ is a conjunction of positive atomic formulas over the given signature. We will consider unions of conjunctive queries, UCQs for short. A UCQ is Boolean if it has no free variable.

To conclude this section, we briefly recall some known decidability results on the containment problem for datalog programs.

First, we consider arbitrary structures, then trees. For arbitrary structures, the following result (that will be used in Section 4) is known:

Theorem 2.1. [9]
• The problem of containment of a datalog program in a UCQ for relational structures is 2Exptime-complete.

• The problem of containment of a linear datalog program in a UCQ for relational structures is Expspacecomplete.

The following result for trees without data and monadic datalog programs not using the descendant relation is also known: Theorem 2.2. [START_REF] Gottlob | Monadic datalog and the expressive power of languages for web information extraction[END_REF] Let P be a monadic datalog program over the schema S \ {desc} = {child } ∪ Σ. Then there exists an unranked query tree automaton 1 AP such that for each tree t over Σ and the representation I of t, P (I) = AP (t).

Using the previous result, we observe: Corollary 2.3. The containment problem for monadic datalog programs over trees not using the relation desc (i.e., over the schema {child } ∪ Σ) is decidable.

The containment problem for monadic datalog programs over trees remains open. We will see in the next section that it is undecidable over data trees. And in the following one, that the problem is decidable for bounded-depth data trees.

UNDECIDABILITY RESULTS

The containment problem for datalog programs is known to be undecidable for arbitrary structures [START_REF] Abiteboul | Foundations of Databases[END_REF]. However, it has been shown to be decidable for two important natural restrictions: (i) for the containment of a datalog program in a non-recursive program [START_REF] Chaudhuri | On the equivalence of recursive and nonrecursive datalog programs[END_REF], and (ii) for monadic datalog programs [START_REF] Cosmadakis | Decidable optimization problems for database logic programs (preliminary report)[END_REF]. These decidability results hold for arbitrary structures. In this section, we show that the problem is more complex for datalog programs over data trees.

With respect to (i), we show that the problem of the containment of datalog programs in UCQs over trees (even without data) is undecidable (Corollary 3.2). Indeed, we even 1 For a definition of query tree automaton, see [START_REF] Neven | Query automata over finite trees[END_REF].

prove that the problem of emptiness of datalog programs on trees without data is undecidable (Proposition 3.1).

With respect to (ii), we show that the problem of containment of a linear monadic datalog program in a union of conjunctive queries on data trees is undecidable (Proposition 3.3).

Lastly, we also consider bounded depth data trees. We show that the containment of a linear monadic datalog program in a union of conjunctive queries with data inequalities is undecidable for bounded depth data trees (Proposition 3.5). This is to set limitations to a result of next section that states that this problem is decidable in absence of inequalities.

Datalog on trees without data

A datalog program P over schema S is empty if for each instance I over S, P (I) is empty. Checking datalog program emptiness is decidable over relational structures [START_REF] Abiteboul | Foundations of Databases[END_REF]. However, it becomes undecidable if the instances are constrained to be trees. We believe this result to be known. But since we could not find a reference for it, we include it here for completeness.

Proposition 3.1. Emptiness of datalog programs over words or trees with schema S, is undecidable.

Proof. We encode a run of a deterministic Turing machine on empty input by a datalog program over trees as follows. Let Γ be the tape alphabet, Q the set of states and ∆ :

Q × Γ → Q × Γ × {-1, 0, 1} the transition function. A run C0 C1 • • • Cn is a sequence of configurations Ci,
where each Ci is encoded as a word from Γ * (Γ × Q)Γ * of length K (where K ≥ maxi |Ci|). The datalog program will check that an accepting run #C0#C1# • • • Cn# labels some path leading upwards in the tree.

The program consists of three subprograms, with binary goal predicates R0, R∆, R f . We define R0 such that for any two nodes n, n , we have R0(n, n ) iff n is an ancestor of n and the path from n to n is labeled by #C0#. The program R∆ is such that R∆(n, n ) iff n is an ancestor of n separated by one #, and such that n corresponds to the j-th position in some configuration C, whereas n is the j-th position in the configuration C with C C . Finally, R f is such that R f (n, n ) iff R∆(n, n ) and n has label from ΓF = Γ × F , with F the set of accepting states. All three programs are linear (and binary). Let ΓQ = Γ ∪ Γ × Q and S ⊆ (ΓQ) 4 be the relation corresponding to the transition function of the TM: (α, β, γ, δ) ∈ S iff for some C C and some position 1 ≤ j ≤ K = |C| = |C |, the j-th symbol in C is δ, and the j -1, j, j + 1-th symbols in C are α, β, γ, respectively (for i = 0 and i = K + 1 we set the symbol to be #). Below, we use S(x, y, z, w) as a shorthand for (α,β,γ,δ)∈S α(x) ∧ β(y) ∧ γ(z) ∧ δ(w) and describe R∆ and R f (R0 is similar).

• R∆(x, y) :-ΓQ(x), ΓQ(y), child (x, x1), child (y, y1), child (z, x), S(x1, x, z, y), R0(x1, y1)

• R∆(x, y) :-ΓQ(x), ΓQ(y), child (x, x1), child (y, y1), child (z, x), S(x1, x, z, y), R∆(x1, y1)

• R f (x, y) :-R∆(x, y), ΓF (y)

Observe that the datalog program in the above proof is linear and binary (i.e., 2-datalog). Now this implies: Corollary 3.2. Containment of 2-datalog programs in CQs over words or trees with schema S, is undecidable.

Proof. Let P be a datalog program and let Q be the conjunctive query ∃x child (x, x), then Q never holds for trees. Thus over trees, P ⊆ Q iff P is empty.

Linear monadic datalog over data trees

We show the following result: Proposition 3.3. Containment of linear monadic datalog programs in UCQs over data words or over data trees with schema S ∼ , is undecidable.

Proof. We first show the result for words. We reduce the Post Correspondence Problem (PCP) to our problem on data words. Let (ui, vi) 1≤i≤k be a PCP instance over alphabet Σ.

We want to build a linear, monadic datalog program P and a UCQ Q (both Boolean) such that P is not contained in Q iff there exist m ≥ 1 and indices i1, . . . , im such that

ui 1 • • • ui m = vi 1 • • • vi m .
We start with an informal description. The linear monadic program encodes a data word with labels from Σ∪ Σ∪{#, $}, where Σ is a (disjoint) copy of Σ. The following conditions should hold:

1. The string projection of this data word belongs to the set #( 1≤i≤k uivi) + $, where v denotes the copy of the word v over Σ.

2. All positions labelled by Σ ( Σ, respectively) carry different data values.

3. Let ρ (ρ, respectively) denote the sequence of data values of the subword with labels from Σ ( Σ, respectively). The sequences ρ and ρ are equal, and any two positions in ρ and ρ with equal data value have the same label (i.e., a and ā for some a ∈ Σ).

A monadic datalog program P can check Condition (1), assuming that we have the special markers #, $ for the first and last position, respectively (that these markers are used only at the first and last position, respectively, can be guaranteed by the UCQ). More generally, any finite-state automaton A can be simulated by a monadic datalog program, ensuring that the string projection of the data word belongs to #L(A)$.

Condition (2) is enforced by the negation of the UCQ Q, as follows. A UCQ can express the existence of two positions x = y such that both x, y have label in Σ ( Σ, respectively) and x ∼ y. Notice that we do not actually need the atomic predicate x = y: due to Condition (1) we can distinguish several cases, depending on whether x, y belong to the same occurrence of some ui (vi, respectively), so we can use the child (successor) predicate, or they are separated by some symbol from Σ) (Σ, respectively), so we use the desc (linear order) predicate.

Condition (3) is enforced by the datalog program: First, P checks that the first (last, respectively) node with label from Σ has the same value as the first (last, respectively) node with label from Σ, and that the labels are the same. For identifying these nodes, the special markers #, $ for the first/last node are used. Then, P checks recursively for every node x in ρ: there exists a node x in ρ such that x ∼ x and y ∼ y hold, where y is the successor of x in ρ and y is the successor of x in ρ. Notice that P can refer to the successor in ρ (resp. ρ) by using the child predicate, since the distance between two consecutive nodes labeled by Σ ( Σ, respectively) is bounded by the maximal length of the words vi and ui. The requirement for equal labels a, ā is checked at the same time.

For data trees, the crux is (as in Proposition 3.1) to follow paths leading upwards in the tree. One needs to pay attention in particular to Condition (3) above.

It is interesting to note that Proposition 3.3 remains true even for programs using desc but not child . It remains open whether using child , but not desc, remains undecidable. Proposition 3.4. Containment of linear monadic datalog programs in UCQs over data words or trees (with schema S ∼ ) is undecidable, even for programs without the child relation.

Bounded depth and inequalities

The inclusion problem for conjunctive queries over data trees where queries can use data inequalities, is known to be undecidable [START_REF] Björklund | Optimizing conjunctive queries over trees using schema information[END_REF]. We will prove in the next section that containment of a linear monadic datalog program in a UCQ is decidable for bounded depth data trees, in absence of node and data inequalities. This is in the spirit of [START_REF] David | Complexity of data tree patterns over XML documents[END_REF], which showed that satisfiability of certain queries restricted to trees of bounded depth is decidable, while being undecidable for unbounded depth. We next show that the decidability result in the next section cannot be extended to datalog and UCQs using inequalities. Proposition 3.5. Containment of linear, monadic datalog programs in UCQs over schema S ∼, , is undecidable for data trees of depth 2.

Proof. We simulate the proof of Proposition 3.3 on data trees of depth 2 as follows. The basic idea is to encode a list L on (some of) the nodes at depth 1. We describe first how trees satisfying P ∩ ¬Q should look like.

1. Nodes at depth 1 have labels from Σ ∪ Σ, and nodes at depth 2 have label L or R.

2. If an L-node and an R-node have the same parent, then they have different data.

3. If two L-nodes have the same parent, then they have equal data, too. Same for R-nodes.

If two nodes

x, y at depth 1 are such that their Lchildren have equal data, then their R-children also have equal data (if they exist), and both the labels and the data of x, y are identical. Same for L, R interchanged.

5. There are two distinguished nodes at depth 1, one denoted as "start", the other as "end".

6. Node "end" can be reached from "start" by iterating the following successor relation: y is the successor of x if the data of the L-child of y is equal to the data of the R-child of x. Notice that there might be several nodes y that satisfy this condition, but they all agree in their label and data (Condition ( 4)). So the path from "start" to "end" is unique (if it exists) if we consider the label/data of the nodes on the path.

Note that the datalog ∼, program P can enforce Condition (6) (and the existence of "start", "end"), whereas the remaining conditions are expressed by the negation of Q.

We show how to mimic the proof of Proposition 3.3 on the list L from "start" to "end".

First, notice that the program P can verify the first and last condition in the proof of Proposition 3.3, by restricting the checks to nodes in L. It suffices to start the checks at node "start" -the unicity of the path from "start" to "end" ensures that we are considering only nodes in the list L.

The condition ensured by the UCQ in the proof of Proposition 3.3 is that there exist two nodes x = y both with label from Σ (or Σ) such that x ∼ y. We can express x = y by saying that the L-child of x, say x , and the L-child of y, say y , are such that x y .

CONTAINMENT PROBLEM: DECIDABI-LITY

As shown in the previous section, the static analysis of datalog programs over trees rapidly leads to undecidability results. In this section, we show two positive results about query containment for data trees, both for trees of bounded depth. A third positive result for the emptiness problem over unbounded depth trees is presented in the next section.

As already mentioned, the undecidability results in Section 3 rely in an essential way on the presence of data values. (Recall the decidability results mentioned in Section 2.) Interestingly, we next show that one regains decidability in the presence of data values by imposing that the depth is bounded. We next consider inclusion of datalog in UCQs, then monadic datalog.

Bounded depth, datalog and UCQs

We show next that surprisingly, containment of datalog programs into UCQs becomes decidable over bounded depth data trees. Note that the restriction to bounded depth trees is reasonable, since in practice, XML trees are quite often of very small depth. Theorem 4.1. Let k > 0 be a fixed integer. The problem of containment of datalog programs in UCQs with schema S ∼ over data trees of depth less than k, is decidable. The complexity is in 3Exptime and 2Exptime-hard.

Proof. Let P be a datalog program and Q be a UCQ with the schema S ∼ . We assume without loss of generality that both P, Q are Boolean. The proof goes as follows. We define a new relational schema S and transform P and Q into a datalog program P and a UCQ Q over S (both Boolean) such that:

P ⊆ Q over data trees of depth at most k iff P ⊆ Q .
Then using Theorem 2.1, this will show decidability. The key point in the translation is as follows. Each node n at depth j ∈ {0, . . . , k} in the data tree t will be identified by a relational tuple (n0, v0, . . . , nj, vj). The v-components in the tuples are needed for translating the predicate ∼. Different tuples represent different tree nodes, and the node encoded by (n0, v0, . . . , nj, vj) is a child of the node encoded by (n0, v0, . . . , nj-1, vj-1). Moreover, two tuples (n0, v0, . . . , ni, vi, . . .) and (n0, v0, . . . , ni, wi, . . .) with vi = wi represent different tree nodes. We will need to assert some more things in order to ensure that a relational structure can be indeed decoded into a data tree.

We will do the transformation for each rule r of P separately. We show first that we may assume that the predicate desc does not occur in the body of r, at the cost of increasing the number of rules by k d , where d is the maximal number of desc atoms in the body of a rule. We may do this by replacing every atom desc(x, y) by some conjunction child (x, z1), child (z1, z2, ), . . . , child (zi, y), 0 ≤ i < k -1, where z1, . . . , zi are new variables (by convention, for i = 0 the sequence equals child (x, y)).

Without loss of generality, we also assume that (**) no rule contains atoms child (x, z) and child (y, z) with x = y, since in this case, x, y denote the same node in the data tree and y can be replaced by x or vice versa. In the following, we show how to transform every rule r over S ∼ into a set of datalog rules over the relational schema S = {αj | α ∈ Σ, 0 ≤ j ≤ k}. First we fix a new variable name u, which will stand for the root and will be used in all transformations of rules.

Let Var(r) be the set of variables in the body of a rule r. We assign to each variable x in Var(r) a depth: let D : Var(r) → {0, . . . , k}. This assignment is done consistently with the child (x, y) atoms in r, so that D(y) = D(x)+1 must hold in that case. For each variable x in r such that there is no atom child (z, x) in r we also add to r the sequence of atoms child (u, x1), child (x1, x2), . . . , child (x D(x)-1 , x), with x1, . . . fresh variables (we might have xi = yj for some x = y, but we should respect the constraint (**) above). We call the modified rule r(D).

Let us consider a rule r(D) modified as above and choose a labeling (x) ∈ Σ for the variables in r(D). This choice should be consistent with the atoms of the form α(x) in r(D). Note that there are at most ((k + 1) ˙|Σ|) |Var(r)| many pairs (r(D), ).

For each pair (r(D), ) we define now a rule r over S as follows:

1. For every variable z in r(D) add a new variable, say vz. The variable vu associated with the "root" u should be the same for all transformations.

Suppose that u, z1, . . . , zj = z is the "path" from the "root" u to variable z in r(D), with D(z) = j. Set πz to be the sequence of variable-pairs (u, vu), (z1, vz 1 ), . . . , (zj, vz j ).

2. For every intensional predicate R(x1, . . . , x l ) in r(D) there is a (new) intensional predicate R (πx 1 , . . . , πx l ) in r , of arity l i=1 D(xi).

3. For each variable x in r(D) with D(x) = j and (x) = α we have an atom αj(πx) in r .

4. For every intensional predicate x ∼ y in r(D) we have the atom vx = vy in r .

The datalog program P over S consists of all rules r obtained from some pair r(D), as above. The size of P is at most exponential in the size of P .

Similar transformations can be applied to each disjunct in the UCQ Q and we get an UCQ Q over S .

There remains one final issue: by choosing the mapping we ensure that every node in the tree decoded from some instance over S has a label from Σ. However we also need to guarantee that the label is unique. To ensure this, for every i : 0 ≤ i ≤ k and α, β ∈ Σ with α = β, we add the formula ∃x0, v0, . . . xi, vi(αi(x0, v0, . . . , xi, vi) ∧ βi(x0, v0, . . . , xi, vi)) as a disjunct of Q .

Finally we show that P ⊆ Q over data trees of depth at most k iff P ⊆ Q .

Suppose first that there is some data tree t (of depth at most k) such that P (I) holds but Q(I) does not, for some I representing t over S ∼ . Let I be some representation of t over S , according to our encoding of nodes by sequences of nodes/values. It is easy to check that P (I ) holds, but Q (I ) does not.

Conversely, assume that P holds but Q does not, and let I be an instance over S witnessing this. Consider a proof tree showing that P (I ) holds, and let I be the instance obtained from I by keeping each fact occurring in this proof tree. Observe that I is the representation of a (data) tree t of depth at most k, since there is a unique root node (corresponding to the variable pair u, vu), and each node (corresponding to a distinct tuple) has a unique label from Σ -otherwise Q (I ) would hold. Moreover, it is easy to check that P holds on t, but Q does not.

Complexity upper bound. First there is an exponential blow-up in the translation from P to P and from Q to Q . Due to the fact that the containment of a datalog program in a UCQ over arbitrary relational structures is in 2Exptime, we conclude that the containment of datalog programs in UCQs over the schema S ∼ is in 3Exptime.

Hardness. 2Exptime hardness is proved by a reduction from the problem of containment of a datalog program P in a UCQ Q over arbitrary relational structures. Consider a relational schema R. An instance of R is represented as a tree with one subtree labelled p of the root for each relation p in R. The p-node has a child labeled ptup for each tuple in p with children labelled p1, ..., p l if p has arity l. In each rule r of P , an atom p(x1, ..., x l ) is translated into the conjunction of the following atoms, root(y), child(y, z), p(z), child(z, x), ptup(x), child(x, x 1 ), p1(x 1 ), child(x 1 , x1), . . . , child(x, x l ), p l (x l ), child(x l , x l ), where x, y, z, x 1 , . . . , x l are new variables. In addition, an atom x1 = x2 is replaced by x1 ∼ x2. Let P , Q denote the resulting datalog program and the UCQ. Then one can show that P ⊆ Q over the instances of R iff P ⊆ Q over bounded depth data trees.

As a corollary we have: Corollary 4.2. Let k > 0 be fixed. The emptiness problem for datalog programs over data trees of depth less than k over the schema S ∼ , is decidable.

Bounded depth and monadic datalog

Our result in this section shows that the containment problem for monadic datalog programs over bounded depth data trees is also decidable. For comparison, containment of monadic datalog programs over relational structures is 2Exptimecomplete [START_REF] Cosmadakis | Decidable optimization problems for database logic programs (preliminary report)[END_REF][START_REF] Benedikt | Monadic datalog containment[END_REF]. We do not have a precise complexity bound for data trees, as explained below.

We use the following result 2 , which is a specialization of Theorem 5.5 of [START_REF] Courcelle | Recursive queries and context-free graph grammars[END_REF] to datalog programs. Note that the upper bound in the corollary below is (at least) non-elementary, since [START_REF] Courcelle | Recursive queries and context-free graph grammars[END_REF] talks about inclusion of hypergraph grammars in monadic second-order logic. We conjecture that the complexity is lower for datalog.

Corollary 4.3. The problem of containment of datalog programs in monadic datalog programs over relational schemes is decidable.

Proof. It is known that each Boolean monadic datalog program over a relational schema can be rewritten into an MSO formula without free variables over the same schema. In addition, properties expressed by Boolean monadic datalog programs are closed under homomorphisms, as a result of the lack of negation symbols in datalog programs. Then the result follows from Theorem 5.5 in [START_REF] Courcelle | Recursive queries and context-free graph grammars[END_REF]. Now we have the following result.

Theorem 4.4. The problem of containment of datalog programs in monadic datalog programs with the schema S ∼ over bounded depth data trees is decidable.

Proof. We reduce the problem to the problem of containment of datalog programs in monadic datalog programs over relational structures. Let P and Q be two datalog programs over S ∼ , with Q monadic. We assume that P does not use node equalities (they can be replaced by syntactically replacing variable names). We translate P to a relational datalog program P using the construction in the proof of Theorem 4.1. Note that P does not use variable equalities either. We would like to proceed similarly with Q, to obtain Q . However doing it naively would lead to a non-monadic program, since a variable in Q is simulated by a tuple of variables in Q . Nevertheless, it turns out that it suffices to use one variable to represent the tuple of variables in Q . The main idea is that Q does not need to enforce the tree structure anymore, since P does. So let Q be the non-monadic datalog program obtained from Q as in the proof of Theorem 4.1. We define Q as the monadic datalog program obtained from Q by replacing each intensional atom R (x0, v0, . . . , xi, vi) by R (xi). If R (x0, v0, . . . , xi, vi) was the head of a rule, this means of course that x0, v0, . . . , xi-1, vi-1, vi will be quantified existentially in the body of the rule.

In the following, we will show that

P ⊆ Q over data trees of depth at most k iff P ⊆ Q . ( * )
To prove ( * ), we need to make sure that in a relational instance a2i properly identifies the node of the tree that we previously identified by the tuple a0, a1, . . . , a2i, a2i+1. For that, consider the following property for the instances I over S . Assume that (a0, a1, . . . , a2i, a2i+1) and (b0, b1, . . . , b2i, b2i+1) are two tuples occurring in the interpretations of some extensional predicate αi in I. Then the following two conditions hold: 2 We thank Michael Benedikt for pointing this result to us.

1. if a2j = b2j, then for each j < 2j, a j = b j , and a2j+1 = b2j+1.

2. for each j = j , a2j = a 2j .

First suppose P Q . Let I be an instance satisfying P but not Q . Now, consider the proof tree that demonstrates P using I. We can assume without loss of generality that I only contains facts occurring in that proof tree. Similar to the argument in the proof of Theorem 4.1, we also observe that I is the representation of a data tree t of depth at most k. The instance I may not satisfy conditions (1) and (2) above. But for every tuple (n0, v0, . . . , ni, vi) in I, we can choose a tuple of new elements (n 0 , . . . , n i ) and replace the tuple (n0, v0, . . . , ni, vi) by (n 0 , v0, . . . , n i , vi), so that conditions (1) and ( 2) above are satisfied. We do this by preserving common prefixes: if (n0, v0, . . . , ni, vi) is a common prefix of two tuples, then we use the same new elements (n 0 , . . . , n i ) in both tuples. Let I be the resulting instance.

It is easy to observe that there is a (non-injective) mapping ϕ from the domain of I to that of I such that ϕ is consistent with the interpretations of the relations αi in I and I, more precisely, if αi(n0, v0, . . . , ni, vi) holds in I , then αi(ϕ(n0), ϕ(v0), . . . , ϕ(ni), ϕ(vi)) holds in I. Clearly, I satisfies P , because I already did and because P does not use equalities. We show by contradiction that I does not satisfy Q . Because Q contains no negations, if I would satisfy Q then I would satisfy Q as well, a contradiction. Therefore, we get an instance I which satisfies P but not Q , and that satisfies the condition (1) and ( 2) above. Since I is also a representation of t, it follows that t satisfies P . Since I satisfies conditions (1) and ( 2), we also infer that t does not satisfy Q. We conclude that P ⊆ Q. Now suppose P Q. Let t be a bounded depth data tree satisfying P but not Q, and I be an encoding of t, satisfying conditions (1) and [START_REF] Abiteboul | On the equivalence of distributed systems with queries and communication[END_REF]. Then P and Q on I correctly simulate P and Q on t, respectively, thus I satisfies P but not Q . Hence P Q .

EMPTINESS PROBLEM AND PATTERN AUTOMATA

In this section, we define pattern automata that are essentially equivalent to linear datalog programs over data trees. Using these automata, we show that over data trees, the emptiness problem for datalog ∼, programs is decidable.

We first describe pattern automata informally. They use data tree patterns in the form of state invariants and transition constraints. Transitions are guarded by constraints that relate variables of the source and the target state.

Data tree patterns (patterns for short) are conjunctive queries over the schema S ∼, , or equivalently, formulas of the form ∃x1 • • • ∃x k ϕ with ϕ a conjunction of positive atomic formulas over S ∼, . Free variables of patterns are defined as usual. For a pattern P , let Var(P ) (resp. Free(P )) denote the set of variables (resp. free variables) occurring in P . Matchings of patterns into data trees have the standard (non-injective) meaning. Let also P denote the collection of all patterns. It is easy to see that the satisfiability problem of patterns can be solved in NP.

For notational convenience, in this section, we will use the schema S ∼, ,-1 which is the extension of the schema S ∼, with child -1 and desc -1 , the inverse relation of child and desc. The formula child -1 (x, y) and desc -1 (x, y) can be thought as respectively the formula child (y, x) and desc(y, x) within the schema S ∼, .

A constraint ψ is a conjunction of atomic formulas over S ∼, ,-1 \Σ and variables x, y, . . . and x , y , . . .. Let C denote the collection of all constraints. For ψ ∈ C, let Var(ψ) denote the set of variables occurring in ψ. Definition 5.1. A pattern automaton (PA for short) A is a tuple (Q, I, F, γ, ∆) such that

• Q is a finite set of states, I ⊆ Q is the set of initial states, F ⊆ Q is the set of final states,
• γ : Q → P assigns to each state in Q a pattern (state invariant),

• ∆ ⊆ Q × C × Q is a set of guarded transitions: for each (q, ψ, q ) ∈ ∆, the constraint ψ is such that each atom is of the form α(x, x ), where α ∈ S ∼, ,-1 \ Σ, x ∈ Free(γ(q)), and x ∈ Free(γ(q )). Notice that the first variable in ψ refers to q, whereas the second one refers to q .

We assume for the remaining of the section that all state invariants and transition constraints of PA are satisfiable 3 .

A run of A over a data tree t is a sequence

(q0, π0)(q0, ψ1, q1)(q1, π1) • • • (q k-1 , π k-1 )(q k-1 , ψ k , q k )(q k , π k )
such that for every i,

• (qi, ψi+1, qi+1) ∈ ∆,
• πi is a matching of γ(qi) into t,

• let ψi+1 = j αj(xj, x j ), where for every j: αj ∈ S ∼, ,-1 \ Σ, xj ∈ Free(γ(qi)), x j ∈ Free(γ(qi+1)); moreover, αj(πi(xj), πi+1(x j )) holds in t.

A run (q0, π0) • • • (q k , π k ) on t as above is accepting if q0 ∈ I and q k ∈ F . The PA A is said to be non-empty if it has some accepting run.

Let A = (Q, I, F, γ, ∆) be a PA. The arity of a transition (q, ψ, q ) ∈ ∆ is defined as max |Free(γ(q)) ∩ Var(ψ)|, |Free(γ(q )) ∩ Var(ψ)}| .

The arity of a PA is the maximum of the arities of its transitions.

A PA of arity one is called unary. So, if A is unary then each transition (q, ψ, q ) of A can be written as ψ(x, x ) = α α(x, x ) for some x ∈ Free(γ(q)), x ∈ Free(γ(q )) and each α is from S ∼, ,-1 \ Σ. A = (Q,I,F,γ,∆) is illustrated in Figure 1, where 3 This check can be seen as a preprocessing in Exptime and will not affect the 2Exptime upper bound in Theorem 5.5.

Example 5.2 A pattern automaton

• Q = {q0, q1, q2}, I = {q0}, F = {q2}, • γ is defined as follows, -γ(q0) = ∃x1∃x3 (a(x1)∧b(x2)∧c(x3)∧child (x1, x2)∧ desc(x1, x3) ∧ x2 ∼ x3), -γ(q1) = ∃x6(b(x4) ∧ b(x5) ∧ c(x6) ∧ child (x4, x5) ∧ desc(x4, x6) ∧ x5 ∼ x6),
-

γ(q2) = ∃x8∃x9(b(x7)∧d(x8)∧c(x9)∧child (x7, x8)∧ desc(x7, x9) ∧ x8 x9), • ∆ = {(q0, x2 = x4, q1), (q1, x5 = x4, q1), (q1, x5 = x7, q2)}.
Intuitively, A starts from an a-node, looks downwards for a sequence of b-nodes v, each of them having another c-node v such that v is a descendant of the parent of v, and v has the same data value as v; finally, A stops at a d-node w such that there is a c-node w which is a descendant of the parent of w, and has a different data value from w.

q 0 q 1 q 2

x 2 = x 4

x 5 = x 4

x 5 = x 7

x 1

x 2 x 3 ∼ a b c x 4 x 5 x 6 ∼ b b c x 7 x 8 x 9 ∼ b d c γ(q 0 ) γ(q 1 ) γ(q 2 )

Figure 1: Example for pattern automata

The following theorem shows that pattern automata are equivalent to (Boolean) linear datalog ∼, programs.

Theorem 5.3. The following result holds.

For any Boolean linear datalog ∼, program P , a PA

A of the same arity as P can be constructed in linear time such that for every data tree t, P evaluates to true over t iff t is accepted by A.

2. For any PA A, a Boolean linear datalog ∼, program P of the same arity as A can be constructed in linear time, such that for every data tree t, t is accepted by A iff P evaluates to true over t.

Proof. (Sketch) A PA can simulate a datalog ∼, program with states corresponding to rules, state invariants corresponding to the body of the corresponding rule, and transition constraints relating the variables of the intensional predicate of the body with the one of the head. Conversely, a datalog ∼, program simulates a PA by using one intensional predicate for each transition. • r1 : R0() :-γ(q0), R1(x2),

• r2 : R1(x2) :-x2 = x4, γ(q1), R2(x5), • r3 : R1(x2) :-x2 = x4, γ(q1), R3(x5), • r4 : R2(x5) :-x5 = x 4 , γ (q1), R2(x 5 ), • r5 : R2(x5) :-x5 = x 4 , γ (q1), R3(x 5 ), • r6 : R3(x5) :-x5 = x7, γ(q2),
where x i 's are new variables and γ (q1) is obtained from γ(q1) by replacing each variable xi with x i .

Note here we abuse the notations a bit: For instance, by γ(q0), we mean the tuple of atomic formulas occurring in γ(q0). Similarly for γ(q1), γ(q2), γ (q1).

With one state per rule, we can translate P A back into the PA B = ({r1, . . . , r6}, {r1}, {r6}, γ1, ∆1) illustrated in Figure 2, where for every i : 1 ≤ i ≤ 6, γ1(ri) is an existential quantification of the conjunction of the extensional atoms in the body of the rule ri, e.g. γ1(r2) = ∃x4∃x6(x2 = x4 ∧ γ(q1)), with variables x2 and x5 free. From Theorem 5.3 and Proposition 3.1, we know that the nonemptiness of PA of arity two is already undecidable over data trees (actually even over trees). On the other hand, in the following, we will prove that the nonemptiness problem for unary PA is decidable over data trees.

r 1 r 2 r 6 x 2 = x 2 r 3 x 5 = x 5 r 4 r 5 x 2 = x 2 x 5 = x 5 x 5 = x 5 x 5 = x 5 x 5 = x 5 x 5 = x 5
Theorem 5.5. The nonemptiness problem for unary PA over data trees is in 2Exptime and Exptime-hard.

Using the previous theorem, it follows that: Corollary 5.6. The emptiness problem for linear monadic datalog ∼, programs over data trees is in 2Exptime and Exptime-hard.

Before giving the proof of the theorem, we need some additional notations.

Let P be a pattern and x a variable in P . Then the set of all variables y in P (in particular, x itself) such that there is a sequence of variables z1, . . . , z k satisfying that z1 = x, z k = y and for every i : 1 ≤ i < k, child (zi, zi+1) or child (zi+1, zi) or zi = zi+1, is called a component of P . A local pattern is a pattern with a unique component, which is the set of all its variables. Then a non-local pattern has at least two distinct components. Definition 5.7. Let A = (Q, I, F, γ, ∆) be a unary PA. A run ρ of A is said to be local if the following two conditions are satisfied:

• for every (q, ψ, q ) in ρ, the constraint ψ(x, y) has an atomic formula of the form child (x, y), or child -1 (x, y), or x = y.

• for every two consecutive transitions (q, ψ, q ), (q , ψ , q ) in ρ, if ψ(x, y) and ψ (x , y ) (where x ∈ Free(γ(q)), y, x ∈ Free(γ(q )) and y ∈ Free(γ(q ))), then x , y belong to the same component of γ(q ). Notice that in this case, every matching of γ(q ) maps x , y to nodes that are at bounded distance in the tree.

A run ρ of A is said to be global if for every (q, ψ, q ) in ρ, the constraint ψ(x, y) is such that every conjunct is of the form α(x, y) with α ∈ {desc, desc -1 , ∼, , =}.

A two-way nondeterministic tree walking automaton over ranked trees (TWA for short) is a finite state automaton with transitions defined by the rules of the following form: "if the current state is q and the reading head is at some node n labeled by σ, then the state changes to q , and the reading head goes to the parent of n or goes to the i-th child of n (where i ∈ N)". Such an automaton starts at the root and accepts if it reaches a final state.

We are ready to present the proof of Theorem 5.5 and we first focus on the upper bound.

Upper bound

The proof schema of the upper bound goes as follows.

1. First we show how to decide in polynomial time whether a unary PA has a global accepting run.

2. Second we show how to decide in doubly exponential time whether a unary PA has some local accepting run.

Here we use tree-walking automata.

3. Finally, we combine the previous proof ideas to show the general case.

For the proposition below, recall that we assume that all invariants and constraints in our PA are satisfiable.

Global runs for unary PA Proposition 5.8. The following question is in PTIME. Given a unary PA and two states q, q , does a data tree exist with a global run from q to q ? Proof. We prove the result by showing the following claim.

Claim. There exists a data tree with a global run from q to q iff state q can be reached from q in the transition graph of A by global transitions, only.

The "only if" direction is immediate. For the "if" direction let us consider a path (q0, ψ1, q1)(q1, ψ2, q2), . . . , (q k-1 , ψ k , q k ) in the transition graph of A, such that q = q0, q k = q , and all transitions (qi-1, ψi, qi) are global. Recall that we assume that all state invariants (and constraints) are satisfiable. So for each i, let si be a data tree such that there is a matching from γ(qi) to si. We show how to construct a data tree t, together with a run (q0, π0)(q0, ψ1, q1)(q1, π1)

• • • (q k-1 , ψ k , q k )(q k , π k ) of A on t.
Suppose that t is already defined, together with a run (q0, π0)(q0, ψ1, q1)(q1, π1) • • • (qi, πi) on t . The construction procedure goes as follows.

• If ψi+1 requires desc(x, y) (with x in γ(qi), y in γ(qi+1)), then let ρ be a path in t to which πi(x) belongs and n be the leaf of t in ρ. We extend t by attaching s i+1 as a subtree of n, where s i+1 is obtained from si+1 by renaming possibly data values to account for data constraints in ψi+1.

• If ψi+1 requires desc -1 (x, y) (with x in γ(qi), y in γ(qi+1)), then let π be a matching of γ(qi+1) to si+1, ρ be a path in si+1 to which π(y) belongs to, and n be the leaf of si+1 in ρ. We extend t by attaching t as a subtree of n in s i+1 , where s i+1 is obtained from si+1 by renaming possibly data values to account for data constraints in ψi+1.

• Otherwise, we extend t by choosing an arbitrary node n in t and attaching s i+1 as a subtree of n, where s i+1 is obtained from si+1 just as before.

Step 2 of the upper bound proof is more complicated. We start with the slightly simpler case where all state invariants γ(q) of a unary PA A are local patterns.

Suppose A = (Q, I, F, γ, ∆) is a unary PA such that all its state invariants are local patterns. Because we are concerned with the existence of local accepting runs, we assume that each transition (q, ψ, q ) in A is such that the constraint ψ(x, y) is local, i.e. ψ(x, y) contains an atomic formula child (x, y) or child -1 (x, y) or x = y. Let P A be the collection of all local patterns occurring in A.

In the following, when we mention accepting runs of A, we always mean local accepting runs. Proposition 5.9. Let A be a unary PA such that all its state invariants are local patterns and for each transition (q, ψ, q ) of A, the constraint ψ(x, y) is local. Then A can be transformed into an equivalent unary PA A1 in linear time such that all the state invariants of A1 are still local patterns, and for each transition (q, ψ, q ) of A1, the constraint ψ(x, y) is equal to x = y. By Proposition 5.9 we assume in the following that:

For every transition (q, ψ, q ) in A, ψ is equal to x = y for some variables x, y.

The algorithm to decide the existence of local accepting runs for A (for local invariants) goes as follows.

1. At first, a concept of "backbones of accepting runs" is defined and it is shown that the nonemptiness of A can be reduced to the nonemptiness of a PA A to check the existence of "accepting" backbones. Moreover, the size of A is polynomial over the size of A.

2. We show that if A is nonempty, then it accepts a data tree where every node have exponentially many children (with respect to the size of A ).

3. In addition, we prove that if A is nonempty, then A accepts a data tree containing only exponentially many data values.

4. Finally A can be seen as a TWA B over ranked (nondata) trees with exponentially many states.

Because it is known that the nonemptiness of a TWA over ranked trees can be solved in exponential time, it follows that the existence of local accepting runs of a unary PA where all the state invariants are local patterns, can be solved in doubly exponential time.

Before presenting the detailed proof, we introduce some vocabulary. Let t be a tree or data tree. We use paths and walks to distinguish between directed paths and undirected paths in t. A path from n to n in t is a sequence of nodes n1, . . . , n k in t such that n1 = n, n k = n , and for every i : 1 ≤ i < k, child (ni, ni+1) holds in t. Note that the sequence n1 . . . n k in a path of t must be non-repeating. On the other hand, a walk between n and n in t is a sequence of vertices n1, . . . , n k such that n1 = n, n k = n , and for every i : 1 ≤ i < k, child (ni, ni+1) or child (ni+1, ni) holds in t. A walk n1 . . . n k is simple if n1 . . . n k is non-repeating. It is easy to observe that for every two distinct nodes in trees or data trees, there is a unique simple walk between them.

Backbones of accepting runs

Let ρ = (q0, π0)(q0, ψ1, q1)(q1, π1) . . . (q k-1 , ψ k , q k )(q k , π k ) be an accepting run of A over a data tree t.

Let x0, x1,1, x1,2, . . . , x k-1,1 , x k-1,2 , x k be a list of variables such that ψ1 = (x0 = x1,1), ψ k = (x k-1,2 = x k ), and for every 1 < i < k, ψi = (xi-1,2 = xi,1). In addition, for every 1 ≤ i < k, let π t [xi,1, xi,2] denote the unique simple walk between πi(xi,1) and πi(xi,2) in t.

The backbone of ρ is the walk

π t [x1,1, x1,2], π t [x2,1, x2,2], . . . , π t [x k-1,1 , x k-1,2 ].
Note that in general the backbone of an accepting run is not a simple walk in t.

Roughly speaking, the backbone of an accepting run describes all the essential information of the run. Thus the nonemptiness of a local unary PA is reduced to the existence of an "accepting" backbone. We define a unary PA A = (Q , I , F , γ , ∆ ) from A as follows.

• Q = {(y, q, x) | x, y ∈ Free(γ(q))},

• I = {(y, q, x) | q ∈ I}, F = {(y, q, x) | q ∈ F },
• For every state (y, q, x) ∈ Q , the invariant γ ((y, q, x))

is defined as follows. Let first P q be the data pattern obtained from γ(q) by applying successively the following operation until no more new constraints are obtained:

if x ∼ y and y ∼ z are two atomic formulas, then x ∼ z is added, if x ∼ y and y z are two atomic formulas, then x z is added.

The invariant γ ((y, q, x)) is now defined as P q restricted to the set of nodes consisting of all ancestors of x, y in γ(q), and of all nodes on the unique simple walk between x and y in γ(q).

• ((y1, q, x1), ψ, (y2, q , x2)) ∈ ∆ if (q, ψ, q ) ∈ ∆ and ψ = (x1 = y2).

Remark 5.11. Note that each state invariant γ ((y, q, x)) in A is either a tree consisting of exactly a path (if x is the ancestor of y or vice versa), or a tree consisting of three to t and get a tree t accepted by A. Because all the state invariants of A1 are local patterns, it follows that the algorithm stated above can be used to solve the nonemptiness of A1, thus also the nonemptiness of A.

Nonemptiness for arbitrary unary PAs

Let A = (Q, I, F, γ, ∆) be a unary PA. By the arguments for the local accepting runs of unary PAs, we can first compute all tuples (q, q ) with q, q ∈ Q such that there is a local run of A from q to q over some data tree t. Actually we need a more precise computation. We say that a run ρ starts in state q at the i-th component if ρ = (q, π)(q, ψ, q1) • • • and the variable x ∈ Free(γ(q)) of ψ is mapped by π to the i-th component of γ(q). Similarly, we say that a run ends in state q at the j-th component. It is clear from the arguments for local accepting runs of unary PAs that all tuples (q, q , i, j) such that there is a data tree with a local run starting at q at the i-th component and ending at q at the j-th component, can be computed in 2Exptime. Let X be the set of all such tuples.

Similarly to the proof of Proposition 5.8, we claim that A is nonempty iff there exist tuples (q1, q 1 , i1, j1), . . . , (q k , q k , i k , j k ) in X satisfying the following:

• there exist global runs from some q0 ∈ I to q1, and from q k to some q f ∈ F ,

• for every 1 ≤ l < k, either there is a global run from q l to q l+1 , or otherwise q l = q l+1 and j l = i l+1 .

The "only if" direction is clear, since every run can be decomposed as above. For the "if" direction we show as in Proposition 5.8 how to build a data tree together with an accepting run of A. Suppose that a data tree t together with a run on t from q0 to q l have been defined. If there exists a global run from q l to q l+1 , then we proceed as before; if q l = q l+1 , then we attach a data tree t0 witnessing the local run for (q l+1 , q l+1 , i l+1 , j l+1 ) at a proper place of t according to the relative position of the j l -th component and i l+1 -th component in γ(q l ), by renaming some data values in t0 according to γ(q l ).

Lower bound

For the lower bound, we show a polynomial-time reduction from Pspace alternating Turing machines to the nonemptiness of unary PA over data trees. Then the lower bound follows from the equivalence of Exptime and APspace.

Let M be a polynomial-space alternating Turing machine and w be an input of length m. We can construct a unary PA A to simulate the computation of M on w as follows. Each configuration in the computation of M over w is encoded by a path of polynomial length m = p(m) and the computation of M over w is encoded into a tree, by representing configurations vertically.

The automaton A needs to traverse a (sub)tree representing an accepting computation tree of M. If the current configuration C is existential then A guesses a branch to go down. If C is universal, then a first guess downwards is done, and when returning to C from below, the next guess downwards needs to be done (we assume that every configuration has 0 or 2 successors, and that we see at the beginning of the encoding if it is the first or the second successor).

Suppose that from C the automaton went down into a branch corresponding to C . The automaton checks that C C as follows: going down on C it checks the i-th position of C w.r.t. the i-th position in C. Notice that the latter is the (unique) position located at distance m + 1 upwards, so this can be expressed by the state invariants and the transition constraints (formally we have a disjunction on polynomially many cases accounting for the symbols that should occur at some in C and C, respectively; this can be handled by nondeterministic transitions of A).

Remark 5.15. Over data words, we can show that the upper and lower bound match, and the nonemptiness problem of unary PA is Pspace-complete.

Moreover, if we assume that all the data tree patterns in a unary PA A are over the schema S ∼ , instead of S ∼, , then we basically have no data values, since all values can be made equal. So we have to consider TWA over unranked trees and the complexity can be shown to be Exptime-complete.

RELATED WORK

The datalog language has been studied in depth for twenty five years. The emptiness problem of datalog is decidable [START_REF] Abiteboul | Foundations of Databases[END_REF]. On the other hand, the containment problem is in general undecidable [START_REF] Shmueli | Decidability and expressiveness of logic queries[END_REF]. As already stated, decidability is obtained in two restricted settings: (i) the problem of containment of datalog programs in non-recursive datalog programs [START_REF] Chaudhuri | On the equivalence of recursive and nonrecursive datalog programs[END_REF] and (ii) the containment problem for monadic datalog programs [START_REF] Cosmadakis | Decidable optimization problems for database logic programs (preliminary report)[END_REF]. The first problem is 3Exptime-complete and the second is 2Exptime-complete. The lower bound of the second problem is proved in [START_REF] Benedikt | Monadic datalog containment[END_REF]. It is shown in [START_REF] Chaudhuri | On the complexity of equivalence between recursive and nonrecursive datalog programs[END_REF][START_REF] Benedikt | Monadic datalog containment[END_REF] that the containment for monadic datalog programs becomes more tractable under some restrictions.

Query languages over data trees have been studied for less than a decade. Some restrictions of the language XPath over unranked ordered data trees have been notably studied. In general, XPath does not allow recursive operators other than the descendant relation and restricts the use of the node equality tests. In general, the problem of the satisfiability of XPath queries is undecidable over unranked ordered data trees [START_REF] Benedikt | Xpath satisfiability in the presence of DTDs[END_REF]. Decidability for some restricted fragments of the language is shown in [START_REF] Figueira | Bottom-up automata on data trees and vertical XPath[END_REF]. Other decidable fragments of logic over data trees with restricted data value comparisons have been studied. In particular, the satisfiability of the fragment of first-order logic over data trees using only two variables is decidable [START_REF] Bojanczyk | Two-variable logic on data trees and XML reasoning[END_REF].

The language XPath can be generalized to tree pattern queries or conjunctive queries over unordered data trees that allow data equality test. [START_REF] David | Complexity of data tree patterns over XML documents[END_REF] studies some kind of tree patterns that have to be mapped to the tree by an injective homomorphism. The problem of the containment of these tree patterns with equality and inequality tests is undecidable. However it becomes decidable over bounded depth trees. The containment of conjunctive queries over unordered data trees under regular language constraints is considered in [START_REF] Björklund | Optimizing conjunctive queries over trees using schema information[END_REF]. They show the decidability of the fragment where only data value equalities are allowed and the undecidability when both data value equalities and inequalities are allowed.

Datalog over trees have been originally considered in [START_REF] Gottlob | Monadic datalog and the expressive power of languages for web information extraction[END_REF]. They show that monadic datalog over unranked ordered trees with the signature first-child, next-sibling, last-child is equivalent to monadic second order logic on the same signature. A query language based on recursive patterns is introduced in [START_REF] Abiteboul | On the equivalence of distributed systems with queries and communication[END_REF]. They show that for some restricted form of data value equalities, the problem of containment of two recursive patterns is decidable.

CONCLUSION

We have presented an in-depth study of the analysis of datalog programs over data trees. We have shown that the structure of data trees greatly complicates the problem. We have demonstrated that on the other hand, bounding the depth of the trees simplifies the problem. We have also introduced the new notion of pattern automata that roughly correspond to linear datalog programs and used them to obtain a novel decidability result in presence of data inequalities.

Some important questions remain open.

• One can consider restrictions on the use of navigational operators:

-It is proved in [START_REF] Gottlob | Monadic datalog and the expressive power of languages for web information extraction[END_REF] that monadic datalog over trees without data and MSO over trees are equivalent in absence of the relation desc. This result leads to the decidability of the containment problem for monadic datalog programs over trees using only the relation child (and not desc). The problem is still open when desc is considered. -The problem of containment of monadic datalog programs in unions of conjunctive queries over data trees is undecidable. This is for data trees with the operator desc. The question remains for programs without desc.

• One can consider restrictions on the use of data equalities. Indeed [START_REF] Abiteboul | On the equivalence of distributed systems with queries and communication[END_REF] shows that the containment problem, for a regular language of patterns with data equalities, is decidable when the use of data equalities is contrained in some manner. It would be interesting to consider analogous restrictions in the context of the containment of monadic datalog programs in unions of conjunctive queries.

• By Corollary 5.6, the emptiness problem for linear monadic datalog ∼, programs is decidable. On the other hand, by Proposition 3.1, the emptiness problem for linear binary datalog ∼, programs is undecidable over data trees. The decidability of the emptiness problem for non-linear and monadic datalog ∼, programs over data trees remains open.

Example 5 . 4

 54 We first illustrate how to transform the PA A in Example 5.2 into a datalog ∼, program P A . Then we show how to translate P A back into a (different) PA B. Using one intentional predicate for each transition, say R1, R2, R3 for respectively the transition (q0, x2 = x4, q1), (q1, x5 = x4, q1), and (q1, x5 = x7, q2), the datalog ∼, program P A for A in Example 5.2 is constructed as follows,

Figure 2 :

 2 Figure 2: Transformation from datalog ∼, to PA

Example 5 . 10

 510 The backbone of an accepting run for the PA in Example 5.2 is the (simple) walk consisting of the downward path of b-nodes. Each π t [xj,1, xj,2] is a child -edge from one b-node to the next b-node.

* This work has been partially funded by the European Research Council under the European Community's Seventh Framework Programme (FP7/2007-2013), ERC grant Webdam, agreement 226513, http://webdam.inria.fr/, by the National Natural Science Foundation of China under Grant No. 61100062 by the Engineering and Physical Sciences Research Council project "Query-Driven Data Acquisition from Web-based Datasources" (EPSRC EP/H017690/1) and by LaBRI for Zhilin Wu's visit 2012.

paths sharing a common endpoint (if neither x is the ancestor of y nor y is the ancestor of x). In the PA of Example 5.2 all invariants γ ((y, q, x)) are a single child -edge between two b-nodes.

The following lemma is shown by completing every accepting run of A to an accepting run of A. This is possible, since every matching of state invariants in A can be lifted to a matching of state invariants in A by adding subtrees. Lemma 5.12. A is nonempty iff A is nonempty.

In the following, we let r denote the maximum size of the state invariants of A .

Bounding the number of branches

We introduce some additional notations. Let

is an accepting run of A over a data tree t. By a technical argument, we can show that there exists another tree t and an accepting run ρ over t such that any node n in t has exponentially many children. The idea is to consider all simple walks π

, and modify t and ρ such that ρ has only exponentially many walks around n. For this we consider the set Dc(n) of data values occurring in ancestors of n at distance at most r, together with data values in

around n have the same (data-free) structure, contain the same values from Dc(n), and have the same data equality relation among the nodes, then we can use them, renaming some data values, in order to get a run ρ with less simple walks around n. The argument is iterated until there are only exponentially many simple walks around n. Details can be found in the extended version.

Because only the simple walks around n in ρ may visit the children of t , it follows that the arity of n in t can be assumed to be at most exponential. This argument is applied bottom-up for every node n.

From Lemma 5.13, it follows that A can be seen as a unary PA over ranked data trees of exponential arity.

In the following, we restrict our discussion to ranked data trees of exponential arity.

Bounding the number of data values

Lemma 5.14. If A is nonempty (over ranked data trees of exponential arity), then it accepts a data tree containing only exponentially many data values.

Proof. Recall that r is the maximum size of the state invariants of A . For a ranked data tree t and a node n in t, let t r n denote the subtree of t rooted at n, with all the descendants of n at distance (strictly) greater than r from n removed. The profile of t r n is the tree t r n , with the data values removed and replaced by the data value (in)equality relations ∼, (restricted to t r n ). Because all the state invariants in A are local patterns, it is not difficult to observe that if two data trees t, t of the same tree structure satisfy that for every node n, t r n and t r n have the same profile, then t is accepted by A iff t is accepted by A .

From the fact that there are at most exponentially many data values in each of those t r n (this is due to the fact that a 2 k -ary ranked tree of depth at most r has 2 O(kr) nodes), it follows that if t is a data tree accepted by A , then some data renaming can be applied bottom-up to t, and a data tree t can be obtained so that for every node n, t r n and t r n have the same profile, moreover, t contains only exponentially many data values. According to the above observation, it follows that t is accepted by A .

TWA over ranked trees

From Lemma 5.14, it follows that for the nonemptiness problem we can restrict our attention to data trees containing exponentially many data values. By viewing the exponentially many data values as additional labelings, A can be seen as a TWA B over ranked (non-data) trees. Because B needs to remember only polynomially many such labelings (data values), in order to check the data constraints in state invariants of A , it follows that B has exponentially many states.

On the other hand, it is known that the nonemptiness of TWA over ranked trees can be solved in exponential time [START_REF] Bojańczyk | Tree-walking automata[END_REF]. Thus it follows that the nonemptiness of A , thus the nonemptiness of A, can be solved in doubly exponential time.

Local runs for unary PA where state invariants are not local patterns

Finally to decide the local accepting runs of a unary PA A, we consider the slightly more general case that the state invariants of A are not necessarily local patterns. In this situation, for each state q with the state invariant P in A, there is a variable x in P such that for every transition into or out of q, if a variable y in P is used in the transition invariant of the transition, then y belongs to the same component of P as x. Therefore, for each state q with the state invariant P , we are able to first ignore the variables of P not in the same component as x and get a unary PA A1 whose state invariants are all local patterns. Moreover, it is easy to see that A is nonempty iff A1 is nonempty, since from any data tree t accepted by A1, we can append some additional subtrees