Diego Figueira

On XPath with Transitive Axes and Data Tests *

Keywords: I.7.2 [Document Preparation]: Markup Languages, H.2.3 [Database Management]: Languages, H.2.3 [Languages]: Query Languages Algorithms, Languages XML, XPath, unranked unordered tree, reflexive transitive axes, data-tree, infinite alphabet, data values

We study the satisfiability problem for XPath with data equality tests. XPath is a node selecting language for XML documents whose satisfiability problem is known to be undecidable, even for very simple fragments. However, we show that the satisfiability for XPath with the rightward, leftward and downward reflexive-transitive axes (namely followingsibling-or-self, preceding-sibling-or-self, descendant-or-self) is decidable. Our algorithm yields a complexity of 3ExpSpace, and we also identify an expressive-equivalent normal form for the logic for which the satisfiability problem is in 2Exp-Space. These results are in contrast with the undecidability of the satisfiability problem as soon as we replace the reflexive-transitive axes with just transitive (non-reflexive) ones.

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 consider an XML modeled 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 multiattribute 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 formalisms is FO 2 (< h , succ h , <v, succv, ∼), first order logic with two variables, and binary relations to navigate the tree: the descendant <v, child succv, 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] Miko Laj 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 , succv, ∼)-the logic is decidable in 3NExpTime as shown in [START_REF] Miko Laj Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF].

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 in [START_REF] Figueira | Forward-XPath and extended register automata on data-trees[END_REF][START_REF] Figueira | Alternating register automata on finite data words and trees[END_REF] to show decidability of the satisfiability problem for forward-XPath. The work [START_REF] Miko | 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, succv, ∼), 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] Miko Laj Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF].

In an 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 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 ( [START_REF] Figueira | Reasoning on Words and Trees with Data[END_REF]).

• The downward fragment of XPath, containing the child and descendant axes, is decidable, ExpTime-complete [START_REF] Figueira | Satisfiability of downward XPath with data equality tests[END_REF][START_REF] Figueira | Decidability of downward XPath[END_REF].

• 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 [START_REF] Figueira | Forward-XPath and extended register automata on data-trees[END_REF][START_REF] Figueira | Alternating register automata on finite data words and trees[END_REF].

• 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 nonreflexive 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 even when 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 non-reflexive 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 2Exp-Space (or ExpSpace if we adopt a certain normal form of the formulas). This was a first step 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 highly non-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], we cannot aim for much better complexities.

Due to space limitations, all the proofs are included in the Appendix, although the main intuitions, general strategy, and decomposition of the proof in simpler problems are presented in the body of the paper.

PRELIMINARIES

Basic notation.

Let N0 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 of data values; for simplicity in our examples we will consider D = N0. 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 with at least one element over E. We write ' ' for the empty sequence and 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, and alph(t) = E denotes the alphabet of the tree. From now on, we informally refer by 'node' to a position x together with the value t(x).

Given two trees t1 ∈ Trees(E), t2 ∈ Trees(F) such that pos(t1) = pos(t2) = P , we define t1 ⊗ t2 : P → (E×F) as

(t1 ⊗ t2)(x) def = (t1(x), t2(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 multi-attribute 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 multiattribute data forests over A and k is (Trees(A×D k )) * . We will normally use the symbol t for a forest of multiattribute 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 , let us write (a, d) t for the multi-attribute data tree that results from adding (a, d) as a root of t. We call this operation rooting. We will usually write t (resp. t) to denote multi-attribute data trees (resp. forests) and 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 that test a property of a node like, for example, that is has a certain label, or that it has a descendant labeled a with the same data value in attribute i as the attribute j of an ancestor labeled b, which is expressed by ↓ * [a]@i = ↑ * [b]@j . 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. 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. 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 . Given a tree t as in Figure 1, we have

[[ϕ]] t = { , 2, 3, 4, 5, 311}. We write t, x |= ϕ (resp. t, (x, y) |= α) for x ∈ pos(t) (resp. x, y ∈ pos(t)) as short for x ∈ [[ϕ]] t (resp. (x, y) ∈ [[α]] t ). We write t |= ϕ as short for ∈ [[ϕ]] t .
In the case of XPath( * ←, ↓ * , → * , =), we also extend the evaluation to multi-attribute 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 noted SAT-XPath(O, =)) is the problem of, given a formula ϕ of XPath(O, =), wether there exists a multi-attribute 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).

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. A forest profile contains, for each data value d and each path expression, 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 (the node x ↓ i in Figure 3),

• inside the main forest but starting with the rightmost root (the node x ↓ i in Figure 3),

• in the left context forest (starting from the node x ↓ e in Figure 3), or

• in the right context forest (starting from the node x ↓ e in Figure 3).

In this setting, path expressions are called patterns and their navigation is greatly simplified. Patterns can go first to the left, and then down, or first to the right and then down, or only down. They correspond to path expressions like, for example,

→ * [a]→ * [b]↓ * [c]↓ * [a ∨ b]@1, or * ←[¬a]↓ * [a]@2.
Further, node expressions contained in patterns are simple boolean combinations of tests for labels.

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 path expression α@i. 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 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 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, that is, 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 Aroot 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 2Exp-Space in Section 5. We first define a partial 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 partial 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.

α, β ::= 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 [[[ϕ]]] t = {(x, x) ∈| x ∈ pos(t), x ∈ [[ϕ]] t } (x, y) ∈ [[α]] t , (y, z) ∈ [[β]] t } [[a]] t = {x ∈ pos(t) | a(x) = a} [[ α ]] t = {x ∈ pos(t) | ∃y.(x, y) ∈ [[α]] t } [[¬ϕ]] t = pos(t) \ [[ϕ]] t [[ϕ ∧ ψ]] t = [[ϕ]] t ∩ [[ψ]] t [[ α@i=β@j ]] t = {x ∈ pos(t) | ∃y,z (x, y) ∈ [[α]] t , [[ α@i =β@j ]] t = {x ∈ pos(t) | ∃y,z (x, y) ∈ [[α]] t , (x, z) ∈ [[β]] t , d(y)(i) = d(z)(j)} (x, z) ∈ [[β]] t , d(y)(i) = d(z)(j)}

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 Note that ε ∈ σa. We define the set of composed patte as

Π def = (P \ {ε}) × P × [k],
the intended meaning is that the first component oper on the sibligns, the second on a downward path, and third retrieves a data value from an attribute index.

A forest profile f is a tuple

