Diego Figueira

On XPath with Reflexive-Transitive Axes and Data Tests

INTRODUCTION

The simplest way of abstracting an XML document is by seeing it as a tree over a finite alphabet of tags or labels. However, this abstraction ignores all actual data stored in the document attributes. This is why there has been an increasing interest in data trees: trees that also carry data from an infinite domain. Here, we model an XML document as an unranked ordered finite tree whose every node contains a label, and a vector of data values, one for each attribute. Labels belong to some finite alphabet, and data values to some infinite domain. We call these models multi-attribute data trees (see Figure 1). We study logics on these models, that can express data properties, namely equality of attributes' data values.

Here, we show decidability of the satisfiability problem for XPath where navigation can be done going downwards, rightwards or leftwards in the XML document, that is, where navigation is done using the reflexive-transitive XPath axes descendant-or-self, following-sibling-or-self, and preceding-sibling-or-self.

Formalisms for trees with data values

Several formalisms have been studied lately in relation to static analysis on trees with data values.

First-order logic. One such formalism is FO 2 (< h , succ h , < v , succ v , ∼), first order logic with two variables, and binary relations to navigate the tree: the descendant < v , child succ v , next sibling succ h and following sibling < h (i.e., the transitive closure of succ h ); and an equivalence relation ∼ to express that two nodes of the trees have the same data value. Although the decidability status for the satisfiability problem of this logic is unknown, it is known to be as hard as the reachability problem for BVASS (Branching Vector Addition System with States) [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF]]. If the signature has only the child and next sibling relation-FO 2 (succ h , succ v , ∼)-the logic is decidable in 3NExpTime as shown in [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF]. In [START_REF] Tan | An automata model for trees with ordered data values[END_REF]] a decidable automaton model that captures (an extension of) this logic is introduced.

Automata. There have also been works on automata models for trees with data. Tree automata with registers to store and compare data values were studied in [START_REF] Kaminski | Tree automata over infinite alphabets[END_REF] as an extension to a similar model on words [START_REF] Kaminski | Finite-memory automata[END_REF][START_REF] Neven | Finite state machines for strings over infinite alphabets[END_REF]. A decidable alternating version of these automata called ATRA was studied in [START_REF] Jurdziński | Alternating automata on data trees and XPath satisfiability[END_REF], and it was extended • Diego Figueira in [Figueira 2012a] to show decidability of the satisfiability problem for forward-XPath. The work [START_REF] Bojańczyk | An extension of data automata that captures XPath[END_REF] introduces a simple yet powerful automata model called Class Automata on data trees that can capture FO 2 (< h , succ h , < v , succ v , ∼), XPath, ATRA, and other models. Although its emptiness problem is undecidable, classes of data trees for which it is decidable are studied in [START_REF] Bárány | Decidable classes of documents for XPath[END_REF]. Other formalisms include tree automata with set and linear constraints on cardinalities of sets of data values [START_REF] David | Efficient reasoning about data trees via integer linear programming[END_REF][START_REF] Tan | An automata model for trees with ordered data values[END_REF].

XPath. Here we concentrate on XPath, which is incomparable in terms of expressiveness with all the previously mentioned formalisms (except for Class Automata).

XPath is arguably the most widely used XML query language. It is implemented in XSLT and XQuery and it is used as a constituent part of several 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].

Query containment and query equivalence are important static analysis problems, which are useful to, for example, query optimization tasks. In logics closed under boolean operators-as the one treated here-, these problems reduce to checking for satisfiability: Is there a document on which a given query has a non-empty result? By answering this question we can decide at compile time whether the query contains a contradiction and thus the computation of the query (or subquery) on the document can be avoided. Or, by answering the query equivalence problem, one can test if a query can be safely replaced by another one which is more optimized in some sense (e.g., in the use of some resource). Moreover, the satisfiability problem is crucial for applications on security [START_REF] Fan | Secure XML querying with security views[END_REF]], type checking transformations [START_REF] Martens | Frontiers of tractability for typechecking simple XML transformations[END_REF], and consistency of XML specifications.

Core-XPath (term coined in [START_REF] Gottlob | Efficient algorithms for processing XPath queries[END_REF]) is the fragment of XPath 1.0 that captures all the navigational behavior of XPath. It has been well studied and its satisfiability problem is known to be decidable even in the presence of DTDs. The extension of this language with the possibility to make equality and inequality tests between attributes of elements in the XML document is named Core-Data-XPath in [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF].

In a nutshell, the important formulas of Core-Data-XPath (henceforth XPath) are of the form α@ i = β@ j , where α, β are path expressions, that navigate the tree using axes: descendant, child, ancestor, next-sibling, etc. and can make tests in intermediary nodes. Such a formula is true at a node x of a multi-attribute data tree if there are two nodes y, z in the tree that can be reached with the relations denoted by α, β respectively, so that the ith attribute of y carries the same datum as the jth attribute of z.

Unfortunately, the satisfiability problem for XPath is undecidable [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF]. How can we regain decidability for satisfiability of XPath then? We can restrict the models, or restrict the logic. The first possibility is to restrict the classes of documents in which one is interested, which is the approach taken in [START_REF] Bárány | Decidable classes of documents for XPath[END_REF]. Another, more studied, approach is to restrict the syntax, which is On XPath with Reflexive-Transitive Axes and Data Tests • 3 the one taken here. One way to regain decidability is to syntactically restrict the amount of nodes that the XPath properties can talk about. In this vein, there have been studies on fragments without negation or without transitive axes [START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF][START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF]. These fragments enjoy a small model property and are decidable. However, they cannot state global properties, involving all the nodes in an XML document. Ideally, we seek fragments with the following desirable features -closed under boolean operators, -having as much freedom as possible to navigate the tree in many directions: up, down, left, right, -having the possibility to reach any node of the tree, with transitive axes, like descendant, following sibling (the transitive closure of the next sibling axis), etc.

However, decidability results are scarce, and most fragments with the characteristics just described are undecidable. There are, however, some exceptions.

-The downward fragment of XPath, containing the child and descendant axes, is decidable, ExpTime-complete [Figueira 2012b]. -The forward fragment of XPath, extending the downward fragment with the next sibling and the following sibling axes, is decidable with non-primitive recursive complexity [Figueira 2012a]. -The vertical fragment of XPath, extending the downward fragment with the parent and ancestor axes, is decidable with non-primitive recursive complexity [START_REF] Figueira | Bottom-up automata on data trees and vertical XPath[END_REF]]. -A last example is the present work: XPath with the reflexive transitive closure of the child, next-sibling and previous-sibling relations is decidable.

All the non-primitive recursive (NPR) upper bounds of the forward and vertical fragments are also matched with NPR lower bounds. That is, there is no primitive recursive function that bounds the time or space needed by any algorithm that computes the satisfiability for any of these two logics. Moreover, it is known that any fragment of XPath containing a transitive rightward, leftward or upward axis has a satisfiability problem which is either undecidable or decidable with a NPR lower bound [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]].1 Further, as soon as we have both the rightward and leftward transitive axes, the satisfiability becomes undecidable [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. (Indeed, the downward fragment of XPath seemed to be the only one with elementary complexity up to now.)

The aforementioned hardness results make use of non-reflexive transitive relations. Surprisingly, the reductions do not seem to work when the relations are also reflexive. What is then the decidability status of the fragments of XPath with reflexive-transitive relations? This was a question raised in [START_REF] Figueira | Future-looking logics on data words and trees[END_REF].

A partial answer to this question was given in [START_REF] Figueira | A decidable two-way logic on data words[END_REF]]. There, it was shown that XPath restricted to data words is decidable in 2ExpSpace even when

• Diego Figueira we have both a reflexive-transitive future and past relations. (One can think of data words as XML documents of height 1, with only one attribute per node.) This result may seem surprising taking into account that if one of these relations is nonreflexive it is no longer decidable; and if we have only one non-reflexive transitive relation it is decidable with non-primitive recursive complexity. In [START_REF] Figueira | A decidable two-way logic on data words[END_REF]] it was shown that the satisfiability problem is in 2ExpSpace, or ExpSpace if we adopt a certain normal form of the formulas. This was a first part in our study of the computational behavior of XPath with reflexive-transitive axes. The present work corresponds to the second part, in which we study XPath on XML documents (i.e., trees) instead of words.

Contribution

We show decidability of the satisfiability for XPath with data equality tests between attributes, where navigation can be done going downwards, rightwards or leftwards in the XML document. The navigation can only be done by reflexivetransitive relations. These correspond to the XPath axes: preceding-sibling-or-self, following-sibling-or-self, and descendant-or-self axes. 2 Here we denote these axes with * ←, → * and ↓ * respectively. As already mentioned, the fact that the relations are reflexive-transitive (as opposed to just transitive) is an essential feature to achieve decidability. Given the known complexity results on XPath, this fragment seems to be in balance between navigation and complexity. This work then argues in favor of studying XPath-like logics for trees with data with reflexive-transitive relations, since they may behave computationally much better than the non-reflexive counterpart, as evidenced here.

The extension of the prior work [START_REF] Figueira | A decidable two-way logic on data words[END_REF]] on data words to work with trees with a descendant axis is not trivial, requiring an altogether different formalism and algorithm strategy. Whereas in [START_REF] Figueira | A decidable two-way logic on data words[END_REF]] the main object of study is a transition system-which comes naturally when working with words-this does not adapt well to working with trees. Instead, here we work with an algebra operating on abstractions of forests of multi-attribute data trees. Over this algebra, we prove some monotonicity properties, which are necessarily more involved than those used in [START_REF] Figueira | A decidable two-way logic on data words[END_REF]] to account for the interplay between horizontal and vertical navigation of the logic.

Our algorithm yields a 3ExpSpace upper bound for the satisfiability problem of this XPath fragment. We also show that this can be lowered to 2ExpSpace if we work with an expressive-equivalent normal form, called direct normal form. Since XPath with just one reflexive-transitive relation is already ExpSpace-hard (even when the formula is in direct normal form) by [START_REF] Figueira | A decidable two-way logic on data words[END_REF]], a gap remains between the ExpSpace lower bound and the 2ExpSpace upper bound. of data values; for simplicity in our examples we will consider D = N 0 . In general we use the symbols A, B for finite alphabets, and the symbols E and F for any kind of alphabet. By E * we denote the set of finite sequences over E, by E + the set of finite sequences over E with at least one element. We write ' ' for the empty sequence and '•' as the concatenation operator between sequences. By E k (with k ∈ N) we denote the k-tuples of elements of E, and for ā ∈ E k we write ā(i) (with 1 ≤ i ≤ k) to denote the i-th component of ā. By |S| we denote the length of S (if S is a finite sequence), or its cardinality (if S is a set). We use (a i ) i∈{j,...,j+n} as short form for a j a j+1 • • • a j+n .

PRELIMINARIES

Unranked finite trees with data. By Trees(E) we denote the set of finite ordered and unranked trees over an alphabet E. We view each position in a tree as an element of N * . Formally, we define POS ⊆ 2 N * as the set of sets of finite tree positions, such that: X ∈ POS iff (a) X ⊆ N * , |X| < ∞; (b) X is prefix-closed; and (c) if n•(i + 1) ∈ X for i ∈ N, then n•i ∈ X. A tree is then a mapping from a set of positions to labels of the alphabet Trees(E) def = {t : P → E | P ∈ POS}. The root's position is the empty string . The position of any other node in the tree is the concatenation of the position of its parent and the node's index in the ordered list of siblings.

Given a tree t ∈ Trees(E), pos(t) denotes the domain of t, which consists of the set of positions of the tree. From now on, we informally refer by 'node' to a position x together with the value t(x).

Given two trees t 1 ∈ Trees(E), t 2 ∈ Trees(F) such that pos(t 1 ) = pos(t 2 ) = P , we define t 1 ⊗ t 2 : P → (E×F) as (t 1 ⊗ t 2 )(x) def = (t 1 (x), t 2 (x)).

The set of multi-attribute data trees over a finite alphabet A of labels, k different attributes, and an infinite domain D is defined as Trees(A×D k ). Note that every tree t ∈ Trees(A×D k ) can be decomposed into two trees a ∈ Trees(A) and d ∈ Trees(D k ) such that t = a ⊗ d. Figure 1 shows an example of a multiattribute data tree. The notation for the set of data values used in a data tree is data(a ⊗ d)

def = {d(x)(i) | x ∈ pos(d), i ∈ [k]}.
With an abuse of notation we write data(X) to denote all the elements of D contained in X, for whatever object X may be.

A forest is a sequence of trees, and the set of multi-attribute data forests over A and k is (Trees(A×D k )) * . We will normally use the t to denote multiattribute data trees and t to denote forests of multi-attribute data trees. That is, t ∈ (Trees(A×D k )) * . (Note that in particular t can be an empty forest.) For any (a, d) ∈ A × D k , we write (a, d) t for the multi-attribute data tree that results from adding (a, d) as a root of t. We use t (resp. t) to denote trees (resp. forests) over a finite alphabet.

XPath. Next we define transitive XPath, the fragment of XPath where all axes are reflexive and transitive.

Transitive XPath is a two-sorted language, with path expressions (that we write α, β, γ, δ) and node expressions (that we write ϕ, ψ, η). Path expressions denote binary relations, resulting from composing the descendant, ancestor, preceding sibling and following sibling relations (which are denoted respectively by ↓ * , ↑ * , * ←, → * respectively), and node expressions. Node expressions are boolean formulas

• Diego Figueira a @ :
1 5 @ : 2 8 b @ : 1 5 @ : 2 3 a @ : 1 4 @ : 2 8 b @ : 1 2 @ : 2 8 a @ : 1 5 @ : 2 3 c @ : 1 5 @ : 2 3 b @ : 1 9 @ : 2 2 a @ : 1 5 @ : 2 5 c @ : 1 2 @ : 2 7 c @ : 1 9 @ : that test a property of a node. For example, they can test that the node has a certain label, or that it has a descendant labeled a with the same data value in attribute 1 as the attribute 2 of an ancestor labeled b, which is expressed by

↓ * [a]@ 1 = ↑ * [b]@ 2 .
As another example, we can select the nodes that have a sibling labeled a to the left whose first attribute is the same as the second attribute of some descendant of a right sibling by the formula

φ = * ←[a]@ 1 = → * ↓ * @ 2 . A formula of XPath(↓ * , ↑ * , → * , * ←, =
) is either a node expression or a path expression of the logic. Its syntax and semantics are defined in Figure 2. Given a tree t as in Figure 1, we have In the case of XPath( * ←, ↓ * , → * , =), we also extend the evaluation to multiattribute data forests. Let (a, d) be an arbitrary fix element of A × D k . Given a forest t and x, y ∈ pos((a, d) t), x, y = , we define the satisfaction relation |=, as t, x |= ϕ (resp. t, (x, y) |= α) if (a, d) t, x |= ϕ (resp. (a, d) t, (x, y) |= α). (Note that since XPath( * ←, ↓ * , → * , =) has no ascending axes, whether t, x |= ϕ or not does not depend on (a, d), we use it as a simple way of defining its semantics.)

The satisfiability problem for XPath(O, =) (henceforth SAT-XPath(O, =)) is the problem of, given a formula ϕ of XPath(O, =), wether there exists a multiattribute data tree t such that t |= ϕ.

PROOF SKETCH

The main contribution of this paper is the following.

Theorem 3.1. SAT-XPath( * ←, ↓ * , → * , =) is decidable in 3 ExpSpace.
We reduce the problem of whether a formula ϕ of our logic XPath( * ←, ↓ * , → * , =) is satisfiable, to the problem of whether one can obtain an element with a certain property by repeated applications of operations in some algebra, starting from a basic set of elements. We call it the derivation problem. First we introduce the algebra (Section 4), we then solve the derivation problem (Section 5) and finally we show the reduction from the logic into the derivation problem (Section 6).

On XPath with Reflexive-Transitive Axes and Data Tests

• 7 α, β ::= o | [ϕ] | αβ o ∈ {ε, ↓ * , ↑ * , → * , * ←}, ϕ, ψ ::= a | ¬ϕ | ϕ ∧ ψ | ϕ ∨ ψ | α | α@i = β@j | α@i = β@j a ∈ A, i, j ∈ [k]. [[↓ * ]] t = {(x, x•i) | x•i ∈ pos(t)} * [[↑ * ]] t = {(x•i, x) | x•i ∈ pos(t)} * [[→ * ]] t = {(x•i, x•(i + 1)) | x•i, x•(i + 1) ∈ pos(t)} * [[ * ←]] t = {(x•(i + 1), x•i) | x•i, x•(i + 1) ∈ pos(t)} * [[ε]] t = {(x, x) | x ∈ pos(t)} [[αβ]] t = {(x, z) | there exists y such that (x, y) ∈ [[α]] t , (y, z) ∈ [[β]] t } [[[ϕ]]] t = {(x, x) ∈| x ∈ pos(t), x ∈ [[ϕ]] t } [[a]] t = {x ∈ pos(t) | a(x) = a} [[ α ]] t = {x ∈ pos(t) | ∃y.(x, y) ∈ [[α]] t } [[¬ϕ]] t = pos(t) \ [[ϕ]] t [[ϕ ∧ ψ]] t = [[ϕ]] t ∩ [[ψ]] t [[ϕ ∨ ψ]] t = [[ϕ]] t ∪ [[ψ]] t [[ α@i=β@j ]] t = {x ∈ pos(t) | ∃y,z (x, y) ∈ [[α]] t , (x, z) ∈ [[β]] t , d(y)(i) = d(z)(j)} [[ α@i =β@j ]] t = {x ∈ pos(t) | ∃y,z (x, y) ∈ [[α]] t , (x, z) ∈ [[β]] t , d(y)(i) = d(z)(j)}
Fig. 2. The syntax of transitive XPath; and its semantics for a multi-attribute data tree t = a ⊗ d. b @ : 1 5 @ : 2 3 a @ : 1 4 @ : 2 8 b @ : 1 2 @ : 2 8 a @ : 1 5 @ : 2 3 c @ : 1 5 @ : 2 3 b @ : 1 9 @ : 2 2 a @ : 1 5 @ : 2 5 c @ : 1 2 @ : 2 7 c @ : 1 9 @ : 2 4 b @ : 1 5 @ : 2 3 a @ : 1 4 @ : 2 8 b @ : 1 2 @ : 2 8 a @ : 1 5 @ : 2 3 c @ : 1 5 @ : 2 5 b @ : 1 9 @ : 2 2 a @ : 1 5 @ : 2 3 c @ : 1 2 @ : 2 7 c @ : 1 9 @ : 2 4

Figure 2: A forest profile.

INTRO

We are interested in reasoning on XML documents. Where XML document is considered not just a mere squeleton of the node types, but with the actual data. We study hierarchically structured data. It is a tree whose every node contains: a letter from a finite alphabet, and a data value from an infinite domain for each attribute.

TRANSITIVE XPATH

Theorem 1. Full transitive XPath is non primitive recursive.

Proof. We prove this by using the results of [FS09]. There, it is shown that XPath with one non-reflexive functional transitive axis is enough to prove non-primitive recursiveness. Here, however, we feature reflexive-transitive axes instead of only transitive. Therefore, in principle we cannot use this result. However, note that we can code

↑ + with → * [a]↑ * [¬a].
Theorem 2. Non-ascending transitive XPath is decidable in 2NEXPSPACE.

Theorem 3. Non-ascending direct transitive XPath is decidable in NEXPSPACE.

FOREST PROFILES

x ↓ i x ↓ e x ↓ i x ↓ e
We define abstractions of forests of multi-attribute trees.