f def = (χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e , R)
where R ⊆ D, and we call it the set of rigid values and χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e ⊆ D × Π, and we call them the se left/right exterior/interior descriptions respectively. use χ to denote the quadruple ( χ

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

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

f = (χ, R) is valid if ev d so that χ ↓ e (α, β, i) = {d} or χ ↓ e (α, β, i) = {d} for s (α, β, i) ∈ Π, is in R.
We define F as the set of all v profiles. The set of root patterns of a forest profile f, denoted

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 Note that ε ∈ σa. We define the set of composed patterns as

Π def = (P \ {ε}) × P × [k],
the intended meaning is that the first component operates on the sibligns, the second on a downward path, and the third retrieves a data value from an attribute index.

A forest profile f is a tuple

f def = (χ ↓ 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 exterior/interior descriptions respectively. We use χ to denote the quadruple ( χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e ). For every

χ ∈ { χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e }, we define χ(d) def = {(α, β, i) ∈ Π | (d, α, β, i) ∈ χ}, and
χ(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 say that a forest profile

f = (χ, R) is valid if every d so that χ ↓ e (α, β, i) = {d} or χ ↓ e (α, β, i) = {d} for some (α, β, i) ∈ Π, is in R.
We define F as the set of all valid profiles. The set of root patterns of a forest profile f, denoted by

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 Note that ε ∈ σa. We define the set of composed patterns as

Π def = (P \ {ε}) × P × [k],
the intended meaning is that the first component operates on the sibligns, the second on a downward path, and the third retrieves a data value from an attribute index.

A forest profile f is a tuple

f def = (χ ↓ 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 exterior/interior descriptions respectively. We use χ to denote the quadruple ( χ

↓ e , χ ↓ i , χ ↓ i , χ ↓ e ). For every χ ∈ { χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e }, we define χ(d) def = {(α, β, i) ∈ Π | (d, α, β, i) ∈ χ}, and
χ(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 say that a forest profile

f = (χ, R) is valid if every d so that χ ↓ e (α, β, i) = {d} or χ ↓ e (α, β, i) = {d} for some (α, β, i) ∈ Π, is in R.
We define F as the set of all valid profiles. The set of root patterns of a forest profile f, denoted by

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 Note that ε ∈ σa. We define the set of composed patterns as

Π def = (P \ {ε}) × P × [k],
the intended meaning is that the first component operates on the sibligns, the second on a downward path, and the third retrieves a data value from an attribute index.

A forest profile f is a tuple

f def = (χ ↓ 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 exterior/interior descriptions respectively. We use χ to denote the quadruple ( χ

↓ e , χ ↓ i , χ ↓ i , χ ↓ e ). For every χ ∈ { χ ↓ e , χ ↓ i , χ ↓ i , χ ↓ e }, we define χ(d) def = {(α, β, i) ∈ Π | (d, α, β, i) ∈ χ}, and
χ(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 say that a forest profile

f = (χ, R) is valid if every d so that χ ↓ e (α, β, i) = {d} or χ ↓ e (α, β, i) = {d} for some (α, β, i) ∈ Π, is in R.
We define F as the set of all valid profiles. The set of root patterns of a forest profile f, denoted by 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, obtaining a 3ExpSpace decidability procedure for SAT-XPath( * ←, ↓ * , → * , =), obtaining 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. Take for instance the forest in the middle of Figure 3. For every forest there we identify 4 nodes: the leftmost root, the rightmost root, the node to the left of the leftmost root (if any), and the node to the right of the rightmost root (if any). 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, all those that can reach 2, etc. Take as an example the data value 5; this data value can be reached by

(i) → * [a]@1 from x ↓ e , (ii) * ←[b]↓ * [a]@1 from x ↓ i , (iii) → * [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), 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). Let A be a finite alphabet of labels, let Aroot ⊆ A be the set of root labels, 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. We define the set of patterns, as any finite, subword-closed, subset of (B(A)) * , and we denote it by P. 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. 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 explicit the components of the composed pattern.

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. In the example before, one shall interpret (i) as (5, a, , 1) ∈ χ ↓ e , (ii) as (5, b, a, 1) ∈ χ ↓ i and (iii) as (5, a•b, c, 1) ∈ χ ↓ i . We use χ to denote a subset of D × Π; and we write χ (resp. χi) to denote the 4-uple ( χ

↓ e , χ ↓ i , χ ↓ i , χ ↓ e ) (resp. ( χ ↓ e i , χ ↓ i i , χ ↓ i i , χ ↓ e i )). Likewise, we use f (resp. fi) to denote ( χ, R) (resp. ( χi, Ri)).
We define, for every χ ⊆ D × Π,

χ(d) def = {(α, β, i) ∈ Π | (d, α, β, i) ∈ χ}, χ(α, β, i) def = {d ∈ D | (d, α, β, i) ∈ χ}, and
χ(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 where t, i |= ϕ, suppose there is a data value d such that: there is some position 1 ≤ j ≤ | t| and some path expression α of ϕ of the form α = → * β@ k or α = * ← β@ k so that d is the only data value that can be reached through α from j. 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 of t (which are the flexible values) play the role of assuring that "there are at least two data values reachable through α from position j" for some α and j. As such, its importance is only relative. In particular, if 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 same notions hold for our algebra on forest profiles. This is a key property that we need to exploit and hence the 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.1) the aforementioned argument as a monotonicity property of the algebra.

We say that a forest profile f = ( χ, R) is valid if every d ∈ D so that χ ↓ e (α, β, i) = {d} or χ ↓ e (α, β, i) = {d} for some (α, β, i) ∈ Π, is in R. 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}.
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 (i.e., P

•(χ ∪ χ ) = P •χ ∪ P •χ and (P ∪ P )•χ = P •χ ∪ P •χ).

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 ∈ F and a ∈ A, we define the set f.χa as

• χ ↓ i ∪ → [f]• χ ↓ e if a = • ↓ , • χ ↓ i ∪ [f] →• χ ↓ e if a = • ↓ , • {(d, α , β, i) ∈ D × Π | ∃α.(d, α, β, i) ∈ χ ↓ i ∪ χ ↓ i } if a = • ↓ , or • {(d, α, β, i) ∈ χ ↓ i ∪ χ ↓ i | β = } if a = •.
Note that f.χa(α, β, i) is independent of α when a = • ↓ , but it takes an element of Π as argument for the sake of uniformity of notation. The fingerprint of a profile f, noted ξ(f), is an element of

F def = Π × A → {0, 1, 2+} ∪ Π × A × Π × A → {0, 1+},
where for ᾱ, ᾱ ∈ Π, a, a ∈ A, we define ξ(f)( ᾱ, a, ᾱ , a ) as 0 or 1+ depending on whether |f.χa( ᾱ) ∩ f.χ a ( ᾱ )| = 0 or not; and we define ξ(f)( ᾱ, a) as 0, 1, or 2+ depending on |f.χa( ᾱ)| being 0, 1 or greater than 1 respectively. We fix the set of consistent fingerprints, as a set of fingerprints Γ ⊆ F. 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 multiattribute 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 f1, f2 ∈ F so that

(a) R1 = R2, (b) χ ↓ e 1 = χ ↓ i 2 ∪ [f2] →• χ ↓ e 2 , and (c) χ ↓ e 2 = χ ↓ i 1 ∪ → [f1]• χ ↓ e 1 ;
we define the concatenation of f1 and f2, denoted as f1 + f2 as f3, where

R3 = R1 = R2 (+1) χ ↓ e 3 = χ ↓ e 2 (+2) χ ↓ e 3 = χ ↓ e 1 (+3) χ ↓ i 3 = χ ↓ i 1 ∪ [f1] →• χ ↓ i 2 (+4) χ ↓ i 3 = χ ↓ i 2 ∪ → [f2]• χ ↓ i 1 . (+5)
Notice that

• the concatenation is associative ((f1 + f2)

+ f3 = f1 + (f2 + f3)),
• the extension operation • distributes over the concate-

nation operation + ([f1 + f2] →•χ = [f1] →•([f 2] →•χ)), • if f1 + f2 = f3 and f1, f2 ∈ F, then f3 ∈ F.

Rooting

Given a ∈ A, and d ∈ D k , we define (a, d)f1 ⊆ F, where f2 ∈ (a, d)f1 if

(a) ξ(f2) ∈ Γ, (b) χ ↓ e 1 = χ ↓ e 1 = ∅, (c) χ ↓ i 2 = χ ↓ i 2 = {(d, α, β•γ, i) ∈ D × Π | ∃α .(d, α , γ, i) ∈ χ ↓ i 1 ∪ χ ↓ i 1 , α, β ∈ σa}∪ i∈[k] ({ d(i)}×(σa \{ })×σa ×{i})
We say that f2 is a rooting of f1 with (a, d).

Notice that since the root pattern of any pair of profiles f1, f2 ∈ (a, d)f3 is the same, it is idempotent and absorbing

([f1] →•[f 2] →•χ = [f1] →•χ = [f2] →•χ, [f1] →• χ ↓ i 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. We say that f is a derivable root profile if χ ↓ e = χ ↓ e = ∅ and f ∈ (a, d)f for some f ∈ D, a ∈ Aroot 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)(f1 + • • • + fn), where f1, . . . , fn are the labels of the children of x.

Similarly, a derivation forest t for f is a forest of derivation trees t = t1 • • • tn for some profiles f1, . . . , fn so that f = f1 + • • • + fn. 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, Aroot, P and Γ.

Problem: The derivation problem

Input: A finite alphabet A, Aroot ⊆ A, a set of patterns P, a set of 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 this problem is reducible from SAT-XPath( * ←, ↓ * , → * , =).

COMPUTING DERIVABLE PROFILES

In this section we solve the derivation problem, showing that it is decidable in 2ExpSpace. To show this problem we work with some partial 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).

Preliminaries

Given f1, f2 ∈ F we define that f1 and f2 are equivalent, and we note it f1 ∼ f2, if there is some bijection g : D → D so that f2 is the result of replacing d by g(d) in f1; in this case we write g(f1) = f2. 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.
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 strict external data value of f. If d ∈ data(f)
is not a strict external data value, it is then an internal data value, and if it is not en external data value, it is then a strict internal data value.

Ordering on profiles

We define a partial 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 f1, f2 ∈ F, we define f1 f2 if either f1 = f2, or there is a flexible datum d of f1 so that f1[d → d, d ] f2 for some d ∈ data(f1). Note that is recursive, reflexive and transitive, and it is hence a partial order.

Note that if f1 f2 then → [f1] = → [f2] and [f1] → = [f2] →. Note also that if f f then ξ(f) = ξ(f ).
We write f f if f f for some f ∼ f . We say that a set of forest profiles G ⊆ F is upward closed (resp. downward

The algorithm

We show an algorithm to compute a finite set C so that Db = ↑C. When we write

C ∼ we mean {f | f ∼ f ∈ C} and by ↑C = {f ∈ Fb | f f , f ∈ C}. 1. Let C = {f ∅ }.
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 Fb, 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 = Db.

Proof.

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

[⊇] Let f ∈ Db. Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ Db 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

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,
= {f ∈ Fb | f f , f ∈ C}. 1. Let C = {f ∅ }.
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 Fb, 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 = Db.

Proof.

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

[⊇] Let f ∈ Db. Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ Db 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. closed) with respect to , if for every f ∈ G and f f (resp. f f ), we have f ∈ G. We write

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 f 1 f 2 + f 1 f 2 f 3 + f 1 f 2 f 3 (bounded) (bounded)
↑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.1 states that for any two profiles f1 f2, f1 can be seen as a concatenation of profiles that share the same descriptions of internal values as f1, under certain restrictions, as it is shown next. This is a crucial property that follows from our discussion in Section 4.1.

Lemma 5.1 (Figure 4). For every f1 f2 ∈ (a, d)f3, there is n ∈ N, and

f i ∈ ∼ (a, d)f3 for every i ∈ [n] so that f1 = f 1 + • • • + f n .
The lemma above implies that the set of derivable profiles is upward closed. (Details in the Appendix.) Lemma 5.2. D = ↑D.

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 any profiles f1, f2 ∈ ↑G, there are bounded extensions f 1 , f 2 of profiles of G so that f 1 + f 2 f1 + f2, as in Figure 5.

(a, d) Lemma 5.3 (Figure 5).

f 1 f 5 f 2 ∈ (a, d) f 1 f 3 f 4 f 5 f 2 ∈ (a, d) ∈ (bounded)
If f1 + f2 = f3 and f 1 f1, f 2 f2, then f 1 + f 2 f3, for some f 1 , f 2 ∈ F so that f i is a bounded extension of f i , for all i ∈ {1, 2}.
A similar lemma holds for the rooting operation.

Lemma 5.4 (Figure 6). For every f1 ∈ (a, d)f2 and f2 f5, there is f4 f5 and f3 ∈ ∼ (a, d)f4 so that |data(f4)| ≤ |data(f5)| + |Π| 4 + |R1| and f3 f1, f4 f2.

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

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.6. By Lemma 5.5 and in light of the definition of bounded extension, it follows that Lemma 5.4, when applied to profiles of F b , yields a profile f4 that is a bounded extension of f5.

By the Lemma just shown, we have the following Lemma 5.7. 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.8. 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

R (a, d) up (G) def = {f ∈ F b | f ∈ (a, d)f , f ∈ G} for (a, d) ∈ A × D k , Rup(G) def = (a, d)∈A×D k R (a, d) up (G), R+(G) def = {f ∈ F b | f = f1 + f2 where f1, f2 ∈ G}, R(G) def = Rup(G) ∪ R+(G).
Lemma 5.9. R(↑↓D b ) ⊆ ↓D b .

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 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 ∈ N0 as

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

C ∼ k 0 = C ∼ k 0 +1 .
Remark 5.10. For every i ∈ N0, Ci ⊆ min(F b ).

As a consequence of the property of the preceding section, we have that this algorithm computes min(↓D b ).

Lemma 5.11.

C ∼ k 0 = min(↓D b ).
We further have that this computation is in 2ExpSpace since |min(F b )/∼| is doubly exponential in |P|, hence we obtain the following. (Details in the Appendix.)

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

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 α = a1 • • • an with n > 0 be a XPath( * ←, ↓ * , → * , =) path expression, where for every i, ai = [ψ] for some node expression ψ, or ai ∈ {ε, * ←, ↓ * , → * }. 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, ai = [ψ]
for some node expression ψ,

• if i is odd, ai ∈ { * ←, ↓ * , → * }.
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 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.

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 {a1, . . . , an} then it satisfies ψ" for some non-recursive formula ψ and labels a1, . . . , an ∈ 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. 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.

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 Aroot 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:

Po( ) def = ε if k = 0, Po(ψ1 • • • ψ k ) def = o[ψ 1] o • • • o[ψ k ] if k > 0.
Note that Po 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 φ.

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]@
[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 ψ.

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) ∈ Γ φ .
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 |= φ. (The formal definition of abs and the properties are described in the Appendix.) As a corollary from these properties, we have the following.

Corollary 6.6. There is a derivable root forest profile if, and only if, φ is satisfiable.

By the above Corollary 6.6 and Proposition 5.12, 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. Theorem 6.7. 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 reflexive-transitive 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 non-reflexive 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. We leave the proof of this claim for the journal version of the present work.

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 [START_REF] Figueira | A decidable two-way logic on data words[END_REF]Conjecture 2], stating that XPath( * ←, ↓ * , ↑ * , → * , =) be decidable in elementary time.

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.

• [f1 + f2] →•χ = [f1] →•([f 2] →•χ), • → [f1 + f2]•χ = → [f2]•( → [f1]•χ).
Proof. Let f+ = f1 + f2.

[f1 + f2] →•χ = {α | (d, α, β, i) ∈ χ ↓ i + }•χ (by definition of [ ] →) = {α | (d, α, β, i) ∈ χ ↓ i 1 ∪ [f1] →• χ ↓ i 2 }•χ (by definition of f1 + f2) = {α | (d, α, β, i) ∈ χ ↓ i 1 } ∪ {α | (d, α, β, i) ∈ [f1] →• χ ↓ i 2 } •χ = [f1] → ∪ {α | (d, α, β, i) ∈ [f1] →• χ ↓ i 2 } •χ (by (•, ∪) distributivity) = [f1] →•{α | (d, α, β, i) ∈ [f1] →• χ ↓ i 2 }•χ = [f1] →•{(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ {α | (d, α, β, i) ∈ [f1] →• χ ↓ i 2 }} = [f1] →•χ ∪ {(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ {α | (d, α, β, i) ∈ {α | (d, α, β, i) ∈ χ ↓ i 1 }• χ ↓ i 2 }} = [f1] →•χ ∪ {(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ {α•α | (d, α, β, i) ∈ χ ↓ i 1 ∧ ((d , α , β , i ) ∈ χ ↓ i 2 ∨ α = )}} = [f1] →•χ ∪ {(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ {α•α | α ∈ [f1] →, α ∈ [f2] → ∪ { }}} = [f1] →•χ ∪ {(d, α •α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ [f1] →, α ∈ [f2] → ∪ { }} = [f1] →•χ∪ {(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ [f1] →}∪ {(d, α •α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ [f1] →, α ∈ [f2] →} = [f1] →•χ ∪ [f1] →•χ∪ {(d, α •α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ [f1] →, α ∈ [f2] →} = [f1] →•χ∪ [f1] →•{(d, α •α, β, i) | (d, α, β, i) ∈ χ, α ∈ [f2] →} = [f1] →•χ ∪ [f1] →•([f 2] →•χ) = [f1] →•([f 2] →•χ) An identical reasoning can be used to prove that → [f1 + f2]•χ = → [f2]•( → [f1]•χ).
Lemma A.4 (+ associativity). For every f1, f2, f3 ∈ F, (f1 + f2) + f3 = f1 + (f2 + f3). Proof. Let f12 = f1 + f2, f23 = f2 + f3. We first show that if (f1 + f2) + f3 can be applied, then f1 + (f2 + f3) can also be applied. Condition (a) is immediate, since R1 = R2 = R3. Now we show that conditions (b) and (c) hold for f2 + f3. Since χ

↓ e 2 = χ ↓ e
12 and since the conditions between f12 + f3 hold, we have that χ

↓ e 2 = χ ↓ i 3 ∪ [f3] →• χ ↓ e
3 and hence that condition (b) holds for f2 + f3.

To show that condition (c) holds, note that

χ ↓ e 3 = χ ↓ i 12 ∪ → [f12]• χ ↓ e 12 (by condition (c) of f12 + f3) = χ ↓ i 2 ∪ → [f2]• χ ↓ i 1 ∪ → [f12]• χ ↓ e 1
(by definition of f1 + f2)

= χ ↓ i 2 ∪ → [f2]• χ ↓ i 1 ∪ → [f2]•( → [f1]• χ ↓ e 1 ) (by (•, +) distributivity) = χ ↓ i 2 ∪ → [f2]•( χ ↓ i 1 ∪ → [f1]• χ ↓ e 1 ) (by (•, ∪) distributivity) = χ ↓ i 2 ∪ → [f2]• χ ↓ e 2 .
(by condition (c) of f1 + f2)

Hence, we obtain that χ

↓ e 3 = χ ↓ i 2 ∪ → [f2]• χ ↓ e
2 , and thus condition (c) holds for f2 + f3. On the other hand, assuming that f1 + (f2 + f3), we can show that the conditions to apply (f1 + f2) + f3 hold, in the same way as before, since all the definitions are symmetrical, where χ

↓ e 1 = χ ↓ i 2 ∪ [f2] →• χ ↓ e 2 and χ ↓ e 2 = χ ↓ i 1 ∪ → [f1]• χ ↓ e 1 .
We now show that (f1 + f2)

+ f3 = f1 + (f2 + f3). Let f 1(23) = f1 + (f2 + f3) and f (12)3 = (f1 + f2) + f3.
We have that χ

χ ↓ i 1(23) = χ ↓ i 1 ∪ [f1] →• χ ↓ i 23 (by condition (+4)) = χ ↓ i 1 ∪ [f1] →•( χ ↓ i 2 ∪ [f2] →• χ ↓ i 3 ) (by condition (+4)) = χ ↓ i 1 ∪ [f1] →• χ ↓ i 2 ∪ [f1] →•([f 2] →• χ ↓ i 3 ) (by (•, ∪) distributivity) = χ ↓ i 1 ∪ [f1] →• χ ↓ i 2 ∪ [f12] →• χ ↓ i 3 (by (•, +) distributivity) = χ ↓ i 12 ∪ [f12] →• χ ↓ 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, (f1 + f2) + f3 = f1 + (f2 + f3).
Lemma A.5. For every f1, f2 ∈ (a, d)f3 and every χ ⊆ D × Π,

[f1] →•[f 2] →•χ = [f1] →•χ = [f2] →•χ = → [f1]• → [f2]•χ = → [f1]•χ = → [f2]•χ.

Proof. By condition (c) of rooting and definition of [ ]

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

Lemma A.6. For every f1 ∈ (a, d)f2,

χ ↓ i 1 = [f1] →• χ ↓ i 1 χ ↓ i 1 = [f1] →• χ ↓ i 1 .
Proof. By condition (c) of rooting, [f1] → = σ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 = [f1] →• χ ↓ i 1 . Since χ ↓ i 1 = χ ↓ i
1 by condition (c), we also obtain that χ

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

B. APPENDIX TO SECTION 5

Lemma B.1. and are partial orders over F.

Proof. If f f f , suppose f = f[d1 → d1, d 1 ] • • • f[dn → dn, d n ] and f = f [e1 → e1, e 1 ] • • • f[em → en, e m ]. Therefore, f = f[d1 → d1, d 1 ] • • • f[dn → dn, d n ][e1 → e1, e 1 ] • • • f[em → en, e m ]
and hence f f . On the other hand, it is plain that ∼ preserves transitivity and reflexivity, and that f f.

Lemma B.2. If f1 f2 then → [f1] = → [f2] and [f1] → = [f2] →.
Proof. This is immediate from the definition of → [ ], [ ] →, and . Note that, since f1 f2 we have

{(α, β, i) | ∃d ∈ D.(d, α, β, i) ∈ f1} = {(α, β, i) | ∃d ∈ D.(d, α, β, i) ∈ f2}. Hence, we obtain that α ∈ [f1] → 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 α ∈ [f2] →. A similar argument shows that → [f1] = → [f2]. Lemma B.3. 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 ( ᾱ ). Lemma B.4. If d ∈ data(f) \ R and d ∈ data(f), we have that if f ∈ F then f[d → d, d ] ∈ F.
Proof. This is immediate from the definition of validity. 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 . Since f ∈ F, there is some {d } = χ ↓ e ( ᾱ) for ᾱ ∈ Π and d ∈ R. By definition of f , this means that d = d and d = d, and hence that {d } = χ ↓ e ( ᾱ), and thus f ∈ F, which is a contradiction. A symmetric argument can also be applied to χ ↓ e .

Appendix to Section 5.3

Lemma 5.1 (Figure 4). For every f1 f2 ∈ (a, d)f3, there is n ∈ N, and

f i ∈ ∼ (a, d)f3 for every i ∈ [n] so that f1 = f 1 + • • • + f n .
Proof of Lemma 5.1. Since f1 f2, suppose

f1 = f2[d1 → d1, d 1 ] • • • [dt → dt, d t ] ( †)
where {d1, . . . , dt} ⊆ data(f2) \ R2; {d 1 , . . . , d t } ∩ data(f2) = ∅; 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, same as f2 for all internal values, same descriptions. However, f i has more external data values than f2-namely d 1 , . . . , d t -that have basically the same descriptions as d1, . . . , dt in f2. 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 ??.

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

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

• For every a ∈ A, ᾱ ∈ Π, and every data value e ∈ data(f2), we have that e ∈ χa( ᾱ) in f2 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 2 (e), we have that: for all a ∈ {•, • ↓ , • ↓ }, χa(e) in f 0 is equal to χa(e) in f2; and for all a ∈ {•, • ↓ , • ↓ }, χa(e) in f t+1 is equal to χa(e) in f2. And further, -if a = • ↓ , f 0 .χa(e) = χ ↓ i 0 (e) ∪ [f 0 ] →• χ ↓ e 0 (e) = χ ↓ i 2 (e) ∪ [f2] →•( ↓ i 2 (e) ∪ [f2] →• χ ↓ e 2 (e)) = χ ↓ i 2 (e) ∪ [f2] →• χ ↓ e 2 (e)
(by Lemmas ?? and ??) = f2.χa(e)

-if a = • ↓ , f t+1 .χa(e) = χ ↓ i 0 (e) ∪ → [f t+1 ]• χ ↓ e t+1 (e)
f 0 :

             R 0 = R 2 , χ 0 (e) = ( χ ↓ e 2 (e), χ ↓ i 2 (e), χ ↓ i 2 (e), χ ↓ i 2 (e) ∪ [f 2 ] →• χ ↓ e 2 (e)) for every e ∈ data(f 2 ), χ 0 (d j ) = ( χ ↓ e 2 (d j ), ∅, ∅, χ ↓ i 2 (d j ) ∪ [f 2 ] →• χ ↓ e 2 (d j )) for every j ∈ [t].
For every i ∈ {1, . . . , t} we define f i as

f i :                                        R i = R 2 , χ i (e) = ( χ ↓ i 2 (e) ∪ → [f 2 ]• χ ↓ e 2 (e), χ ↓ i 2 (e), χ ↓ i 2 (e), χ ↓ i 2 (e) ∪ [f 2 ] →• χ ↓ e 2 (e)) for every e ∈ data(f 2 ) \ {d i }, χ i (d i ) = ( χ ↓ i 2 (d i ) ∪ → [f 2 ]• χ ↓ e 2 (d i ), ∅, ∅, χ ↓ i 2 (d i ) ∪ [f 2 ] →• χ ↓ e 2 (d i )), χ i (d i ) = ( → [f 2 ]• χ ↓ e 2 (d i ), χ ↓ i 2 (d i ), χ ↓ i 2 (d i ), [f 2 ] →• χ ↓ e 2 (d i )), χ i (d j ) = ( χ ↓ i 2 (d j ) ∪ → [f 2 ]• χ ↓ e 2 (d j ), ∅, ∅, [f 2 ] →• χ ↓ e 2 (d j )) for every j < i, χ i (d j ) = ( → [f 2 ]• χ ↓ e 2 (d j ), ∅, ∅, χ ↓ i 2 (d j ) ∪ [f 2 ] →• χ ↓ e 2 (d j ))
for every j > i.

f t+1 :              R t+1 = R 2 , χ t+1 (e) = ( χ ↓ i 2 (e) ∪ → [f 2 ]• χ ↓ e 2 (e), χ ↓ i 2 (e), χ ↓ i 2 (e), χ ↓ e 2 (e)) for every e ∈ data(f 2 ), χ t+1 (d j ) = ( χ ↓ i 2 (d j ) ∪ → [f 2 ]• χ ↓ e 2 (d j ), ∅, ∅, χ ↓ e 2 (d j )) for every j ∈ [t].
f i for all i ∈ [t]. = χ ↓ i 2 (e) ∪ → [f2]•( χ ↓ i 2 (e) ∪ → [f2]• χ ↓ e 2 (e)) = χ ↓ i 2 (e) ∪ → [f2]• χ ↓ e 2 (e)
(by Lemmas ?? and ??) = f2.χa(e).

• The data values d j do not change the fingerprint ξ(f2), because d j is added to all those χa( ᾱ) where dj ∈ f2.χa( ᾱ), and f2.χa( ᾱ) has already two data values (otherwise dj would be rigid). Therefore, for any a ∈ A, ᾱ ∈ Π, if some d j ∈ f 0 .χa( ᾱ), then |f2.χa( ᾱ)| ≥ 2, and f2.χa( ᾱ) ⊆ f 0 .χa( ᾱ) (thus, |f 0 .χa( ᾱ)| ≥ 2). Otherwise, if d j ∈ f 0 .χa( ᾱ) for every j ∈ [t], then f 0 .χa( ᾱ) = f2.χa( ᾱ). Moreover, for any a, a

∈ A, ᾱ, ᾱ ∈ Π, if d j is in some f 0 .χa( ᾱ) ∩ f 0 .χ a ( ᾱ ) it means that dj ∈ f2.χa( ᾱ) ∩ f2.χ a ( ᾱ ). Hence, |f 0 .χa( ᾱ) ∩ f 0 .χ a ( ᾱ )| ≥ 1 iff |f2.χa( ᾱ) ∩ f2.χ a ( ᾱ )| ≥ 1.
As a result the fingerprint of f2 and f 0 are equal, and hence ξ(f 0 ) = ξ(f2) ∈ Γ. The same reasoning applies to f t+1 . Thus, f 0 , f t+1 ∈ ∼ (a, d)f3.

We now show that for every i ∈ [t], there is

f i so that f i ∼ f i ∈ (a, d)f3. We define f i as f i [di → d i ] for every i ∈ [t]. Observe that f i ∼ f i for every i ∈ [t]
. Since every di is not rigid, f i ∈ F and hence f i ∈ F. Further, note that f i and f2 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 f2. Also in this case we have that ξ(f i ) = ξ(f2) for the same reason as before:

• For all e ∈ data(f2), a ∈ A and ᾱ ∈ Π we have that e ∈ χa( ᾱ) in f2 iff e ∈ χa( ᾱ) in f i .

• The fresh data values d j only add data values to sets χa( ᾱ) that already at least 2 data values.

And j ∈ f i .χa( ᾱ) ∩ f i .χ a ( ᾱ ) iff dj ∈ f2.χa( ᾱ) ∩ f2.χ a ( ᾱ ). This shows that ξ(f i ) = ξ(f2) ∈ Γ. Thus, f i ∈ (a, d)f3 since f2 (a, d)f3. We now check that f1 = f 0 + • • + f t+1 . Claim B.4.2. f1 = 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 .
• Let us take any data value d ∈ data(f2) \ {d1, . . . , dt}. We first check that condition (b) holds for d, in other words, that for every i ∈ {0, . . . , t}, χ

↓ i i+1 (d) ∪ [fi+1] →• χ ↓ e i+1 (d) = χ ↓ e i (d).
We have

χ ↓ i i+1 (d) ∪ [fi+1] →• χ ↓ e i+1 (d) = χ ↓ i i+1 (d) ∪ [f2] →• χ ↓ e i+1 (d) (by Lemma ??) = χ ↓ i 2 (d) ∪ [f2] →• χ ↓ e i+1 (d) (by definition) =      χ ↓ i 2 (d) ∪ [f2] →• χ ↓ e 2 (d) if i = t, or χ ↓ i 2 (d) ∪ [f2] →•( χ ↓ i 2 (d) ∪ [f2] →• χ ↓ e 2 (d)) otherwise.
If i = t, we further have that χ

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

= χ ↓ 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 ∪ [f2] →• χ ↓ i 2 ∪ [f2] →•[f 2] →• χ ↓ i 2 ∪ • • • ∪ [f2] → • • • [f2] → n -1 times • χ ↓ i 2 (d) (by (+4)) = ([f2] →• χ ↓ i 2 )(d) (by Lemma ??) = χ ↓ i 2 (d) (by Lemma ??) = χ ↓ i 1 (d).
(by (??), since d ∈ data(f2))

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

↓ i i+1 (d) ∪ [fi+1] →• χ ↓ e i+1 (d) = χ ↓ e i (d). We have χ ↓ i i+1 (d) ∪ [fi+1] →• χ ↓ e i+1 (d) = ↓ i i+1 (d) ∪ →• χ ↓ e i+1 (d)
(by Lemma ??)

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

d). (by definition)

If i = t and j = i + 1,

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

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

Condition (c) follows by symmetry.

We check that χ

χ ↓ i + (d) = χ ↓ i 2 ∪ [f2] →•∅ ∪ • • • ∪ [f2] → • • • [f2] → n -2 times •∅ ∪ [f2] → • • • [f2] → n -1 times • χ ↓ i 2 (d) (by (+4)) = ( χ ↓ i 2 ∪ [f2] →• χ ↓ i 2 )(d) (by Lemma ??) = ([f2] →• χ ↓ i 2 )(d) (since χ ↓ i 2 ⊆ [f2] →• χ ↓ i 2 ) = χ ↓ i 2 (d)
(by Lemma ??)

= χ ↓ i 1 (d).
(by (??), since d ∈ data(f2))

• 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 ) ∪ [fi+1] →• χ ↓ e i+1 (d j ) = χ ↓ e i (d j ).
By definition, we have

χ ↓ i i+1 (d j ) ∪ [fi+1] →• χ ↓ e i+1 (d j ) = χ ↓ i i+1 (d j ) ∪ [f2] →• χ ↓ e i+1 (d j )
(by Lemma ??)

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

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

χ ↓ i i+1 (d j ) ∪ [f2] →• χ ↓ e i+1 (d j ) = ∅ ∪ [f2] →•[f 2] →• χ ↓ e 2 (dj) (by definition) = [f2] →• χ ↓ e 2 (
∈ ∈ • • • • • • • • • 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 )
1. Let C = {f ∅ }. 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 Fb, 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 = Db. Proof.

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

[⊇] Let f ∈ Db. Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ Db 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

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 9 depicts the general idea of the argument.

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 Fb, 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 = Db. Proof.

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

[⊇] Let f ∈ Db. Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ Db 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

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 9 depicts the general idea of the argument. 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 Fb, 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 = Db. Proof.

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

[⊇] Let f ∈ Db. Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ Db 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
there are minimal elements in Fb, 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 = Db. Proof.

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

[⊇] Let f ∈ Db. Then, there must be a forest t of derivation trees for profiles f1, . . . , fn ∈ Db 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
↓ i + (d j ) = ∅ ∪ [f2] →•∅ ∪ • • • ∪ [f2] → • • • [f2] → j times •∅ ∪ [f2] → • • • [f2] → j + 1 times • χ ↓ i 2 ∪ [f2] → • • • [f2] → j + 2 times •∅ ∪ • • • ∪ [f2] → • • • [f2] → n -1 times •∅ (dj) (by (+4)) = ([f2] →• χ ↓ i
Appendix to Section 5.4

Lemma 5.5. 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 of Lemma 5.5. Suppose we have f = f1+• • •+fn. 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 fj, 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 ∈ χ ,β,i). This is in contradiction with the fact that χ (a, d) 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). 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.

↓ e j (α, β, i) and fj + • • • + f k is defined- d ∈ χ ↓ e k (α
f 1 f f 1 f f f (a, d) ∈ f 1 f f f (a, d) ∈ ∈
Appendix to Section 5.5 Lemma 5.9 is the consequence of the following properties.

Lemma B.6 (Figure

??). For every f, f , f , f 1 ∈ F b and (a, d) ∈ A × D k so that f f , f f and f 1 ∈ (a, d)f , there are f , f 1 ∈ F b so that f f , f f , f 1 ∈ (a, d)f and f 1 f 1 .
Proof of Lemma ??. Without any loss of generality, let us assume that f f and f f so that data

(f ) ∩ data(f ) = data(f ) ∩ data(f 1 ) = data(f). We define f so that R = R and χ (d) = χ (d) if d ∈ data(f else, if d ∈ data(f ).
The following statement follows straight from this definition. Claim B.6.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 (d1) → f (d1), d1] • • • [f (dn) → f (dn)
, dn] for {d1, . . . , dn} = data(f ) \ data(f ), and

• f = f [f (d1) → f (d1), d1] • • • [f (dn) → f (dn)
, dn] for {d1, . . . , dn} = 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 B.6.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 ??, ξ(f 1 ) ∈ Γ and f 1 f 1 , we have that ξ(f 1 ) ∈ Γ. Hence, f 1 ∈ (a, d)f . By definition of f 1 , it also follows that f 1 f 1 .

Claim B.6.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 Proof of Lemma ??. Let f 1 ∈ Rup(↑↓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 ??, 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.8, 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 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 + f 2 f 1 +
f 1 ∈ ↓D b . Lemma B.8 (Figure ??). For every i {1, 2} and fi, f i i ∈ F b so that fi f i , fi 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 of Lemma ??. Without any loss of generality, assume that fi f i , fi f i and data(f i ) ∩ data(f i ) = data(fi) for every i ∈ {1, 2}. Remember that by definition of fi f i , for every data value d ∈ data(f i ) there must be some data value f (d) ∈ data(fi) so that χi(d) = χ i (d) = χ i (d). We then define f i for every i ∈ {1, 2} so that R i = Ri 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(f3-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. Claim B.8.1. f i f i , f i f i for all i ∈ {1, 2}.

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

d ∈ data(f i ), f (d) ∈ data(fi) so that χ i (d) = χi( f (d)) = χ i ( f (d)) and d ∈ Ri iff f (d) ∈ Ri.
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 (d1) → f (d1), d1] • • • [f (dm) → f (dm), dm]
where {d1, . . . , dm} = data(f 3-i ) and { d1, . . . , dn} = data(f i ) \ data(f i ).

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

d ∈ data(f i ), f (d) ∈ data(fi) so that χ i (d) = χi( f (d)) = χ i ( f (d)) = χ i ( f (d)) and d ∈ Ri iff f (d) ∈ Ri.
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 (d1) → f (d1), d1] • • • [f (dm) → f (dm), dm]
where each di and di is so that {d1, . . . , dm} = data(f 3-i ) and { d1, . . . , dn} = data(f i ).

We are then left with the following easy claim. Claim B.8.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 (d1) → f (d1), d1] • • • [f (dn) → f (dn), dn]
for {d1, . . . , dn} = data(f 1 + f 2 ) \ data(f 1 + f 2 ). This concludes the proof of the lemma.

Lemma B.9. R+(↑↓D b ) ⊆ ↓D b .

Proof of Lemma ??. 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 f1, f2, f 1 , f 2 where f i ∈ D b , fi f i , fi f i for all i ∈ {1, 2}. Therefore, by Lemma ??, 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.8, 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.9. Immediate from Lemmas ?? and ??. 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 @ : 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 forest t of Figure 11-b and the nodes x, y depicted, the corresponding expression µ α t,x,y would be the one appearing in Figure 11-c.

Let α be a path expresion, and let ne(α) be the set of all node expressions of α.

WHAT IS WITNESS FOREST? Given a mult data tree t so that t, (x, y) |= α, we call a witn of α for t, (x, y) to a forest t over the alphabet nodes x, y, where t are the nodes involved in the s of α, and they are labeled with the node expres they must verify. For example, given the mult data tree of Figure 11-a, and α as defined in Fig possible witness forest is depicted in Figure 11-b. all witness forests of α for t, (x, y) are bounded by some polynomial p( ).

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

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

Claim From right to left: If there is some forest t, x , t, (x, y) |= µ α t,x ,y , then t, x , y |= μα t,x ,y . Fur t, (x, y) |= µ α t,x ,y , we have that t, x , y is a po ness forest of µ α t,x ,y for t, (x, y). Then, it is also witness forest of α, and hence t, (x, y) |= α. Claim 6.1.2. For every multi-attribute data 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 tree t, (x, y) |= α, if we consider t as the forest that re we restrict t to only the nodes that witness α, rep label of every node by the node expression that we then have that t, (x, y) |= µ α t,x,y . [⇐] Since µ α t,x,y is a direct normal form linea α, we have that t, (x, y) |= α. This means that t order of the nodes of t are compatible with the of α. path. We then build a more complex path expression nesting expressions that the existence of paths as depicted in Figure ??-c. We iterate until we have covered the whole tree t, at each iteration, we add for paths that are at a deeper nesting degree in the resulting direct path expression. For example, the paths of Figure ??-c are at depth 1, the paths of Figure ??-d at depth 2, and the path of Figure ??-e at depth 3. Note that if we apply this construction to the forest of Figure ??-c and the path α of Figure ??-e, we obtain the expression µ α t,x,y of Figure ??-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 ??-a, and α as defined in Figure ??-e, a possible witness forest of α for t, (x, y) is depicted in Figure ??-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 ??-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.

Figure 2 :

 2 Figure 2: The syntax of transitive XPath; and its semantics for a multi-attribute data tree t = a ⊗ d.

  b

Figure 3 :

 3 Figure 3: A multi-attribute data forest, with its left and right forests.

  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 other e = d . Note that if d

  there must be some f2 f2 + • • • + fm by inductive hypothesis. • If t = t1• t2 with t1, t2 = ε... XXXXX Figure9depicts the general idea of the argument.Db = ↑C. When we write C we mean {f | f ∼ f ∈ C} and by ↑C

Figure 4 :

 4 Figure 4: Statement of Lemma 5.1.

Figure 5 :

 5 Figure 5: Statement of Lemma 5.3.

Figure 6 :

 6 Figure 6: Statement of Lemma 5.4.

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

  , 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), . . . }.

3

 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

Figure 7 :

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

  ??), since d ∈ data(f2))

  i = t and j = i + 1,

  (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 χ ↓ e + (d j ) = χ ↓ e 2 (dj) (by (+2)) = χ ↓ e 1 (d j ), (since χ1(d j ) = χ2(dj) by (??))

Figure 8 :

 8 Figure 8: Statement of Lemma ??.

  χ

k

  (α, β, i) = {d }. The same happens by symmetry with χ ↓ e . Let us defineR 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, f1, . . . , fn but with Rχ 1 ,..., χn as the set of rigid values. By construction of Rχ 1 ,..., χn we have thatf = f 1 + • • • + f n .In other words we have the following.Claim B.5.6. For every (R, χ) = (R, χ1) + • • • + (R, χn) we have that (Rχ 1 ,..., χn , χ) = (Rχ 1 ,..., χn , χ1) + • • • + (Rχ 1 ,..., χn , χn).

Figure 9 :

 9 Figure 9: Statement of Lemma ??.

Figure 10 :

 10 Figure 10: Statement of Lemma ??.

  ,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 Figure 11 :

 a11 Figure 11: Example for the proof of Lemma 6.1.α = * ←[ψ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]

Figure 11 :Figure 12 :

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

  •' as the concatenation operator between sequences. By |S| we denote the length of S (if S is a finite sequence), or its cardinality (if S is a set). We use (ai) i∈{j,...,j+n} as short for ajaj+1 • • • aj+n.

			a	label
			@ : 1 5 @ : 2 8		node
	b @ : 1 5 @ : 2 3	a @ : 1 4 @ : 2 8	b @ : 1 2 @ : 2 8	a @ : 1 5 @ : 2 3	c @ : 1 9 @ : 2 4
	@ : @ : 2 7 1 2 c	c @ : 1 5 @ : 2 3	@ : 1 9 @ : 2 2 b	attribute index data value
		a		node's position: 32
		@ : 1 5 @ : 2 5		subforest
	Figure 1: A multi-attribute data tree, where A = {a, b, c} and k = 2.

'

  then χ+(d) = χ1(d). Here we only deal with χ

	and χ ↓ i + because the cases for χ ↓ e + and χ ↓ i + are symmetrical. By definition of +, we have that	↓ e +
	χ ↓ e + (d) = χ ↓ e 2 (d)	(by (+2))
	= χ ↓ e 1 (d),	(by (??), since d ∈ data(f2))

  6.1.1. If t, (x, y) |= α if, and only if, µ α t,x ,y for some forest t, x , y over 2 ne(α) of size p(|α|). Proof. From left to right: If t, (x, y) |= α, witness forest of α for t, (x, y), call it t, x , y , t, x , y |= μα

	FINISH THE PROOF HERE????

t,x ,y , and therefore t, (x, y) |= µ α t,x ,y

  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 som forest t, x , y of t, (x, y) |= α.

			a @ : 1 9 @ : 2 7
	b @ : 1 9 @ : 2 4	x	b @ : 1 9 @ : 2 4	a @ : 1 9 @ : 2 4	c @ : 1 1 @ : 2 4
	c @ : 1 9 @ : 2 7		a @ : 1 9 @ : 2 2		b @ : 1 7 @ : 2 4
			c @ : 1 5 @ : 2 1	y	b @ : 1 9 @ : 2 4
			a @ : 1 2 @ :
					USE FIGURE, IMPROVE
					There are exponentially many trees, and thus ther
					nentially many direct normal form linearizations

These are the axes that are called preceding-sibling, followingsibling 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 precedingsibling, following-sibling and descendant axes respectively.

)(dj) (by Lemma ??)

We acknowledge the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Pro-Commission, under the FET-Open grant agreement FOX, number FP7-ICT-233599.

APPENDIX

We organize this appendix with the missing proofs, grouped by sections on the main body. In each case we repeat the statements for the reader's convenience.

A. APPENDIX TO SECTION 4

Lemma A.1 (distributivity of (•, ∪)). For every P, P ⊆ P and χ, χ ⊆ D × Π 1. P •(χ ∪ χ ) = P •χ ∪ P •χ , 2. (P ∪ P )•χ = P •χ ∪ P •χ.

Proof. We have that

(by definition of '•') which proves the first statement.

On the other hand, (by Lemma ??)

(since χ1(d j ) = χ2(dj) by (??))

Therefore, we have that condition (a) as as conditions (b) and (c) hold true for every data value, and that f 0 + • • + f t+1 and f1 coincide. Thus, Claim follows. This concludes our proof. As a corollary of the previous lemma, we obtain the following. Lemma B.5 (Figure ??). For every f f1 + • • • + ft with fi ∈ (ai, di)f3,i, there are f i,j ∈ ∼ (ai, di)f3,i for every i ∈ [t], j ∈ [ni] so that

Proof of Lemma ??. This is a direct consequence of Lemma 5.1. Since f f1

for some d1, . . . , dn, d 1 , . . . , d n ∈ D so that {d1, . . . , dn}∩R = ∅ and {d 1 , . . . , d n }∩data(f1

fi ∈ (ai, di)f3,i for every i ∈ [t]. We can hence apply Lemma 5.1, and we obtain, for some ni ∈ N, f i,1 , . . . , f i,n i ∈ ∼ (ai, di)f3,i so that

which concludes the proof.

Lemma 5.2. D = ↑D. Proof of Lemma 5.2. This is a direct consequence of Lemma ??. Lemma 5.3 (Figure 5). If f1 + f2 = f3 and f 1 f1, f 2 f2, then f 1 + f 2 f3, for some f 1 , f 2 ∈ F so that f i is a bounded extension of f i , for all i ∈ {1, 2}.

Proof of Lemma 5.3. For every description π so that χ3(π) \ R3 = ∅, let dπ ∈ D be a data value so that dπ ∈ χ3(π) \ R3. Let D be the set of all these data values. Note that |D| ≤ |Π| 4 .

We define f i = (R3, χ i ), where

dn] where {d1, . . . , dn} = D \ data(f i ) and for every j ∈ [n], d j ∈ Ri, dj ∈ data(f i ), and χ i (d j ) = χi(dj). In other words, we have that f i f i fi for all i ∈ {1, 2}. Therefore, f i is a bounded extension of f i for i ∈ {1, 2}.

Claim B.5.2. f 1 + f 2 f3. Proof. First, we have that f 1 , f 2 ∈ F because otherwise f1 or f2 would not be in F. Since f i fi, by Lemma ?? it follows that

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 f1 + f2 they must also hold for f 1 + f 2 . Therefore, all the preconditions to apply

Note that all the profiles in question share the same set of rigid values,

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(f3) \ data(f 3 ), it must be that d ∈ R3 and there must be some d ∈ D so that χ3( d) = χ3(d) by definition of D. Then, if data(f3) \ data(f 3 ) = {d1, . . . , dn} we have that

and hence, f 3 f3. By Claims ?? and ??, and since data(f i ) ≤ data(f i ) + |Π| 4 , the lemma follows.

Lemma 5.4 (Figure 6). For every f1 ∈ (a, d)f2 and f2 f5, there is f4 f5 and f3 ∈ ∼ (a, d)f4 so that |data(f4)| ≤ |data(f5)| + |Π| 4 + |R1| and f3 f1, f4 f2.

Proof of Lemma 5.4. We are given f1, f2, f5 and (a, d). We show that there must be some f3 and f4 so that f1 f3 ∈ (a, d)f4 with f4 f5. Figure 6 contains a graphical representation of the profiles we work with in the proof.

We first define f4. For every internal description π so that π We finish the proof of f4 f5 by showing that for every d ∈ data(f4)\R4 there is some d ∈ data(f5)\R4 so that χ4 We finish the proof of f4 f2 by showing that for every d ∈ data(f2)\R2 there is some d ∈ data(f4)\R2 so that χ2 We must show that for every d ∈ data(f1) \ (R1 ∪ data(f3)) there is some d ∈ data(f3) \ R1 so that χ1(d) = χ3(d ). Take any such d. Note that d must be necessarily an internal data value, since f3 contains any strict external data value of f1. Hence, let π = χ1(d), where π

By definition of D, there must be some dπ ∈ D so that χ1(dπ) = π and dπ ∈ R1. Since π is internal and f1 ∈ (a, d)f2, dπ ∈ d ∪ data(f2). If dπ ∈ d, we have, by definition of f3, that χ3(dπ) = χ1(dπ) = π = χ1(d). Hence, there is such d ∈ data(f3) \ R1 so that χ1(d) = χ3(d ). Otherwise, suppose dπ ∈ data(f2), which means, since π

. By definition of f4, χ4(dπ) = χ2(dπ) = (∅, ∅, ∅, ∅), thus dπ ∈ data(f4). Then, by definition of f3 we have that χ3(dπ) = χ1(dπ) = π = χ1(d). Hence, in this case we also have that there is such d ∈ data(f3) \ R1 so that χ1(d) = χ3(d ).

Claim B.5.5. f3 ∈ (a, d)f4.

Proof. Since f4 f2 and f1 ∈ (a, d)f2, we have that • ξ(f4) ∈ Γ since ξ(f2) ∈ Γ, by Lemma ??, and

↓ e 2 = ∅. Therefore, conditions (a) and (b) hold for f4. We must show condition (c), that is, χ

This, together with the fact that all internal values of f3 are in data(f4) ∪ d, implies that χ

Hence, condition (c) holds, and we have that f3 ∈ (a, d)f4.

This concludes the proof.

Appendix to Section

Thanks to the property R(↑↓D b ) ⊆ ↓D b one can show that C ∼ k 0 = 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.

Lemma 5.11. Lemma 5.11. By Lemma 5.9 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 ∼ k 0 . Suppose, by means of contradiction, that there is some

). We further have that this computation is in 2ExpSpace. Since |min(F b )/∼| is doubly exponential in |P|, we have the following.

Lemma B.10. k0 is bounded by a doubly exponential function on |P|.

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

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 represented with an element of

Therefore, there are doubly exponentially many elements in min(F b )/∼, and hence k0 is bounded by a doubly exponential function in |Π|. Since |Π| is polynomial in |P|, the statement follows.

Proof of Lemma ??. First we check that f ∈ min(↓F b ).

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

Finally, to check f ∈ min(↓Rup(↑↓G)), we verify that f f3 ∈ min((a, d)f4) in 2ExpSpace, where f4 is a bounded extension of a profile of min(↓G). If the condition holds of course f ∈ min(↓Rup(↑↓G)). On the other hand, by Lemma 5.4 cum Remark 5.6, if f ∈ (a, d)f2 with f2 f5, then f f3 ∈ min((a, d)f4) for some bounded extension f4 of f5, and hence the condition holds.

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

Proposition 5.12. (↑↓{f })). Claim B.12.1. The following statements are equivalent.

1. There is some f ∈ min({f ∈ F | ξ(f) ∈ Γ}) with no external values so that

There is a derivable root profile in D b .

Proof. [??⇒??] Assume first that condition ?? holds. We change the names for the profiles to make the explanation clear. Suppose that there is some

, 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 ?? obtaining that there is some f and

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 .

[??⇐??] Suppose, on the other hand, that condition ?? holds. If there is a derivable root profile in D b , then there are

C. APPENDIX TO SECTION 6

Appendix to Section 6.1 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 of Lemma 6.1. 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 in the reflexive-transitive closure of the next-sibling relation (resp. of the child relation) in t . 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 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 ??-a and α as defined in Figure ??-e, the tree tα is the one of Figure ??-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 relative order of nodes satisfying the labels as in the tree. For example, for the forest t of Figure ??-c and the nodes x, y depicted, the corresponding expression μα t,x,y would be the one appearing in Figure ??-e.

Claim C.0.1. A 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 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 ??-a, we build a path as in Figure ??-b that tests all the node expressions of the nodes in Claim C.0.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 C.0.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 C.0.4. t, (x, y) |= α if, and only if, t, (x, y) |= µ α t,x ,y for some direct normal form linearization µ α t,x ,y of α. Proof. If t, (x, y) |= α, then by Claim ?? 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 ??. Since t, (x , y ) |= α, we then have that t, (x, y) |= α by Claim ??.

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.

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 of Lemma 6.2. 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 ( 1 To build the formula ϕ = ϕ1 ∧ϕ2 in normal form, we define ϕ1 = ζη, and we build ϕ2 as a conjunction of formulas

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 polynomial space. Proof of Corollary 6.3. 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.

Appendix to Section 6.2 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.

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 -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,

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. Lemma 6.5. f a∈A (a ⇒ γϕ(a)) if, and only if, ξ(f) ∈ Γ φ . Proof of Lemma 6.5. This is a direct consequence of Lemma 6.4 and the definition of Γ φ .

Abstractions.

We now define abs( tl , t, tr) for any forests tl , t, tr. Let t l = a l ⊗d l , t = a⊗d, tr = ar⊗dr 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 absR( tl , t, tr) def = (abs( tl , t, tr), R). Remark C.1. Note that abs ∅ ( , , ) = f ∅ . 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 C.2. Given R ⊆ D, and multi-attribute data forests t, tl , tr, t1, t2, 1. provided that absR( tl , t1, t2• tr), absR( tl • t1, t2, tr), absR( tl , t1• t2, tr) ∈ F, absR( tl , t1, t2• tr) + absR( tl • t1, t2, tr)=absR( tl , t1• t2, tr).

2. Given (a, d) ∈ A×D k , R ⊆ D so that abs R ( , t, ) ∈ F, absR( tl , (a, d) t, tr) ∈ F, and ξ(absR( tl , (a, d) t, tr)) ∈ Γ φ , we have absR( tl , (a, d) t, tr) ∈ (a, d) abs R ( , t, ). Proof of Lemma ??. ??. Condition (a) is obvious because we have the same set R of rigid values in all profiles. Conditions (b) and (c) follow straight from the semantics of XPath and the definition of abs. By definition of abs, the set χ ↓ e 1 where = absR( tl • t1, t2, tr) is composed by all the paths that can reach data values in t2• tr, which is precisely χ

2 where = absR( 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.

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

For any derivation forest t (as defined in Section 4.3) we associate a multi-attribute data forest tt which is the result of removing all leaf nodes from t and projecting the tree onto A × D k . • If ψ = ψ1 ∧ ψ2 or ψ = ¬ψ , we proceed by induction.

• Now suppose ψ = α•β@i = γ•δ@j , 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 -1 * ← (α), P -1 ↓ * (β), i) ∈

, by definition of abs we have that χ ↓ i is the set of all (d(y)(k), α1, α2, k) so that (1, y) ∈ [[P→ * (α1)P ↓ * (α2)@ k ]] (a, d)t . It then follows that there must be some y so that (i0,

If on the other hand (P -1

* ← (α), P -1

, or there must be some α 1 , α 2 so that α 1 ∈ → [f] and (α 2 , P -1

. Suppose that the latter occurs (the former being only easier). Since by definition of abs we have that χ ↓ e is the set of all (d l (y)(k), α1, β1, k) so that (n, y) ∈ [[P * ←(α1)P ↓ * (β1

where α1 = P * ←(α 1 ). Then, there is some y

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 (i0,

By similar arguments, we have that there must be some z ∈ pos((a, d)( tl

[⇐] Suppose that tl •t• tr, i0 |= α•β@i = γ•δ@j . In other words, there are y, z ∈ pos(t ), y = , z = , so that (i0,

, 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

, where α 1 = P -1 * ← (α1), α 2 = P -1 * ← (α2). If the latter case holds (the former being only easier), we have that

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 .

The next lemma basically shows that every derivable root profile is the abstraction of some tree satisfying φ.

Lemma C.4. Let froot ∈ 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 f1, . . . , fn are the profile labels of the roots of t. Let R be the rigid set for f1, . . . , fn. Then,

• absR( , t, ) = f1 + • • • + fn, and

Proof of Lemma ??. We will make use of the following easy fact. Claim C.4.1. Given f1, . . . , fn ∈ F, so that f+ = f1 + • • • + fn where χ

Proof. This is by conditions (b) and (c) of profile concatenation:

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 = (a1 d1) t1 • • • (an, dn) tn and each ti has height less than m. Let fi = absR ((aj, dj) tj)j<i, (ai, di) ti, ((aj, dj) tj)j>i for every i. We then have the following.

Claim C.4.2. For every i ∈ [n], fi = fi. Proof. For every ti = , we have that f 1 + • • • + f l = absR i ( , 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 fi ∈ (ai, di)(f 1 + • • • + f l ) by definition of derivation tree, we have that fi ∈ (ai, di)absR i ( , ti, ). If ti = , then, since abs ∅ ( , , ) = f ∅ and fi ∈ (ai, di)f∅, we also have that fi ∈ (ai, di)absR i ( , ti, ). Hence, for all i ∈ [n], fi ∈ (ai, di)absR i ( , ti, ). Now, since • all the internal descriptions of any forest profile inside (ai, di)abs∅( , ti, ) is completely determined by (ai, di) and abs ∅ ( , ti, ), and hence fi and fi have the same internal descriptions, On the other hand, since ξ(f1), . . . , ξ(fn) ∈ Γ φ by condition (a) of rooting, we have fi = fi a∈A φ (a ⇒ γ φ (a)) for every i. Hence, by Lemma ??, (a1, d1) t1 • • • (an, dn) tn, i |= a∈A (a ⇒ γϕ(a)) 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 (a1, d1) • • • (an, dn) tn, i |= φ2 for every i.

We now show that if φ is satisfiable, then there must be a derivable root profile. Lemma C.5. 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 = absR( tl t, tr), where R = data( tl • t• tr). Further, if t is a tree, f is so that f ∈ (a, d)f , with f ∈ D.

Proof of Lemma ??. 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 absR( tl , (a, d), tr) ∈ (a, d)f ∅ .

Since tl •(a, d)• for j = | tl | + 1, we have that absR( tl , t, tr) γ φ (a) by Lemma ??. In other words, we have ξ(absR( tl , t, tr)) ∈ Γ φ . Then, by Lemma ??-?? we have absR( tl , (a, d), tr) ∈ (a, d)abs ∅ ( , , ). Since f ∅ = abs ∅ ( , , ) (Remark ??), we have that (a, d)abs ∅ ( , , ) = (a, d)f ∅ . Therefore, absR( 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 ?? since tl •(a, d) t • tr, j |= φ2 for j = | tl | + 1, we have that ξ(absR( tl , (a, d) t , tr)) ∈ Γ φ . We then have that absR( tl , (a, d) t , tr) ∈ (a, d)f = (a, d)abs R ( , t , ) again by Lemma ??-??. Therefore, absR( 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 f1, f2 ∈ D so that f1 = absR( tl , t1, t2• tr) and f2 = absR( tl • t1, t2, tr). As absR( tl , t1• t2, tr) = absR( tl , t1, t2• tr) + absR( tl • t1, t2, tr) by Lemma ??-??, it follows that absR( tl , t1• t2, tr) = f1 + f2 ∈ D since f1, f2 ∈ D.

Corollary 6.6. There is a derivable root forest profile if, and only if, φ is satisfiable. Proof of Corollary 6.6.

[⇒] 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 ??, we have that absR( , t, ) = f and that t |= φ2. Since f is a root profile, the root of t must have a label (a, d) with a ∈ Aroot, and hence t |= φ1 as well. Therefore, φ is satisfiable.

[⇐] Let t be so that t |= φ. Then by Lemma ?? we have that 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 ∈ Aroot. Hence, f is a derivable root profile.