↓ e , χ ↓ i , χ ↓ i , left/right exteri use χ to denote χ ∈ { χ ↓ e , χ ↓ i , χ ↓ i χ(d) def = χ(d) def = We define data( call data(f) \ R We say that d so that χ ↓ e (α (α, β, i) ∈ Π, is profiles.
The set of ro b @ : 1 5 @ : 2 3 a @ : 1 4 @ : 2 8 b @ : 1 2 @ : 2 8 a @ : 1 5 @ : 2 3 c @ : 1 5 @ : 2 5 b @ : 1 9 @ : 2 2 a @ : 1 5 @ : 2 3 c @ : 1 2 @ : 2 7 c @ : 1 9 @ : 2 4

Figure 2: A forest profile.

INTRO

We are interested in reasoning on XML documents. Where XML document is considered not just a mere squeleton of the node types, but with the actual data. We study hierarchically structured data. It is a tree whose every node contains: a letter from a finite alphabet, and a data value from an infinite domain for each attribute.

TRANSITIVE XPATH

Theorem 1. Full transitive XPath is non primitive recursive.

Proof. We prove this by using the results of [FS09]. There, it is shown that XPath with one non-reflexive functional transitive axis is enough to prove non-primitive recursiveness. Here, however, we feature reflexive-transitive axes instead of only transitive. Therefore, in principle we cannot use this result. However, note that we can code

↑ + with → * [a]↑ * [¬a].
Theorem 2. Non-ascending transitive XPath is decidable in 2NEXPSPACE.

Theorem 3. Non-ascending direct transitive XPath is decidable in NEXPSPACE.

FOREST PROFILES

x ↓ i x ↓ e x ↓ i x ↓ e
We define abstractions of forests of multi-attribute trees. These are called forest profiles. They are the main object outside the forest.

Let A be a finite alphabet of lette the set of root letters, and let D be data values. The set B(A) is the bool any a ∈ A and ψ ∈ B(A), we write a tation assigning true to a, and false t satisfies ψ. Let k be a fixed natural nu ber of attributes at each node. We s attribute index. We define the set of nite, subword-closed, reversal-closed, su we denote it by P. We generally use th to denote patterns. For every letter a ∈ lowing set of patterns σa ⊆ P

σa def = {ψ1 • • • ψ k ∈ P | a |= ψ1
Note that ε ∈ σa. We define the set of c as Π def = (P \ {ε}) × P × the intended meaning is that the first on the sibligns, the second on a down third retrieves a data value from an at A forest profile f is a tuple

f def = (χ ↓ e , χ ↓ i , χ ↓ i , χ
↓ e , χ ↓ χ ∈ { χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e }, we define χ(d) def = {(α, β, i) ∈ Π | (d, α, β, χ(d) def = ( χ ↓ e (d), χ ↓ i (d), χ ↓ i (d), χ
We define data(f)

def = R ∪ {d ∈ D | χ(d call data(f) \ R the set of flexible val
We say that a forest profile f = (χ,

d so that χ ↓ e (α, β, i) = {d} or χ ↓ e (α, (α, β, i) ∈ Π, is in R. We define F a profiles.
The set of root patterns of a forest b @ : 1 5 @ : 2 3 a @ : 1 4 @ : 2 8 b @ : 1 2 @ : 2 8 a @ : 1 5 @ : 2 3 c @ : 1 5 @ : 2 5 b @ : 1 9 @ : 2 2 a @ : 1 5 @ : 2 3 c @ : 1 2 @ : 2 7 c @ : 1 9 @ : 2 4

Figure 2: A forest profile.

INTRO

We are interested in reasoning on XML documents. Where XML document is considered not just a mere squeleton of the node types, but with the actual data. We study hierarchically structured data. It is a tree whose every node contains: a letter from a finite alphabet, and a data value from an infinite domain for each attribute.

TRANSITIVE XPATH

Theorem 1. Full transitive XPath is non primitive recursive.

Proof. We prove this by using the results of [FS09]. There, it is shown that XPath with one non-reflexive functional transitive axis is enough to prove non-primitive recursiveness. Here, however, we feature reflexive-transitive axes instead of only transitive. Therefore, in principle we cannot use this result. However, note that we can code

↑ + with → * [a]↑ * [¬a].
Theorem 2. Non-ascending transitive XPath is decidable in 2NEXPSPACE.

Theorem 3. Non-ascending direct transitive XPath is decidable in NEXPSPACE.

FOREST PROFILES

x ↓ i x ↓ e x ↓ i x ↓ e
We define abstractions of forests of multi-attribute trees. These are called forest profiles. They are the main object outside the forest.

Let A be a finite alphabet of lett the set of root letters, and let D b data values. The set B(A) is the bo any a ∈ A and ψ ∈ B(A), we write tation assigning true to a, and false satisfies ψ. Let k be a fixed natural ber of attributes at each node. We attribute index. We define the set nite, subword-closed, reversal-closed, we denote it by P. We generally use t to denote patterns. For every letter a lowing set of patterns σa ⊆ P

σa def = {ψ1 • • • ψ k ∈ P | a |= ψ
Note that ε ∈ σa. We define the set of as Π def = (P \ {ε}) × P the intended meaning is that the fir on the sibligns, the second on a dow third retrieves a data value from an a A forest profile f is a tuple

f def = (χ ↓ e , χ ↓ i , χ ↓ i , χ
where R ⊆ D, and we call it the set and χ

↓ e , χ ↓ i , χ ↓ i , χ ↓ e ⊆ D × Π,
↓ e , χ ∈ { χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e }, we define χ(d) def = {(α, β, i) ∈ Π | (d, α, χ(d) def = ( χ ↓ e (d), χ ↓ i (d), χ ↓ i (d),
We define data(f)

def = R ∪ {d ∈ D | χ call data(f) \ R the set of flexible va
We say that a forest profile f = (

d so that χ ↓ e (α, β, i) = {d} or χ ↓ e (α (α, β, i) ∈ Π, is in R. We define F profiles.
The set of root patterns of a fore b @ : 1 5 @ : 2 3 a @ : 1 4 @ : 2 8 b @ : 1 2 @ : 2 8 a @ : 1 5 @ : 2 3 c @ : 1 5 @ : 2 5 b @ : 1 9 @ : 2 2 a @ : 1 5 @ : 2 3 c @ : 1 2 @ : 2 7 c @ : 1 9 @ : 2 4

Figure 2: A forest profile.

INTRO

We are interested in reasoning on XML documents. Where XML document is considered not just a mere squeleton of the node types, but with the actual data. We study hierarchically structured data. It is a tree whose every node contains: a letter from a finite alphabet, and a data value from an infinite domain for each attribute.

TRANSITIVE XPATH

Theorem 1. Full transitive XPath is non primitive recursive.

Proof. We prove this by using the results of [FS09]. There, it is shown that XPath with one non-reflexive functional transitive axis is enough to prove non-primitive recursiveness. Here, however, we feature reflexive-transitive axes instead of only transitive. Therefore, in principle we cannot use this result. However, note that we can code

↑ + with → * [a]↑ * [¬a].
Theorem 2. Non-ascending transitive XPath is decidable in 2NEXPSPACE.

Theorem 3. Non-ascending direct transitive XPath is decidable in NEXPSPACE.

FOREST PROFILES

x ↓ i x ↓ e x ↓ i x ↓ e
We define abstractions of forests of multi-attribute trees. These are called forest profiles. They are the main object outside the forest.

Let A be a finite alphab the set of root letters, an data values. The set B(A any a ∈ A and ψ ∈ B(A), tation assigning true to a, satisfies ψ. Let k be a fixe ber of attributes at each attribute index. We defin nite, subword-closed, revers we denote it by P. We gene to denote patterns. For eve lowing set of patterns σa ⊆

σa def = {ψ1 • • • ψ k ∈ Note that ε ∈ σa. We defin as Π def = (P \
the intended meaning is th on the sibligns, the second third retrieves a data value A forest profile f is a t

f def = (χ ↓ e
where R ⊆ D, and we call and χ

↓ e , χ ↓ i , χ ↓ i , χ ↓ e ⊆ D × left/right exterior/interior use χ to denote the quadr χ ∈ { χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e }, we d χ(d) def = {(α, β, i) ∈ χ(d) def = ( χ ↓ e (d), χ ↓ i We define data(f) def = R ∪ { call data(f) \ R the set of fl
We say that a forest pr d so that χ ↓ e (α,

β, i) = {d (α, β, i) ∈ Π, is in R. We profiles.
The set of root pattern Fig. 3. A multi-attribute data forest, with its left and right forests.

We first introduce forest profiles in Section 4, which constitute the algebra domain. A forest profile is an abstraction of a multi-attribute data forest inside a context, where the context consists of the two (possibly empty) forests that are to the left and to the right. Figure 3 depicts one such possible forest, together with the left and right context forests. Intuitively, the forest profile consists of all the path expressions that can reach a data value d, for every d ∈ D. That is, assuming D = {d 1 , d 2 , . . . }, the forest profile can be thought of an infinite vector whose i-th component contains the set of all path expressions α so that there is some node y reached through α from a root to y, sot that y carries the data value d i . Note that • Diego Figueira there are two sources of infinity here: the dimension of the vector, and the sets of path expressions. However, since we are working with finite trees, only finitely many components will have a set different from ∅. On the other hand, we will limit ourselves to path expressions from a finite set (i.e., basically the set of subexpressions of the formula φ we want to satify). We assume these path expressions to have a very simple navigation: they go first to the right and then down (a navigation to which we will refer with the symbol ' ↓ '), or first left and then down (' ↓ ').

More concretely, a forest profile contains, for each data value d and each path expression of interest, the information of whether d can be reached by the path expression, and where it can be reached, either -inside the main forest, starting from the leftmost root by going first right and then down (the node x ↓ i in Figure 3, where i stands for 'internal' to the abstracted forest), -inside the main forest but starting with the rightmost root by going first left and then down (the node x ↓ i in Figure 3), -in the left context forest by going first left and then down (starting from the node x ↓ e in Figure 3, where e stands for 'external' to the abstracted forest), or -in the right context forest by going first right and then down (starting from the node x ↓ e in Figure 3).

In this setting, path expressions are called patterns and their navigation is greatly simplified. As already mentioned, patterns can go first to the left, and then down, or first to the right and then down (or only down, only left, only right). Furthermore, node expressions contained in patterns are simple boolean combinations of tests for labels (i.e., no nesting is of path expressions is allowed). They correspond to path expressions3 like, for example,

→ * [a]→ * [b]↓ * [c]↓ * [a ∨ b]@ 1 , or * ←[¬a]↓ * [a]@ 2 .
A forest profile also keeps track of a set of important data values called the rigid values. These are data values that play a determined function in the forest containing the abstracted forest (i.e., in the concatenation of the left, main and right forests). Intuitively, a data value is rigid in a forest if it can be pinpointed by a path expression, in the sense that it is the only data value that can be reached with some pattern expression α from a root of the forest. For example, if our finite set of patterns is {→ * ↓ * [c]@ 2 , ↓ * [a]@ 2 }, then in the example of Figure 3, we have that 8, 5, 3 are rigid values since they are the only values reachable through ↓ * [a]@ 2 from the second, third and fourth roots respectively (counting from left to right); we also have that 4 is a rigid value since it is the only data value reachable through → * ↓ * [c]@ 2 from the fifth root. However, 7 is not a rigid value, because although it can be reached through → * ↓ * [c]@ 2 from the first root, other data values (namely 3 and 4) can also be reached from that root with the same pattern. At this level of detail, we just mention that some special care must be taken for these rigid data values.

We equip the set of forest profiles with two operations, one that corresponds to concatenating two of the forests being abstracted, and another operation that On XPath with Reflexive-Transitive Axes and Data Tests • 9 corresponds to adding a root to the forest, converting it into a tree. This algebra is introduced in Section 4.2. In particular, the root operation is restricted to work only with forest profiles that are from a certain set of consistent profiles. Consistent profiles will play an important role in the reduction from the logic to the algebra. The idea is that they are those profiles that are not in contradiction with the formula ϕ to test for satisfiability, and therefore that could abstract subforests of a model of ϕ.

A root profile, is a profile that comes from the application of the root operation with a certain label of a certain alphabet A root of root labels. An empty profile is the profile corresponding to the empty forest with an empty context. In Section 5 we define the derivation problem for forest profiles as the problem of whether there is a way of obtaining a root profile from the empty profile by repeated applications of the algebra operations.

We show that the derivation problem is decidable in 2ExpSpace in Section 5. We first define a quasi-ordering on profiles in Section 5.2, this ordering will be of chief importance in our decidability result. We show a series of monotonicity properties that show that the set of derivable profiles is upward-closed. The purpose of the quasi-ordering is to reduce the derivation problem on the infinite set of forest profiles into a problem on a finite set of minimal profiles. The fact that the derivable profiles is upward-closed is indeed a key ingredient for this reduction to work.

However, one problem we need to face is that the ordering has infinite antichains: every two profiles with different set of rigid values are incomparable. We tackle this in Section 5.4, where we show that we can bound the set of rigid values, obtaining an equivalent derivation problem on profiles with a small set of rigid values. Once we obtain this bound, the set of minimal profiles becomes finite, doubly exponential. Next, in Section 5.5 we show that, thanks to the monotonicity properties enjoyed by the algebra, we can work only with minimal elements. Finally, in Section 5.6 we give the concrete saturation-style algorithm that solves the derivation problem using doubly exponential space.

In Section 6 we show that the satisfiability problem for XPath( * ←, ↓ * , → * , =) can be reduced to the derivation problem in ExpSpace. In Section 6.1 we show a normal form, called direct unnested normal form, where direct unnested path expressions correspond, precisely, to the pattern expressions used in the forest profiles (basically all path expressions are of the form already described). We then show in Section 6.2 that one can reduce, in ExpSpace, the satisfiability problem for formulas in this normal form into the derivation problem, and therefore we obtain a 3ExpSpace decidability procedure for SAT-XPath( * ←, ↓ * , → * , =), proving Theorem 3.1.

FOREST PROFILES

We define abstractions of forests of multi-attribute data trees. These are called forest profiles. They are the main construct in our solution. One must think of a forest profile as the description, for every data value d ∈ D, of all the possible ways of reaching the data value d via path expressions of XPath( * ←, ↓ * , → * , =). Some ways of reaching the data value may lie inside the forest being abstracted, and some outside the forest. For every forest we identify 4 nodes: the leftmost root, the rightmost root, the node to the left of the leftmost root (if any), and the • Diego Figueira node to the right of the rightmost root (if any). Take for instance the forest in the middle of Figure 3. These are the nodes identified by x ↓ i , x ↓ i , x ↓ e , x ↓ e respectively in the figure. The profile of this forest is represented by all the paths that can reach the data value 4 (i.e., so that there is a node reached through the path with data value 4), all those that can reach 2, etc. Take as an example the data value 5; this data value can be reached by

(path 1 ) → * [a]@ 1 from x ↓ e , ( path
2 ) * ←[b]↓ * [a]@ 1 from x ↓ i , ( path
3 ) → * [a]→ * [b]↓ * [c]@ 1 from x ↓ i , etc.
Remember that expressions are evaluated in a forest and, for example, an expression starting with → * denotes the possibility to move forward in the sequence of tree roots of the forest. The idea is that we limit ourselves that whenever there are paths departing from x ↓ i or x ↓ i they must be internal to the forest (i.e., internal to the gray forest in Figure 3), like the examples (path 2 ) and (path 3 ); and whenever there are paths from x ↓ e or x ↓ e they must be external to the forest (i.e., either in the forest depicted to the left or to the right of the gray forest in Figure 3), like the example (path 1 ). Thus, in the notation we use, the i in x ↓ i , x ↓ i stands for the fact that the nodes are internal to the forest, and the e in x ↓ e , x ↓ e stands for the fact that the nodes are external. Further, the ↓ notation of x ↓ i , x ↓ e stands for being the reference nodes from which to consider paths going right and down, or right, or down; whereas the ↓ notation of x ↓ i , x ↓ e are the nodes from which we consider the paths going left and down, or left, or down. This symbology will be used in the sequel.

Let A be a finite alphabet of labels, let A root ⊆ A be the set of root labels (containing the labels that the roots can have), and let D be an infinite domain of data values. The set B(A) is the boolean closure of tests for labels from A. For any a ∈ A and ψ ∈ B(A), we write a |= ψ if the interpretation assigning true to a, and false to every other b ∈ A, satisfies ψ. Let k ∈ N be a fixed natural number, corresponding to the number of attributes at each node. We say that i ∈ [k] is an attribute index. Let P be a finite, subword-closed, subset of (B(A)) * . We call P the set of patterns. We generally use the symbols α, β, γ, δ ∈ P to denote patterns. For every label a ∈ A we define the following set of patterns σ a ⊆ P

σ a def = {ψ 1 • • • ψ k ∈ P | a |= ψ 1 ∧ • • • ∧ ψ k }. Note that ∈ σ a . For example, if P = { , ¬b, b, c ∨ a, c, (¬b)•b, (¬b)•(c ∨ a)} then σ a = { , ¬b, c ∨ a, (¬b)•(c ∨ a)}. The set of composed patterns is Π def = (P \ { }) × P × [k].
The intended meaning is that the first component operates on the siblings, the second on a downward path, and the third retrieves a data value from an attribute index. We will sometimes use the symbol ᾱ to represent elements from Π, or (α, β, i) if we need to make explicit the components of the composed pattern. A composed pattern (ψ

1 • • • ψ k , ψ 1 • • • ψ t , i) abstracts the path expression → * [ψ 1 ]→ * • • • → * [ψ k ]↓ * [ψ 1 ]↓ * • • • ↓ * [ψ t ]@ i or ( ↓ )
On XPath with Reflexive-Transitive Axes and Data Tests

• 11 * ←[ψ 1 ] * ← • • • * ←[ψ k ]↓ * [ψ 1 ]↓ * • • • ↓ * [ψ t ]@ i ( ↓ )
depending on the context. The idea is that through a composed pattern like, for example, (a•(¬a)•b, (c ∨ a), 2) we can reach to the right (i.e., via the interpretation ( ↓ )) the data value 3 from the node x ↓ i in the forest of Figure 3. Also, note that from a node x labeled a, we can reach x's attribute i through any (α, β, i) ∈ σ a × σ a × [k] (independently of going left or right).

A forest profile f is a tuple

f = ( χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e , R)
where R ⊆ D, and we call it the set of rigid values of f, and χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e ⊆ D×Π, and we call them the set of left/right external/internal descriptions respectively. Composed patterns in χ ↓ e , χ ↓ i can be thought of as path expressions according to ( ↓ ), and composed patterns in χ ↓ e , χ ↓ i as path expressions according to ( ↓ ). In the previous example (on page 10), one shall interpret (path 1 ) as the fact that (5, a, , 1) ∈ χ ↓ e , (path 2 ) as (5, b, a, 1) ∈ χ ↓ i and (path 3 ) as (5, a•b, c, 1) ∈ χ ↓ i . We use χ to denote a subset of D × Π; and we write χ (resp. χi ) to denote the 4-tuple

( χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e ) (resp. ( χ ↓ e i , χ ↓ i i , χ ↓ i i , χ ↓ e i )). Likewise, we use f (resp. f i ) to denote ( χ, R) (resp. ( χi , R i )).
We define, for every χ, χ

↓ e , χ ↓ i , χ ↓ i , χ ↓ e ⊆ D × Π, d ∈ D, α, β ∈ P and i ∈ [k], χ(d) def = {(α, β, i) ∈ Π | (d, α, β, i) ∈ χ}, χ(α, β, i) def = {d ∈ D | (d, α, β, i) ∈ χ}, and
( χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e )(d) def = ( χ ↓ e (d), χ ↓ i (d), χ ↓ i (d), χ ↓ e (d)).
We define data(f)

def = R ∪ {d ∈ D | χ(d) = (∅, ∅, ∅, ∅)}.
We call data(f) \ R the set of flexible values of f. We use the symbol π to denote ( π

↓ e , π ↓ i , π ↓ i , π ↓ e ) where π ↓ e , π ↓ i , π ↓ i , π ↓ e ⊆ Π.
We further say that π is the description of d ∈ D in f if χ(d) = π.

Rigid and flexible values

In a forest satisfying some XPath formula, different data values have different roles. We distinguish here two categories of data values: rigid and flexible. Rigid data values are important for the satisfaction of the formula and special care is needed to treat these, whereas flexible values are not crucial, and they can be sometimes removed from the tree. Let us give some more precise intuition. We use the logic XPath to make this intuition clear, but we will then state the definitions in terms of forest profiles.

Given a multi-attribute data forest t and i ∈ N where t, i |= ϕ, suppose there is a data value d such that: there is some position 1 ≤ j ≤ | t| and some path expression α inside ϕ of the form α = → * β@ k or α = * ← β@ k so that d is the only data value that can be reached through α from the j-th root of the forest. When there is such a d we call it a rigid value for j, since the logic can identify it and pinpoint it from the rest of the data values. If d is rigid for at least one position j ∈ {1, . . . , | t|} we say that d is rigid for t. All the remaining data values d of t (which are the flexible values) have the property that for any path α and position j, if d is reachable from position j through α, then there is also some other flexible value d that is also reachabe from j through α. Therefore, the logic cannot tell these data values apart. In particular, assuming t is a forest satisfying ϕ and containing d as a flexible value, consider t as the result of replacing, for some fresh data value d , every tree t of t with the forest t •(t [d → d ]), where t [d → d ] is the result of replacing the data value d with d in t , and leaving all the structures and labels as they were. Indeed, t will continue to satisfy ϕ; but this is not necessarily true if d was a rigid value. The idea is that since the logic can only test whether there are 0, 1 or more than one data values reachable by some path expression, whether there are n > 1 data values reachable (as in t) or n + 1 makes no difference at all. This is why t still satisfies ϕ. The same notions hold for our algebra on forest profiles. The fact that if t verifies a property of our logic then so does t is a key property that we need to exploit; hence, we need to make explicit the set of rigid values of any given profile. We formalize this by defining an ordering on profiles corresponding to the operation just described, so that the forest profile abstracting t is bigger than the profile abstracting t. We make explicit (in Lemma 5.5) the aforementioned argument as a monotonicity property of the algebra.

We say that a forest profile

f = ( χ, R) is valid if R contains all d ∈ D so that χ ↓ e (α, β, i) = {d} or χ ↓ e (α, β, i) = {d} for some (α, β, i) ∈ Π. Note that R may
contain more data values than those that are accessible only through one pattern.

Intuitively, this is because there could be other rigid values that are manifested as such in the profiles corresponding to other positions of the data forest we will be trying to build. We define F as the set of all valid profiles.

Algebra

We equip F with two operations. The idea is that these operations correspond to the concatenation of two forests, and to the addition of a root to a forest (called rooting), turning it into a tree.

Preliminaries. The set of root patterns of a forest profile f, denoted by

[f] →, → [f] ⊆ P is defined as follows [f] → def = {α | (d, α, β, i) ∈ χ ↓ i for some d, β, i}, → [f] def = {α | (d, α, β, i) ∈ χ ↓ i for some d, β, i}.
The idea is that [f] → has all the patterns that "go through f", in the sense that verify the labels of the roots of the forest abstracted by f. For example, if f abstracts the forest of Figure 3 and if

P = {a, b, a•a, a•b, b•b, b•a}, then [f] → will contain a, b, a•b, b•b, a•a, but it will certainly not have b•a.
Given P ⊆ P and χ ⊆ D × Π, we define the extension of χ by P , denoted by P •χ, as the set

P •χ def = χ ∪ {(d, α • α, β, i) ∈ D × Π | (d, α, β, i) ∈ χ, α ∈ P }
It is easy to see that the extension operation distributes over union. (2 ) (P ∪ P )•χ = P •χ ∪ P •χ.

We defer the proof of this lemma to the Appendix.

Fingerprints. We now define the fingerprint of a forest profile. It contains a summary information, sufficient to decide whether the tree abstracted by the profile satisfies a formula of XPath-as we show in Section 6.

Let

A = { • ↓ , • ↓ , • ↓ , •}. Given a profile f = ( χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e , R) ∈ F and z ∈ A, we define the set f.χ z as -χ ↓ i ∪ → [f]• χ ↓ e if z = • ↓ , -χ ↓ i ∪ [f] →• χ ↓ e if z = • ↓ , -{(d, α , β, i) ∈ D × Π | ∃α.(d, α, β, i) ∈ χ ↓ i ∪ χ ↓ i } if z = • ↓ , or -{(d, α, β, i) ∈ χ ↓ i ∪ χ ↓ i | β = } if z = •.
Note that f.χ z (α, β, i) is independent of α when z = • ↓ , but it takes an element of Π as argument for the sake of uniformity of notation. The idea here is that f.χ • ↓ contains the data values and patterns inside the forest that f abstracts starting from any root of the forest (here α should be disregarded, the only part of the path important is β, i); f.χ • contains the data values (with its descriptions) that can be found at the root of the forest starting from any root (i.e., navigating horizontally); f.χ • ↓ the data values that can be found going right and down from the first root of the forest (i.e., the node x ↓ i in Figure 3), which can be inside the forest or in the right context forest; and f.χ • ↓ the data values taht can be found going left and down from the last root of the forest (i.e., the node x ↓ i in Figure 3).

The fingerprint of a profile f, noted ξ(f), is an element of

F def = (Π × A ∪ Π × A × Π × A) → {0, 1, 1+, 2+},
where for ᾱ, ᾱ ∈ Π, z, z ∈ A, we define ξ(f)(ᾱ, z, ᾱ , z ) as 0 or 1+ depending on whether |f.χ z (ᾱ) ∩ f.χ z ( ᾱ )| = 0 or not; and we define ξ(f)( ᾱ, z) as 0, 1, or 2+ depending on |f.χ z (ᾱ)| being 0, 1 or greater than 1 respectively. Intuitively, the fingerprint is related to what formulas of our logic are true at the forest that f abstract. For example, a formula α = β ∧ ¬ α = β (saying "there is exactly one data value reachable simultaneously by α and β") will be related with |f.χ z ( ᾱ) ∩ f.χ z (ᾱ )| = 1 for suitable ᾱ, ᾱ , z, z ; and a formula α = α (saying "there are two distinct data values reachable by α") will be related with |f.χ z (ᾱ)| ≥ 2 suitable ᾱ, z.

The precise relations will become clear in Section 6.2, through a strong normal form of the logic. Let us fix a set Γ ⊆ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider Γ as a given arbitrary set of fingerprints.

Concatenation. For every two

f 1 , f 2 ∈ F (recall, f i = ( χ ↓ e i , χ ↓ i i , χ ↓ i i , χ ↓ e i , R i )) so that (a) R 1 = R 2 ,
• Diego Figueira abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e
2 , and (c)

# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e
2 , and (c)

# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e
2 , and (c)

# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e
2 , and (c)

# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

The fingerprint of a profile f, noted ⇠(f), is an element of

F def = (⇧ ⇥ A [ ⇧ ⇥ A ⇥ ⇧ ⇥ A) ! {0, 1, 1+, 2+},
where for ↵, ↵0 2 ⇧, z, z 0 2 A, we define ⇠(f)(↵, z, ↵0 , z 0 ) as 0 or 1+ depending on whether |f. z (↵) \ f. z 0 (↵ 0 )| = 0 or not; and we define ⇠(f)( ↵, z) as 0, 1, or 2+ depending on |f. z (↵)| being 0, 1 or greater than 1 respectively. 5 Intuitively, the fingerprint is related to what formulas of our logic are true at the forest that f abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints.

xxx and(c)

f 1 f 2 f 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

The fingerprint of a profile f, noted ⇠(f), is an element of

F def = (⇧ ⇥ A [ ⇧ ⇥ A ⇥ ⇧ ⇥ A) ! {0, 1, 1+, 2+},
where for ↵, ↵0 2 ⇧, z, z 0 2 A, we define ⇠(f)(↵, z, ↵0 , z 0 ) as 0 or 1+ depending on whether |f. z (↵) \ f. z 0 (↵ 0 )| = 0 or not; and we define ⇠(f)( ↵, z) as 0, 1, or 2+ depending on |f. z (↵)| being 0, 1 or greater than 1 respectively. 5 Intuitively, the fingerprint is related to what formulas of our logic are true at the forest that f abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints.

xxx and(c)

f 1 f 2 f 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

going left and down from the last root of the forest (i.e., the node x # i in Figure 3).

The fingerprint of a profile f, noted ⇠(f), is an element of

F def = (⇧ ⇥ A [ ⇧ ⇥ A ⇥ ⇧ ⇥ A) ! {0, 1, 1+, 2+},
where for ↵, ↵0 2 ⇧, z, z 0 2 A, we define ⇠(f)(↵, z, ↵0 , z 0 ) as 0 or 1+ depending on whether |f. z (↵) \ f. z 0 (↵ 0 )| = 0 or not; and we define ⇠(f)( ↵, z) as 0, 1, or 2+ depending on |f. z (↵)| being 0, 1 or greater than 1 respectively. 5 Intuitively, the fingerprint is related to what formulas of our logic are true at the forest that f abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z.

The precise relations will become clear in Section 6.2, through a strong normal form of the logic. Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints.

xxx and(c)

f 1 f 2 f 3 = f 1 + f 2 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

Fig. 4. Assuming we have two consecutive forests abstracted by f 1 , f 2 , the idea is that we obtain f 3 = f 1 + f 2 as the abstraction corresponding to the concatenation of these forests.

(b) χ ↓ e 1 = χ ↓ i 2 ∪ [f 2 ] →• χ ↓ e 2 , and (c) χ ↓ e 2 = χ ↓ i 1 ∪ → [f 1 ]• χ ↓ e 1 ;
we define the concatenation of f 1 and f 2 , denoted as f 1 + f 2 as f 3 , where

R 3 = R 1 = R 2 (+1) χ ↓ e 3 = χ ↓ e 2 (+2) χ ↓ e 3 = χ ↓ e 1 (+3) χ ↓ i 3 = χ ↓ i 1 ∪ [f 1 ] →• χ ↓ i 2 (+4) χ ↓ i 3 = χ ↓ i 2 ∪ → [f 2 ]• χ ↓ i 1 . (+5)
We say that f 1 and f 2 are compatible if they verify the conditions (a)-(c). The idea is that the concatenation of two profiles f 1 + f 2 is the profile that abstract the concatention of the forests that f 1 and f 2 abstract. Figure 4 illustrates this intuition, using the notation for the nodes as we have done before with Figure 3. We will show the following properties:

-the concatenation is associative, that is, (

f 1 + f 2 ) + f 3 = f 1 + (f 2 + f 3 ), -[f 1 + f 2 ] →•χ = [f 1 ] →•([f 2 ] →•χ), -if f 1 + f 2 = f 3 and f 1 , f 2 ∈ F, then f 3 ∈ F. Lemma 4.2. If f 1 + f 2 = f 3 and f 1 , f 2 ∈ F, then f 3 ∈ F. Proof. If χ ↓ e 3 (α, β, i) = {d}, then χ ↓ e 1 (α, β, i) = {d}, and hence d ∈ R 1 and therefore d ∈ R 3 = R 1 . A symmetrical argument applies for χ ↓ e 3 and χ ↓ e 2 . Lemma 4.3. For every f 1 , f 2 ∈ F and χ ⊆ D × Π -[f 1 + f 2 ] →•χ = [f 1 ] →•([f 2 ] →•χ), -→ [f 1 + f 2 ]•χ = → [f 2 ]•( → [f 1 ]•χ).
Lemma 4.4 (+ associativity). For every

f 1 , f 2 , f 3 ∈ F, (f 1 + f 2 ) + f 3 = f 1 + (f 2 + f 3 ).
The proofs of the two lemmas above can be found in the Appendix.

On XPath with Reflexive-Transitive Axes and Data Tests

• 15

where for ↵, ↵ 2 ⇧, z, z 2 A, we define ⇠(f)(↵, z, ↵ , z ) as 0 or 1+ depending on whether |f. z (↵) \ f. z 0 (↵ 0 )| = 0 or not; and we define ⇠(f)( ↵, z) as 0, 1, or 2+ depending on |f. z (↵)| being 0, 1 or greater than 1 respectively. 5 Intuitively, the fingerprint is related to what formulas of our logic are true at the forest that f abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z.

The precise relations will become clear in Section 6.2, through a strong normal form of the logic. Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

where for ↵, ↵ 2 ⇧, z, z 2 A, we define ⇠(f)(↵, z, ↵ , z ) as 0 or 1+ depending on whether |f. z (↵) \ f. z 0 (↵ 0 )| = 0 or not; and we define ⇠(f)( ↵, z) as 0, 1, or 2+ depending on |f. z (↵)| being 0, 1 or greater than 1 respectively. 5 Intuitively, the fingerprint is related to what formulas of our logic are true at the forest that f abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints.

xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

forest or in the right context forest; and f. # the data values taht can be found going left and down from the last root of the forest (i.e., the node x # i in Figure 3).

The fingerprint of a profile f, noted ⇠(f), is an element of

F def = (⇧ ⇥ A [ ⇧ ⇥ A ⇥ ⇧ ⇥ A) ! {0, 1, 1+, 2+},
where for ↵, ↵0 2 ⇧, z, z 0 2 A, we define ⇠(f)(↵, z, ↵0 , z 0 ) as 0 or 1+ depending on whether |f. z (↵) \ f. z 0 (↵ 0 )| = 0 or not; and we define ⇠(f)( ↵, z) as 0, 1, or 2+ depending on |f. z (↵)| being 0, 1 or greater than 1 respectively. 5 Intuitively, the fingerprint is related to what formulas of our logic are true at the forest that f abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z.

The precise relations will become clear in Section 6.2, through a strong normal form of the logic. Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints.

xxx and(c)

f 1 f 2 f 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

We have that

# i 1(23) = # i 1 [ [f 1 ] !• # i 23 (by condition (+4)) = # i 1 [ [f 1 ] !•( # i 2 [ [f 2 ] !• # i 3 ) (by condition (+4)) = # i 1 [ [f 1 ] !• # i 2 [ [f 1 ] !•([f 2 ] !• # i 3 ) ( b y( •, [) distributivity) = # i 1 [ [f 1 ] !• # i 2 [ [f 12 ] !• # i 3 (by Lemma 4.3) = # i 12 [ [f 12 ] !• # i 3 (by condition (+4)) = # i (12)3
(by condition (+4))

and by a similar reasoning using condition (+5) we obtain that

# i 1(23) = # i (12)3 . Hence, (f 1 + f 2 ) + f 3 = f 1 + (f 2 + f 3 ).
Rooting. Given a 2 A, and d 2 D k (remember that k is the number of attributes per node of our multi-attribute data trees), we define (a, d)

f 1 ✓ F, where f 2 2 (a, d)f 1 if (a) ⇠(f 2 ) 2 , (b) # e 1 = # e 1 = ;, (c) # i 2 = # i 2 = {(d, ↵, • , i) 2 D ⇥ ⇧ | 9↵ 0 .(d, ↵ 0 , , i) 2 # i 1 [ # i 1 , ↵, 2 a } [ S i2[k] ({ d(i)} ⇥ ( a \ {✏}) ⇥ a ⇥ {i}) We say that f 2 is a rooting of f 1 with (a, d).
The idea is that it corresponds to the abstraction of the tree resulting from adding a common root to a forest, see

Figure xxx. f 2 = (a, d)f 1
Notice that since the root pattern of any pair of profiles

f 1 , f 2 2 (a, d)f 3 is the same, it is idempotent and absorbing ([f 1 ] !•[f 2 ] !• = [f 1 ] !• = [f 2 ] !• , [f 1 ] !• # i 1 = # i 1 ). Lemma 4.5. For every f 1 , f 2 2 (a, d)f 3 and every ✓ D ⇥ ⇧, [f 1 ] !•[f 2 ] !• = [f 1 ] !• = [f 2 ] !• = ! [f 1 ]• ! [f 2 ]• = ! [f 1 ]• = ! [f 2 ]• . Proof. By condition (c) of rooting and definition of [ ] !, ! [ ], we have that ! [f 1 ] = [f 1 ] ! = ! [f 2 ] = [f 2 ] ! = a . By definition of a , it is immediate that a • a • = a • .
Hence, the statement follows.

ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R = R 2 , (b) # e = # i 2 [ [f 2 ] !• # e
2 , and (c)

# e = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

abstract. For example, a formula h↵ = i ^¬h↵ 6 = i (saying "there is exactly one data value reachable simultaneously by ↵ and ") will be related with |f. z (↵) \ f. z 0 (↵ 0 )| = 1 for suitable ↵, ↵0 , z, z 0 ; and a formula h↵ 6 = ↵i (saying "there are two distinct data values reachable by ↵") will be related with |f. z (↵)| 2 suitable ↵, z. The precise relations will become clear in Section 6.2, through a strong normal form of the logic.

Let us fix a set ✓ F, which we will call the set of consistent fingerprints henceforward. The usefulness of this set will become apparent in the reduction from XPath to the derivation problem of forest profiles in Section 6.2, but we can anticipate that this set will represent all the profiles abstracting multi-attribute data trees that do not contradict the formula we are trying to satisfy. For the moment, however, the reader may simply consider as a given arbitrary set of fingerprints. xxx and(c)

x # i 1 x # e 1 x # i 1 x # e 1 x # i 2 x # e 2 x # i 2 x # e 2 x # i 3 x # e 3 x # i 3 x # e 3 xxx Concatenation. For every two f 1 , f 2 2 F (recall, f i = ( # e i , # i i , # i i , # e i , R i )) so that (a) R 1 = R 2 , (b) # e 1 = # i 2 [ [f 2 ] !• # e 2 ,
# e 2 = # i 1 [ ! [f 1 ]• # e 1 ;
5 explain why we have up to 1+ in one case and up to 2+ in the other ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

= # i 12 [ [f 12 ] !• # i 3 (by condition (+4)) = # i (12)3
(by condition (+4))

and by a similar reasoning using condition (+5) we obtain that

# i 1(23) = # i (12)3 . Hence, (f 1 + f 2 ) + f 3 = f 1 + (f 2 + f 3 ).
Rooting. Given a 2 A, and d 2 D k (remember that k is the number of attributes per node of our multi-attribute data trees), we define (a, d)

f 1 ✓ F, where f 2 2 (a, d)f 1 if (a) ⇠(f 2 ) 2 , (b) # e 1 = # e 1 = ;, (c) # i 2 = # i 2 = {(d, ↵, • , i) 2 D ⇥ ⇧ | 9↵ 0 .(d, ↵ 0 , , i) 2 # i 1 [ # i 1 , ↵, 2 a } [ S i2[k] ({ d(i)} ⇥ ( a \ {✏}) ⇥ a ⇥ {i}) We say that f 2 is a rooting of f 1 with (a, d).
The idea is that it corresponds to the abstraction of the tree resulting from adding a common root to a forest, see Figure

xxx. f 2 = (a, d)f 1
Notice that since the root pattern of any pair of profiles f 1 , f 2 2 (a, d)f 3 is the same, it is idempotent and absorbing ([

f 1 ] !•[f 2 ] !• = [f 1 ] !• = [f 2 ] !• , [f 1 ] !• # i 1 = # i 1 ). Lemma 4.5. For every f 1 , f 2 2 (a, d)f 3 and every ✓ D ⇥ ⇧, [f 1 ] !•[f 2 ] !• = [f 1 ] !• = [f 2 ] !• = ! [f 1 ]• ! [f 2 ]• = ! [f 1 ]• = ! [f 2 ]• . Proof. By condition (c) of rooting and definition of [ ] !, ! [ ], we have that ! [f 1 ] = [f 1 ] ! = ! [f 2 ] = [f 2 ] ! = a . By definition of a , it is immediate that a • a • = a • .
Hence, the statement follows.

ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY. Rooting. Given a ∈ A, f 1 ∈ F, and d ∈ D k (remember that k is the number of attributes per node of our multi-attribute data trees), we define (a, d)f 1 ⊆ F, where

f 2 ∈ (a, d)f 1 if (i) ξ(f 2 ) ∈ Γ, (ii) χ ↓ e 1 = χ ↓ e 1 = ∅, (iii) χ ↓ i 2 = χ ↓ i 2 = {(d, α, β•γ, i) ∈ D × Π | ∃α .(d, α , γ, i) ∈ χ ↓ i 1 ∪ χ ↓ i 1 , α, β ∈ σ a } ∪ i∈[k] ({ d(i)} × (σ a \ { }) × σ a × {i})
We say that f 2 is a rooting of f 1 with (a, d). The idea is that it corresponds to the abstraction of the tree resulting from adding a common root to a forest, see Figure 5. The intuition behind (iii), is that all the data values d in the tree are to be found either -at some strict descendant of the root, by going first rightwards with some pattern α of σ a (i.e., consistent with the label of the root) and then downwards by some pattern γ already present in χ

↓ i
1 , possibly prefixed by some pattern β of σ a . The idea is that α, β are readily verified at the root whereas γ actually reaches the data value. Otherwise, d can be found -at the root, by nagivating rightwards and downwards with elements of σ a .

Observe that the root pattern of the produced profile f ∈ (a, d)f is unique in the sense [f] → = → [f] = σ a since it abstracts a tree and there is only one root, labeled a. As a consequence, the root pattern of any pair of profiles

f 1 , f 2 ∈ (a, d)f 3 is idempotent and absorbing: [f 1 ] →•[f 2 ] →•χ = [f 1 ] →•χ = [f 2 ] →•χ, [f 1 ] →• χ ↓ i 1 = χ ↓ i 1 . Lemma 4.5. For every f 1 , f 2 ∈ (a, d)f 3 and every χ ⊆ D × Π, [f 1 ] →•[f 2 ] →•χ = [f 1 ] →•χ = [f 2 ] →•χ = → [f 1 ]• → [f 2 ]•χ = → [f 1 ]•χ = → [f 2 ]•χ.
Proof. By condition (iii) of rooting and definition of [ ]

→, → [ ], we have that → [f 1 ] = [f 1 ] → = → [f 2 ] = [f 2 ] → = σ a . By definition of σ a , it is immediate that σ a •σ a •χ = σ a •χ.
Hence, the statement follows.

Lemma 4.6. For every

f 1 ∈ (a, d)f 2 , χ ↓ i 1 = [f 1 ] →• χ ↓ i 1 χ ↓ i 1 = [f 1 ] →• χ ↓ i 1 .
• Diego Figueira

Proof. By condition (iii) of rooting, [f 1 ] → = σ a and since χ

↓ i 1 = {(d, α, β•γ, i) | ∃α .(d, α , γ, i) ∈ χ ↓ i 2 ∪ χ ↓ i 2 , α, β ∈ σ a }∪ i∈[k] ({d(i)}×(σ a \{ })×σ a × {i}) it follows that σ a • χ ↓ i 1 = χ ↓ i 1 , obtaining that χ ↓ i 1 = [f 1 ] →• χ ↓ i 1 . Since χ ↓ i 1 = χ ↓ i
1 by condition (iii), we also obtain that χ

↓ i 1 = [f 1 ] →• χ ↓ i 1 .

The derivation problem

We define the empty profile as f ∅ def = (∅, ∅, ∅, ∅, ∅). Note that f ∅ ∈ F. The set of profiles that can be obtained from empty profiles by applying the rooting and concatenation operations is called the set of derivable profiles, and noted D. Notice that the definition of F and D depend on the given alphabets A, A root , the set of patterns P, and the set of consistent fingerprints Γ, but we use F and D instead of F A,Aroot,P,Γ and D A,Aroot,P,Γ for simplicity and economy of space. We say that f is a derivable root profile if χ ↓ e = χ ↓ e = ∅ and f ∈ (a, d)f for some f ∈ D, a ∈ A root and d ∈ D k . Let a derivation tree for f be a tree t whose every node is labeled by a forest profile and an element from A × D k , except the leaves that are labeled only by the forest profile f ∅ and -the root is labeled with f, -every internal node x of t labeled with a forest profile f and (a, d) is so that

f ∈ (a, d)(f 1 + • • • + f n ),
where f 1 , . . . , f n are the labels of the children of x.

Similarly, a derivation forest t for f is a forest of derivation trees t

= t 1 • • • t n for some profiles f 1 , . . . , f n so that f = f 1 + • • • + f n .
Therefore, a profile f is derivable if, and only if, there is a derivation forest for f. We can now state the derivation problem, that is, whether there exists a derivable root profile, given A, A root , P and Γ.

Problem: The derivation problem

Input: A finite alphabet A, A root ⊆ A, a set of patterns P, a set of consistent fingerprints Γ ⊆ F. Question: Is there a derivable root profile?

In the next section we show that this problem is decidable. Later, in Section 6, we show that there is a reduction from the satisfiability problem for XPath( * ←, ↓ * , → * , =) to the derivation problem.

COMPUTING DERIVABLE PROFILES

In this section we solve the derivation problem, showing that it is decidable in 2Exp-Space. To solve this problem we work with some quasi-ordering on forest profiles (Section 5.2) that has some good monotonicity closure properties with our forest profile algebra (Section 5.3). This allows us to reduce the problem to a restricted derivation problem in which solutions can be found by only inspecting profiles with a bounded number of rigid values (Section 5.4), that are minimal elements of the ordering (Section 5.5). These are bounded and computable, allowing us to produce an algorithm solving the problem (Section 5.6).

On XPath with Reflexive-Transitive Axes and Data Tests • 17

Preliminaries

Given f 1 , f 2 ∈ F we define that f 1 and f 2 are equivalent, and we denote it by f 1 ∼ f 2 , if there is some bijection g : D → D so that f 2 is the result of replacing d by g(d) in f 1 ; in this case we write g(f

1 ) = f 2 . For a set C ⊆ F, we write f ∈ ∼ C if there is f ∼ f so that f ∈ C.
∈ data(f) \ R and d ∈ data(f), we have that if f ∈ F then f[d → d, d ] ∈ F. Lemma 5.1. If d ∈ data(f) \ R and d ∈ data(f), we have that if f is a valid forest profile, then f[d → d, d ] is valid as well. Proof. Since d ∈ data(f), then f = f[d → d, d
] is the result of adding some fresh data value d ∈ R with the same description as d to f. Suppose, by means of contradiction, that f ∈ F. Then, by definition of F, there must be some d ∈ R so that {d } = χ or {d } = χ ↓ e (ᾱ), and thus f ∈ F, which is a contradiction.

We say that a data value

d ∈ D is an external data value of f if χ ↓ e (d)∪ χ ↓ e (d) = ∅. If further χ ↓ i (d) ∩ χ ↓ i (d) = ∅, we say that d is a strictly external data value of f. If d ∈ data(f)
is not a strictly external data value, it is then an internal data value, and if it is not an external data value, it is then a strictly internal data value.

Ordering on profiles

We define a quasi-order on forest profiles, that follows from our discussion of Section 4 on the role of flexible and rigid data values. It is the order in which we can make a profile bigger by adding a fresh data value to it, with the same description as that of a flexible data value already contained in it.

Given

f 1 , f 2 ∈ F, we define f 1 ; f 2 if either f 1 = f 2 , or there is a flexible data value d of f 1 so that f 2 = f 1 [d → d, d
] for some d ∈ data(f 1 ). We define the quasi-order as the reflexive-transitive closure of ; (i.e., f 1 f 2 iff f 1 ; * f 2 ). We write f f if f f for some f ∼ f . Note that , are recursive, reflexive and transitive, and they are hence quasi-orders.

Lemma 5.2.

and are quasi-orders over F.

Proof. We first show transitivity of , reflexivity being obvious.

If f f f , suppose f = f[d 1 → d 1 , d 1 ] • • • f[d n → d n , d n ] and f = f [e 1 → e 1 , e 1 ] • • • f[e m → e n , e m ]. Therefore, f = f[d 1 → d 1 , d 1 ] • • • f[d n → d n , d n ][e 1 → e 1 , e 1 ] • • • f[e m →
e n , e m ] and hence f f .

On the other hand, it is plain that ∼ preserves transitivity and reflexivity, and that f f.

Note that if f 1 f 2 then → [f 1 ] = → [f 2 ] and [f 1 ] → = [f 2 ] →. Note also that if f f then ξ(f) = ξ(f ). Lemma 5.3. If f 1 f 2 then → [f 1 ] = → [f 2 ] and [f 1 ] → = [f 2 ]
→.

• Diego Figueira

[n]} [n]} n | ≤ 2|Π|. χ1 ,..., χn as n we have following. + (R, χn) χn , χn). , f). Let t of siblings 1 ,..., χn , χn) or (Rχ, f). tion there values of root pro-he lemma than 2|Π| restricted ble profile D b . Also, closed. . of ext-minimal profiles of C so that f1 + f2 ∈ ↑C, then add f1 + f2 to C. Repeat. Go to step 2. 5. Output C. Note that step 2 can only be repeated as many times as there are minimal elements in F b , which is exponential. Idem with 3 and 4. So it is easy to check that this algorithm uses exponential space. Now we prove that it is correct, as a consequence of the lemmas presented before. Lemma 5.14. The algorithm uses at most exponential space. Lemma 5.15. ↑C = D b . Proof.

[⊆] This is immediate, since by construction C ⊆ D b and by Remark 5.13 D b is upward closed.

[⊇] Let f ∈ D b . Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ D b so that f = f1+• • •+fn, where n ≥ 1. We proceed by induction on the size of t.

• If t has only one node, then it is trivial. TBC.

• If t = t is a tree with height n > 0. Suppose that the root is labeled with f and with some (a, d) ∈ A × D k . Let t be the forest of immediate subtrees of t, let m = | t |. For every 1 ≤ i ≤ m, let f i be the profile label of the root of t (i)

for every i ∈ [m].
Let us show that there is some f ∈ C so that f f. We have that f 9 depicts the general idea of the argument.

1 + • • • + f m ∈ ↑C by inductive hypothesis, let f f 1 + • • • + f m for f ∈ ∼ C. Further, let us assume that f is -minimal among the profiles of C. Let f i ∈ ∼ C so that f i fi. If m = 1 it is trivial. If m > 1, there must be some f 2 f2 + • • • + fm by inductive hypothesis. • If t = t1• t2 with t1, t2 = ε... XXXXX Figure
[n]} n | ≤ 2|Π|. χ1 ,..., χn as n we have following. + (R, χn) χn , χn). , f). Let t of siblings 1 ,..., χn , χn) or (Rχ, f). tion there values of root pro-he lemma than 2|Π| restricted ble profile D b . Also, closed. . Note that step 2 can only be repeated as many times as there are minimal elements in F b , which is exponential. Idem with 3 and 4. So it is easy to check that this algorithm uses exponential space. Now we prove that it is correct, as a consequence of the lemmas presented before. Lemma 5.14. The algorithm uses at most exponential space. Lemma 5.15. ↑C = D b . Proof.

[⊆] This is immediate, since by construction C ⊆ D b and by Remark 5.13 D b is upward closed.

[⊇] Let f ∈ D b . Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ D b so that f = f1+• • •+fn, where n ≥ 1. We proceed by induction on the size of t.

• If t has only one node, then it is trivial. TBC.

• If t = t is a tree with height n > 0. Suppose that the root is labeled with f and with some (a, d) ∈ A × D k . Let t be the forest of immediate subtrees of t, let m = | t |. For every 1 ≤ i ≤ m, let f i be the profile label of the root of t (i)

for every i ∈ [m].
Let us show that there is some f ∈ C so that f f. We have that f 9 depicts the general idea of the argument. Proof. This is immediate from the definition of → [ ], [ ] →, and . Note that, since

1 + • • • + f m ∈ ↑C by inductive hypothesis, let f f 1 + • • • + f m for f ∈ ∼ C. Further, let us assume that f is -minimal among the profiles of C. Let f i ∈ ∼ C so that f i fi. If m = 1 it is trivial. If m > 1, there must be some f 2 f2 + • • • + fm by inductive hypothesis. • If t = t1• t2 with t1, t2 = ε... XXXXX Figure
f 3 (a, d) ∈ f 2 f 1 f 3 (a, d) f 1 = f 1 + • • • + f n f 3 (a, d)
f 1 f 2 we have {(α, β, i) | ∃d ∈ D.(d, α, β, i) ∈ f 1 } = {(α, β, i) | ∃d ∈ D.(d, α, β, i) ∈ f 2 }. Hence, we obtain that α ∈ [f 1 ] → if and only if there is some (d, α, β, i) ∈ χ ↓ i 1 if and only if there is some (d , α, β, i) ∈ χ ↓ i 2 if and only if α ∈ [f 2 ] →. A similar argument shows that → [f 1 ] = → [f 2 ]. Lemma 5.4. If f f then ξ(f) = ξ(f ).
Proof. Suppose, without any loss of generality, that

f = f[d → d, d ], where d ∈ data(f) \ R and d ∈ data(f). Since d behaves just as d, we have that, for any ᾱ, ᾱ ∈ Π, a, a ∈ { • ↓ , • ↓ , • ↓ , •}, d ∈ f .χ a (ᾱ) ∩ χ a (ᾱ ) iff d ∈ f.χ a ( ᾱ) ∩ f.χ a (ᾱ ). Hence, f .χ a (ᾱ) ∩ f .χ a (ᾱ ) = ∅ iff f.χ a (ᾱ) ∩ f.χ a ( ᾱ ) = ∅. Further, since d ∈ R we have that if d ∈ χ a ( ᾱ) in f (or in f) then |χ a ( ᾱ)| > 1. Hence ξ(f)(ᾱ, a) = ξ(f )( ᾱ, a) = 2+ whenever d ∈ f.χ a ( ᾱ). Further, since f preserves all the data values of f with their descriptions, ξ(f)(ᾱ, a) = ξ(f )(ᾱ, a) whenever d ∈ f.χ a (ᾱ) ∩ f.χ a ( ᾱ ).
We say that a set of forest profiles G ⊆ F is upward closed (resp. downward closed) with respect to , if for every f ∈ G and f f (resp. f f ), we have f ∈ G. We write

↑G def = {f ∈ F | f f for some f ∈ G} ↓G def = {f ∈ F | f f for some f ∈ G}
for the upward and downward closure of G with respect to . We say that G is ↑↓-closed, if it is both upward and downward closed, that is, G = ↑↓G.

Monotonicity properties

In order to devise an algorithm that tests the existence of a derivable root profile, we will need some monotonicity lemmas evidencing the relationship between and the rooting and concatenation operations on profiles. The ultimate goal of these lemmas is to restrict the derivation problem to profiles that are minimal with respect to . The next Lemma 5.5 states that for any two profiles f 1 f 2 , f 1 can be seen as a concatenation of profiles that share the same descriptions of internal values as f 1 , under certain restrictions, as it is shown next. This is a crucial property that follows from our discussion in Section 4.1.

Lemma 5.5 (Figure 6). For every

f 1 , f 2 , f 3 ∈ F, (a, d) ∈ A × D k so that f 1 f 2 ∈ (a, d)f 3 , there are n ∈ N, f 1 , . . . , f n ∈ F so that f i ∈ ∼ (a, d)f 3 for every i ∈ [n],
On XPath with Reflexive-Transitive Axes and Data Tests

• 19

f 0 :      R 0 = R2, χ 0 (e) = ( χ ↓ e 2 (e), χ ↓ i 2 (e), χ ↓ i 2 (e), χ ↓ i 2 (e) ∪ [f2] →• χ ↓ e 2 (e))
for every e ∈ data(f2),

χ 0 (d j ) = ( χ ↓ e 2 (dj), ∅, ∅, χ ↓ i 2 (dj) ∪ [f2] →• χ ↓ e 2 (dj)) for every j ∈ [t].
For every i ∈ {1, . . . , t} we define f i as and

f i :                          R i = R2, χ i (e) = ( χ ↓ i 2 (e) ∪ → [f2]• χ ↓ e 2 (e), χ ↓ i 2 (e), χ ↓ i 2 (e), χ ↓ i 2 (e) ∪ [f2] →• χ ↓ e 2 (e)) for every e ∈ data(f2) \ {di}, χ i (di) = ( χ ↓ i 2 (di) ∪ → [f2]• χ ↓ e 2 (di), ∅, ∅, χ ↓ i 2 (di) ∪ [f2] →• χ ↓ e 2 (di)), χ i (d i ) = ( → [f2]• χ ↓ e 2 (di), χ ↓ i 2 (di), χ ↓ i 2 (di), [f2] →• χ ↓ e 2 (di)), χ i (d j ) = ( χ ↓ i 2 (dj) ∪ → [f2]• χ ↓ e 2 (dj), ∅, ∅, [f2] →• χ ↓ e 2 (dj)) for every j < i, χ i (d j ) = ( → [f2]• χ ↓ e 2 (dj), ∅, ∅, χ ↓ i 2 (dj) ∪ [f2] →• χ ↓ e 2 (dj)) for every j > i. f t+1 :      R t+1 = R2, χ t+1 (e) = ( χ ↓ i 2 (e) ∪ → [f2]• χ ↓ e 2 (e), χ ↓ i 2 (e), χ ↓ i 2 (e), χ ↓ e 2 (e)) for every e ∈ data(f2), χ t+1 (d j ) = ( χ ↓ i 2 (dj) ∪ → [f2]• χ ↓ e 2 (dj), ∅, ∅, χ ↓ e 2 (dj)) for every j ∈ [t].
f 1 = f 1 + • • • + f n . Proof. Since f 1 f 2 , suppose f 1 = f 2 [d 1 → d 1 , d 1 ] • • • [d t → d t , d t ] ( †)
where {d 1 , . . . , d t } ⊆ data(f 2 ) \ R 2 ; {d 1 , . . . , d t } ∩ data(f 2 ) = ∅; and d i = d j for all i = j. We define n = t + 2.

The idea is that we will define f 0 , f 1 , . . . , f t+1 so that f i is, modulo some renaming of data values, the same as f 2 for all strictly internal values, and with the same descriptions. However, f i has more external data values than f 2 -namely d 1 , . . . , d t -that have basically the same descriptions as d 1 , . . . , d t in f 2 . Although technically we could make use of less profiles, we prefer to define t + 1 different profiles, to preserve some symmetries in the definitions, and thus to simplify proofs. We define f 0 , . . . , f t+1 in Figure 7.

We shall now show that for every f i there is some

f i so that f i ∼ f i ∈ (a, d)f 3 . Claim 5.5.1. For every i ∈ [n], f i ∈ ∼ (a, d)f 3 . Proof. First note that f 0 , f t+1 ∈ (a, d)f 3 ,
since all the internal descriptions of the internal data values are preserved, and ξ(f 0 ) = ξ(f t+1 ) = ξ(f 2 ). The fact that they all have the same fingerprints is because:

-For every a ∈ A, ᾱ ∈ Π, and every data value e ∈ data(f 2 ), we have that e ∈ χ a ( ᾱ) in f 2 iff e ∈ χ a (ᾱ) in f 0 iff e ∈ χ a (ᾱ) in f t+1 . This is because, since χ

↓ i t+1 (e) = χ ↓ i 0 (e) = χ ↓ i 2 (e), χ ↓ i t+1 (e) = χ ↓ i 0 (e) = χ ↓ i 2 (e), χ ↓ e 0 (e) = χ ↓ e 2 (e), χ ↓ e t+1 (e) = χ ↓ e • Diego Figueira χ a (e) in f 2 ; and for all a ∈ {•, • ↓ , • ↓ }, χ a (e) in f t+1 is equal to χ a (e) in f 2 . And further, -if a = • ↓ , f 0 .χ a (e) = χ ↓ i 0 (e) ∪ [f 0 ] →• χ ↓ e 0 (e) = χ ↓ i 2 (e) ∪ [f 2 ] →•( χ ↓ i 2 (e) ∪ [f 2 ] →• χ ↓ e 2 (e)) = χ ↓ i 2 (e) ∪ [f 2 ] →• χ ↓ e
2 (e) (by Lemmas 4.5 and 4.6)

= f 2 .χ a (e) -if a = • ↓ , f t+1 .χ a (e) = χ ↓ i 0 (e) ∪ → [f t+1 ]• χ ↓ e t+1 (e) = χ ↓ i 2 (e) ∪ → [f 2 ]•( χ ↓ i 2 (e) ∪ → [f 2 ]• χ ↓ e 2 (e)) = χ ↓ i 2 (e) ∪ → [f 2 ]• χ ↓ e 2 (e)
(by Lemmas 4.5 and 4.6)

= f 2 .χ a (e).
-The data values d j do not change the fingerprint ξ(f 2 ), because d j is added to all those χ a (ᾱ) where d j ∈ f 2 .χ a (ᾱ), and f 2 .χ a (ᾱ) has already two data values (otherwise d j would be rigid). Therefore, for any a ∈ A, ᾱ ∈ Π, if some

d j ∈ f 0 .χ a (ᾱ), then |f 2 .χ a ( ᾱ)| ≥ 2, and f 2 .χ a (ᾱ) ⊆ f 0 .χ a (ᾱ) (thus, |f 0 .χ a (ᾱ)| ≥ 2). Otherwise, if d j ∈ f 0 .χ a ( ᾱ) for every j ∈ [t], then f 0 .χ a (ᾱ) = f 2 .χ a (ᾱ). Moreover, for any a, a ∈ A, ᾱ, ᾱ ∈ Π, if d j is in some f 0 .χ a (ᾱ) ∩ f 0 .χ a (ᾱ ) it means that d j ∈ f 2 .χ a ( ᾱ) ∩ f 2 .χ a (ᾱ ). Hence, |f 0 .χ a (ᾱ) ∩ f 0 .χ a (ᾱ )| ≥ 1 iff |f 2 .χ a (ᾱ) ∩ f 2 .χ a ( ᾱ )| ≥ 1.
As a result the fingerprint of f 2 and f 0 are equal, and hence ξ(f 0 ) = ξ(f 2 ) ∈ Γ.

The same reasoning applies to f t+1 .

Thus, f 0 , f t+1 ∈ ∼ (a, d)f 3 . We now show that for every i ∈ [t], there is

f i so that f i ∼ f i ∈ (a, d)f 3 . We define f i as f i [d i → d i ] for every i ∈ [t]. Observe that f i ∼ f i for every i ∈ [t].
Since every d i is not rigid, f i ∈ F and hence f i ∈ F. Further, note that f i and f 2 share the same set of internal data values, and that the internal descriptions of these internal data values are the same in f i and f 2 . Also in this case we have that ξ(f i ) = ξ(f 2 ) for the same reason as before:

-For all e ∈ data(f 2 ), a ∈ A and ᾱ ∈ Π we have that e ∈ χ a ( ᾱ) in f 2 iff e ∈ χ a (ᾱ) in f i . -The fresh data values d j only add data values to sets χ a (ᾱ) that already have at least 2 data values. And

d j ∈ f i .χ a (ᾱ) ∩ f i .χ a (ᾱ ) iff d j ∈ f 2 .χ a (ᾱ) ∩ f 2 .χ a (ᾱ ).
This shows that ξ(

f i ) = ξ(f 2 ) ∈ Γ. Thus, f i ∈ (a, d)f 3 since f 2 ∈ (a, d)f 3 .
We now check that

f 1 = f 0 + • • • + f t+1 . Claim 5.5.2. f 1 = f 0 + • • • + f t+1 .
Proof. For each data value d, we are going to show that conditions (b) and (c) of concatenation hold, and that χ1 (d) equals to the profile of

d in f 1 , + • • • + f n .
On XPath with Reflexive-Transitive Axes and Data Tests

• 21

• Let us take any data value d ∈ data(f 2 ) \ {d 1 , . . . , d t }. We first check that condition (b) holds for d, in other words, that for every i ∈ {0, . . . , t}, χ

↓ i i+1 (d) ∪ [f i+1 ] →• χ ↓ e i+1 (d) = χ ↓ e i (d). We have χ ↓ i i+1 (d) ∪ [f i+1 ] →• χ ↓ e i+1 (d) = χ ↓ i i+1 (d) ∪ [f 2 ] →• χ ↓ e i+1 (d) (by Lemma 4.5) = χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e i+1 (d) (by definition) = χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) if i = t, or χ ↓ i 2 (d) ∪ [f 2 ] →•( χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d)) otherwise.
If i = t, we further have that χ

↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) = χ ↓ e i (d), verifying (b). Otherwise, if i = t, χ ↓ i i+1 (d) ∪ [f i+1 ] →• χ ↓ e i+1 (d) = • • • = = χ ↓ i 2 (d) ∪ [f 2 ] →•( χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d)) = χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ i 2 (d) ∪ [f 2 ] →•[f 2 ] →• χ ↓ e 2 (d) (by (•, ∪) distributivity) = χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) (by Lemma 4.5) = [f 2 ] →• χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) (since χ ↓ i 2 (d) ⊆ [f 2 ] →• χ ↓ i 2 (d)) = χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) (by Lemma 4.6) = χ ↓ e i (d).
(by definition)

In any case, condition (b) holds between f i and f i+1 for the data value d. Note that since all definitions are symmetrical, it also follows that condition (c) holds for d.

We now check that, if we call

f + to f 1 + • • • + f n ,
χ ↓ i + (d) = χ ↓ i 2 ∪ [f 2 ] →• χ ↓ i 2 ∪ [f 2 ] →•[f 2 ] →• χ ↓ i 2 ∪ • • • ∪ [f 2 ] → • • • [f 2 ] → n -1 times • χ ↓ i 2 (d) (by (+4)) = ([f 2 ] →• χ ↓ i 2 )(d) (by Lemma 4.5) = χ ↓ i 2 (d) (by Lemma 4.6) = χ ↓ i 1 (d).
(by ( †), since d ∈ data(f 2 ))

• Suppose now that we have d = d j for some j ∈ [t]. We check that condition (b) holds for d, in other words that for every i ∈ {0, . . . , t}, χ

↓ i i+1 (d) ∪ [f i+1 ] →• χ ↓ e i+1 (d) = χ ↓ e i (d).
• Diego Figueira

We have

χ ↓ i i+1 (d) ∪ [f i+1 ] →• χ ↓ e i+1 (d) = χ ↓ i i+1 (d) ∪ [f 2 ] →• χ ↓ e i+1 (d) (by Lemma 4.5) If i = t, χ ↓ i i+1 (d) ∪ [f 2 ] →• χ ↓ e i+1 (d) = χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) (by definition) = χ ↓ e i (d).
(by definition)

If i = t and j = i + 1, χ ↓ i i+1 (d) ∪ [f 2 ] →• χ ↓ e i+1 (d) = ∅ ∪ [f 2 ] →•( χ ↓ i 2 ∪ [f 2 ] →• χ ↓ e 2 )(d) (by definition) = [f 2 ] →• χ ↓ i 2 (d) ∪ [f 2 ] →•[f 2 ] →• χ ↓ e 2 (d) (by (•, ∪) distributivity) = [f 2 ] →• χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) (by Lemma 4.5) = χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) (by Lemma 4.6) = χ ↓ e i (

d). (by definition)

If i = t and j = i + 1,

χ ↓ i i+1 (d) ∪ [f 2 ] →• χ ↓ e i+1 (d) = χ ↓ i 2 (d) ∪ [f 2 ] →•( χ ↓ i 2 ∪ [f 2 ] →• χ ↓ e 2 )(d) (by definition) = χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ i 2 (d) ∪ [f 2 ] →•[f 2 ] →• χ ↓ e 2 (d) (by (•, ∪) distributivity) = χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) (by Lemma 4.5) = χ ↓ i 2 (d) ∪ χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) (by Lemma 4.6) = χ ↓ i 2 (d) ∪ [f 2 ] →• χ ↓ e 2 (d) = χ ↓ e i (d).
(by definition)

Condition (c) follows by symmetry.

We check that χ d). By definition of +, we have that

↓ e + (d) = χ ↓ e 1 (d) and χ ↓ i + (d) = χ ↓ i 1 (
χ ↓ e + (d) = χ ↓ e 2 (d) (by (+2)) = χ ↓ e 1 (d), (by ( †), since d ∈ data(f 2 )) χ ↓ i + (d) = χ ↓ i 2 ∪ [f 2 ] →•∅ ∪ • • • ∪ [f 2 ] → • • • [f 2 ] → n -2 times •∅ ∪ [f 2 ] → • • • [f 2 ] → n -1 times • χ ↓ i 2 (d) (by (+4)) = ( χ ↓ i 2 ∪ [f 2 ] →• χ ↓ i 2 )(d) (by Lemma 4.5) = ([f 2 ] →• χ ↓ i 2 )(d) (since χ ↓ i 2 ⊆ [f 2 ] →• χ ↓ i 2 ) = χ ↓ i 2 (d) (by Lemma 4.6) = χ ↓ i 1 (d).
(by ( †), since d ∈ data(f 2 ))

• Finally, suppose d = d j for some j ∈ [t]. We check that condition (b) holds for d, in other words that for every i ∈ {0, . . . , t}, χ

↓ i i+1 (d j ) ∪ [f i+1 ] →• χ ↓ e i+1 (d j ) = χ ↓ e i (d j ).
On XPath with Reflexive-Transitive Axes and Data Tests

• 23

By definition, we have

χ ↓ i i+1 (d j ) ∪ [f i+1 ] →• χ ↓ e i+1 (d j ) = χ ↓ i i+1 (d j ) ∪ [f 2 ] →• χ ↓ e i+1 (d j ) (by Lemma 4.5) If i = t, χ ↓ i i+1 (d j ) ∪ [f 2 ] →• χ ↓ e i+1 (d j ) = ∅ ∪ [f 2 ] →• χ ↓ e 2 (d j ) (by definition) = χ ↓ e i (d j ).
(by definition)

If i = t and j = i + 1, χ ↓ i i+1 (d j ) ∪ [f 2 ] →• χ ↓ e i+1 (d j ) = χ ↓ i 2 (d j ) ∪ [f 2 ] →•[f 2 ] →• χ ↓ e 2 (d j ) (by definition) = χ ↓ i 2 (d j ) ∪ [f 2 ] →• χ ↓ e 2 (d j ) (by Lemma 4.5) = χ ↓ e i (d j ).
(by definition)

If i = t and j > i + 1, χ ↓ i i+1 (d j ) ∪ [f 2 ] →• χ ↓ e i+1 (d j ) = ∅ ∪ [f 2 ] →•( χ ↓ i 2 (d j ) ∪ [f 2 ] →• χ ↓ e 2 (d j )) (by definition) = [f 2 ] →• χ ↓ i 2 (d j ) ∪ [f 2 ] →•[f 2 ] →• χ ↓ e 2 (d j ) (by (•, ∪) distributivity) = [f 2 ] →• χ ↓ i 2 (d j ) ∪ [f 2 ] →• χ ↓ e 2 (d j ) (by Lemma 4.5) = χ ↓ i 2 (d j ) ∪ [f 2 ] →• χ ↓ e 2 (d j ) (by Lemma 4.6) = χ ↓ e i (d j ). (by definition) If i = t and j < i + 1, χ ↓ i i+1 (d j ) ∪ [f 2 ] →• χ ↓ e i+1 (d j ) = ∅ ∪ [f 2 ] →•[f 2 ] →• χ ↓ e 2 (d j ) (by definition) = [f 2 ] →• χ ↓ e 2 (d j ) (by Lemma 4.5) = χ ↓ e i (d j ).
(by definition)

Condition (c) follows by symmetry.

We check that χ

↓ e + (d j ) = χ ↓ e 1 (d j ) and χ ↓ i + (d j ) = χ ↓ i 1 (d j )
. By definition of +, we have that 2. Take any -minimal f ∈ C and a -minimal f1 ∈ (a, d)f so that f1 ∈ ↑C, and add f1 to C. If there isn't any, go to next step. 3. For every ext-minimal f ∈ C, add all bounded extensions to C. 4. If there are two f1, f2 ∈ C ∼ that are bounded extensions of ext-minimal profiles of C so that f1 + f2 ∈ ↑C, then add f1 + f2 to C. Repeat. Go to step 2. 5. Output C. Note that step 2 can only be repeated as many times as there are minimal elements in F b , which is exponential. Idem with 3 and 4. So it is easy to check that this algorithm uses exponential space. Now we prove that it is correct, as a consequence of the lemmas presented before. Lemma 5.14. The algorithm uses at most exponential space. Lemma 5.15. ↑C = D b . Proof.

χ ↓ e + (d j ) = χ ↓ e 2 (d j ) (by (+2)) = χ ↓ e 1 (d j ), (since χ1 (d j ) = χ2 (d j ) by ( †)) χ ↓ i + (d j ) = ∅ ∪ [f 2 ] →•∅ ∪ • • • ∪ [f 2 ] → • • • [f 2 ] → j times •∅ ∪ [f 2 ] → • • • [f 2 ] → j + 1 times • χ ↓ i 2 ∪ [f 2 ] → • • • [f 2 ] → j + 2 times •∅ ∪ • • • ∪ [f 2 ] → • • • [f 2 ] → n -1 times •∅ (d j ) (by (+4)) = ([f 2 ] →• χ ↓ i 2 )(d j ) (by Lemma 4.5) = χ ↓ i 2 (d j ) (by Lemma 4.6) = χ ↓ i • Diego Figueira ∈ ∈ • • • • • • • • • f 3,t f 3,1 f 1,1 + • • • + f 1,n1 + • • • + f t,1 + • • • + f t,nt f (a t , dt ) (a 1 , d1 ) f 1 + • • • + f t f f 3,1 (a 1 , d1 ) f 3,1 (a 1 , d1 ) f 3,t (a t , dt ) f 3,t (a t , dt ) k {d }. Sup- Then, by χ ↓ e j (α, β, i) s is in con- The same [n]} [n]} n | ≤ 2|Π|. χ1 ,...,
[⊆] This is immediate, since by construction C ⊆ D b and by Remark 5.13 D b is upward closed.

[⊇] Let f ∈ D b . Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ D b so that f = f1+• • •+fn, where n ≥ 1. We proceed by induction on the size of t.

• If t has only one node, then it is trivial. TBC.

• If t = t is a tree with height n > 0. Suppose that the root is labeled with f and with some (a, d) ∈ A × D k . Let t be the forest of immediate subtrees of t, let m = | t |. For every 1 ≤ i ≤ m, let f i be the profile label of the root of t (i)

for every i ∈ [m].
Let us show that there is some f ∈ C so that f f. We have that f 9 depicts the general idea of the argument. to C. 4. If there are two f1, f2 ∈ C ∼ that are bounded extensions of ext-minimal profiles of C so that f1 + f2 ∈ ↑C, then add f1 + f2 to C. Repeat. Go to step 2. 5. Output C. Note that step 2 can only be repeated as many times as there are minimal elements in F b , which is exponential. Idem with 3 and 4. So it is easy to check that this algorithm uses exponential space. Now we prove that it is correct, as a consequence of the lemmas presented before. Lemma 5.14. The algorithm uses at most exponential space. Lemma 5.15. ↑C = D b . Proof.

1 + • • • + f m ∈ ↑C by inductive hypothesis, let f f 1 + • • • + f m for f ∈ ∼ C. Further, let us assume that f is -minimal among the profiles of C. Let f i ∈ ∼ C so that f i fi. If m = 1 it is trivial. If m > 1, there must be some f 2 f2 + • • • + fm by inductive hypothesis. • If t = t1• t2 with t1, t2 = ε... XXXXX Figure
[⊆] This is immediate, since by construction C ⊆ D b and by Remark 5.13 D b is upward closed.

[⊇] Let f ∈ D b . Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ D b so that f = f1+• • •+fn, where n ≥ 1. We proceed by induction on the size of t.

• If t has only one node, then it is trivial. TBC.

• If t = t is a tree with height n > 0. Suppose that the root is labeled with f and with some (a, d) ∈ A × D k . Let t be the forest of immediate subtrees of t, let m = | t |. For every 1 ≤ i ≤ m, let f i be the profile label of the root of t (i)

for every i ∈ [m].
Let us show that there is some f ∈ C so that f f. We have that f 9 depicts the general idea of the argument.

1 + • • • + f m ∈ ↑C by inductive hypothesis, let f f 1 + • • • + f m for f ∈ ∼ C. Further, let us assume that f is -minimal among the profiles of C. Let f i ∈ ∼ C so that f i fi. If m = 1 it is trivial. If m > 1, there must be some f 2 f2 + • • • + fm by inductive hypothesis. • If t = t1• t2 with t1, t2 = ε... XXXXX Figure
[n]} [n]} n | ≤ 2|Π|. χ1 ,..., χn as χn we have e following.

• + (R, χn) , χn , χn). , f). Let t of siblings ¯ 1 ,..., χn , χn) for (Rχ, f). ation there id values of a root pro-the lemma than 2|Π| s restricted able profile n D b . Also, closed. e.

Output C.

Note that step 2 can only be repeated as many times as there are minimal elements in F b , which is exponential. Idem with 3 and 4. So it is easy to check that this algorithm uses exponential space. Now we prove that it is correct, as a consequence of the lemmas presented before. Lemma 5.14. The algorithm uses at most exponential space. Lemma 5.15. ↑C = D b . Proof.

[⊆] This is immediate, since by construction C ⊆ D b and by Remark 5.13 D b is upward closed.

[⊇] Let f ∈ D b . Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ D b so that f = f1+• • •+fn, where n ≥ 1. We proceed by induction on the size of t.

• If t has only one node, then it is trivial. TBC.

• If t = t is a tree with height n > 0. Suppose that the root is labeled with f and with some (a, d) ∈ A × D k . Let t be the forest of immediate subtrees of t, let m = | t |. For every 1 ≤ i ≤ m, let f i be the profile label of the root of t (i)

for every i ∈ [m].
Let us show that there is some f ∈ C so that f f. We have that f 9 depicts the general idea of the argument.

1 + • • • + f m ∈ ↑C by inductive hypothesis, let f f 1 + • • • + f m for f ∈ ∼ C. Further, let us assume that f is -minimal among the profiles of C. Let f i ∈ ∼ C so that f i fi. If m = 1 it is trivial. If m > 1, there must be some f 2 f2 + • • • + fm by inductive hypothesis. • If t = t1• t2 with t1, t2 = ε... XXXXX Figure
n | ≤ 2|Π|. χ1 ,..., χn as χn we have e following.

• + (R, χn) , χn , χn). , f). Let t of siblings ¯ 1 ,..., χn , χn) for (Rχ, f). ation there id values of a root pro-the lemma than 2|Π| s restricted able profile n D b . Also, closed. e. exponential space. Now we prove that it is correct, as a consequence of the lemmas presented before. Lemma 5.14. The algorithm uses at most exponential space. Lemma 5.15. ↑C = D b . Proof.

[⊆] This is immediate, since by construction C ⊆ D b and by Remark 5.13 D b is upward closed.

[⊇] Let f ∈ D b . Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ D b so that f = f1+• • •+fn, where n ≥ 1. We proceed by induction on the size of t.

• If t has only one node, then it is trivial. TBC.

• If t = t is a tree with height n > 0. Suppose that the root is labeled with f and with some (a, d) ∈ A × D k . Let t be the forest of immediate subtrees of t, let m = | t |. For every 1 ≤ i ≤ m, let f i be the profile label of the root of t (i)

for every i ∈ [m].
Let us show that there is some f ∈ C so that f f. We have that f 9 depicts the general idea of the argument. Therefore, we have that condition (a) as well as conditions (b) and (c) hold true for every data value, and that f 0 + • • • + f t+1 and f 1 coincide. Thus, the Claim follows.

1 + • • • + f m ∈ ↑C by inductive hypothesis, let f f 1 + • • • + f m for f ∈ ∼ C. Further, let us assume that f is -minimal among the profiles of C. Let f i ∈ ∼ C so that f i fi. If m = 1 it is trivial. If m > 1, there must be some f 2 f2 + • • • + fm by inductive hypothesis. • If t = t1• t2 with t1, t2 = ε... XXXXX Figure
This concludes our proof.

As a corollary of the previous lemma, we obtain the following.

Lemma 5.6 (Figure 8). For every f, f 1 , . . . ,

f t , f 3,1 , . . . , f 3,t ∈ F and (a 1 , d1 ), . . . , (a t , dt ) ∈ A × D k so that f f 1 + • • • + f t and f i ∈ (a i , di )f 3,i for each i ∈ [t], there is a profile f i,j ∈ F for every i ∈ [t], j ∈ [n i ] so that f i,j ∈ ∼ (a i , di )f 3,i and f = f 1,1 + • • • + f 1,n1 + • • • + f t,1 + • • • + f t,nt .
Proof. This is a direct consequence of Lemma 5.5. Since

f f 1 + • • • + f t , then f = (f 1 + • • • + f t )[d 1 → d 1 , d 1 ] • • • [d n → d n , d n ] for some d 1 , . . . , d n , d 1 , . . . , d n ∈ D so that {d 1 , . . . , d n } ∩ R = ∅ and {d 1 , . . . , d n } ∩ data(f 1 + • • • + f t ) = ∅. It follows that f = (f 1 + • • • + f t )[d 1 → d 1 , d 1 ] • • • [d n → d n , d n ] = f 1 [d 1 → d 1 , d 1 ] • • • [d n → d n , d n ] + • • • + f t [d 1 → d 1 , d 1 ] • • • [d n → d n , d n ]. Note that f i [d 1 → d 1 , d 1 ] • • • [d n → d n , d n ] f i ∈ (a i , di )f 3,i for every i ∈ [t]
. We can hence apply Lemma 5.5, and we obtain, for some

n i ∈ N, f i,1 , . . . , f i,ni ∈ ∼ (a i , di )f 3,i so that f i,1 + • • • + f i,ni = f i [d 1 → d 1 , d 1 ] • • • [d n → d n , d n ]. Therefore, f = f 1 [d 1 → d 1 , d 1 ] • • • [d n → d n , d n ] + • • • + f t [d 1 → d 1 , d 1 ] • • • [d n → d n , d n ] = f 1,1 + • • • + f 1,n1 + • • • + f t,1 + • • • + f t,nt ,
which concludes the proof.

The lemmas above imply that the set of derivable profiles is upward closed.

Lemma 5.7. D = ↑D.

Proof. This is a direct consequence of Lemma 5.6.

We finally state two other monotonicity properties that will be required to reduce the derivation problem into a similar problem that works only with minimal profiles in Section 5.5.

We say that a profile f is a bounded extension of a profile f if f f and |data(f )| ≤ |data(f)| + 3|Π| 4 . The following lemma tells us that for any G ⊆ F and On XPath with Reflexive-Transitive Axes and Data Tests any profiles f 1 , f 2 ∈ ↑G, there are bounded extensions f 1 , f 2 of profiles of G so that f 1 + f 2 f 1 + f 2 , as in Figure 9.

• 25 f 1 f 2 f 1 f 2 + f 1 f 2 f 3 + f 1 f 2 f 3 (bounded) (bounded)
Lemma 5.8 (Figure 9). For every

f 1 , f 2 , f 3 , f 1 , f 2 ∈ F, if f 1 +f 2 = f 3 and f 1 f 1 , f 2 f 2 , then f 1 + f 2 f 3 , for some f 1 , f 2 ∈ F so that f i is a bounded extension of f i , for all i ∈ {1, 2}.
Proof. For every description π so that χ3 (π) \ R 3 = ∅, let d π ∈ D be a data value so that d π ∈ χ3 (π) \ R 3 . Let D be the set of all these data values. Note that |D| ≤ |Π| 4 .

We define

f i = (R 3 , χ i ), where χ i (d) = χ i (d) if d ∈ D χi (d) if d ∈ D. Note that data(f i ) ≤ data(f i ) + |D| ≤ data(f i ) + |Π| 4 . Claim 5.8.1. f i f i f i for all i ∈ {1, 2}.
Proof. By definition of , for every d ∈ D there is some

d ∈ data(f i ) \ R i so that χi (d) = χ i (d ). Therefore, f i = f i [d 1 → d 1 , d 1 ] • • • [d 1 → d n , d n ]
where {d 1 , . . . , d n } = D \ data(f i ) and for every j ∈ [n], d j ∈ R i , d j ∈ data(f i ), and χ i (d j ) = χi (d j ). In other words, we have that

f i f i f i for all i ∈ {1, 2}.
Therefore, f i is a bounded extension of f i for i ∈ {1, 2}.

Claim 5.8.2.

f 1 + f 2 f 3 .
Proof. First, we have that f 1 , f 2 ∈ F because otherwise f 1 or f 2 would not be in F.

Since f i f i , by Lemma 5.3 it follows that

→ [f i ] = → [f i ], [f i ] → = [f i ] →. ( †)
This means that, since f i is the result of adding data values d with profile χi (d), if conditions (a), (b), (c) hold for f 1 + f 2 they must also hold for f 1 + f 2 . Therefore, all the preconditions to apply

f 1 + f 2 hold. Let f 3 = f 1 + f 2 .
Note that all the profiles in question share the same set of rigid values,

R 3 = R 1 = R 2 = R 1 = R 2 =
R 3 by definition of and +. Every data value d ∈ data(f 3 ) is so that χ i (d) = χi (d), and with ( †) this means that χ3 (d) = χ 3 (d), by definition of f 1 + f 2 . For every other data value d ∈ data(f 3 ) \ data(f 3 ), it must be that d ∈ R 3 and there must be some d ∈ D so that χ3 ( d) = χ3 (d) by definition of D. Then, if data(f 3 ) \ data(f 3 ) = {d 1 , . . . , d n } we have that

• Diego Figueira (a, d) f 1 f 5 f 2 ∈ (a, d) f 1 f 3 f 4 f 5 f 2 ∈ (a, d) ∈ (bounded)
f 3 = f 3 [ d1 → d1 , d 1 ] • • • [ dn → dn , d n ],
and hence, f 3 f 3 . By Claims 5.8.1 and 5.8.2, and since data(f i ) ≤ data(f i ) + |Π| 4 , the lemma follows.

A similar lemma holds for the rooting operation.

Lemma 5.9 (Figure 10). For every

f 1 , f 2 , f 5 ∈ F, (a, d) ∈ A × D k so that f 1 ∈ (a, d)f 2 and f 2 f 5 , there exist f 3 , f 4 ∈ F so that f 4 f 5 , f 3 ∈ ∼ (a, d)f 4 , |data(f 4 )| ≤ |data(f 5 )| + |Π| 4 + |R 1 |, and f 3 f 1 , f 4 f 2 .
Proof. We are given f 1 , f 2 , f 5 and (a, d). We show that there must be some f 3 and f 4 so that f 1 f 3 ∈ (a, d)f 4 with f 4 f 5 . Figure 10 contains a graphical representation of the profiles we work with in the proof.

We first define f 4 . For every internal description π so that π

↓ i 1 ∪ π ↓ i 1 = ∅ and χ1 (π) \ R 1 = ∅, let d π ∈ D be a data value of χ1 (π) \ R 1 . Let D be the set of all such data values. Note that |D| ≤ |Π| 4 . f 4 :      R 4 = R 5 for every d ∈ D ∪ R 1 , χ4 (d) = χ2 (d) for every d ∈ D ∪ R 1 , χ4 (d) = χ5 (d) Note that |data(f 4 )| ≤ |data(f 5 )| + |Π| 4 + |R 1 |. Since f 5 f 2 , we have that f 5 f 4 f 2 . Claim 5.9.1. f 5 f 4 f 2 . Proof. • We first show that f 5 f 4 . First notice that R 5 = R 2 since f 5 f 2 , and that R 4 = R 5 by definition of R 4 .
We then have that for every

d ∈ R 5 = R 4 , χ4 (d) = χ2 (d) = χ5 (d).
We show that for every

d ∈ data(f 5 ), χ4 (d) = χ5 (d). If d ∈ data(f 5 ) \ (D ∪ R 1 ), we have that χ4 (d) = χ5 (d). If on the other hand d ∈ D ∪ R 1 , we have χ4 (d) = χ2 (d). Then d ∈ data(f 2 ), and since f 5 f 2 we have that either d ∈ data(f 5 ) or χ2 (d) = χ5 (d). Hence, for every d ∈ data(f 5 ), χ4 (d) = χ5 (d).
We finish the proof of f 4 f 5 by showing that for every

d ∈ data(f 4 ) \ R 4 there is some d ∈ data(f 5 ) \ R 4 so that χ4 (d) = χ5 (d ). If d ∈ D ∪ R 1 , then of course we can take d = d and χ4 (d) = χ5 (d ). If d ∈ D ∪ R 1 , we have that χ4 (d) = χ2 (d)
by definition. Since f 5 f 2 , there must be some d ∈ data(f 5 ) \ R 5 so that χ5 (d ) = χ2 (d) = χ5 (d), and we are done. This finishes the proof that f 5 f 4 .

On XPath with Reflexive-Transitive Axes and Data Tests

• 27

• We now show that f 4 f 2 . Again, notice that R 4 = R 2 = R 5 , and since for every d ∈ D, χ4 (d) is either χ2 (d) or χ5 (d), it follows that for every

d ∈ R 4 = R 5 , χ4 (d) = χ2 (d).
We show that for every

d ∈ data(f 4 ), χ4 (d) = χ2 (d). If d ∈ D ∪ R 1 , then χ4 (d) = χ2 (d) by definition. If d ∈ R 4 , then χ4 (d) = χ2 (d) as shown before. If d ∈ D ∪ R 1 ∪ R 4 , χ4 (d) = χ5 (d). Notice that χ5 (d) = (∅, ∅, ∅, ∅), since otherwise d ∈ data(f 4 ). Then, d ∈ data(f 5 ) and since f 5 f 2 , χ5 (d) = χ2 (d) = χ4 (d).
We finish the proof of f 4 f 2 by showing that for every

d ∈ data(f 2 ) \ R 2 there is some d ∈ data(f 4 ) \ R 2 so that χ2 (d) = χ4 (d ). If d ∈ D ∪ R 1 , then we can just simply take d = d and χ2 (d) = χ4 (d ). If d ∈ D ∪ R 1 , then χ4 (d) = χ5 (d), notice that χ5 (d) = (∅, ∅, ∅, ∅) because otherwise d ∈ data(f 4 ) (since d ∈ R 4 ). Hence, d ∈ data(f 5 ) and since f 5 f 2 , we have that χ2 (d) = χ5 (d), hence χ2 (d) = χ4 (d).
We just showed that f 4 f 2 .

We define f 3 as follows

f 3 :                R 3 = R 1 for every d ∈ R 1 , χ3 (d) = χ1 (d) for every d ∈ data(f 4 ), χ3 (d) = χ1 (d) for every d ∈ d, χ3 (d) = χ1 (d) for every strictly external value d of f 1 , χ3 (d) = χ1 (d).
Claim 5.9.2. f 3 f 1 .

Proof. By definition we have that R 1 = R 3 , and that χ3 (d) = χ1 (d) for all d ∈ R 1 . Also by definition, for every d ∈ data(f 3 ) we have χ3 (d) = χ1 (d).

We must show that for every d ∈ data(f 1 ) \ (R 1 ∪ data(f 3 )) there is some d ∈ data(f 3 ) \ R 1 so that χ1 (d) = χ3 (d ). Take any such d. Note that d must be necessarily an internal data value, since f 3 contains any strictly external data value of f 1 . Hence, let π = χ1 (d), where π

↓ i 1 ∪ π ↓ i 1 = ∅. By definition of D, there must be some d π ∈ D so that χ1 (d π ) = π and d π ∈ R 1 . Since π is internal and f 1 ∈ (a, d)f 2 , d π ∈ d∪data(f 2 ). If d π ∈ d, we have, by definition of f 3 , that χ3 (d π ) = χ1 (d π ) = π = χ1 (d). Hence, there is such d ∈ data(f 3 ) \ R 1 so that χ1 (d) = χ3 (d ). Otherwise, suppose d π ∈ data(f 2 ), which means, since π ↓ i 1 ∪ π ↓ i 1 = ∅, that χ2 (d π ) = (∅, ∅, ∅, ∅). By definition of f 4 , χ4 (d π ) = χ2 (d π ) = (∅, ∅, ∅, ∅), thus d π ∈ data(f 4 ). Then, by definition of f 3 we have that χ3 (d π ) = χ1 (d π ) = π = χ1 (d).
Hence, in this case we also have that there is such

d ∈ data(f 3 ) \ R 1 so that χ1 (d) = χ3 (d ). Claim 5.9.3. f 3 ∈ (a, d)f 4 . Proof. Since f 4 f 2 and f 1 ∈ (a, d)f 2 , we have that -ξ(f 4 ) ∈ Γ since ξ(f 2 ) ∈ Γ, by Lemma 5.4, and -χ ↓ e 4 = χ ↓ e 4 = ∅ since χ ↓ e 2 = χ ↓ e 2 = ∅.
Therefore, conditions (i) and (ii) hold for f 4 . We must show condition (iii), that is, χ

↓ i 3 = χ ↓ i 3 = {(d, α, βγ, i) ∈ D × Π | ∃α .(d, α , γ, i) ∈ χ ↓ i 4 ∪ χ ↓ i 4 , α, β ∈ σ a } ∪ i∈[k] ({ d(i)} × (σ a \ { }) × σ a × {i}) Take any data value of d ∈ d ∪ data(f 4 ). We have that χ ↓ i 3 (d) = χ ↓ i 1 (d) by definition. We also have that χ ↓ i 1 (d) = χ ↓ i 1 (d) = {(α, βγ, i) ∈ Π | ∃α .(d, α , γ, i) ∈ • Diego Figueira χ ↓ i 2 ∪ χ ↓ i 2 , α, β ∈ σ a } ∪ d= d(i),i∈[k] ((σ a \ { }) × σ a × {i}). Since f 2 and f 4 coincide in d, we also have that the set above is equal to {(α, βγ, i) ∈ Π | ∃α .(d, α , γ, i) ∈ χ ↓ i 4 ∪ χ ↓ i 4 , α, β ∈ σ a } ∪ d= d(i),i∈[k] ((σ a \ { }) × σ a × {i}).
This, together with the fact that all internal values of f 3 are in data(f 4 ) ∪ d, implies that χ

↓ i 3 = χ ↓ i 3 = {(d, α, βγ, i) ∈ D × Π | ∃α .(d, α , γ, i) ∈ χ ↓ i 4 ∪ χ ↓ i 4 , α, β ∈ σ a } ∪ i∈[k] ({ d(i)} × (σ a \ { }) × σ a × {i})
as desired. Hence, condition (iii) holds, and we have that f 3 ∈ (a, d)f 4 . This concludes the proof.

Bounding the rigid values

In this section we show that we can reduce the derivation problem into a similar problem where all the profiles have boundedly many rigid values. This will be combined with the result of the next sections, stating that the derivation problem restricted to profiles with boundedly many rigid values is decidable in 2ExpSpace, to solve the derivation problem.

Lemma 5.10. If there is a derivable root profile, then there is a derivation tree for a root profile so that all the profiles in the forest have no more than 2|Π| rigid values.

Proof. Suppose we have

f = f 1 + • • • + f n .
Let us first show that for every (α, β, i) ∈ Π there can be at most one data value d ∈ D so that there is some j ∈ [n] with χ ↓ e j (α, β, i) = {d}. By means of contradiction, if there were two distinct data values d, d then there would be two f j , f k with j = k so that χ ↓ e j (α, β, i) = {d} and χ ↓ e k (α, β, i) = {d }. Suppose without any loss of generality that j < k. Then, by definition of +, we must have that-since d ∈ χ ↓ e j (α, β, i) and , β, i). This is in contradiction with the fact that χ Let us define

f j +• • •+f k is defined- d ∈ χ ↓ e k (α
R l χ1,..., χn def = {d ∈ D | χ ↓ e j (α, β, i) = {d} for some (α, β, i) ∈ Π and j ∈ [n]}, R r χ1,..., χn def = {d ∈ D | χ ↓ e j (α, β, i) = {d} for some (α, β, i) ∈ Π and j ∈ [n]}, R χ1,..., χn def = R l χ1,.
.., χn ∪ R r χ1,..., χn . By the discussion before, it follows that |R χ1,..., χn | ≤ 2|Π|. Consider the profiles f , f 1 , . . . , f n to be as f, f 1 , . . . , f n but with R χ1,..., χn as the set of rigid values. By construction of R χ1,..., χn we have that

f = f 1 + • • • + f n .
In other words we have the following.

Claim 5.10.1. For every (R, χ) = (R, χ1 ) + • • • + (R, χn ) we have that (R χ1,..., χn , χ) = (R χ1,..., χn , χ1 ) + • • • + (R χ1,..., χn , χn ).
Using the above statement we can now prove the lemma. Let t be a derivation tree for a root profile (R, f). Let t be the derivation tree that results from replacing in t the profile labels (R, χ1 ), . . . , (R, χn ) of any maximal sequence of siblings with the labels (R χ1,..., χn , χ1 ), . . . , (R χ1,..., χn , χn ). Proof. Without any loss of generality, let us assume that f f and f f so that data(f

• Diego Figueira (a, d) f 1 f f 1 f f f (a, d) ∈ f 1 f f f (a,
) ∩ data(f ) = data(f ) ∩ data(f 1 ) = data(f). We define f so that R = R and χ (d) = χ (d) if d ∈ data(f ), χ (d) else, if d ∈ data(f ).
The following statement follows straight from this definition.

Claim 5.15.1. f f , f f . Proof. By definition of f f and f f for every data value d ∈ data(f ) ∪ data(f ) there is a data value f (d) ∈ data(f) so that χ(d) = χ (d) = χ (d) and d ∈ R iff f (d) ∈ R. Then, -f = f [f (d 1 ) → f (d 1 ), d 1 ] • • • [f (d n ) → f (d n ), d n ] for {d 1 , . . . , d n } = data(f ) \ data(f ), and -f = f [f (d 1 ) → f (d 1 ), d 1 ] • • • [f (d n ) → f (d n ), d n ] for {d 1 , . . . , d n } = data(f ) \ data(f ). Thus, f f , f f .
Remember that by definition of f f , for every data value d ∈ data(f ) there must be some data value f (d) ∈ data(f ) so that χ (d) = χ (d). We can further assume that for every

d ∈ data(f ), d ∈ R 1 iff f (d) ∈ R 1 (i.e., we can simply define f (d) = d for all d ∈ R 1 ∩ data(f )). We define f 1 as R 1 = R 1 and χ 1 (d) = χ 1 (d) if d ∈ data(f 1 ) χ 1 (f (d)) else, if d ∈ data(f ). Claim 5.15.2. f 1 ∈ (a, d)f .
Proof. For every data value of d ∈ data(f 1 ) we have that χ 1 (d) and χ (d) are equal to χ 1 (d) and χ (d), and it therefore verifies the conditions imposed by the rooting operation. Further, any other data value of data(f 1 ) (namely any data value from data(f ) \ data(f 1 )) behaves as some data value f (d) in f 1 . That is χ 1 (d) and χ (d) are equal to χ 1 (f (d)) and χ (f (d)). It then follows that that the data value must verify the conditions imposed by the rooting operation. Finally, by Lemma 5.4, ξ(f 1 ) ∈ Γ and f 1 f 1 , we have that ξ(f 1 ) ∈ Γ. Hence, f 1 ∈ (a, d)f .

On XPath with Reflexive-Transitive Axes and Data Tests 12. Statement of Lemma 5.17.

• 31 f 2 f 1 f 2 f 1 + f 2 f 1 f 2 f 1 f 2 f 1 f 2 f 1 + f 2 f 1 + Fig.
By definition of f 1 , it also follows that f 1 f 1 .

Claim 5.15.3. f 1 f 1 .

Proof. It is immediate from the definition that

f 1 = f 1 [f ( d1 ) → f ( d1 ), d1 , . . . , f ( ds ) → f ( ds ), ds ],
where { d1 , . . . , ds } = data(f ) \ data(f 1 ). By definition of f , f ( d1 ), . . . , f ( ds ) ∈ data(f ) \ R 1 , and hence f 1 f 1 . This concludes the proof.

Lemma 5.16. R up (↑↓D b ) ⊆ ↓D b . Proof. Let f 1 ∈ R up (↑↓D b ).
This means that there is some f ∈ D b and f so that f f , f f , and f 1 ∈ (a, d)f for some (a, d) ∈ A × D k . We can then apply Lemma 5.15, obtaining that there is some f and f 1 so that f f , f f , f 1 f 1 , and f 1 ∈ (a, d)f . Since D b is upward-closed by Remark 5.13, f ∈ D b , and therefore f 1 ∈ D b as well since f 1 ∈ (a, d)f . Thus, as f 1 f 1 , we obtain f 1 ∈ ↓D b .

Lemma 5.17 (Figure 12). For every i ∈ {1, 2} and f i ,

f i f i ∈ F b so that f i f i , f i f i and f 1 + f 2 is defined, there are f 1 , f 2 ∈ F b so that f 1 + f 2 f 1 + f 2 and f i f i , f i f i for every i ∈ {1, 2}.
Proof. Without any loss of generality, assume that f i f i , f i f i and data(f i )∩ data(f i ) = data(f i ) for every i ∈ {1, 2}. Remember that by definition of f i f i , for every data value d ∈ data(f i ) there must be some data value f (d) ∈ data(f i ) so that χi (d) = χ i (d) = χ i (d). We then define f i for every i ∈ {1, 2} so that R i = R i and

χ i (d) =          χ i (d) if d ∈ data(f i ), χ i (d) else, if d ∈ data(f i ), χ i (f (d)) else, if d ∈ data(f 3-i ), (∅, ∅, ∅, ∅) otherwise.
In the definition above, notice that for every d ∈ data(f 3-i ) we have that f (d) ∈ data(f 3-i ) and hence f (d) ∈ data(f 3-i ) which, by definition of

f 1 + f 2 , means that f (d) ∈ data(f i ).
The following claim follows straight from the definition just given.

• Diego Figueira

Claim 5.17.1. f i f i , f i f i for all i ∈ {1, 2}.

Proof. Since f i f i and f i f i , there is some f so that for every

d ∈ data(f i ), f (d) ∈ data(f i ) so that χ i (d) = χi ( f (d)) = χ i ( f (d)) and d ∈ R i iff f (d) ∈ R i .
For every i ∈ {1, 2}, it is immediate from the definition of f i that

f i = f i [f ( d1 ) → f ( d1 ), d1 ] • • • [f ( dn ) → f ( dn ), dn ] [f (d 1 ) → f (d 1 ), d 1 ] • • • [f (d m ) → f (d m ), d m ]
where {d 1 , . . . , d m } = data(f 3-i ) and { d1 , . . . , dn } = data(f i ) \ data(f i ).

Since f i f i and f i f i , there is some f so that for every

d ∈ data(f i ), f (d) ∈ data(f i ) so that χ i (d) = χi ( f (d)) = χ i ( f (d)) = χ i ( f (d)) and d ∈ R i iff f (d) ∈ R i .
For every i ∈ {1, 2}, it is immediate from the definition of f i that

f i = f i [ f ( d1 ) → f ( d1 ), d 1 ] • • • [ f ( dn ) → f ( dn ), d n ] [f (d 1 ) → f (d 1 ), d 1 ] • • • [f (d m ) → f (d m ), d m ]
where each d i and di is so that {d 1 , . . . , d m } = data(f 3-i ) and { d1 , . . . , dn } = data(f i ).

We are then left with the following easy claim.

Claim 5.17.2.

f 1 + f 2 f 1 + f 2 .
Proof. For every data value d ∈ data(f 1 ) ∪ data(f 2 ) it is easy to see that the conditions of + apply for f 1 and f 2 since they have the same description for d. For any other data value d ∈ data(f 1 ) ∪ data(f 2 ) we have that f 1 and f 2 behave just as f 1 and f 2 for the data value f (d). Therefore, the conditions of + hold, and f 1 + f 2 is well defined. Moreover, f 1 + f 2 f 1 + f 2 since, by definition of f 1 , f 2 we have

f 1 + f 2 = (f 1 + f 2 )[f (d 1 ) → f (d 1 ), d 1 ] • • • [f (d n ) → f (d n ), d n ] for {d 1 , . . . , d n } = data(f 1 + f 2 ) \ data(f 1 + f 2 ).
This concludes the proof of the lemma. Proof. Let f 3 ∈ R + (↑↓D b ). Then, there must be some

f 1 , f 2 ∈ F b so that f 1 + f 2 = f 3 so that there exist f 1 , f 2 , f 1 , f 2 where f i ∈ D b , f i f i , f i f i for all i ∈ {1, 2}
. Therefore, by Lemma 5.17, there must be some

f 1 , f 2 ∈ F b so that f 3 = f 1 + f 2 f 1 + f 2 and f i f i , f i f i for all i ∈ {1, 2}. Since f 1 , f 2 ∈ D b ,
and since D b is upward-closed by Remark 5.13, we have that f 1 , f 2 ∈ D b and hence

f 1 + f 2 ∈ D b . Hence, since f 3 f 1 + f 2 it follows that f 2 ∈ ↓D b .
Proof of Lemma 5.14. Immediate from Lemmas 5.16 and 5.18.

The algorithm

In this section we show how to compute, in 2ExpSpace, whether there exists a derivable root profile in D b , solving thus the derivation problem.

For G ⊆ F b , we define G ∼ def = {f | f ∼ f for some f ∈ G}. We define G/∼ as the set containing one representative profile of G for each ∼-equivalence class. We On XPath with Reflexive-Transitive Axes and Data Tests

• 33 define min(G) as the set of -minimal elements of G,

min(G) def = {f ∈ G | for all f ∈ G so that f f we have f ∼ f }.
For any f ∈ F, we write |f|-the size of f-, as the size needed to write f. Note that for all f ∈ min(F b ), |f| is at most exponential in |P|. For any G ⊆ F, we write |G| to denote f∈G |f|.

Let us define C i for every i ∈ N 0 as

C 0 def = {f ∅ }, C i+1 def = C i ∪ min ↓R(↑↓C i ) /∼.
Let k 0 ∈ N 0 be the first index so that

C ∼ k0 = C ∼ k0+1 . Remark 5.19. For every i ∈ N 0 , C i ⊆ min(F b ).
As a consequence of the property of the preceding section, we have that this algorithm computes min(↓D b ). Proof of Lemma 5.20. By Lemma 5.14 we know that R(↑↓D b ) ⊆ ↓D b . Therefore, since C 0 ⊆ min(↓D b ), we have that for every i, C i ⊆ min(↓D b ). We then need to show that min(↓D b ) ⊆ C ∼ k0 . Suppose, by means of contradiction, that there is some f ∈ F b so that f ∈ min(↓D b ) but f ∈ C ∼ k0 . Then, since {f ∅ } = C 0 ⊆ C k0 there must be one such f so that f f for some f ∈ D b where f

= f 1 + f 2 for f 1 , f 2 ∈ C ∼ k0 , or f ∈ (a, d)f for f ∈ C ∼ k0 , (a, d) ∈ A × D k . -If f = f 1 + f 2 where f 1 , f 2 ∈ C ∼ k0 , then f ∈ R + (↑↓C k0
), and hence we have that , d) up (↑↓C k0 ), and hence we have that f ∈ min(R (a, d) up ) ⊆ C ∼ k0+1 = C ∼ k0 , which is also an absurd. Therefore, min(↓D b ) ⊆ C ∼ k0 and thus C ∼ k0 = min(↓D b ). We further have that this computation is in 2ExpSpace. Since |min(F b )/∼| is doubly exponential in |P|, we have the following.

f ∈ min(R + (↑↓C k0 )) ⊆ C ∼ k0+1 = C ∼ k0 , which is an absurd. -If f ∈ (a, d)f where f ∈ C ∼ k0 , then f ∈ R (a
Lemma 5.21. k 0 is bounded by a doubly exponential function on |P|.

Proof. Remember that F b is the set of profiles that have less than 2|Π| rigid values. Then,

2 Π × 2 Π × 2 Π × 2 Π 2|Π|
represent all the possible profiles of the rigid values. We must also remember which profiles have either 0, or 1 or more flexible values, and this information can be

• 35 f 1 ∈ min({f ∈ F b | ξ(f) ∈ Γ})
, and f ∈ min(↓D b ). This means that there must be some f ∈ D b so that f f and some f so that f f and f 1 ∈ (a, d)f . We can then apply Lemma 5.15 obtaining that there is some f and f 1 so that f f , f f , f 1 f 1 , and f 1 ∈ (a, d)f . Since D b is upward closed (Remark 5.13), f ∈ D b and hence f 1 ∈ D b . By definition of , it follows that, since f 1 has no external data values, f 1 has no external data values either. Thus, there is a derivable root profile, namely f 1 .

[1⇐2] Suppose, on the other hand, that condition 2 holds. If there is a derivable root profile in D b , then there are f, f ∈ D b and (a, d) Since there is a derivable root profile in D b if and only if there is a derivable root profile in D by Lemma 5.12, the proposition follows.

∈ A root × D k so that χ ↓ e = χ ↓ e = ∅ and f ∈ (a, d)f . Let f 1 ∈ min(↓{f })/∼, that is, f 1 is a minimal element corresponding to f . Also, let f 1 ∈ min(↓{f})/∼, that is, f 1 is a minimal element corresponding to f. Of course, it follows that f 1 ∈ min(↓R (a, d) up (↑↓{f 1 })). Note that f 1 ∈ min({f ∈ F b | ξ(f) ∈ Γ}),

FROM XPATH TO FOREST PROFILES

In this section we reduce the satisfiability problem for XPath( * ←, ↓ * , → * , =) into the derivation problem for forest profiles.

In Section 6.1 we define a normal form for XPath( * ←, ↓ * , → * , =), called direct unnested normal form, and in Section 6.2 we show the reduction from the satisfiability problem of direct unnested XPath( * ←, ↓ * , → * , =) formulas into the derivation problem for forest profiles.

Normal forms

We will assume a certain normal form of the formula ϕ ∈ XPath( * ←, ↓ * , → * , =) to test for satisfiability. This will simplify the reduction into the derivation problem for forest profiles.

The normal form has two main properties. Firstly, it contains only path expressions that are direct, in the sense that the navigation consists in going left and then down, or going right and then down. And secondly, path expressions do not contain data tests as node expressions, in other words the formula is unnested. Next, we explain in detail these properties.

Preliminaries. Let α = a 1 • • • a n with n > 0 be a XPath( * ←, ↓ * , → * , =) path expression, where for every i, a i = [ψ] for some node expression ψ, or a i ∈ {ε, * ←, ↓ * , → * }. We say that α is in alternating path normal form if either α = ε, or n is even and for all 1 ≤ i ≤ n

-if i is even, a i = [ψ] for some node expression ψ, -if i is odd, a i ∈ { * ←, ↓ * , → * }.
In other words, the path alternates between axes and tests for node expressions. We say that a formula is in alternating path normal form if all its path expressions are in alternating path normal form. Note that one can turn any formula ϕ ∈ XPath( * ←, ↓ * , → * , =) into an equivalent formula ϕ in alternating path normal form • Diego Figueira in polynomial time, using the equivalences [ψ]α@ i β@ j ≡ ψ ∧ α@ i β@ j for ∈ {=, =},

α@ i [ψ]β@ j ≡ ψ ∧ α@ i β@ j for ∈ {=, =}, α[ψ 1 ][ψ 2 ]β ≡ α[ψ 1 ∧ ψ 2 ]β,

( )

For simplicity and without any loss of generality we can further assume that all our formulas do not contain formulas of the type α , since it is equivalent to α@ 1 = α@ 1 . We will henceforth assume that all the formulas we work with are in this form.

We say that a path expression in alternating path normal form is a rightward path expression, if it starts with → * and all the axes in it are → * (similarly with leftward, downward and * ←, ↓ * ). Notice that, for example, a leftward expression may contain node tests using rightward or downward axes. For example, *

←[ ↓ * [a] ] * ←[b] is a leftward expression while * ←[a]↓ * [ * ←[a] ] is not.
Direct normal form. The object of the direct normal form is to avoid having unnecessary mixed directions in path formulas, that use perhaps → * and * ← in the same expression, or that contain a * ← (or → * ) axis after a ↓ * axis. That is, we avoid having formulas like

→ * [a] * ←@ 1 = ↓ * [b]→ * @ 2
in favor of equivalent formulas with a more direct navigation, like

→ * [ → * [a] ]@ 1 = ↓ * [ * ←[b] ]@ 2 ∨ [ → * [a] ] * ←@ 1 = ↓ * [ * ←[b] ]@ 2 . ( ‡)
In the formula above we factor the loops that may be in the navigation of the path expression to obtain a simple navigation that goes in only one horizontal direction. We say that a formula ϕ ∈ XPath( * ←, ↓ * , → * , =) is in direct normal form, if every path expression is ε, or of the form α•β, where α•β = (i.e., it is not the empty string), α is leftward, rightward or empty, and β is downward or empty. Note that, strictly speaking, the formula ( ‡) is not in direct normal form since its second disjunct is not in alternating path normal form, but the equivalent alternating path expression-using ( )-is in direct normal form. Lemma 6.1 (Direct normal form). There exists an exponential time translation that for every node expression ϕ ∈ XPath( * ←, ↓ * , → * , =) returns an equivalent node expression ψ in direct normal form.

Proof. The idea is that every data test expression α@ i = β@ j is translated into a big disjunction of expressions in direct normal form, where loops in the tree navigation of α, β are factored as node expressions, as done in ( ‡).

For any finite alphabet B, we define tree order morphisms between forests over a powerset alphabet 2 B . Given two forests t, t over 2 B , a tree order morphism from t to t is a function f from the nodes of t to the nodes of t so that -for every node x of t, the label of x in t is a subset of the label of f (x) in t , and -for every two nodes x, y of t, if (x, y) is in the reflexive-transitive closure of the next-sibling relation (resp. of the child relation) in t, then (f (x), f (y)) is also 1 9 @ : 2 4 c @ : 1 9 @ : 2 7 b @ : 1 9 @ : 2 4 a @ : 1 9 @ : 2 7 a @ : 1 9 @ : 2 4 c @ :

1 1 @ : 2 4 a @ : 1 9 @ : 2 2 b @ : 1 7 @ : 2 4 b @ : 1 9 @ : 2 4 c @ : 1 5 @ : 2 1 a @ : 1 2 @ : 2 4 x y ψ1 ψ3 ψ4 ψ6 ψ5 a b c ψ2 µ α t,x,y = [ψ6 ∧ ψ7]→ * [ψ1 ∧ → * [ψ3]]↓ * [ ∧ → * [ψ4]]↓ * [ψ2] α = * ←[ψ6]→ * [ψ3] * ←[ψ7]→ * [ψ1]↓ * [ψ4] * ←[]↓ * [ψ2] ψ 6 = ¬ * ← [a] ψ 5 = ¬a ψ 4 = b ψ 3 = c ψ 2 = ↓ * [a] ψ 1 = a
α = * ←[ψ6]→ * [ψ3] * ←[ψ7]→ * [ψ1]↓ * [ψ4] * ←[]↓ * [ψ2] µ α t,x,y = [ψ6 ∧ ψ7]→ * [ψ1 ∧ → * [ψ3]]↓ * [ ∧ → * [ψ4]]↓ * [ψ2] where ψ1 = a ψ3 = c ψ5 = ¬a ψ2 = ↓ * [a] ψ4 = b ψ6 = ¬ * ←[a]
form α•β, where α•β = (i.e., it is not the empty string), α is leftward, rightward or empty, and β is downward or empty.

Lemma 6.1 (Direct normal form). There exists an exponential time translation that for every node expression ϕ ∈ XPath( * ←, ↓ * , → * , =) returns an equivalent node expression ψ in direct normal form.

Proof. The idea is that every data test expression α@i = β@j is translated into a big disjunction of expressions in direct normal form, where possible loops in the tree navigation of α, β are factored away as node expressions.

We define a order homomorphisms between forests as follows. Given two forests t, t , a reflexive homomorphisms between t and t is a function f from the nodes of t into the nodes of t so that for every two nodes x, y of t, if (x, y) are in the reflexive-transitive closure of the next-sibling relation (resp. the child relation), then (f (x), f(y) are also in the reflexive-transitive closure of the next-sibling relation (resp. the child relation).

Consider a forest t labeled with sets of node expressions of XPath( * ←, ↓ * , → * , =), and let x, y be two nodes of t, so that x is a root. For such a forest and nodes, one can build a direct path expression µ α t,x,y that tests if there is a path between x and y satisfying the relative appearance of nodes satisfying the labels as in the tree. For example, for the WHAT IS WITNESS FOREST? Given a mu data tree t so that t, (x, y) |= α, we call a w of α for t, (x, y) to a forest t over the alphabe nodes x, y, where t are the nodes involved in th of α, and they are labeled with the node exp they must verify. For example, given the mu data tree of Figure 11-a, and α as defined in F possible witness forest is depicted in Figure 11all witness forests of α for t, (x, y) are bounded some polynomial p( ).

xxx We define a contraction of a forest over the alp as the transitive clausure of the following ope two successive nodes (horizontally or vertically them by only one, whose tag is the union of th being contracted.

xxx Given a path expression α, consider α as the sion over the alphabet 2 ne(α) , where every nod ψ is replaced by S⊆ne(α),ψ∈S S, that is, it is test for a letters from the alphabet. For every the alphabet 2 ne(α) and nodes x, y so that t, (x say that µ α t,x,y is a direct normal form lineariza follows that t, (x, y) |= µ α t,x ,y if, and only if, eit -or a contraction of t, (x , y )-is a witness fo t, (x, y). Note that if t , x , y is a contractio then: If t, (x, y) |= µ α t ,x ,y then t, (x, y) |= µ α t,

Therefore, the following follows. We say that t , (x , y ) is a contraction of t, (x, y) if there is a tree order morphism f from t to t so that f (x) = x and f (y) = y . We also say that t, (x, y) is an expansion of t , (x , y ). Notice that the function need not be surjective, and hence the fact that one forest is a contraction of another does not have any implication on the sizes of the forests: a forest may have less or more nodes than its contraction. For example, both the tree of Figure 13-b and the forest of Figure 13-d are contractions of the forest of Figure 13-c.

ψ 1 ψ 3 ψ 4 ψ 2 ψ 6 ψ 5 ψ 1 ψ 1 ψ 1 ψ 3 ψ 3 ψ 5 ψ 5 ψ 5 ψ 5 ψ 5 ψ 5 ψ 2 ψ 2 ψ 2 ψ 2 ψ 4 ψ 4 ψ 4 ψ 6 ψ 6 ψ 6 ψ 6 x y b @ : 1 9 @ : 2 4 c @ : 1 9 @ : 2 7 b @ : 1 9 @ : 2 4 a @ : 1 9 @ : 2 7 a @ : 1 9 @ : 2 4 c @ : 1 1 @ : 2 4 a @ : 1 9 @ : 2 2 b @ : 1 7 @ : 2 4 b @ : 1 9 @ : 2 4 c @ : 1 5 @ : 2 1 a @ : 1 2 @ : 2 4 a x y ψ 1 ψ 3 ψ 4 ψ 6 ψ 5 ψ 2 d

• Diego Figueira

Let α be a path expression, and let ne(α) be the set of all node expressions of α. Consider tα the tree over the alphabet 2 ne(α) , where every node is labeled by those ψ ∈ ne(α) that are true at the node. For example, for the multi-attribute data tree t defined in Figure 13-a and α as defined in Figure 13-e, the tree tα is the one of Figure 13-b.

Let t be any forest over 2 ne(α) , and let x, y be two nodes of t, so that x is a root. For such a forest and nodes, one can build a direct path expression µ α t,x,y that tests if there is a path between x and y satisfying the order of nodes satisfying the labels as in the tree. For example, for the forest t of Figure 13-c and the nodes x, y depicted, the corresponding expression μα t,x,y would be the one appearing in Figure 13-e. Claim 6.1.1. A direct path expression µ α t,x,y can be built from t in polynomial time, such that for every multi-attribute data tree t we have that t, (x , y ) |= µ α t,x,y if and only if tα , (x , y ) is a contraction of t, (x, y).

Proof. Given a forest t and nodes x, y so that x is a root, one can build µ α t,x,y iteratively. We first build a path expression that starts in x and and ends in y and checks all the labels of 2 ne(α) between x and y in the unique path between x and y that corresponds to a direct navigation. For example if t, x, y are as in Figure 14-a, we build a path as in Figure 14-b that tests all the node expressions of the nodes in the path. In this example the path has three nodes, so the expression would be of the form

[ 1 ]→ * [ 2 ]↓ * [ 3 ] where i ⊆ ne(α)
is the label of the node i in the figure. We then build a more complex path expression nesting expressions that test the existence of paths as depicted in Figure 14-c. In our example, it would correspond to

[ 1 ∧ * ←[ 4 ]↓ * [ 5 ] nesting ]→ * [ 2 ]↓ * [ 3 ∧ * ←[ 6 ] nesting ∧ ↓ * [ 7 ] nesting ].
We iterate until we have covered the whole tree t, at each iteration, we add tests for paths that are at a deeper nesting degree in the resulting direct path expression. For example, the paths of Figure 14-c are at depth 1, the paths of Figure 14-d at depth 2, and the path of Figure 14-e at depth 3. The resulting expression µ α t,x,y in our example would then be

1 ∧ * ←[ 4 ]↓ * [ 5 ∧ → * [ 8 ] nesting 2 ] nesting 1 → * 2 ↓ * 3 ∧ * ←[ 6 ] nesting 1 ∧ ↓ * [ 7 ∧ → * [ 9 ]↓ * [ 10 ∧ → * [ 11 ]→ * [ 12 ] nesting 3 ] nesting 2 ] nesting 1
.

Note that if we apply this construction to the forest of Figure 13-c and the path α of Figure 13-e, we obtain the expression µ α t,x,y of Figure 13-e. Given a multi-attribute data tree t so that t, (x, y) |= α, we call a witness forest of α for t, (x, y) to a forest t over the alphabet 2 ne(α) together with some nodes x, y, so that t contains only the nodes involved in the satisfaction of α, and they are labeled with the node expressions that they must verify. For example, given the multi-attribute data tree t of Figure 13-a, and α as defined in Figure 13-e, a possible witness forest of α for t, (x, y) is depicted in Figure 13-c. Of course, there may be several witness forests of α for a given t, (x, y). Let ||α|| be the size of α, computed as the number of axes in α, irrespective of the size of node expressions. For example the path expression α defined in Figure 13-e is so that ||α|| = 7.

Notice that the number of nodes of any witness forest of α for t, (x, y) is bounded by p(||α||) for some polynomial p( ). Given a path expression α, let α be the path expression over the alphabet 2 ne(α) , where every node expressions ψ is replaced by S⊆ne(α),ψ∈S S, that is, it is treated as a disjunction of tests for labels from the alphabet. Notice that any witness forest t, (x , y ) of α for t, (x, y) is an expansion of tα , (x, y), and we have t, (x , y ) |= α. We then have the following. Claim 6.1.2. t, (x, y) |= α if, and only if, t, (x , y ) |= α, for some expansion t, (x , y ) of tα , (x, y).

For every contraction t, (x, y) of t , (x , y ), if t , (x , y ) |= α then t , (x , y ) |= α. This observation, together with the previous claim and the fact that every witness forest t, (x , y ) of α for t, (x, y) is bounded by p(||α||) yields the following. Claim 6.1.3. There is an expansion t, (x , y ) of tα , (x, y) of size at most p(||α||) so that t, (x , y ) |= α if, and only if, t, (x, y) |= α.

For every forest t over 2 ne(α) of size ≤ p(||α||) and nodes x, y so that t, (x, y) |= α, we say that µ α t,x,y is a direct normal form linearization of α. It follows that t, (x, y) |= µ α t,x ,y if, and only if, a contraction of t, (x , y ) is a witness forest of α for t, (x, y). Thus, the following claim follows. Claim 6.1.4. t, (x, y) |= α if, and only if, t, (x, y) |= µ α t,x ,y for some direct normal form linearization µ α t,x ,y of α.

• Diego Figueira

Proof. If t, (x, y) |= α, then by Claim 6.1.3 there is a forest t, (x , y ) over 2 ne(α) (the witness forest) of size ≤ p(||α||) so that t, (x , y ) |= α. Hence, µ α t,x ,y is a direct normal form linearization of α. Since t, (x , y ) is an expansion of tα , (x, y) and t, (x , y ) |= α, then t, (x, y) |= µ α t,x ,y . Suppose now that t, (x, y) |= µ α t,x ,y for some t, (x , y ) over 2 ne(α) of size ≤ p(||α||) so that t, (x , y ) |= α. Then, t, (x , y ) must be an expansion of tα , (x, y) by Claim 6.1.1. Since t, (x , y ) |= α, we then have that t, (x, y) |= α by Claim 6.1.3.

Note that there are exponentially many trees in ||α|| over ne(α) of size ≤ p(||α||). Hence, all the direct normal form linearizations of a given path expression α are computable in exponential time ||α||. Hence, given ϕ ∈ XPath( * ←, ↓ * , → * , =), consider ϕ as the result of replacing every appearance of α@ i = β@ j (resp. =) by a disjunction of µ α t,x,y @ i = µ β t ,x ,y @ j (resp. =) for every direct normal form linearization µ α t,x,y of α and µ β t ,x ,y of β. Since these are all the possible linearizations, the translated formula is satisfied in the same multi-attribute data trees and nodes as the original formula. Further, ϕ is in direct normal form. Since every replacement is exponential in ||α||, and since ||α|| does not depend on the size of sub-node expressions, it follows that |ϕ | in time exponential in |ϕ|. Thus, the lemma follows.

Unnested normal form. The second normal form consists in having formulas without nesting of data tests. That is, we avoid treating formulas like, for example

↓ * [ * ←[a]@ 1 = → * [b]@ 1 nested data test ]@ 1 = → * [c]@ 2 .
If a formula is such that all its path expressions α contain only (boolean combinations of) tests for labels we call it a non-recursive formula.

We say that ϕ is in unnested normal form if ϕ = ϕ 1 ∧ ϕ 2 where ϕ 1 ∈ B(A) and ϕ 2 is a conjunction of tests of the form "if a node has some of the labels {a 1 , . . . , a n } then it satisfies ψ" for some non-recursive formula ψ and labels a 1 , . . . , a n ∈ A. Formally, ϕ 2 contains a conjunction of tests of the form

¬ ↓ * [τ ∧ ¬ψ]
for τ a disjunction of labels and ψ a non-recursive formula. Given ϕ = ϕ 1 ∧ ϕ 2 in unnested normal form, we write γ ϕ (a) for a ∈ A to denote the function where γ ϕ (a) is the conjunction of all the formulas ψ such that ϕ 2 contains ¬ → * [τ ∧ ¬ψ] as a subformula, for some disjunctive formula τ containing the label a.

Then, we obtain the following.

Lemma 6.2 (Unnested normal form).

There exists an exponential time translation that for every formula η ∈ XPath( * ←, ↓ * , → * , =) returns a formula ϕ in unnested normal form such that η is satisfiable iff ϕ is satisfiable. Further, the translation of a formula in direct normal form is in direct normal form.

Proof. Given a formula η we define the alphabet A ϕ of the translation ϕ as all the locally consistent sets of subformulas of η. That is, the sets S such that for every subformula ψ of η: To build the formula ϕ = ϕ 1 ∧ ϕ 2 in normal form, we define ϕ 1 = ζ η , and we build ϕ 2 as a conjunction of formulas

(1) if ψ = ¬ψ then {ψ , ¬ψ } ⊆ S; (2) if ψ = ψ ∧ ψ then ψ ∈ S iff {ψ , ψ } ⊆ S; and (3) if ψ = ψ ∨ ψ then ψ ∈ S iff ψ ∈ S or ψ ∈ S.
¬ ↓ * [ζ ψ ∧ ¬tr(ψ)]
for all subformulas ψ of η. It is easy to see that this translation preserves satisfiability.

Corollary 6.3. About the translation of Lemma 6.2:

1. The set of path subformulas resulting from the translation has cardinality polynomial in η. 2. Every path subformula resulting from the translation can be written using polynomial space.

Proof. The blowup in the exponential translation comes only from the formulas ζ ψ . In fact, ϕ can be symbolically written in polynomial space just as we did, using a symbol ζ ψ instead of a big exponential disjunction. Remark that testing whether a label S ∈ A ϕ satisfies ζ ψ reduces to testing ψ ∈ S.

Reduction to the derivation problem

In this section we show how we can reduce the satisfiability problem of direct unnested XPath( * ←, ↓ * , → * , =) formulas into the derivation problem for forest profiles.

Let us fix φ = φ 1 ∧ φ 2 in direct unnested normal form, where A as the finite alphabet, k as the number of attributes, D as any infinite domain, and A root is the set of all a ∈ A that make φ 1 true.

Given a pattern α = ψ 1 • • • ψ k ∈ P, and an axis o ∈ { * ←, ↓ * , → * }, we can convert α into a path expression as follows:

P o ( ) def = ε if k = 0, P o (ψ 1 • • • ψ k ) def = o[ψ 1 ] o • • • o[ψ k ] if k > 0.
Note that P o is injective.

Let us define P φ as the set of patterns consisting of -the constant and the empty string , -ψ, for every ψ ∈ B(A) that is a subformula of φ, -every α ∈ (B(A)) * so that P → * (α), P * ← (α), or P ↓ * (α) is a substring of φ.

• Diego Figueira

It follows that P φ is finite and subword-closed.

For any direct non-recursive formula ψ that is a boolean combination of subformulas of φ and forest profile f, we define f ψ as follows. If ψ ∈ A, then f ψ if and only if there is some d ∈ D and i ∈ [k] so that (ψ, , i) ∈ χ ↓ i (d). For all the boolean cases is homomorphic. Suppose now that ψ = α•β@ i = γ•δ@ j where α is leftward, ε or empty, γ is rightward, ε or empty, and β, δ are downward or empty. We define f ψ if there are some d, d ∈ D so that d = d and -if α = or α = ε, ( ,

P -1 ↓ * (β), i) ∈ χ ↓ i (d), -if α = , α = ε, (P -1 * ← (α), P -1 ↓ * (β), i) ∈ ( → [f]• χ ↓ e ∪ χ ↓ i )(d),
-if γ = or γ = ε, ( , P -1 ↓ * (δ), j) ∈ χ ↓ i (d ),

-if γ = , γ = ε, (P -1 → * (γ), P -1 ↓ * (δ), j)

∈ ([f] →• χ ↓ e ∪ χ ↓ i )(d ).
Note that if α = ε then β = (resp. with γ and δ). If both α and γ are rightwards or leftwards it is defined in an analogous way. The case for = is also analogous, where d = d . The idea is that f ψ makes only sense when the derivation forest for f is a tree, and the multi-attribute data tree t associated to the derivation tree is so that t |= ψ.

For example, testing ψ is the same as testing if there is some pattern (ψ, , ) in χ ↓ i or χ ↓ i . In a similar way, checking a formula like

→ * [a]↓ * [b]@ 1 = ↓ * [c]@ 2
reduces to checking if there is a data value d ∈ D that can be reached with ( , c, 2) in the main forest (i.e., in χ ↓ i or χ ↓ i ), and either -d can be reached by (a, b, 1) in the main forest, that is, (a, b, 1) ∈ χ ↓ i (or equivalently χ ↓ i ), or -d can be reached in the right forest by (a, b, 1), where a could be tested in the main forest (i.e., a ∈ [f] →), that is, (a, b, 1)

∈ [f] →• χ ↓ e .
Note that checking f ψ takes polynomial time in the size of f and ψ. Also, whether f a∈A (a ⇒ γ ϕ (a)) holds or not depends only on ξ(f). Lemma 6.4. Given a direct non-recursive formula ψ that is a boolean combination of subformulas of φ, and two forest profiles f, f ∈ F so that ξ(f) = ξ(f ) then f ψ if, and only if, f ψ.

Proof. If ψ ∈ B(A), then it is immediate that f ψ iff ξ(f)((ψ, , i), •) = 0 for some i ∈ [k].

Suppose now that ψ = α•β@ i = γ•δ@ j where α is leftward, ε or empty and γ is rightward, ε or empty, and β, δ are downward or empty. We show that whether f ψ depends only on ξ(f). We show one of the possible cases in the definition of , while the remaining ones are analogous or simpler. Suppose, for example, that α = , α = ε, γ = . We then have that f ψ iff -there is at least one data value reachable with αβ@ i , that is, ξ(f)(ᾱ, • ↓ ) = 0, with ᾱ = (P -1 * ← (α), P -1 ↓ * (β), i), and -there is at least one data value reachable with γδ@ j , that is, ξ(f)( β, • ↓ ) = 0, with β = ( , P -1 ↓ * (δ), j) and either

On XPath with Reflexive-Transitive Axes and Data Tests

• 43

-there are two data values reachable with αβ@ i , that is, ξ(f)(ᾱ, • ↓ ) = 2+, or -there are two data values reachable with γδ@ j , that is, ξ(f)( β, • ↓ ) = 2+, or -there is one data value reachable with αβ@ i and only one data value reachable with γδ@ j , but they are different, that is, ξ(f)(ᾱ, • ↓ ) = 1, ξ(f)( β, • ↓ ) = 1, and

ξ(f)(ᾱ, • ↓ , β, • ↓ ) = 0.
These are indeed the necessary and sufficient conditions for the existence of two data values d = d so that d ∈ χ a ( ᾱ) and d ∈ χ a ( β), where a = • ↓ , a = • ↓ . Hence, these are the necessary and sufficient conditions to verify f ψ.

The remaining cases are analogous or easier.

We can then write ξ |= ψ for ξ ∈ F instead of f |= ψ for any f so that ξ(f) = ξ. We define the set of consistent profiles Γ φ as all ξ ∈ F so that ξ a∈A (a ⇒ γ ϕ (a)). The following lemma follows straight from the above definition of . Lemma 6.5. f a∈A (a ⇒ γ ϕ (a)) iff ξ(f) ∈ Γ φ . Proof. This is a direct consequence of Lemma 6.4 and the definition of Γ φ .

Abstractions. Given multi-attribute data forests tl , t, tr , we define abs( tl , t, tr ) as the forest profile that abstracts the forest t in the context of the forests tl to the left and tr to the right. We have already discussed the idea of this abstraction in Section 4. For example, for the forest of Figure 3 We have that abs is basically an algebra morphism between multi-attribute data forests with rooting and concatenation and forest profiles with profile rooting and profile concatenation. Further, the profile abs( , t, ) is a derivable root profile whenever t |= φ; and every derivable root profile is the abstraction of some tree t so that t |= φ.

We now define formally abs( tl , t, tr ) for any forests tl , t, tr . Let t l = a l ⊗d l , t = a⊗d, t r = a r ⊗d r be the multi-attributes data trees (a, d) tl , (a, d) t, and (a, d) tr respectively, for some fixed arbitrary (a, d). We then define abs( tl , t, tr ) = χ where For any R ⊆ D we define abs R ( tl , t, tr ) def = (abs( tl , t, tr ), R).

Remark 6.6. Note that abs ∅ ( , , ) = f ∅ .

• 45

2. If on the other hand (P -1 * ← (α), P -1 ↓ * (β), i) ∈ → [f]• χ ↓ e (d), either (P -1 * ← (α), P -1 ↓ * (β), i) ∈ χ ↓ e (d), or there must be some α 1 , α 2 so that α 1 ∈ → [f] and (α 2 , P -1

↓ * (β), i) ∈ χ ↓ e (d)
and α 1 •α 2 = P -1 * ← (α). Suppose that the latter occurs (the former being only easier). Since by definition of abs we have that χ The case where α = , or α = ε, γ = is only easier (it is basically as in the item 1). In any case we obtain that there is some y so that (i [⇐] Suppose that tl •t• tr , i 0 |= α•β@ i = γ•δ@ j . In other words, there are y, z ∈ pos(t ), y = , z = , so that (i 0 , y) ∈ [[α•β]] t , (i 0 , z) ∈ [[γ•δ]] t , and d = d (z)(i) = d (y)(j) for some d ∈ D. Let α = if α = ε or α = and α = P -1 * ← (α) otherwise.

1. If y is inside the subtree t of t , then (α , P -1 ↓ * (β), i) ∈ χ ↓ i (d), by definition of abs.

2. If y is inside the subforest tl of t , then we have that either (α , P -1 ↓ * (β), j) ∈ χ ↓ e (d), or there must be some α 1 , α 2 so that α 1 •α 2 = α, α 1 ∈ → [f] and (α 2 , P -1 ↓ * (β), j) ∈ χ ↓ e (d), where α 1 = P -1 * ← (α 1 ), α 2 = P -1 * ← (α 2 ). If the latter case holds (the former being only easier), we have that (α 1 •α 2 , P -1 ↓ * (β), j) ∈ ( → [f]• χ ↓ e )(d), which implies that (α , P -1 ↓ * (β), j) ∈ ( → [f]• χ ↓ e )(d).

By similar arguments, we obtain some (γ , P -1 ↓ * (δ), j) ∈ ( χ ), where γ = if γ = ε or γ = and γ = P -1 → * (γ) otherwise. Hence, f α•β@ i = γ•δ@ j . • The cases of α•β@ i = γ•δ@ j where both α and γ are rightwards or leftwards is similar. The same applies to the inequality formulas α•β@ i = γ•δ@ j .

↓ i ∪ [f] →• χ ↓ e )(d
The next lemma basically shows that every derivable root profile is the abstraction of some tree satisfying φ. Lemma 6.9. Let f root ∈ D be a root profile, and let t be its derivation tree. Let t be a maximal subforest of t, where t is the multi-attribute data forest associated with t, and f 1 , . . . , f n are the profile labels of the roots of t. Let R be the rigid set for f 1 , . . . , f n . Then, -abs R ( , t, ) = f 1 + • • • + f n , and t, i |= φ 2 for every 1 ≤ i ≤ | t|.

Proof. We will make use of the following easy fact. Claim 6.9.1. Given f 1 , . . . , f n ∈ F, so that f + = f 1 +• • •+f n where χ

↓ i i , χ ↓ i i | i ∈ [n]} determine the sets { χ ↓ e i , χ ↓ e i | i ∈ [n]}.
Proof. This is by conditions (b) and (c) of profile concatenation:

• Diego Figueira Theorem 6.12. The satisfiability problem for formulas of XPath( * ←, ↓ * , → * , =) in direct normal form is decidable in 2ExpSpace.

DISCUSSION

We have shown that XPath with downward, rightward and leftward reflexivetransitive axes is decidable. To show this, we devised an algebra with good monotonicity properties. This seems to be the right kind of approach to work with transitive relations, and it generalizes and simplifies, in some aspects, the work of [START_REF] Figueira | A decidable two-way logic on data words[END_REF]].

Upward axes. One natural question that stems from the result presented here is whether it can be extended to work with an upward axis as well. However, we claim (without a proof) that already SAT-XPath(↑ * , → * , =) has a non-primitive recursive lower bound. Indeed, this can be proved by reusing the results on lower bounds of [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. The cited work shows that XPath with one nonreflexive transitive axis is enough to prove non-primitive recursiveness provided that the axis is functional (i.e., the transitive closure of an axis like →, ←, ↑ but unlike ↓). Here, however, we feature reflexive-transitive axes instead of only transitive. Therefore, in principle we cannot use this result. However, one can somehow code ↑ + with → * [a]↑ * [¬a] for some label a.

By the previous claim, although it could be that full transitive XPath is decidable, it would have a non-primitive recursive lower bound. We can then answer negatively to the conjecture proposed in [Figueira 2011, Conjecture 2], stating that XPath( * ←, ↓ * , ↑ * , → * , =) be decidable in elementary time.

Satisfiability in the presence of a DTD. In the presence of DTD's, the satisfiability problem for XPath(↓ * , =) or XPath(→ * , =) has already a non-primitive recursive lower bound; and XPath( * ←, → * , =) has an undecidable satisfiability problem. This is a consequence of the lower bounds shown in [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. More precisely, consider the language L ⊆ (A × D) * of all data words where no two consecutive positions have the same label (i.e., it does not contain (a, d)(a, d ) as a substring for any a ∈ A, d, d ∈ D). From [START_REF] Figueira | Future-looking logics on data words and trees[END_REF] it follows that SAT-XPath(→ * , =) restricted to L is non-primitive recursive, and that SAT-XPath(→ * , * ←, =) restricted to L is undecidable.

Future work

-The present work can be seen as a step forward in answering [START_REF] Figueira | A decidable two-way logic on data words[END_REF],

Conjecture 1], suggesting that the extension of XPath( * ←, ↓ * , → * , =) with the child axis is decidable with elementary complexity. Our approach may perhaps be extended to handle the child relation.

-We suspect that XPath( * ←, ↓ * , → * , =) is in fact hard for 2ExpSpace, even when the formulas are in direct normal form, and hence that SAT-direct-XPath( * ←, ↓ * , → * , =) is 2ExpSpace-complete.

-We would also like to investigate further the approach taken in this paper to attempt to generalize it to work with the class of reflexive-transitive closures of regular languages.

↓ i 1 ∪ → [f 1 ]• χ ↓ e
1 and hence that condition (c) holds for f 1 + f 23 . To show that condition (b) holds, note that On the other hand, assuming that we can apply f 1 + (f 2 + f 3 ) (i.e., that f 2 and f 3 are compatible, and that f 1 and f 23 are compatible) we can show that the conditions to apply (f 1 + f 2 ) + f 3 hold, in the same way as before, since all the definitions are symmetrical, where χ

χ ↓ e 1 = χ ↓ i 2 ∪ [f 2 ] →• χ ↓ e 2 (by condition (b) of f 1 + f 2 ) = χ ↓ i 2 ∪ [f 2 ] →•( χ ↓ i 3 ∪ [f 3 ] →• χ ↓ e 3 ) (by condition (b) of f 2 + f 3 ) = χ ↓ i 2 ∪ [f 2 ] →• χ ↓ i 3 ∪ [f 2 ] →•([f 3 ] →• χ ↓ e 3 ) (by (•, ∪) distributivity) = χ ↓ i 2 ∪ [f 2 ] →• χ ↓ i 3 ∪ [f 23 ] →• χ
↓ e 1 = χ ↓ i 2 ∪ [f 2 ] →• χ ↓ e 2 and χ ↓ e 2 = χ ↓ i 1 ∪ → [f 1 ]• χ ↓ e
1 . We now show that (f 1 + f 2 ) + f 3 = f 1 + (f 2 + f 3 ). Let f 1(23) = f 1 + (f 2 + f 3 ) and f (12)3 = (f 1 + f 2 ) + f 3 .

We have that χ

χ ↓ i 1(23) = χ ↓ i 1 ∪ [f 1 ] →• χ ↓ i 23 (by condition (+4)) = χ ↓ i 1 ∪ [f 1 ] →•( χ ↓ i 2 ∪ [f 2 ] →• χ ↓ i 3 ) (by condition (+4)) = χ ↓ i 1 ∪ [f 1 ] →• χ ↓ i 2 ∪ [f 1 ] →•([f 2 ] →• χ ↓ i 3 ) (by (•, ∪) distributivity) = χ ↓ i 1 ∪ [f 1 ] →• χ ↓ i 2 ∪ [f 12 ] →• χ ↓ i 3 (by Lemma 4.3) = χ ↓ i 12 ∪ [f 12 ] →• χ ↓ i 3 (by condition (+4)) = χ ↓ i (12)3
(by condition (+4))

and by a similar reasoning using condition (+5) we obtain that χ

↓ i 1(23) = χ ↓ i (12)3 . Hence, (f 1 + f 2 ) + f 3 = f 1 + (f 2 + f 3 ). Proof of Lemma 4.3. Let f + = f 1 + f 2 . [f 1 + f 2 ] →•χ = {α | (d, α, β, i) ∈ χ ↓ i + }•χ (by definition of [ ] →) = {α | (d, α, β, i) ∈ χ ↓ i 1 ∪ [f 1 ] →• χ ↓ i 2 }•χ (by definition of f 1 + f 2 ) = {α | (d, α, β, i) ∈ χ ↓ i 1 } ∪ {α | (d, α, β, i) ∈ [f 1 ] →• χ ↓ i 2 } •χ = [f 1 ] → ∪ {α | (d, α, β, i) ∈ [f 1 ] →• χ ↓ i 2 } •χ = [f 1 ] →•χ ∪ {α | (d, α, β, i) ∈ [f 1 ] →• χ ↓ i 2 }•χ (by (•, ∪) distributivity) = [f 1 ] →•χ ∪ {(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ {α | (d, α, β, i) ∈ [f 1 ] →• χ ↓ i 2 }} = [f 1 ] →•χ ∪ {(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ {α | (d, α, β, i) ∈ {α | (d, α, β, i) ∈ χ ↓ i 1 }• χ ↓ i 2 }} = [f 1 ] →•χ ∪ {(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ {α•α | (d, α, β, i) ∈ χ ↓ i 1 ∧ ((d , α , β , i ) ∈ χ ↓ i 2 ∨ α = )}} = [f 1 ] →•χ ∪ {(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ {α•α | α ∈ [f 1 ] →, α ∈ [f 2 ] → ∪ { }}} = [f 1 ] →•χ ∪ {(d, α •α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ [f 1 ] →, α ∈ [f 2 ] → ∪ { }} • Diego Figueira = [f 1 ] →•χ ∪ {(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ [f 1 ] →} ∪ {(d, α •α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ [f 1 ] →, α ∈ [f 2 ] →} = [f 1 ] →•χ ∪ [f 1 ] →•χ ∪ {(d, α •α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ [f 1 ] →, α ∈ [f 2 ] →} = [f 1 ] →•χ ∪ [f 1 ] →•{(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ [f 2 ] →} = [f 1 ] →•χ ∪ [f 1 ] →•([f 2 ] →•χ) = [f 1 ] →•([f 2 ] →•χ)
An identical reasoning can be used to prove that

→ [f 1 + f 2 ]•χ = → [f 2 ]•( → [f 1 ]•χ).

  Basic notation. Let N 0 def = {0, 1, 2, . . . }, N def = {1, 2, 3, . . . }, and let [n] def = {1, . . . , n} for any n ∈ N. We fix once and for all D to be any infinite domain On XPath with Reflexive-Transitive Axes and Data Tests • 5

Fig. 1 .

 1 Fig. 1. A multi-attribute data tree, where A = {a, b, c} and k = 2.

  [[φ]] t = { , 2, 3, 4, 5, 311}. We write XPath(↓ * , ↑ * , → * , * ←, =) to denote this logic, and we write XPath(O, =) for some O ⊆ {↓ * , ↑ * , → * , * ←}, to denote the logic containing only the axes in O.We write t, x |= ϕ (resp. t, (x, y) |= α) for x ∈ pos(t) (resp. x, y ∈ pos(t)) as short form for x ∈ [[ϕ]] t (resp. (x, y) ∈ [[α]] t ). We write t |= ϕ as short form for ∈ [[ϕ]] t .

  Lemma 4.1 (distributivity of (•, ∪)). For every P, P ⊆ P and χ, χ ⊆ D×Π (1 ) P •(χ ∪ χ ) = P •χ ∪ P •χ , On XPath with Reflexive-Transitive Axes and Data Tests • 13

  3 by item condition (+2) of +. In a similar way, by condition (+3) we have that

Fig. 5 .

 5 Fig. 5. Idea of the rooting action.

  Given a forest profile f and two data values d ∈ data(f), d ∈ data(f), we define f[d → d ] as the result of replacing d by d in f. Note that f[d → d ] ∼ f. Given two data values d, d we write f[d → d, d ] to denote f where R = R, χ (d ) = χ(d) and χ (e) = χ(e) for every e ∈ D \ {d }. Note that if d

  ↓ e (ᾱ) or {d } = χ ↓ e (ᾱ), for some ᾱ ∈ Π. By definition of f , this means that d = d and d = d , and hence that {d } = χ ↓ e (ᾱ)

Fig. 6 .

 6 Fig. 6. Statement of Lemma 5.5.

Fig. 7 .

 7 Fig. 7. Definition of f 0 , f t+1 and f i for all i ∈ [t].

  then χ+ (d) = χ1 (d). Here we only deal with χ †), since d ∈ data(f 2 ))

Fig. 8 .

 8 Fig. 8. Statement of Lemma 5.6.

Fig. 9 .

 9 Fig. 9. Statement of Lemma 5.8.

Fig. 10 .

 10 Fig. 10. Statement of Lemma 5.9.

  β, i) = {d }. The same happens by symmetry with χ ↓ e .

  Fig. 11. Statement of Lemma 5.15.

  Lemma 5.18. R + (↑↓D b ) ⊆ ↓D b .

  Lemma 5.20. C ∼ k0 = min(↓D b ). Thanks to the property R(↑↓D b ) ⊆ ↓D b one can show that C ∼ k0 = min(↓D b ) and that C i+1 can be computed from C i in 2ExpSpace in |C i | and |P|. It is possible to test from the set min(↓D b ) whether there is a root derivable profile in D b , hence obtaining that the derivation problem is decidable.

  and that f 1 has no external values since f has no external values. Hence condition 1 holds.

  and, if αβ = , αβ ≡ α[ ]β and αεβ ≡ αβ.

Figure 11 :

 11 Figure 11: Example for the proof of Lemma 6.1.

Fig. 13 .

 13 Fig. 13. Example for the proof of Lemma 6.1.

Fig. 14 .

 14 Fig. 14. Idea of construction of μα t,x,y .

On

  XPath with Reflexive-Transitive Axes and Data Tests • 41Given a formula ψ, tr(ψ) denotes the result of replacing -every instance of a path expression o1 [ψ 1 ]o 2 • • • o n [ψ n ] in ψ (where o 1 , . . . , o n ∈ { * ←, ↓ * , → * })which does not appear nested inside another path expression, with the expressiono 1 [ζ ψ1 ]o 2 • • • o n [ζ ψn ],and -every test for label a which does not appear inside a path expression by ζ a , where ζ ψ def = S∈Aϕ,ψ∈S S.

  , assuming P = { , b•c, b, c, }, we would obtain an abstraction where χ ↓ e = {(5, b, b, 1), (5, b, , 1), (3, b, , 2), (2, b, c, 1), . . . }.

χ

  ↓ i = {(d(y)(i), α, β, i) | (1, y) ∈ [[P → * (α)•P ↓ * (β)]] t , for (α, β, i) ∈ Π and y ∈ pos(t)} χ ↓ i = {(d(y)(i), α, β, i) | (n, y) ∈ [[P * ← (α)•P ↓ * (β)]] t , for n = | t|, (α, β, i) ∈ Π and y ∈ pos(t)} χ ↓ e = {(d r (y)(i), α, β, i) | (1, y) ∈ [[P → * (α)•P ↓ * (β)]] tr , for (α, β, i) ∈ Π and y ∈ pos(t r )} χ ↓ e = {(d l (y)(i), α, β, i) | (n, y) ∈ [[P * ← (α)•P ↓ * (β)]] t l ,for n = | tl |, (α, β, i) ∈ Π and y ∈ pos(t l )}.

  ↓ e is the set of all (d l (y)(k), α 1 , β 1 , k)so that (n, y) ∈ [[P * ← (α 1 )P ↓ * (β 1 )@ k ]] (a, d) tl for n = | tl | = i 0 -1 there is some y so that (i 0 -1, y ) ∈ [[α 2 •β]] (a, d)( tl •t• tr) with d (y )(i) = d and α 2 = P * ← (α 2 ). Also, since α 1 ∈ → [f], we have (i 0 , i 0 -1) ∈ [[α 1 ]] (a, d)( tl •t• tr)where α 1 = P * ← (α 1 ). Then, there is some y so that (i 0 , y) ∈ [[α•β]] (a, d)( tl •t• tr) with d (y )(i) = d.

  0 , y ) ∈ [[α•β]] (a, d)( tl •t• tr) with d (y )(i) = d.By similar arguments, we have that there must be some z ∈ pos((a, d)( tl•t• tr )), z = with (i 0 , z ) ∈ [[α•β]] (a, d)( tl •t• tr) and d (z )(j) = d. Hence, tl •t• tr , i 0 |= α•β@ i = γ•δ@ j .

  thus condition (b) holds for f 1 + f 23 .

  3 by item condition (+2) of +. In a similar way, by condition (+3) we have that χ ↓ e 1(23) = χ ↓ e (12)3 . On the other hand, we have

  These are called forest profiles. They are the main object

	outside the fore Let A be a fi the set of root
	data values. T any a ∈ A and tation assigning
	satisfies ψ. Let
	ber of attribut
	attribute inde
	nite, subword-cl
	we denote it by
	to denote patter
	lowing set of pa
	σa	def = {
	Note that ε ∈ σa as
	the intended m
	on the sibligns,
	third retrieves a
	A forest pro
	where R ⊆ D, a and χ

  Proof. From left to right: If t, (x, y) |= α witness forest of α for t, (x, y), call it t, x , y t, x , y |= μα t,x ,y , and therefore t, (x, y) |= µ α |= α, if we consider t as the forest that we restrict t to only the nodes that witness α, label of every node by the node expression th we then have that t, (x, y) |= µ α t,x,y .

	FINISH THE PROOF HERE????
	t,x
	From right to left: If there is some forest t, t, (x, y) |= µ α t,x ,y , then t, x , y |= μα t,x ,y . F t, (x, y) |= µ α t,x ,y , we have that t, x , y is a ness forest of µ α t,x ,y for t, (x, y). Then, it is al witness forest of α, and hence t, (x, y) |= α.
	Claim 6.1.2. For every multi-attribute dat
	have that t, (x, y) |= α if, and only if, t, (x, y) some direct normal form linearization µ α t,x,y of
	Proof. [⇒] Given a multi-attribute data t
	t, (x, y)

Claim 6.1.1. If t, (x, y) |= α if, and only i µ α t,x ,y for some forest t, x , y over 2 ne(α) of s p(|α|). [⇐] Since µ α t,x,y is a direct normal form lin α, we have that t, (x, y) |= α. This means that order of the nodes of t are compatible with th of α. If further t, (x, y) |= µ α t,x,y , WHAT IS WITNESS? WHAT IS APPEARANCE OF WITNESS? t, (x, y) |= α if, and only if, t, (x , y ) |= α for

This is an extended and revisited version of the paper[START_REF] Figueira | On XPath with transitive axes and data tests[END_REF]].

These are the axes that are called preceding-sibling, following-sibling and ancestor in the XPath jargon.

Strictly speaking, these axes do not exist in XPath[START_REF] Clark | XML path language (XPath)[END_REF]. They must be interpreted as the reflexive version of the preceding-sibling, following-sibling and descendant axes respectively.

Note that, strictly speaking, these are not path expressions since they have a "@ i " at the end. Later on, in §6, we will call expressions of this simple form to be direct unnested.

(e), we have that: for all a ∈ {•, • ↓ , • ↓ }, χ a (e) in f 0 is equal to

(d j). (since χ1 (d j ) = χ2 (d j ) by ( †))

On XPath with Reflexive-Transitive Axes and Data Tests • 29 By the claim above, t is a derivation tree for (R χ, f). (Note that this is true because in the rooting operation there is no restriction on which should be the set of rigid values of the parent profile.) It is immediate that (R, f) is a root profile if and only if (R χ, f) is a root profile. Thus, the lemma follows.

Let F b be the set of all f ∈ F that have no more than 2|Π| rigid values. Let D b be the set of derivable profiles restricted to F b .

Remark 5.11. By Lemma 5.10 and in light of the definition of bounded extension, it follows that Lemma 5.9, when applied to profiles of F b , yields a profile f 4 that is a bounded extension of f 5 .

By the Lemma just shown, we have the following Lemma 5.12. There is a derivable root profile in D if and only if there is a derivable root profile in D b .

We have then reduced the derivation problem into a simpler problem, the bounded derivation problem: testing whether there is a derivable root profile in D b .

Remark 5.13. We have that D b is upward closed since D is upward closed. That is, D b = ↑D b .

Note that F b has boundedly many -minimal elements. In the next section we show how to restrict the problem to a problem that uses only these -minimal profiles. We will show how this yields a 2ExpSpace algorithm in Section 5.6.

Restricting to minimal elements

Thanks to the result from the previous section stating that D b is upward closed, we can now show that we can work only with the minimal elements of F b . The main necessary property concerns all those profiles f ∈ F b that are ' -related' to a profile f ∈ D b , in the sense that f f f ∈ D b for some f. (Note that this set of profiles is precisely ↑↓D b .) The property states that the forest profiles algebra preserves the -relatedness.

Given G ⊆ F b , let

Lemma 5.14 is the consequence of the following properties.

Lemma 5.15 (Figure 11). For every

Therefore, there are doubly exponentially many elements in min(F b )/∼, and hence k 0 is bounded by a doubly exponential function in |Π|. Since |Π| is polynomial in |P|, the statement follows. Proof. First we check that f ∈ min(↓F b ).

To check f ∈ min(↓R + (↑↓G)), we verify if f f 1 + f 2 in 2ExpSpace, where f 1 , f 2 is a pair of the (doubly exponentially many) bounded extensions of elements of min(↓G). By Lemma 5.8, there are such f 1 , f 2 if, and only if, f ∈ min(↓R + (↑↓G)).

Finally, to check f ∈ min(↓R up (↑↓G)), we verify that f f 3 ∈ min((a, d)f 4 ) in 2ExpSpace, where f 4 is a bounded extension of a profile of min(↓G). If the condition holds of course f ∈ min(↓R up (↑↓G)). On the other hand, by Lemma 5.9 cum Remark 5.11, if f ∈ (a, d)f 2 with f 2 f 5 , then f f 3 ∈ min((a, d)f 4 ) for some bounded extension f 4 of f 5 , and hence the condition holds.

By the lemma above, we immediately obtain the following. Proof. For each f ∈ min(F b )/∼ we can check, in 2ExpSpace, wether f ∈ min(↓R(↑↓C i )) thanks to Lemma 5.22. We can therefore compute min(↓R(↑↓C i ))/∼ in 2ExpSpace, and thus we can also compute C i+1 in 2ExpSpace.

Proposition 5.24. The derivation problem is decidable in 2 ExpSpace.

Proof. We can compute all C 0 , . . . , C k0 in 2ExpSpace by Lemmas 5.23 and 5.21. Since C ∼ k0 = min(↓D b ) by Lemma 5.20, it follows that min(↓D b ) is hence computable in 2ExpSpace.

In order to test if there is a derivable profile in D b we choose some

and (a, d) ∈ A root × D k , and test, in 2ExpSpace (Lemma 5.22), whether f ∈ min(↓R (a, d) up (↑↓{f })). Claim 5.24.1. The following statements are equivalent.

2. There is a derivable root profile in D b .

Proof. [1⇒2] Assume first that condition 1 holds. We change the names for the profiles to make the explanation clear. Suppose that there is some f 1 ∈ min(↓R (a, d) up (↑↓{f})) with no external data values, for some (a, d)

We show that abs is basically an algebra morphism between multi-attribute data forests with rooting and concatenation and forest profiles with profile rooting and profile concatenation. This is necessary to show our reduction from SAT-XPath( * ←, ↓ * , → * , =) into the derivation problem for forest profiles. Lemma 6.7. Given R ⊆ D, and multi-attribute data forests t, tl , tr , t1 , t2 ,

2 where f 2 = abs R ( tl • t1 , t2 , tr ). In the same way, χ ↓ e 2 is composed by all the paths that can reach data values in tl • t1 , which is precisely χ

Finally, conditions (+2)-(+5) follow from the definition of abs.

2. Since ξ(abs R ( tl , (a, d) t, tr )) ∈ Γ φ , we only need to show that abs R ( tl , (a, d) t, tr ) is so that the rooting conditions (ii) and (iii) hold. Condition (ii) is immediate since by definition of abs we have that abs R ( , t, ) has empty external descriptions. Condition (iii) holds by definition of abs and the semantics of XPath.

For any derivation forest t (as defined in Section 4.3) we associate a multiattribute data forest tt which is the result of removing all leaf nodes from t and projecting the tree onto A × D k . Lemma 6.8. For every boolean combination ψ of non-recursive subformulas of φ, we have that abs R ( tl , t, tr ) ψ if, and only if, tl

for some y by definition of

where α is leftward or empty, γ is rightward or empty, and β, δ are downward or empty. Let t = a ⊗ d = (a, d)( tl •t• tr ).

[⇒] If f ψ there must be some data value d ∈ D that witnesses this fact, as required by the definition of . Suppose first that α = , α = ε. Hence, there must be some d ∈ D so that (P

, by definition of abs we have that χ

It then follows that there must be some y so that (i 0 , y

We now prove the main statement by generalized induction on the height of t. Suppose that t has height m ≥ 1. Then there must be forests t1 , . . . , tn so that t = (a 1 d1 ) t1 • • • (a n , dn ) tn and each ti has height less than m. Let fi = abs R ((a j , dj ) tj ) j<i , (a i , d i ) ti , ((a j , dj ) tj ) j>i for every i. We then have the following. Claim 6.9.2. For every i ∈ [n], f i = fi .

Proof. For every ti = , we have that f 1 + • • • + f l = abs Ri ( , ti , ) by inductive hypothesis, where f 1 , . . . , f l are the profile labels of the children of the root of the ith tree of t. Then, since

Now, since -all the internal descriptions of any forest profile inside (a i , di )abs ∅ ( , ti , ) is completely determined by (a i , di ) and abs ∅ ( , ti , ), and hence f i and fi have the same internal descriptions, -the external descriptions of we can apply Claim 6.9.1, concluding that f i = fi for every i.

Therefore, since abs R ( , (a 1 , d1 ) t1

On the other hand, since ξ(f 1 ), . . . , ξ(f n ) ∈ Γ φ by condition (i) of rooting, we have fi = f i a∈A φ (a ⇒ γ φ (a)) for every i. Hence, by Lemma 6.8,

for every i. Also, by inductive hypothesis, for all ti = we have that ti , j |= φ 2 for all 1 ≤ j ≤ | ti |. Then, by definition of φ 2 , it follows that

for every i.

On XPath with Reflexive-Transitive Axes and Data Tests

• 47

We now show that if φ is satisfiable, then there must be a derivable root profile.

Lemma 6.10. Let t φ be a tree so that t φ |= φ. For every maximal subforest tl • t• tr of t φ so that t = , there is a derivable forest profile f ∈ D so that f = abs R ( tl , t, tr ), where R = data( tl

Proof. We proceed by induction on the size of t, defined as its number of nodes. Suppose first that t consists in one tree with just one node (a, d). We show that abs R ( tl , (a, d), tr ) ∈ (a, d)f ∅ .

Since tl •(a, d)• tr , j |= φ 2 , for j = | tl | + 1, we have that abs R ( tl , t, tr ) γ φ (a) by Lemma 6.8. In other words, we have ξ(abs R ( tl , t, tr )) ∈ Γ φ . Then, by Lemma 6.7-2 we have abs R ( tl , (a, d), tr ) ∈ (a, d)abs ∅ ( , , ). Since f ∅ = abs ∅ ( , , ) (Remark 6.6), we have that (a, d)abs ∅ ( , , ) = (a, d)f ∅ . Therefore, abs R ( tl , t, tr ) ∈ D.

Suppose now that t consists in one tree (a, d) t where t = . By inductive hypothesis there is some f ∈ D so that f = abs R ( , t , ) for some R . By Lemma 6.8 since tl

again by Lemma 6.7-2. Therefore, abs R ( tl , t, tr ) ∈ D.

Suppose now that t consists in more than one tree, let t1 and t2 be non-empty forests so that t = t1 • t2 . By applying twice the inductive hypothesis there must be f 1 , f 2 ∈ D so that f 1 = abs R ( tl , t1 , t2 • tr ) and f 2 = abs R ( tl • t1 , t2 , tr ). As abs R ( tl , t1 • t2 , tr ) = abs R ( tl , t1 , t2 • tr )+abs R ( tl • t1 , t2 , tr ) by Lemma 6.7-1, it follows that abs R ( tl

As a corollary from these properties, we have the following. Corollary 6.11. There is a derivable root forest profile if, and only if, φ is satisfiable.

Proof. [⇒] Let f be a derivable root forest profile. Then, there must be a derivation tree t for f = (R, χ). Let t be the multi-attribute data tree associated to t. By Lemma 6.9, we have that abs R ( , t, ) = f and that t |= φ 2 . Since f is a root profile, the root of t must have a label (a, d) with a ∈ A root , and hence t |= φ 1 as well. Therefore, φ is satisfiable.

[⇐] Let t be so that t |= φ. Then by Lemma 6.10 we have f = abs data(t) ( , t, ) ∈ D. Further, since t is a tree, we have that in fact f = (a, d)f for some f ∈ D. Further, since t |= φ 1 , a ∈ A root . Hence, f is a derivable root profile.

By the above Corollary 6.11 and Proposition 5.24, we can check in 2ExpSpace if there is a derivable root profile. This is 2ExpSpace in the size of P φ . Although bringing a formula ϕ into direct unnested normal form may result in a doubly exponential formula, by Corollary 6.3 it can be stored in exponential space, and P φ is then singly exponential. Hence, the procedure is 3ExpSpace in the original formula ϕ. Thus, the decision procedure is in 3ExpSpace and Theorem 3.1 follows.

Note that if the input formula is in direct normal form then we save one exponential in the reduction and we hence obtain a 2ExpSpace decision procedure.

• Diego Figueira

A. MISSING PROOFS

Proof of Lemma 4.1. We have that

which proves the first statement.

On the other hand,

We first show that if (f 1 + f 2 ) + f 3 can be applied, then f 1 + (f 2 + f 3 ) can also be applied. In other words, we prove that if f 1 , f 2 are compatible, and f 12 , f 3 as well; then both f 2 , f 3 and f 1 , f 23 are compatible. We first show that f 2 and f 3 are compatible. Condition (a) is immediate, since R 2 = R 3 . Now we show that conditions (b) and (c) hold for f 2 + f 3 . Since χ (by condition (c) of

(by condition (c) of

Hence, we obtain that χ