David Baelde

Anthony Lick

Sylvain Schmitz

John Doejohn Doe

Decidable XPath Fragments in the Real World

Keywords: CCS CONCEPTS, Information systems → XPath, XQuery, • Theory of computation → Logic and verification

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

INTRODUCTION

The XPath language [START_REF]XML Path Language (XPath) 3.0. W3C Recommendation[END_REF] is arguably the most popular querying language for selecting elements in XML documents. It is embedded in the XML processing languages XSLT [START_REF] Kay | XSL Transformations (XSLT) Version 3.0. W3C Recommendation[END_REF] and XQuery [START_REF]XQuery 3.0: An XML Query Language[END_REF], and widely used in general-purpose languages like Java or C# through third-party libraries. It combines the ability to navigate the XML tree-which finds its roots in modal logic [START_REF] Afanasiev | PDL for ordered trees[END_REF]-with that of comparing data values found in several, distantly related attributes.

Alongside the evaluation of the set of elements selected in a document [e.g. [START_REF] Arroyuelo | Fast in-memory XPath search using compressed indexes[END_REF][START_REF] Benedikt | XPath leashed[END_REF][START_REF] Bojańczyk | XPath evaluation in linear time[END_REF][START_REF] Gottlob | The complexity of XPath query evaluation and XML typing[END_REF], the main computational problem associated with a query is the satisfiability problem: given an XPath query, and optionally a schema for the type of XML documents under consideration, does there exist at least one XML document on which this query would select some node? This abstract question Unfortunately, the satisfiability problem is in general undecidable. Even CoreXPath 1.0, a simplified syntax based on the navigational fragment of XPath 1.0, is untractable, more exactly EXPcomplete already when only using the child axis [START_REF] Afanasiev | PDL for ordered trees[END_REF][START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF][START_REF] Neven | On the complexity of XPath containment in the presence of disjunction, DTDs, and variables[END_REF]. Thus with the exception of the work of Genevès et al. [START_REF] Genevès | Efficiently deciding µ-calculus with converse over finite trees[END_REF] on Core-XPath 1.0, most of the literature on the topic is of a theoretical nature [e.g. 2, 5, 12, 20-22, 25, 26, 34], and focuses on decidability and complexity questions in variants of CoreXPath 1.0 that allow limited forms of data joins.

While these results are technically impressive, it is not immediately clear how much is gained in practice by handling data joins. Indeed, data joins are not the sole source of difficulty in XPath: many real-life XPath queries perform calls to a standard library of functions [START_REF] Kay | XPath and XQuery Functions and Operators 3.0. W3C Recommendation[END_REF]-including arithmetic and string-manipulating functions-that also lead to an undecidable satisfiability.

Also, XPath 1.0 dates back to 1999; the more recent versions 2.0 and 3.0 feature path intersections, for loops, etc. [see 45]. As it evolves in pace with XQuery, XPath includes more and more general programming constructs, and is arguably not just a domain-specific language for path navigation-quite tellingly, in our benchmark, we found that only half of the queries use navigation.

In this paper, we evaluate the practical applicability of XPath fragments proposed in the theoretical literature from a basic, syntactic perspective: how many queries are captured by these fragments? The first step to this end is the compilation of a benchmark of 21,141 real-world XPath queries. The queries are extracted from opensource projects that rely heavily on XSLT or XQuery. As described in Sec. 2, the benchmark offers for each XPath query an XML syntax tree representation in XQueryX [START_REF] Melton | XQueryX 3.0. W3C Recommendation[END_REF]. The tools and the resulting benchmark are available from http://git.lsv.fr/schmitz/xpparser/ under open source licenses.

Our aim is then to check the queries in our benchmark against the syntax allowed in theoretical works on XPath satisfiability, namely by writing Relax NG specifications for PositiveXPath [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF][START_REF] Hidders | Satisfiability of XPath expressions[END_REF], CoreXPath 1.0 [START_REF] Gottlob | Monadic queries over tree-structured data[END_REF], CoreXPath 2.0 [START_REF] Balder Ten | The complexity of query containment in expressive fragments of XPath 2.0[END_REF], fragments of Data-XPath [START_REF] Figueira | Alternating register automata on finite words and trees[END_REF][START_REF] Figueira | Decidability of downward XPath[END_REF][START_REF] Figueira | Bottom-up automata on data trees and vertical XPath[END_REF], and fragments of XPath that can be interpreted in EMSO 2 [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF] or using non-mixing MSO constraints [START_REF] Czerwinski | Reasoning about integrity constraints for tree-structured data[END_REF] (see Sec. 4).

Naturally, the syntax defined in these works is simplified and was never meant to be used directly against concrete XPath inputs, while we need a concrete syntax for each one of these fragments in order to implement it in Relax NG. This leads to the interesting question of which XPath features can be 'reasonably' handled in these fragments without losing a decidable satisfiability nor hampering its complexity (see Sec. 5.1). In turn, answering this type of question requires the definition of a palatable semantics for a substantial subset of XPath 3.0, which we provide in Sec. [START_REF] Afanasiev | PDL for ordered trees[END_REF].

As could be expected, the coverage of the naive implementations of the syntactic fragments from the literature is not very good (Sec. 4.2), and one should extend them whenever reasonable. In Sec. 5, we propose six extensions of the original fragments and evaluate their coverage on the benchmark. These extensions are root navigation, free variables, data tests against constants, positive data joins, and restricted calls to the functions last() and id(). Just as interestingly, we exhibit several cases where these extensions cannot be handled.

We analyse our experimental results in Sec. 6, notably concluding that higher coverage is obtained through basic extensions than by using complex academic fragments. We also identify increased function support as a promising direction for improved practical satisfiability checking, with an especially high potential for XPath queries from XSLT sources. We conclude in Sec. 7.

A REAL-WORLD BENCHMARK

We explain here the technical aspects of the construction of a benchmark of 21,141 queries: the parser we developed to this end (Sec. 2.1), the sources we employed (Sec. 2.2), and the way we processed the benchmark to check whether a given query belongs to a syntactic XPath fragment (Sec. 2.3). We finish the section by mentioning the limitations of the current benchmark.

Parser

We have modified the W3C parser for XQuery 3.0, 1 which is (almost) a superset of XPath 3.0, so that we can also use it for XPath queries extracted from XSLT documents. This parser uses a grammar automatically extracted from the language specification, so we are confident in its results. Our implementation further [START_REF] Parosh | Norn: An SMT solver for string constraints[END_REF] extracts XPath queries from XQuery files, by selecting 'maximal XPath subtrees' in the abstract syntax tree of the XQuery document, and (2) outputs syntax trees in the standard XML format XQueryX [START_REF] Melton | XQueryX 3.0. W3C Recommendation[END_REF];

this is what we process to determine to which XPath fragments each query belongs.

See App. B for an example XQuery document and the corresponding parser output.

Sources

Our choice of sources for the benchmark relied on searches through open source GitHub projects containing XSLT or XQuery files, 1 https://www.w3.org/2013/01/qt-applets/ selecting the most popular projects from which we could extract at least 50 queries. We also added one large project not hosted on GitHub, namely DocBook XSL.

The XSLT projects aim to translate enriched text documents between different formats. The XQuery projects we include are most often libraries. The detailed composition is presented in Tab. 6 in the appendices. We make no formal claim about the coverage of the benchmark, but rather see it as a first release, to be enriched later as part of a community-driven effort.

Properties of the Benchmark

Standard Coverage. We exploit this benchmark by validating the syntax trees in XQueryX format against Relax NG [START_REF] Clark | RELAX NG Compact Syntax[END_REF] specifications. Table 1 presents the number of queries that fall within the scope of the three major revisions of the XPath standard. We can observe that the queries extracted from XSLT files are nearly all XPath 1.0 queries, which contrasts with queries extracted from XQuery sources, which rely more often on advanced XPath features from XPath 2.0 and XPath 3.0. 2 Note that the coverage of XPath 1.0, 2.0, and 3.0 given in Tab. 1 does not restrict function calls to the standard library [START_REF] Kay | XPath and XQuery Functions and Operators 3.0. W3C Recommendation[END_REF]. The last column 'XPath 3.0 std' shows the coverage of XPath 3.0 when restricted to standard functions. We see here an essential limitation of analysing XPath queries in isolation, without support for nonstandard functions, and in particular for user-defined functions: more than half of the queries extracted from XQuery documents are beyond the scope of our analyses.

Functions. We show in Fig. 1 the number of occurrences for each of the 400 most frequently occurring functions (among 1,600) and the associated accumulated percentage of the total number of function calls. Darker dots correspond to standard XPath functions, The standard functions only represent 57.23% of the function calls in the benchmark. This is mostly due to queries from XQuery sources, which routinely use functions defined in the surrounding XQuery programs: when restricting to these sources, standard XPath functions represent 42.93% of the function calls. By contrast, when restricting to XSLT sources, we find only 210 functions and standard XPath functions represent 76.32% of the calls. Moreover, the 16 functions with more than 100 occurrences each all belong to the XSLT or XPath standard, and account for 78.35% of the occurrences of function calls. In the XSLT sources, there are 4,650 queries (31.69%) performing at least one function call, roughly as many as the 4,556 queries (70.46%) found in the XQuery sources.

Size. Figure 2 shows the distribution of query sizes, defined as the size of their syntax trees, measured as the number of nodes in the tree. As might be expected, most of the queries are of modest size and a majority of the queries have size at most 8, but there are nevertheless 256 queries of size 100 or more.

Limitations

The benchmark is made of uncurated data, thus no distinction is made between tiny XPath queries and more interesting ones. For instance, only 9,852 of the queries in the benchmark use at least one axis step.

Also, as seen in Tab. 1, the numbers of queries from the various sources are not balanced, which means that results on the whole benchmark might not be very telling, and that one should distinguish the XSLT sources from the XQuery ones.

Finally, the benchmark was compiled specifically for investigating the coverage of syntactic fragments of XPath. It is currently not really suitable for other ends:

XPath satisfiability: in both XSLT and XQuery files, no schema information on the XML to be processed is available. Furthermore, it seems likely that most queries are satisfiablequite possibly all of them. XPath evaluation: similarly, the benchmark does not provide examples of input XML documents on which the XSLT or XQuery should be evaluated. These limitations could probably be lifted by adding manual annotations.

XPATH 3.0

The XPath 3.0 specification is arguably too complex to be reasoned about directly. We work instead with a well-defined sub-language, designed to capture accurately the constructions we witnessed in the benchmark. In order to be compatible with the semantics in the XPath literature, we provide a semantics on data trees, but in Sec. 3.6 we show how to capture the actual XPath semantics on XML documents.

Data Trees

Our models are an abstraction of XML DOM trees called data trees, which are finite trees where each node carries both a label from a finite alphabet Σ and a datum from an infinite countable domain D equipped with an order <. Formally, a data tree is a finite rooted ordered unranked tree with labels in Σ × D: it is a pair t = (ℓ, δ ) of functions ℓ: N → Σ, δ : N → D with a common non-empty finite set of nodes N ⊆ N * as domain; N must be prefix-closed (if p • i ∈ N for some p ∈ N * and i ∈ N, then p ∈ N ) and predecessor-closed (if p • (i + 1) ∈ N for some p ∈ N * and i ∈ N, then p • i ∈ N ); in particular it contains a root node ε. Nodes in N , being finite sequences of natural numbers, are totally ordered by the lexicographic ordering, which is known in this context as the document order and denoted by ≪. Figure 3 displays an example of a data tree.

When working with first-order or monadic second-order logic, a data tree is a relational structure (N , ↓, →, ∼, (P a ) a ∈Σ , (P d ) d ∈D ) where

→ def = {(p • i, p • (i + 1)) ∈ N 2 | p ∈ N * , i ∈ N} , ↓ def = {(p, p • i) ∈ N 2 | p ∈ N * , i ∈ N} , P a def = {p ∈ N | ℓ(p) = a}, ∼ def = {(p, p ′ ) ∈ N 2 | δ (p) = δ (p ′ )} , P d def = {p ∈ N | δ (p) = d}
denote respectively the child relation, the next-sibling relation, data equivalence, and the labelling and data predicates.

Syntax

While our implementation works with concrete syntax (see e.g. the example in App. B), for the sake of readability we use an abstract syntax throughout the paper. It is nevertheless fully compatible Let X be a countable infinite set of variables, and F be a ranked alphabet of function names; we denote by F n its subset of symbols with arity n. As usual, our language has multiple sorts: axes denote directions in the data tree, with abstract syntax

self A def = {(p, p) | p ∈ N 2 } child A def = ↓ parent A def = ↓ -1 following-sibling A def = → + ancestor A def = (↓ -1 ) + preceding-sibling A def = (→ -1 ) + descendant A def = ↓ +
α ::= self | child | descendant | following-sibling | parent | ancestor | preceding-sibling
path expressions describe binary relations between the nodes in a data tree, with abstract syntax π ::= α::

* | /π | π /π | π [φ] | π union π | f (π 1 , . . . , π n ) | $x | let $x := π return π ′ | for $x in π return π
where $x ranges over X, n over N, and f over F n , while node expressions describe sets of nodes, with abstract syntax

φ ::= π | a | false() | not(φ) | φ or φ | π is π | π △ π | π △ + d
where a ranges over Σ, d over D, △ over {eq, ne} and △ + over {eq, ne, le, lt, ge, gt}. Note that only eq and ne are allowed when comparing paths, while the ordered structure of D is only available when comparing a path and a data constant: none of the fragments we consider is known to allow the richer path comparisons.

Data Tree Semantics

For a fixed data tree of domain N , we give in figures 4 and 5 the semantics of axes α A , path and node expressions π ν P and φ ν N . The semantics is relative to a current variable valuation ν : X → 2 N . The semantics of node expressions are sets of nodes of N , while those of axes and path expression are sets of pairs of nodes.

In order to interpret functions, we assume that each function symbol f from F n comes with a semantics f F : (2 N ) n → 2 N . For instance, false() and not() are technically XPath functions, with semantics false F def = ∅ and not F (S ) def = N \S for all S ⊆ N . Likewise, we interpret each comparison operator △ + as a data relation

△ + ∼ ⊆ D × D: eq
∼ is the equality = over D, and ne ∼ the disequality , lt ∼ the strict order <, etc. For binary relations R, R ′ , we employ relational

compositions R R ′ def = {(p, p ′′ ) | ∃p ′ .(p, p ′ ) ∈ R ∧ (p ′ , p ′′ ) ∈ R ′ }, transitive closures R + , converses R -1 def = {(p ′ , p) | (p, p ′ ) ∈ R}, and images R(p) def = {p ′ | (p, p ′ ) ∈ R}.
Beware that the semantics of a path expression π changes when seen as a node expression. In particular, a variable $x is a path expression, and when seen as a node formula $x ν N = N unless ν ($x) = ∅. XPath provides two quantifiers: for expressions bind singleton node sets, while let expressions bind node sets.

Example 3.1. Evaluating for $x in child:: * [o or t] return $x[self:: * eq $x/child:: * ] at the root of the data tree in Fig. 3 binds $x to each of the two children nodes labelled o or t in succession, and returns the o node. Evaluating let $x := child:: * [o or t] return $x[self:: * eq $x/child:: * ] at the root binds $x to the set containing both o and t, and returns both of them.

Our semantics is in line with the ones found in the literature. However, we note that it slightly differs from the actual XPath semantics. In particular, we only account for pure functions acting on paths, while functions from XPath's large standard library [START_REF] Kay | XPath and XQuery Functions and Operators 3.0. W3C Recommendation[END_REF] may be polymorphic and have side-effects-two features that are anyway out of the reach of the current decidable fragments. Also, variables in XPath are bound to ordered collections of nodes and data values, while we only consider sets of nodes. This simpler semantics is not restrictive for our purposes, as discussed further in Sec. 3.6.

The Satisfiability Problem

In this paper, we focus on the satisfiability problem: given a node expression φ, does there exist a data tree t such that t |= φ? As path expressions are also node expressions, this also captures the satisfiability of path expressions. In presence of a DTD, the data tree t should additionally belong to the DTD's language. Remark 3.2. A related problem is query containment: for node expressions φ and φ ′ , we say that φ is contained in φ ′ if, for all data trees and all variable valuations ν , φ ν N ⊆ φ ′ ν N . This is equivalent to asking the unsatisfiability of φ and not(φ ′ ), so it reduces to the satisfiability problem when negation is allowed-which will not always be our case. The problem of path containment asks the same question for path expressions π and π ′ , and is not captured by satisfiability. Furthermore, one might also consider variants of these problems where we ask instead whether for all data trees and variable valuations ν and ν ′ , φ ν N ⊆ φ ′ ν ′ N , which can lead to rather different results [START_REF] Neven | On the complexity of XPath containment in the presence of disjunction, DTDs, and variables[END_REF].

Syntactic Sugar

XPath comes with some handy syntactic sugar.

3.5.1 XPath 1.0 Sugar. Beside standard definitions like true() def = not(false()) or φ and φ ′ def = not(not(φ) or not(φ ′ )), we may use

. def
= self:: * for referring to the current point of focus, .. def = parent:: * for its parent, α::a def = α:: * [a] for testing the label found after an axis step, and a single label a as a path formula for child::a.

The syntax also features four more axes: descendant-or-self:: * is defined as descendant:: * union self:: * and ancestor-or-self is defined similarly. The axis following:: * is defined as the path ancestor-or-self:: * /following-sibling:: * /descendant-or-self:: * .

The preceding axis is defined similarly. The shorthand π //π ′ stands for π /descendant-or-self:: * /π ′ , and //π is defined similarly. Conditional node expressions, while only available in XPath 2.0 and later, are also easily handled: if (φ) then φ ′ else φ ′′ def = (φ and φ ′ ) or (not(φ) and φ ′′ ).

3.5.2 XPath 2.0 Sugar. As shown by ten Cate and Lutz [START_REF] Balder Ten | The complexity of query containment in expressive fragments of XPath 2.0[END_REF], path intersection and complementation (introduced in XPath 2.0) can be α :: expressed using for loops: π intersect π ′ is defined by

* ν P def = α A π ν N def = {p ∈ N | ∃p ′ ∈ π ν P (p)} /π ν P def = N × π ν P (ε) a ν N def = P a π /π ′ ν P def = π ν P π ′ ν P false() ν N def = ∅ π [φ] ν P def = π ν P ∩ (N × φ ν N ) not(φ) ν N def = N \ φ ν N π union π ′ ν P def = π ν P ∪ π ′ ν P φ or φ ′ ν N def = φ ν N ∪ φ ′ ν N f (π 1 , . . . , π n ) ν P def = {(p, f F ( π 1 ν P (p), . . . , π n ν P (p)) | p ∈ N } π is π ′ ν N def = {p ∈ N | ∃p ′ . {p ′ } = π ν P (p) = π ′ ν P (p)} $x ν P def = N × ν ($x) π △ + d ν N def = {p ∈ N | ∃p ′ ∈ π ν P (p) . δ (p ′ ) △ + ∼ d} let $x := π return π ′ ν P def = {(p, π ′ ν [$x → π ν P (p )] P (p)) | p ∈ N } π △ π ′ ν N def = {p ∈ N | ∃p ′ , p ′′ . p ′ ∈ π ν P (p) for $x in π return π ′ ν P def = {(p, p ′′ ) ∈ π ′ ν [$x →{p ′ }] P | p ′ ∈ π ν P (p)} ∧ p ′′ ∈ π ′ ν P (p) ∧ δ (p ′ ) △ ∼ δ (p ′′ )}
for $x in π return for $y in π ′ return $x[$x is $y] (1)
and

π except π ′ by for $x in π return .[not(π ′ [. is $x])]/$x (2)
Similarly, node quantification some $x in π satisfies φ can be expressed using

for $x in π return .[φ] (3)
and every $x in π satisfies φ is defined dually. By first defining the non-standard future(φ) def =(following:: * union descendant:: * )[φ] and singleton(π ) def = π and not(π intersect π /future(true())), then we can also express standard node comparisons π ≪ π ′ with singleton(π ) and singleton(π ′ ) and π ′ intersect (π /future(true())) [START_REF] Arroyuelo | Fast in-memory XPath search using compressed indexes[END_REF] In XPath, a path expression can be forced to end on the last possible node for the document order. This often appears as a predicate π [last()] or π [position() = last()] that calls the nullary last() function [START_REF] Kay | XPath and XQuery Functions and Operators 3.0. W3C Recommendation[END_REF]. However, this syntax cannot be handled with our simplified semantics-and is a bit problematic-, thus we shall only consider the one-argument version of last() [START_REF] Kay | XPath and XQuery Functions and Operators 3.0. W3C Recommendation[END_REF], with semantics last F (S ) def = max ≪ (S ) for any S ⊆ N . Then last(π ) can be expressed in XPath 2.0 by π except (π /ancestor:: * union preceding:: * )

Example 3.3. In the data tree of Fig. 3, when evaluated at the c node, the path expression last(ancestor-or-self:: * /child::lang) returns the lang node with data value 'fr. '

We will discuss the last() function further in Sec. 5.2.5.

XML Semantics

The XPath data model [START_REF]XQuery and XPath Data Model 3.0. W3C Recommendation[END_REF] specifies that nodes can fall into several categories, with multiple types and accessors. In data trees, there are only nodes, and two accessors ℓ and δ . Nevertheless, a large part of the XPath data model can be handled.

3.6.1 Data Tree of an XML Document. Elements, attributes, text nodes, and comments can all be encoded using distinguished labels: we let Σ = E ⊎ A ⊎ {text, comment} where E is the set of element labels and A of attribute labels.

We see all the values as belonging to D. The data in D associated with attribute nodes, text nodes, and comment nodes is their string value; for an element node, it is the concatenation of the string values of all its element and text children. The following XML document corresponds to the data tree of Fig. 3: <n l a n g = " en " ><o i d = " 23 " > John Doe< / o>< t r e f = " 23 " l a n g = " f r " > John < c >Doe< / c >< / t >< / n> 3.6.2 XML-Specific Syntax. When considering XML documents rather than data trees as models, some additional features of XPath become meaningful. We enrich the syntax with the axis

φ ::= • • • | τ π ::= • • • | α::node()
meant to select exactly the appropriate node category, and new syntactic sugar: α::τ def = α::node()[τ ] and @a def = attribute:: * [a] for a ∈ A.

Interpretation into Data

Trees. Given an XPath node expression φ with the XML semantics of [START_REF]XML Path Language (XPath) 3.0. W3C Recommendation[END_REF], we interpret it as an XPath node expression ⌜φ⌝ and not(//.[notxml]) that uses the data tree semantics of Sec. 3.3.

The first conjunct ⌜φ⌝ is defined by induction on φ; the case of node tests τ is straightforward:

⌜attribute()⌝ def = or a ∈A a ⌜comment()⌝ def = comment ⌜element()⌝ def = or e ∈E e ⌜text()⌝ def = text
The semantics of atomic steps is modified to only visit element nodes, except when using the attribute axis or the node() test, and to forbid horizontal axes in attribute nodes: ⌜α::node()⌝ def = α:: * , while ⌜α:: * ⌝ is defined as child:: * [or a ∈A a] if α = attribute, as α:: * [or e ∈E e] if α = parent or α = ancestor, and for all the other axes as .[not(or a ∈A a)]/α:: * [or e ∈E e]. The remaining cases of the induction are by identity homomorphism.

The second conjunct not(//.[notxml]) ensures that the data tree is indeed the encoding of an XML document, by forbidding the node expression notxml everywhere in the tree. We define it by first ensuring that attribute, comments, and text nodes are leaves:

(comment or text or or a ∈A a) and child:: *

Note that this does not enforce the XML standard of having at most one a-labelled attribute for every element. This might actually be desirable, for instance for handling set-valued attributes, like the class ones in HTML 5. But it can be otherwise remedied with a disjunction with (7):

• • • or or a ∈A (for $x in child::a return for $y in child::a return .[not($x is $y)]) (7)
In case we are working with a fragment without for and is, but with data joins, [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] ensures instead that all the a-labelled attributes share the same data

• • • or or a ∈A (child::a ne child::a) (8)
We might want to ensure that identifiers are unique. To simplify matters, let us assume that all the unique identifiers use the attribute name id ∈ A; then we add

• • • or id and (. eq future(id)) (9)
Finally, we should also ensure that data values are consistent throughout the tree. Remember that the value of an element node should be the concatenation of the values of its element and text children.

There is no way to do this without access to string-processing functions, so the XML semantics and data tree semantics do not quite coincide. Most of the literature accordingly restricts data joins π △ π ′ and data tests π △ + d to paths ending with an attribute step:

only π /@a △ π ′ /@a ′ and π /@a △ + d are allowed in their syntax. We do not enforce this restriction in our concrete syntax specifications, but the effect is limited; for instance, there are only 381 occurrences in the benchmark of a data test π △ + d where π is neither a function call nor a variable and does not end with an attribute step.

XPATH FRAGMENTS

We present here the fragments with decidable satisfiability and containment we have considered in our experiments. As there is such an abundant literature on the topic [e.g. 9, 10, 20-22, 25, 29, 34, 40, 43, 45], this is clearly an incomplete sample, but we think it is representative of the main lines of investigation.

The fragments we consider in our experiments and their inclusions are shown in Fig. 6, along with the complexity of satisfiability in each fragment. Regarding complexity, we use the DAG-size of the input expression, where isomorphic sub-expressions are shared. Note that Fig. 6 reports the complexity for the original logics, thus for EMSO 2 and non-mixing MSO constraints, the complexity of the XPath fragments we translate into the logics might be lower. Core 2.0 [START_REF] Balder Ten | The complexity of query containment in expressive fragments of XPath 2.0[END_REF] Core 1.0 [START_REF] Afanasiev | PDL for ordered trees[END_REF][START_REF] Benedikt | XPath satisfiability in the presence of DTDs[END_REF][START_REF] Neven | On the complexity of XPath containment in the presence of disjunction, DTDs, and variables[END_REF] Positive [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF] EMSO 2 [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF][START_REF] Jacquemard | FO 2 (<, +1, ∼) on data trees, data tree automata and branching vector addition systems[END_REF] Vertical [START_REF] Figueira | Future-looking logics on data words and trees[END_REF][START_REF] Figueira | Bottom-up automata on data trees and vertical XPath[END_REF] Forward [START_REF] Figueira | Alternating register automata on finite words and trees[END_REF][START_REF] Figueira | Future-looking logics on data words and trees[END_REF] Downward show that the following PositiveXPath fragment is NP-complete, even in presence of a DTD,

Decidable XPath Fragments

π ::= α:: * | π /π | π [φ] | π union π | π intersect π φ ::= π | a | false() | true() | φ or φ | φ and φ | π △ π
where a ranges over Σ and △ over {eq, ne}. This fragment has a semantics-preserving translation into the existential positive fragment of first-order logic with signature (↓, ↓ * , →, → * , (P a ) a ∈Σ , ∼, ).

4.1.2 Core XPath 1.0. A landmark fragment is the language of Gottlob and Koch [START_REF] Gottlob | Monadic queries over tree-structured data[END_REF], known in the literature as 'CoreXPath'. This language is akin to propositional dynamic logic on trees [START_REF] Afanasiev | PDL for ordered trees[END_REF], and is defined by the abstract syntax

π ::= α:: * | π /π | π [φ] | π union π φ ::= π | a | false() | not(φ) | φ or φ
where a ranges over Σ. CoreXPath has an EXP-complete satisfiability problem, also in presence of a DTD. To the best of our knowledge, this is the only fragment in this section for which an implementation of a satisfiability procedure exists [START_REF] Genevès | Efficiently deciding µ-calculus with converse over finite trees[END_REF].

4.1.3 Core XPath 2.0. The main feature of XPath 2.0 was the introduction of for loops. Having for loops further enriches XPath with variable quantification, and provides a significant jump in expressiveness (see Sec. 3.5.2). Ten Cate and Lutz [START_REF] Balder Ten | The complexity of query containment in expressive fragments of XPath 2.0[END_REF] study the extension of CoreXPath with

π ::= • • • | $x | for $x in π return π φ ::= • • • | $x is $y | . is $x
where $x and $y range over X; we call the resulting fragment Core-XPath 2.0. The syntax of node identity tests in [START_REF] Balder Ten | The complexity of query containment in expressive fragments of XPath 2.0[END_REF] is slightly more restrictive than ours, but this can be fixed by seeing π is π ′ as a shorthand for singleton(π ) and singleton(π ′ ) and for $x in π return for $y in π ′ return .[$x is $y] (10)

A deeper difference lies in the semantics of variables: ten Cate and Lutz [START_REF] Balder Ten | The complexity of query containment in expressive fragments of XPath 2.0[END_REF] assume that valuations map to single nodes. This does not make any difference regarding bound variables, since in CoreXPath 2.0 they must be bound by a for expression, but it does make one for free variables. This is not an issue, since the decision procedure for CoreXPath 2.0 can handle those. Indeed, satisfiability in CoreXPath 2.0 is decidable in time bounded by a tower of exponentials, whose height depends on the size of the expression. This is seen by reducing the problem to satisfiability in MSO(↓, →, (P a ) a ∈Σ ), using the usual standard translation of CoreXPath expressions into MSO formulae [see e.g. [START_REF] Afanasiev | PDL for ordered trees[END_REF][START_REF] Marx | Conditional XPath[END_REF]; the resulting TOWER complexity upper bound is tight [START_REF] Balder Ten | The complexity of query containment in expressive fragments of XPath 2.0[END_REF]Thm. 31]. Thus our free XPath variables translate directly into free second-order variables in MSO(↓, →, (P a ) a ∈Σ ).

Data XPath.

A well-studied XPath fragment with the ability to test data equality and disequality is DataXPath [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF]. It is obtained by adding joins to the syntax of CoreXPath as follows, where △ ranges over {eq, ne}:

φ ::= • • • | π △ π
Although the satisfiability of DataXPath is undecidable [START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF], restricting the navigational power restores decidability [START_REF] Figueira | Automata column: Satisfiability of XPath on data trees[END_REF]. The first decidable fragment we consider is VerticalXPath, shown decidable by Figueira and Segoufin [25, Thm. 2.1], which restricts the syntax of DataXPath to only allow vertical navigation:

α ::= self | child | descendant | parent | ancestor
Another decidable fragment is ForwardXPath, shown decidable by Figueira [START_REF] Figueira | Alternating register automata on finite words and trees[END_REF]Thm. 6.4], where navigation is restricted to forward axes only:

α ::= self | child | descendant | following-sibling
We also consider DownwardXPath [21, Thm. 6.4], the intersection of VerticalXPath and ForwardXPath, where only downward navigation is allowed:

α ::= self | child | descendant
As seen in Fig. 6, the complexity of the satisfiability problem in these three fragments varies considerably: DownwardXPath is EXPcomplete, but VerticalXPath and ForwardXPath are ACKERMANNhard [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. It is also notable that satisfiability of DownwardXPath also becomes ACKERMANN-hard in presence of DTDs [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. 4.1.5 Existential MSO 2 . Bojańczyk, Muscholl, Schwentick, and Segoufin [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF] investigate the satisfiability of formulae of the form ∃X 1 • • • ∃X n . ψ , where X 1 , . . . , X n are monadic second-order variables and ψ is a first-order formula in the two-variable fragment

• over the signature (↓, →, (P a ) a ∈Σ , ∼), which they denote by EMSO 2 (∼, +1), or • over the signature (↓, ↓ + →, → + , (P a ) a ∈Σ , ∼), which they denote by EMSO 2 (∼, <, +1).

In the first instance, they prove the decidability of satisfiability in 3-NEXP [12, Thm. 3.1], while the best known lower bound is NEXPhardness, which holds already for FO 2 (↓, (P a ) a ∈Σ ) [7, Thm. 5.1].

In the second instance, decidability is open, and equivalent to the reachability problem in an extension of branching vector addition systems [START_REF] Jacquemard | FO 2 (<, +1, ∼) on data trees, data tree automata and branching vector addition systems[END_REF], with a TOWER lower bound [START_REF] Lazić | Non-elementary complexities for branching VASS, MELL, and extensions[END_REF]. These results can be exploited for a fragment EMSO 2 XPath of DataXPath: Bojańczyk et al. [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF]Thm. 6.1] allow the following restricted joins in CoreXPath

π ::= • • • | π △ /π | . △ α:: * [φ]
where △ ranges over {eq, ne}. When the above π , π ′ , and α are restricted to using the axes self, child, and parent, this can be translated into EMSO 2 (∼, +1), and the general form into EMSO 2 (∼, <, +1). 3In spite of the unknown decidability status of EMSO 2 (∼, <, +1), we have run our benchmarks against the full logic.

4.1.6 Non-Mixing MSO Constraints. Czerwinski, David, Murlak, and Parys [START_REF] Czerwinski | Reasoning about integrity constraints for tree-structured data[END_REF] define MSO constraints as formulae of the form ψ ( x ) =⇒ η ∼ ( x ) ∧ η ( x ), where ψ is an MSO(↓, →, (P a ) a ∈Σ ) formula with the first-order variables x as its free variables, and η ∼ and η are positive Boolean combinations of atoms, over the respective signatures (∼, (P d ) d ∈D ) and ( , (¬P d ) d ∈D ). Hence data tests and data joins are permitted, as long as they are not mixed. Satisfiability is called consistency in this context, and is decidable [START_REF] Czerwinski | Reasoning about integrity constraints for tree-structured data[END_REF]Thm. 4]; better complexities are achievable when restricting ψ to conjunctive queries.

To quote Czerwinski et al. [START_REF] Czerwinski | Reasoning about integrity constraints for tree-structured data[END_REF], their 'results imply decidability. . . of the containment problem in the presence of a schema for unions of XPath queries without negation, where each query uses either equality or inequality, but never both. ' Here is indeed a Non-MixingXPath fragment of XPath, which can be translated to MSO constraints:

φ c ::= φ eq | φ ne | φ c or φ c
where △-expressions, for △ in {eq, ne}, are defined by

π △ ::= α:: * | π △ /π △ | π △ [φ △ ] | π △ union π △ φ △ ::= true() | false() | π △ | φ | φ △ or φ △ | φ △ and φ △ | π △ △ π △ | π △ △ d
where φ is any CoreXPath 2.0 node expression (see App. C for the translation into MSO constraints).

Baseline Benchmark Results

We have implemented the fragments of this section as Relax NG schemas. In each case we included obvious extensions, such as the syntactic sugars discussed in Sec. 3.5 (in particular, the last() function is included in CoreXPath 2.0 and NonMixingXPath).

The results of these fragments on the benchmark are presented in grey in figures 7 and 8 (p. 10). The fragments allowing free variables, namely CoreXPath 2.0, EMSO 2 XPath, and NonMixingXPath, have the best baseline coverage. We see here the practical interest of a fragment like NonMixingXPath with restricted negation but some support for variables, data tests π △d, and data joins π △π . The other fragments have an essentially negligible coverage in the XQuery benchmarks (Fig. 8). The support for unrestricted joins π △ π ′ in the fragments of Sec. 4.1.4 has a very limited effect, and indeed we only found 65 relevant instances in the entire benchmark, i.e. where neither π nor π ′ is a variable or a function call.

Of course, the fragments defined in the literature were not meant to be run against concrete XPath queries; we will see in the next section that several extensions can be made to these fragments.

EXTENSIONS

In this section, we introduce several extensions of the fragments from Sec. 4, while preserving the decidability and complexity of

Handling an Extension in a Fragment

A first way to prove that an extension can be handled is, when given a node expression φ in the extended syntax, to compute an equivalent node expression φ ′ in the original fragment, i.e. such that for all data trees and valuations ν , φ ν N = φ ′ ν N -and similarly for path expressions. In such a case, we say that the extension can be expressed in the fragment, and polynomially so if φ ′ can be computed in polynomial time.

A second way is instead, when given a node expression φ in the extended syntax, to compute an equisatisfiable node expression φ ′ in the original fragment, i.e. such that there exists t with t |= φ if and only if there exists t ′ with t ′ |= φ ′ . In such a case, we say that the extension can be encoded in the fragment, and that it can be polynomially encoded if φ ′ can be computed in polynomial time.

Clearly, an extension that can be (polynomially) expressed can also be (polynomially) encoded, but the converse might not hold.

Last of all, the proof techniques employed to show the decidability of satisfiability in a fragment might allow to handle the extension at hand.

Extensions

5.2.1 /π : Root Navigation. In XPath, navigation to the root is possible through the /π construct as well as using the nullary root() function [START_REF] Kay | XPath and XQuery Functions and Operators 3.0. W3C Recommendation[END_REF], with semantics root F def = {ε}. We naturally allow these features in CoreXPath 1.0 and 2.0 as well as in the NonMixingXPath and EMSO 2 XPath fragments, where navigation to the root is captured by

ancestor-or-self:: * [not(parent:: * )] (11)
The same goes for VerticalXPath but not for the two other Data-XPath fragments, where one cannot navigate upwards. It is clear that root navigation is not expressible in these fragments. In fact, it cannot even be encoded in ForwardXPath, since it becomes undecidable when extended with navigation to the root, as can be seen by adapting the proofs from [START_REF] Figueira | Future-looking logics on data words and trees[END_REF] (see App. D). We leave open the question whether there is a (polynomial) encoding of root navigation in DownwardXPath.

Finally, regarding PositiveXPath, Hidders's original fragment [START_REF] Hidders | Satisfiability of XPath expressions[END_REF] allowed root navigation, and his proof of a small model property (showing the satisfiability problem to be in NP) applies mutatis mutandis to the fragment with data joins defined in Sec. 4.1.1.

$x:

Free Variables. The XPath specification mentions that all variables are essentially second-order. More precisely, a variable is interpreted as an ordered collection of items which may be nodes or data values. In practice, queries extracted from XQuery or XSLT applications contain variables that are bound by the host language. They may be bound to nodes, node collections, or data values. It is out of the scope of the present work to recover such information to consider a more specific satisfiability problem. Rather, we interpret all variables as unordered collections of nodes, as can be seen in our semantics.

In most of our fragments, free variables are admissible. Indeed, any formula φ over Σ and D with a (necessarily finite) set of free variables X ⊆ X can be translated into an equisatisfiable formula φ X over Σ × 2 X and D with no free variables. Let us write a S for (a, S ) ∈ Σ × 2 X . The key translation steps are:

($x) X def = //. or a ∈Σ, $x∈S ⊆2 X a S (a) X def = or a ∈Σ, S ⊆2 X a S (12)
Assuming without loss of generality that the variables bound by constructs such as for or let do not belong to X , they are not affected by this translation.

Proposition 5.2. Free variables can be encoded in PositiveXPath, CoreXPath 1.0, CoreXPath 2.0, VerticalXPath, NonMixingXPath, and EMSO 2 XPath.

Note that although the encoding is exponential, the extension does not actually impact the complexity of satisfiability: in Positive-XPath and CoreXPath 1.0, a polynomial encoding can be obtained, leveraging a variant of the semantics where multiple propositions may hold at a node. In VerticalXPath, satisfiability is ACKERMANNhard, so an exponential blow-up will not have an effect on the worst-case complexity. The decision procedures for the fragments CoreXPath 2.0, NonMixingXPath, and EMSO 2 XPath are based on second-order logic, hence they actually allow XPath variables in their baseline version.

We finally observe that this translation is not available in Down-wardXPath and ForwardXPath, because they cannot express the root path of [START_REF] Bojańczyk | Two-variable logic on data trees and XML reasoning[END_REF]. In fact, free variables cannot be encoded in ForwardXPath; this is similar to Prop. 5.1 (see App. D). Proposition 5.3. Satisfiability in ForwardXPath extended with one free variable is undecidable. 5.2.3 π △ + d: Data Tests against Constants. We now consider the extension with direct comparisons against constants from D, assuming that < is a dense total order: 4φ

::= • • • | π △ + d
where △ + ∈ {eq, ne, le, lt, ge, gt} and d ∈ D. We show in App. E that any formula over Σ and D featuring comparisons against constants in a finite subset D ⊆ D can be transformed into an equisatisfiable formula over an extended labelling set Σ × C D . This is similar to the treatment of free variables in Sec. 5.2.2, but requires to include data consistency constraints in the encoded formula when the fragment at hand supports data joins. Crucially, these consistency constraints are mixing, and thus not available in NonMixingXPath. Regarding PositiveXPath, the small model property [START_REF] Hidders | Satisfiability of XPath expressions[END_REF]Lem. 1] still holds in the presence of data tests, hence satisfiability remains in NP for this extension.

Going slightly further, we allow comparisons against constant data expressions in our fragments, where constant expressions are built from constant values and the deterministic context-insensitive functions of the XPath specification [START_REF] Kay | XPath and XQuery Functions and Operators 3.0. W3C Recommendation[END_REF]; e.g., @n eq 3 + 1 is allowed. 5.2.4 π △ π : Positive Data Joins. We observe that most of our fragments can be extended to allow restricted occurrences of data joins. Intuitively, we allow data joins in positions that guarantee that the join will be evaluated only once during satisfaction checking, which allows us to replace it by two tests against a specially chosen data constant. Hence, we extend any fragment with

π + ::= π | /π + | π + /π + | π + [φ + ] | π + union π + | π + intersect π + | π + except π | some $x in π + satisfies φ + φ + ::= φ | π + | φ + or φ + | φ + and φ + | π + is π + | π + △ π + | π + △ d
Productions for constructs such as navigation to the root, intersection, node comparison, etc. should only be considered in fragments where they are allowed. We justify this extension in App. F for all relevant fragments: NonMixingXPath does not support the mixing data tests required in our encoding, and PositiveXPath already supports positive data joins in its baseline version. or π [last()] that only keeps the last node in the document order among all those selected by π . We can also check whether a node is the ith one for some i > 0 with π [i], or not the last one with π [position() != last()] or not the ith one with π [position()

!= i].
As seen in Tab. 2, these constructions are quite frequent in the benchmark. Here we discuss the case of last() and its negation, but the other positional predicates can be handled in a similar fashion.

As explained in Sec. 3.5.2, this kind of predicates is not supported in our simplified semantics, thus we rather focus on the one-argument functions last(π ) and notlast (π )-the latter is not a standard function-, with semantics last F (S ) def = max ≪ S and notlast F (S ) def = S \ {max ≪ S } for any S ⊆ N . Recall from Sec. 3.5.2 that last() can be expressed natively in CoreXPath 2.0 and thus in NonMixingXPath. The question here is to which extent it can be handled in the other fragments. Our first result is that in some cases, the last() and notlast () functions cannot be expressed. This result, proved in App. G.1 using bisimulation techniques, shows that last() cannot be expressed in VerticalXPath nor in DownwardXPath, even for simple one-step paths. Furthermore, we can show that it cannot be polynomially encoded in Downward-XPath by adapting the hardness proofs of [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]; see App. D. However, we can still look for some uses of last() that can be reasonably allowed. In particular, the path expressions from the statement of Prop. 5.7 can be handled in ForwardXPath-or at least in its regular extension [START_REF] Balder Ten | The expressivity of XPath with transitive closure[END_REF] with new axes and the Kleene plus and Kleene star operators on paths

α ::= • • • | previous-sibling | next-sibling π ::= • • • | π + | π *
with semantics previous-sibling

A def = → -1 , next-sibling A def = →, π + ν P def = ( π ν P ) + , and π * ν P def = ( π ν P ) * .
As far as satisfiability is concerned, this extension comes 'for free' in CoreXPath 1.0 [START_REF] Afanasiev | PDL for ordered trees[END_REF][START_REF] Marx | Conditional XPath[END_REF], in ForwardXPath [20, Thm.6.4] (where next-sibling is allowed but previous-sibling is not), and in VerticalXPath [25, Thm. 2.1] and DownwardXPath [21, Thm. 6.4] (without the new axes): the complexity of satisfiability does not increase. We show in App. G.2 that we can handle using this regular extension last(π ) and notlast (π ) on any one-step path argument of the form π = α:: * [φ].

id():

Jumps. Another interesting XPath feature in the XML document model is the id/idref mechanism [START_REF] Benedikt | XPath leashed[END_REF][START_REF] Marx | XPath and modal logics of finite DAG's[END_REF]. The function id() takes a path as argument, and returns the nodes of the document (if any) that have an @id attribute matching a datum found at the end of the path given as argument:

id F (S ) def = {p | ∃p ′ ∈ S . δ (p ′ ) = δ ( @id ν P (p))}
The function idref() is its inverse. For instance, in Fig. 3, evaluating id(@ref) at the t node returns the o node.

Adding the id() function makes most of the fragments undecidable, as soon as we can also use (full) data joins or node tests π is π ′ . The proof in App. H reduces from Post's correspondence problem.

Proposition 5.8. Satisfiability is undecidable in both Downward-XPath and CoreXPath 2.0 extended with id().

We nevertheless show in App. H that limited support for the id() function can be provided in VerticalXPath and EMSO 2 XPath.

Extended Benchmark Results

We have implemented the extensions of this section as Relax NG schemas. The results on the benchmark are presented in violet in figures 7 and 8. Generally, the differences observed before still hold but are significantly lessened. Strikingly, the extensions even bring CoreXPath 1.0 above NonMixingXPath: the latter only supports non-mixing data tests. It also differentiates VerticalXPath from the two other DataXPath fragments, due to its support for root paths, which in turn allows to support free variables.

Looking at the influence of each extension separately, Tab. 3 shows that the 'basic' extensions of sections 5.2.1 to 5.2.3 contribute most of the gains, while adding positive joins, positional predicates, or id() jumps to the basic extensions only brings small improvements. Regarding positional predicates, we found that many occurrences are of the form last($x), which is outside the scope of our treatment in Sec. 5.2.5. Regarding id(), Tab. 2 shows that there are very few occurrences of id() in the benchmark; one of these examples is shown in App. B. A quick investigation of the usage of the id attribute in the benchmark shows that developers rather interact with it through variables and data tests.

Figures 7 and8 show the coverage of the benchmark: in grey for the baseline fragments from Sec. 4 and in violet for their extensions described in Sec. 5; the yellow 'extras' are the topic of Sec. 6.2.2. The combined coverage of the extended fragments on the full benchmark is of 12,867 queries (60.86%).

Leaving DownwardXPath and ForwardXPath aside, the extended versions of the remaining six fragments have a somewhat similar coverage: for XSLT queries, between 69.16% for PositiveXPath and 75.03% for CoreXPath 2.0, and for XQuery ones, between 26.35% for NonMixingXPath and 28.08% for CoreXPath 2.0. We look more closely at the differences between the fragments in Sec. 6.1.

Obviously, the coverage of XPath queries extracted from XQuery files is quite poor compared to that of XSLT files. Among the other factors, we see that the size of the query is (negatively) correlated (Tab. 4). Another correlation is the presence of at least one axis step, where the combined coverage is of 74.50%, but only 48.79% for queries without any axis step. The main factor we identify is however the presence of non-standard or unsupported function calls in the query, which we discuss in Sec. 6.2.

Comparisons Between Fragments

In the case of the extended fragments of Sec. 5, the inclusions of Fig. 6 are slightly changed: CoreXPath 2.0 now contains NonMixing-XPath and PositiveXPath is included into CoreXPath 2.0 but disjoint from NonMixingXPath.

These theoretical inclusions are reflected in the difference matrix 5 shown in Tab. 5 and the accompanying chord graph of Fig. 9 in the appendix. There are three maximal incomparable fragments, namely CoreXPath 2.0, VerticalXPath, and EMSO 2 XPath. Moreover, the coverage of the extended CoreXPath 2.0 is almost as large as the combined coverage: only 30 queries from VerticalXPath are not captured by CoreXPath 2.0, and they all contain data joins under a negation; only 12 queries from EMSO 2 XPath are not captured, which include 11 queries with id() plus one of the previous 30.

From a more practical perspective, we think that the extended versions of PositiveXPath and CoreXPath 1.0 are the most promising ones: satisfiability has a more manageable complexity (NPcomplete and EXP-complete, resp.), and the coverage is not too far behind CoreXPath 2.0 (with 942 and 57 fewer queries, resp.). Note that PositiveXPath is nearly included into CoreXPath 1.0, with only four queries (featuring intersections) not captured by CoreXPath 1.0.

Supporting Functions

Due to the large number of calls to non-standard functions in the benchmark, the coverage of 'XPath 3.0 std' (cf. Tab. 1) is an upper bound on the achievable coverage. With respect to the number of queries captured by 'XPath 3.0 std', the combined coverage is 78.33%, and the precise coverage varies between 75.71% for PositiveXPath and 82.14% for CoreXPath 2.0 in XSLT sources and between 56.30% for NonMixingXPath and 60.00% for CoreXPath 2.0 in XQuery sources: the latter sources are more complex even when leaving aside their higher reliance on non-standard functions.

A remaining issue is the support of standard functions. For instance, the four functions that occur the most frequently in the benchmark are in decreasing order count(), concat(), local-name(), and contains(), and they are all standard; local-name() is supported in our fragments, but the remaining three are not. 6.2.1 Aggregation. CoreXPath 1.0 extended with node expressions count(π ) △ + i for an integer i can be translated into the twovariable fragment of first-order logic with counting on trees, which has an EXPSPACE decision procedure [START_REF] Bednarczyk | Extending two-variable logic on trees[END_REF]. There are 314 occurrences of such expressions out of the 624 occurrences of count() in the benchmark, but unfortunately not a single query is gained by adding this feature to the extended CoreXPath 1.0 fragment. Capturing more occurrences of count() requires arithmetic operations, and leads to an undecidable fragment akin to AggXPath [10].

String Processing and Arithmetic. A promising direction

for supporting more functions is the move to SMT solvers-even though it might also mean moving to semi-deciding satisfiability. Linear arithmetic is supported by all solvers, while theories comprising string concatenation, string length, and substring operations are also supported [e.g. [START_REF] Parosh | Norn: An SMT solver for string constraints[END_REF][START_REF] Kiezun | HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars[END_REF][START_REF] Liang | An efficient SMT solver for string constraints[END_REF][START_REF] Trinh | S3: A symbolic string solver for vulnerability detection in Web applications[END_REF][START_REF] Zheng | Z3-str: A Z3-based string solver for web application analysis[END_REF]. SMT solvers have already been used in [START_REF] Benedikt | Destabilizers and independence of XML updates[END_REF] to check XQuery inputs, using the classical interval encoding of trees, and the approach could be enriched to cover basic arithmetic and string support. Furthermore, a custom finite tree theory may be added to SMT solvers for more efficiency [e.g. 11, 14].

These considerations lead us to adding support in the extended PositiveXPath for linear arithmetic, the standard functions concat(), contains(), string-length(), and similar ones such as ends-with(). We view this fragment as a good candidate for practical satisfiability checking. At 62.75%, the coverage of this fragment, shown in yellow in figures 7 and 8, bests the combined coverage of our other fragments. This translates in particular to 84.77% of the subset of XSLT queries captured by 'XPath 3.0 std'. This new fragment is incomparable with the others, with a new combined coverage of 67.40% (83.55% for XSLT sources). If we restrict our attention to the 14,732 queries (69.68%) that only use not() and the functions supported in this new fragment, the new combined coverage reaches 96.69% (98.10% for XSLT sources). Thus our fragments cover nearly all the queries that do not use unsupported or non-standard functions, from which we conclude that the support for more standard functions is the most promising research avenue if one wishes to improve upon the extended fragments described in Sec. 5.

CONCLUDING REMARKS

We have designed a benchmarking infrastructure for testing the practical relevance of XPath fragments, based on the XQueryX format and Relax NG schemas. We have used this benchmark of over 20,000 queries, extracted from the XSLT and XQuery files of open-source projects, to evaluate the syntactic coverage of stateof-the-art XPath fragments for which decidability is known (or still open in the case of EMSO 2 XPath). Concerning the benchmark itself, it would of course be interesting to incorporate new sources, to confirm our observations on a larger scale.

Our analysis shows that, in a hypothetical satisfiability checker for XPath, the differences between the fragments defined in the theoretical literature are not as important as the differences introduced by the front-end translating real XPath inputs to the restricted syntax on which the decision procedure operates. Among the features that such a front-end should support, the most impactful ones would be free variables, data tests against constants (and constant expressions), positive joins, and positional predicates.

According to our benchmark results, such a front-end combined with the decidable fragments from the literature would cover about 70%-75% of the XPath queries found in XSLT files. However, due to the high reliance on user-defined or ill-supported functions, this drops to less than 30% for XPath queries from XQuery files: fullblown program analysis techniques seem necessary for XQuery. As the the support of XPath functions is a key factor, a promising approach would be to harness the power of modern SMT solvers to handle string-manipulating functions and linear arithmetic, which might cover 77.44% of the XPath queries from the XSLT section of the benchmark.

A ADDITIONAL FIGURES

We have implemented an experimental interactive web interface rendering this information in a graphical way and allowing to explore the different benchmarks; see http://www.lsv.fr/~schmitz/xpparser. It mainly features a chord graph rendering of difference matrices, like the one shown in Fig. 9. A chord between fragments i and j has thickness proportional to entry (i, j) on its i end, and to entry (j, i) on its j end; the color is the one of the 'winning' value. Chords with both ends thick, like the one between NonMixingXPath and VerticalXPath, denote fragments with significantly different coverage. This syntax tree in XQueryX format can be validated against XML Schemas or Relax NG syntactic specifications in order to check whether it fits in some XPath fragments.

Positi ve

C o r e 1 .0 C o r e 2 . 0 Verti ca l E M S O 2 N o n M i x i n g

C NON-MIXING MSO CONSTRAINTS

In this section, we show how to translate a formula from our NonMixingXPath fragment presented in Sec. 4.1.6 to a formula of the fragment of Czerwinski et al. [START_REF] Czerwinski | Reasoning about integrity constraints for tree-structured data[END_REF], that is a formula of the form i (∃ xi .

α i ( xi ) ∧ η i △ ( xi ))
, where the α i are MSO formulae and η i △ positive Boolean combinations of △ tests. The general idea of this translation is to first describe the tree structure of a tree satisfying the query (by using enough variables), which will provide formulae α i , and then state all the data constraints that should hold between these variables, which will yield the formulae η i △ . The translation extends the standard translation for CoreXPath 2.0 with a top-level translation for △-expressions:

ST x,y (α:: * ) def = x α A y
where the semantics of all the axes, as defined in Fig. 4, are indeed definable in the logic MSO(↓, →, (P a ) a ∈Σ , (P d ) d ∈D );

ST x,y (π /π ′ ) def = ∃z . ST x,z (π ) ∧ ST z,y (π ′ ) (z fresh) ST x,y (π [φ]) def = ST x,y (π ) ∧ ST y (φ) ST x,y (π union π ′ ) def = ST x,y (π ) ∨ ST x,y (π ′ ) ST x (true()) def = ⊤ ST x (false()) def = ⊥ ST x (π ) def = ∃y . ST x,y (π ) (y fresh) ST x (φ or φ) def = ST x (φ) ∨ ST x (φ ′ ) ST x (φ and φ ′ ) def = ST x (φ) ∧ ST x (φ) ST x (not(φ)) def = ¬ST x (φ) ST x (π △ △ π ′ △ ) def = ∃y∃z . ST x,y (π △ ) ∧ ST x,z (π ′ △ ) ∧ y △ z (y, z fresh)
Since this last case must occur positively, we will always be able to extract the atoms of the form y △ z and regroup them in a formula η △ .

D LOWER BOUNDS IN FORWARD/DOWNWARD XPATH

The following statements are simple consequences of the proofs of Figueira and Segoufin [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. We first prove the undecidability of the following extensions of ForwardXPath.

Proposition 5.1. Satisfiability in ForwardXPath extended with root navigation is undecidable.

Proof. This is similar to the proof of Cor. 4 in Figueira and Segoufin [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]. Their Thm. 2 shows the ACKERMANN-hardness of the satisfiability of simple 1-register freeze LTL over data words, with strict future temporal modalities (denoted by sLTL ↓ 1 (F s )). As explained in their Prop. 1, any formula from this fragment of freeze LTL can be translated into an equivalent XPath formula. In ForwardXPath, we can force the data trees to consist of a single branch, i.e. to be data words.

As seen in the proof of their Thm. 3, the only reason ForwardXPath is 'only' ACKERMANN-hard instead of undecidable is that, in their construction in Thm. 2 of formulae simulating runs of Minsky counter machines, one cannot check in ForwardXPath that every decrement was preceded by a matching increment higher in that tree. But we can check that no matching increment occurs down that point with not //. dec(i) and (. eq .//.[@]) [START_REF] Bojańczyk | XPath evaluation in linear time[END_REF] and thus the following ensures that any decrement has a matching increment closer to the root not //. dec(i) and not(. eq //.

[@])

where dec(i) and @ are labels in Σ introduced in their construction. □ Proposition 5.3. Satisfiability in ForwardXPath extended with one free variable is undecidable.

Proof. We reduce the satisfiability of ForwardXPath + root() over data trees with a single branch to the satisfiability of ForwardXPath with a single variable, which is therefore undecidable by Prop. 5.1.

Let $r be the free variable, and let r be a fresh label not found in Σ. We first ensure that all the nodes in the valuation of $r have r as label, with the constraint not($r[not(r )]).

Since we work with data trees consisting a single branch, there is a lowest node in ν ($r): this is the node selected uniquely by the path expression $r[not(.//r )]. We use it as our root and perform the entire construction of [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]Thm. 3] and Prop. 5.1 below that node; [START_REF] Cheney | Satisfiability algorithms for conjunctive queries over trees[END_REF] becomes not $r[not(.//r )]//. dec(i) and not(. eq //.[@]) . □

The following shows that DownwardXPath becomes non primitive-recursive when last() and notlast () are added. Proof. We adapt the proof of Figueira and Segoufin [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]Cor. 1]. Our aim is to build our formula so as to ensure that the entire simulation of the incrementing counter machine is performed along a single branch of the tree-this will be the rightmost branch. We pick a fresh label last (which is also used in [START_REF] Figueira | Future-looking logics on data words and trees[END_REF]Thm. 2]) and first require last(descendant-or-self:: * )[last] [START_REF] Czerwinski | Reasoning about integrity constraints for tree-structured data[END_REF] so that the last leaf of the (sub)tree below the point of evaluation, in the document order, is labelled by last. We then make sure that no other node in the (sub)tree is not labelled by last not(notlast (descendant-or-self::

* )[last]) (16)
We then apply the construction of [24, Prop. 1], but whenever a step descendant:: * would be used, we replace it by descendant:: * [descendant-or-self::last] to ensure that we only move along the rightmost branch. □

E DATA TESTS AGAINST CONSTANTS

We sketch here the encoding of data tests in XPath. Consider expressions of any of the considered fragments, extended with data tests against constants taken in a finite subset D ⊆ D. We assume that (D, <) is dense and unbounded 6 . For convenience, we assume wlog. that D = {d 1 , . . . , d n } with d i < d j when i < j.

We first define a translation (•) D which maps node and path expressions over Σ with data tests in D to expressions without data tests but over

Σ D def = Σ × C D with C D def = {-∞, +∞} ∪ D ∪ {(d i , d i+1 ) | 1 ≤ i < n}.
As before, compound labels (a, c) ∈ Σ D are written a c . Intuitively, the extra information will classify the value x held by a node: either x < d 1 , or d n < x, or x = d i or d i < x < d i+1 for some i. It will be convenient to define, for any

d i ∈ D, C <d i D def = {-∞} ∪ {d j | j < i} ∪ {(d j , d j+1 ) ∈ C D | j < i}.
We give below the key translation steps:

(a) D def = or d ∈C D a d (π eq d ) D def = (π ) D or a ∈Σ a d (π ne d ) D def = (π ) D or a ∈Σ or c ∈C D ,c d a c (π lt d ) D def = (π ) D or a ∈Σ or c ∈C <d D a c
6 Our argument can easily be adapted to work with the unboundedness assumption: -∞ should simply be dropped from C D when d 1 is minimal, and similarly for +∞ when d n is maximal. For target fragments without data joins, the density assumption can be dropped if we also remove

(d i , d i +1 ) from C D when [(d i , d i +1 )] = ∅.
To get rid of density in other fragments, we would need to know when there exists only finitely many values in some [c] for c ∈ C D and could express in XPath that nodes with this comparison tag should not carry more than this many distinct values. Unfortunately, the latter does not seem to be feasible.

The cases of gt, le and ge are similar. The translation is homomorphic wrt. all other constructs including data joins (π △ π ′ with △ ∈ {eq, ne}).

E.1 Equisatisfiability for Data-Consistent Trees

Define for all c ∈ C D its interpretation [c] ⊆ D in the natural way:

[-∞] def = {d ∈ D | d < d 1 }, [d] def = {d}, [(d i , d i+1 )] def = {d ∈ | d i < d < d i+1 }, etc.
Given a data tree t = (ℓ, δ ), we define t

D def = (ℓ D , δ ) with ℓ D (p) def = ℓ(p) c when δ (p) = d ∈ D and c is the unique element of C D such that d ∈ [c].
We say that trees of the form t D are data-consistent, because their data values respect their comparison tags. Proposition E.1. For all φ with data tests in D, for all t and p, t, p |= φ iff t D , p |= φ D (and similarly for path expressions).

Proof. Immediate by induction over expressions. □

E.2 Equisatisfiability

In CoreXPath 1.0 and CoreXPath 2.0, the encoded formula φ D is insensitive to data values, hence any model t ′ of φ D can be modified into a model of the form t D by changing the data values according to the compound labels. This shows that φ and φ D are equisatisfiable in these fragments.

For the fragments with data joins under consideration, i.e. VerticalXPath, DownwardXPath, and ForwardXPath, we show that φ is equisatisfiable with the following formula:

The above translation is obviously in VerticalXPath when (φ) D is in that fragment. For DownwardXPath and ForwardXPath, because they cannot visit any node above the initial evaluation point and do not allow free variables, it is safe to allow expressions of the form not(//.[not(φ)]) and φ ′ (like ( 17)), meaning that φ holds everywhere in the tree and φ ′ at the point of evaluation. Indeed, this is equivalent in these fragments to not(.//.[not(φ)]) and φ ′ . Assuming that this formula admits a model, we show that it has a model of the form t D , i.e. a model in which data values are consistent with compound labels. We use the fact that modifying the data values of a model in an injective way yields another model, because (φ) D only performs (dis)equality tests on data (through π △ π ′ constructs):

• Thanks to the extra constraints in our formula we know that, for all d ∈ D, all nodes with a tag in Σ × {d} have the same value, and that this value is not present in other nodes of the tree. Thus we can assume wlog. that we have a model t ′ such that, for any node . This relies on the fact that our encoded formula forbids the same data value to occur in nodes with distinct comparison tags. Moreover, by density of the order, we can take this mapping to be injective. Applying this data renaming, we obtain a model of (φ) D of the form t D , hence a model t of φ.

n of t ′ and d ∈ D, δ (n) = d iff ℓ(n) ∈ Σ × {d}. • Further,
It is now clear why we could not add data tests in NonMixingXPath: it is not data-insensitive as CoreXPath fragments, but does not allow the (crucially mixed) axiomatization that was needed to obtain equisatisfiability for data-sensitive fragments. Note that this impossibility is slightly mitigated by the fact that some data tests are natively available in NonMixingXPath (in the form π △ △ d).

F POSITIVE DATA JOINS

We detail further the claims of Sec. 5.2.4. We fix below an ambient fragment among CoreXPath 1.0, CoreX-Path 2.0 and EMSO 2 XPath. We consider formulas φ + of the fragment, extended with positive data joins, and where joins are decorated with distinct marks in M. We shall encode such formulas to φ formulas in the fragment without data joins but with data tests against constants, which we have shown to be admissible. To justify this extension, we design a translation which associates to any φ + expression an equisatisfiable φ expression.

It can be shown that (φ + ) α and (φ + ) β are equisatisfiable whenever α ≈ β. Since ≈ has only finitely many equivalence classes, the formula or α (φ + ) α is well-defined and equisatisfiable with φ + . □ G EXPRESSIVENESS RESULTS ON LAST() G.1 Last() is not Expressible in the Vertical Fragment Proposition 5.6. The expression last(ancestor::a) [child::b] is not expressible in VerticalXPath.

We prove that last() is not in general in VerticalXPath. To do so, we focus on proving the non expressivity of the query last(ancestor::a)[child::b]

If this query could be expressed by a formula φ in VerticalXPath, φ could be assumed not to contain any data test, since the evaluation of the query (18) on a data tree does not depend on the tree's data.

Hence, to study this problem, we can forget about the data in our models, and we will look at a small fragment of CoreXPath 1.0 containing only the vertical axes, noted XPath(↓, ↓ -1 , ↓ + , (↓ -1 ) + ) and defined by the abstract syntax

α ::= child | descendant | parent | ancestor π ::= α:: * | π /π | .[φ] φ ::= π | a | false() | not(φ) | φ or φ
To study whether last() is expressible in this fragment, we will define and use data-free bisimulations. These bisimulations can be seen as Ehrenfeucht-Fraïssé games. Let ℓ, ℓ ′ be two labelled trees N → Σ (or XML documents for which we will ignore the data), let p (resp. p ′ ) be a node from ℓ (resp. ℓ ′ ). Two players take part in the game, called Spoiler and Duplicator. The game starts with a pebble on p and a pebble on p ′ . If those two nodes are not labelled by the same letter, Spoiler wins the game. A game's step goes as follows:

(1) Spoiler moves one of the pebbles according to an axis α among child, parent, descendant, ancestor.

(2) Duplicator must move the other pebble according to the same axis, and on a node labelled by the same letter then the node chosen by Spoiler. If he cannot make such a move, Spoiler wins.

This game corresponds to the following bisimulation:

Definition G.1. Let ℓ and ℓ ′ be two labelled trees of domains N and

N ′ . Let Z ⊆ N × N ′ . Z is a bisimulation if, for all p ∈ N , p ′ ∈ N ′ if p Z p ′ , then:
Harmony p and p ′ have the same label, Zig for all p ⋆ y, there exists p ′ ⋆ y ′ such that y Z y ′ (for ⋆ ∈ {↓, ↓ -1 , ↓ + , (↓ -1 ) + }), and Zag for all p ′ ⋆ y ′ , there exists p ⋆ y such that y Z y ′ (for ⋆ ∈ {↓, ↓ -1 , ↓ + , (↓ -1 ) + }) Theorem G.2. Let ℓ and ℓ ′ be two labelled trees, and let p (resp. p ′ ) be a node from ℓ (resp. ℓ ′ ). If the nodes p and p ′ are bisimilar, then p and p ′ are logically equivalent for XPath(↓, ↓ -1 , ↓ + , (↓ -1 ) + ).

The version of the game restricted to n rounds corresponds to this definition of n-bisimulation:

Definition G.3. Let ℓ and ℓ ′ be two labelled trees. Let (Z i ) i ≤n be a sequence of relations between N and N ′ . For all j, (Z i ) i ≤j is a j-bisimulation if, for all p ∈ N , p ′ ∈ N ′ if p Z j p ′ , then Harmony p and p ′ have the same label, Zig for all p ⋆ y, there exists p ′ ⋆ y ′ such that y Z j-1 y ′ and (Z i ) i ≤j-1 is a (j -1)-bisimulation (for ⋆ ∈ {↓, ↓ -1 , ↓ + , (↓ -1 ) + }), and Zag for all p ′ ⋆ y ′ , there exists p ⋆ y such that y Z j-1 y ′ and

(Z i ) i ≤j-1 is a (j -1)-bisimulation (for ⋆ ∈ {↓, ↓ -1 , ↓ + , (↓ -1 ) + })
In order to get a result linking n-bisimulation and logical equivalence, we must first define the set of formulas using at most n navigational steps: Definition G.4. We define a function ns by induction on the formulas of XPath(↓, ↓ -1 , ↓ + , (↓ -1 ) + ): If ns(φ) = n, we say that φ has n nested steps. We note XPath(↓, ↓ -1 , ↓ + , (↓ -1 )

+ ) n def = {φ ∈ XPath(↓, ↓ -1 , ↓ + , (↓ -1 ) + ) | ns (φ) ≤ n}.
Definition G.5. Let ℓ, ℓ ′ be two labelled trees, and let p (resp. p ′ ) be a node of ℓ (resp. ℓ ′ ). We note p ≡ n p ′ if p and p ′ are logically equivalent for XPath(↓, ↓ -1 , ↓ + , (↓ -1 ) + ) n . Lemma G.6. Let n ≥ 0. Let ℓ and ℓ ′ be two labelled trees, let p (resp. p ′ ) be a node of ℓ (resp. ℓ ′ ), and let (Z i ) i ≤n be an n-bisimulation between ℓ and ℓ ′ . If p Z j p ′ for some j ≤ n, then p ≡ j p ′ .

Proof. We prove this theorem by induction on j:

• j = 0: the only formulas are label tests, and 0-bisimulation between two nodes require that the nodes have the same label. So 0-bisimilar nodes are logically equivalent for formulas of 0 nested steps. • Let us assume that p Z j p ′ and that the theorem is true for i-bisimulations with i < j. First, since p Z j p ′ implies p Z j-1 p ′ , then p ≡ j-1 p ′ by induction hypothesis. Now, let us consider a formula φ = α:: * /φ ′ with ⋆ being the relation corresponding to α. If φ is true on p, then there exists p ⋆y such that φ ′ is true at y. Then we choose p ′ ⋆ y ′ such that y Z j-1 y ′ (such a node exists because (Z i ) i ≤j is a j-bisimulation). And now, because ns (φ ′ ) = j -1, by induction hypothesis, φ ′ is true at y ′ , so φ is true at p ′ . Symmetrically, we can prove that if φ is true at p ′ , then it is also true at p. Now for the case φ = .[φ ′ ] we study φ ′ instead, and the Boolean combinations are handled easily. At the end, we have p ≡ j p ′ . □ Now, let us assume that the query (18) could be expressed by a formula φ in XPath(↓, ↓ -1 , ↓ + , (↓ -1 ) + ). Let n def = ns (φ). Let us show that there exist a tree ℓ n and two nodes p, p ′ ∈ N n such that p and p ′ are n-bisimilar, but such that p satisfies the query [START_REF] Kay | XPath and XQuery Functions and Operators 3.0. W3C Recommendation[END_REF], and p ′ does not.

The tree ℓ n and the bisimulations are represented on figures 10 and 11. We define the tree ℓ n as follows:

• We partition its set N n of nodes into the subsets

-A n def = {a i | i ∈ [-2n + 1, 2n -1]} -B n def = {b 2i+1 | i ∈ [-n, n -1]} -C i n def = {c i,k | k ∈ [-n, n]} for i ∈ [-2n + 1, 2n -2]
• The relation ↓ holds between the following nodes:

-

a 2i+1 ↓ b 2i+1 , for i ∈ [-n, n -2] -c i,k ↓ c i,k-1 pour i ∈ [-2n + 1, 2n -2] et k ∈ [-n + 1, n] (the c i,k are forming a chain of length 2n + 1) -b 2i+1 ↓ c 2i,n et c 2i,-n ↓ a 2i for i ∈ [-n + 1, n -1] (the c chains link the lones a) -a 2i+2 ↓ c 2i+1,n et c 2i+1,-n ↓ a 2i+1 for i ∈ [-n, n -2] (the c chains link the groups a -b)
We now describe the bisimulation relations (Z i ) i ≤n between the nodes of ℓ n :

• c -1,0 Z n c 0,0 (they are the starting nodes of our n rounds game)

• Duplicator must be able to simulate small moves of Spoiler locally around the starting nodes:

-∀i ∈ [1, n], c -1,i Z n-i c 0,i -∀i ∈ [1, n], c -1,-i Z n-i c 0,-i
• Duplicator can simulate bigger moves from Spoiler by doing a shift:

-∀i ∈ [0, n -2], a 2i Z n-1-i a 2i+2 -∀i ∈ [0, n -2], a 2i+1 Z n-2-i a 2i+3 -∀i ∈ [-n + 1, -1], a 2i Z n+i a 2i+2 -∀i ∈ [-n, -1], a 2i+1 Z n+i a 2i+3 -∀i ∈ [0, n -2], c 2i-1,k Z n-1-i c 2i+1,k -∀i ∈ [0, n -2], c 2i,k Z n-1-i c 2i+2,k -∀i ∈ [-n + 1, -1], c 2i-1,k Z n+i c 2i+1,k -∀i ∈ [-n + 1, -1], c 2i,k Z n+i c 2i+2,k
• Duplicator can simulate too big moves from Spoiler by using the identity relation: ∀p ∈ N n , p Z n p • Finally, every relation must contain the smaller ones:

∀(p, p ′ ) ∈ N 2 n , ∀i < j, if p Z j p ′ then p Z i p ′ .
Lemma G.7. (Z i ) i is an n-bisimulation.

Proof. Let us prove by induction on j that (Z i ) i ≤j is a j-bisimulation.

• j = 0: every nodes in relation for Z 0 do have the same labels, so Z 0 is a 0-bisimulation.

• Let us assume that (Z i ) i ≤j is a j-bisimulation for some j < n, and let us prove that (Z i ) i ≤j+1 is a (j + 1)-bisimulation. Let p and p ′ be two nodes from ℓ n such that p Z j+1 p ′ . Then:

(1) By definition of Z j+1 , p and p ′ have the same label.

(2) Let ⋆ ∈ {↓ -1 , ↓, (↓ -1 ) + , ↓ + }. We must prove that for every p ⋆ y, there exists a p ′ ⋆ y ′ such that y Z j y ′ . The cases ⋆ =↓ -1 and ⋆ =↓ are easy because we padded ℓ n with long enough c-chains. Let us focus on the case ⋆ = (↓ -1 ) + (the case ⋆ =↓ + is similar): let y ∈ N n such that p(↓ -1 ) + y. Now, if p ′ (↓ -1 ) + y then we can take y ′ = y and use the identity relation which is contained in Z j . Else, by choosing y ′ above y with the same distance between p and y than between p ′ and y ′ , we will almost always get a node y ′ such that y Z j y ′ . The only case where this won't work is if p = c -1,k , p ′ = c 0,k for some k. In that case, if y is at distance d of p, we will choose y ′ at distance d + 2n + 3 of p ′ instead. This is because the distance between bisimilar nodes around the starting points is smaller than elsewhere in the tree, so this bigger jump is required to close the gap. (3) Similarly, we can prove that for every ⋆ ∈ {↓ -1 , ↓, (↓ -1 ) + , ↓ + }, for every p ′ ⋆y ′ , there exists a p ⋆y such that y Z j y ′ . □

This contradicts the fact that φ was equivalent to the query [START_REF] Kay | XPath and XQuery Functions and Operators 3.0. W3C Recommendation[END_REF], since c -1,0 Z n c 0,0 but only c 0,0 satisfies the query [START_REF] Kay | XPath and XQuery Functions and Operators 3.0. W3C Recommendation[END_REF]. Hence, this query is not expressible in XPath(↓, ↓ -1 , ↓ + , (↓ -1 ) + ), and so it is not expressible in VerticalXPath.

G.2 Expressing Last()

a a 0 c c -1,n c c -1,n-1 . . . c c -1,2 c c -1,1 c c -1,0 c c -1,-1 c c -1,-2 . . . c c -1,-n+1 c c -1,-n a a -1 b b -1 a a 0 c c -1,0 a a -1 b b -1 c c 0,-n c c 0,-n+1 . . . c c 0,-2 c c 0,-1 c c 0,0 c c 0,1 c c 0,2 . . . c c 0,n-1 c c 0,n b b 1 a a 1 c c 0,0 a a 1 b b 1 n n -1 n -2 1 0 n -1 n -2

G.3 Expressing Position() in Regular XPath

In this section, we show how to translate predicates of the form α:: *

[φ][position() = i] in RegularXPath.
This query selects the i-th node for the document order among the nodes that would have been selected by α:: * [φ]. We represent such a predicate by a function pos i . We give a translation for pos i by on i. • Ψ 5 := not(//*[id(@id)[child:: * ] and id(@id)[not(child:: * )]]) (a node has a child iff all the nodes sharing its @id key have a child). Now, we can prove the following lemma: Lemma H.1. Let t be a data tree. Then, t satisfies all the Ψ i formulas if and only if:

(1) all the nodes of t at the same depth level are identical (same label, same @id, @succ and @sym values) and have children with the same label and the same @id key. (2) Two nodes from different depth levels do not share the same @id key.

Proof. It is easy to see that a data tree satisfying the properties (1) and (2) will satisfy the formulas Ψ i . Suppose now that a data tree t satisfies the formulas Ψ i . We prove that the properties (1) and ( 2) are satisfied by induction on the depth level:

• Level depth 0: there is only the root node at this depth level. Thanks to the formula Ψ 1 , and since the root node appears in every branch of the tree, there is no node somewhere else in the tree with the same @id key than the root so the property (2) is satisfied. And now, thanks to Ψ 2 , all its children have the same label, and thanks to Ψ 3 , all its children have the same @id key. So the property ( 1) is also satisfied. • Let's assume that the properties (1) and ( 2) are satisfied down to depth level n, and let's prove they are also satisfied at depth level n + 1. Since the nodes of depth n satisfy the property (1), then all the nodes of depth n + 1 have the same label and the same @id key (they are children from nodes of depth n).

Then, thanks to Ψ 4 , they also have the same @succ and @sym values, so they are identical. Moreover, thanks to Ψ 2 and Ψ 3 , all their children have the same label and @id value (because of the nodes of depth n + 1 have the same @id key). So the property ( 1) is satisfied at depth level n + 1. Furthermore, thanks to Ψ 1 , no node above or below a node of depth n + 1 (that is, no node from a different depth level) share the same @id key than the nodes of depth n + 1, so the property ( 2) is also satisfied. Thus, by induction on the depth level, the properties (1) and ( 2) are satisfied everywhere in the tree. □

This property allows us to only consider non-branching models, as any model will be logically equivalent to one of its branch for DownwardXPath with id.

Then, we start by giving us formulas expressing simple properties:

• φ Σ := self::a 1 union . . . union self::a n , where Σ = {a 1 , . . . a n } (checks that the label of the current node is in Σ). • Symmetrically, we define the formula φ Σ .

• φ f ir st := self::# (checks that the current node is a marker at the beginning of a group u i v i ).

• φ l ast := not(child:: * ) or child::# (checks that the current node is the last letter of a group u i v i ).

We can now express the marker property of the # symbol:

Φ 1 := not(//*[φ Σ ]/child::#) and not(//#/child:: * [φ Σ ]) and not(//#/#) Moreover, we can express that a given word appears correctly between markers, somewhere in the tree. Let u i v i = c i,0 . . . c i,m i . We define the formula φ i that checks that the current node is a marker #, followed by letters forming the word u i v i , and that this word isn't followed by extra letters:

φ i := φ f ir st and ./c i,0 /c i,1 / . . . /(c i,m i [φ l ast ])
Thus, we can express the fact that the word w corresponding to any branch of a model is in

{#u i v i | 0 ≤ i ≤ n} + : Φ 2 := /*[φ f ir st ]
and not(//*[φ f ir st and not(φ 0 ) and not . . . and not(φ n )])

Then, we must express the encoding properties about the id links:

• Φ 3 := not(//*[not(@succ) and ((φ Σ and descendant:: * [φ Σ ]) or (φ Σ and descendant[φ Σ ]))]) and not(//*[@succ and ((φ Σ and not(descendant:: * [φ Σ ])) or (φ Σ and not(descendant[φ Σ ])))]) (every letter has a successor except the last letter of the longest subwords from Σ and Σ). • Φ 4 := not(//*[not(@sym) and not(self::#)]) (every letter has a @sym attribute).

• Φ 5 := not(//*[@succ and not(@succ eq descendant:: * /@id)]) (id(@succ) is non decreasing).

• Φ 6 := not(//*[(φ Σ and id(@succ)[φ Σ ]) or (φ Σ and id(@succ)[φ Σ ])]) (id(@succ) doesn't link letters from Σ with letters from Σ). • Φ 7 := not(//*[φ Σ and @succ eq descendant:: * [φ Σ ]/descendant:: * /@id]) and not(//*[φ Σ and @succ eq descendant:: * [φ Σ ]/descendant:: * /@id]) (id(@succ) doesn't jump over a letter from the same alphabet).

x y y ′ ∃x ′ @succ @sym @sym @succ Figure 12: Φ 10 express the compatibility between id(@succ) and id(@sym): if x has a successor y, then the symmetric of x must also have a successor, which is the symmetric of y.

• Φ 8 := and a ∈Σ (not(//*[self::a and not(id(@sym)/self::a)]) and not(//*[self::a and not(id(@sym)/self::a)]))

(id(@sym) links properly a letter to its bar version). • Φ 9 := not(//*[not(id(sym)/@sym eq @id)]) (id(@sym) is an involution).

• Φ 10 := not(//*[@succ and not((id(@succ)/@sym eq id(@sym)/@succ))]) (compatibility of id(@succ)

and id(@sym), cf. Fig. 12).

It is easy to check that if the PCP problem has a solution, encoding it as described above will give us a data tree satisfying all the formulas. Conversely, let's prove that if all these formulas are satisfied by a data tree t, then we can extract a solution of our PCP problem from t.

First, thanks to lemma H.1, we can assume for the sake of simplicity that t is a non-branching tree. Then, because t satisfies Φ 1 and Φ 2 , the word w of t belongs to {#u i v i } + . Let's call w (resp. w) the longest subword of t in Σ (resp. Σ). Now, thanks to Φ 3 every letter of w and w has a @succ attribute (except their last letter), and thanks to Φ 4 every letter of w and w has a @sym attribute. Moreover, because t satisfies Φ 5 , Φ 6 and Φ 7 , we can prove that the @succ links are jumping as intended from a letter of w (resp. w) to the next one. This give us two @succ chains which correspond to w and w. We note x R succ y if there is a @succ link from x to y.

We now need to check the @sym links. These links are forming a symmetric relation (thanks to Φ 9 ) that we will denote by R sym . First, let's consider the beginning of w: let j be the position in w such that w 0 R sym w j , and let's assume that j > 0. Then, there is a node w j-1 above in t such that w j-1 R succ w j . Now, because of the compatibility property expressed by Φ 10 , there should be a node x above w 0 in the tree such that w j-1 R sym x R succ w 0 , which isn't possible by definition of w 0 . So we have w 0 R sym w 0 . Now, thanks to the same compatibility property, we can prove by induction on i that we have w i R sym w i for every i.

What could still happen is that w and w are not of the same length. This is also forbidden by Φ 10 : let w n-1 be the last letter of w, and let's assume that w is of length ≥ n (the other case is symmetric). Then we have w n-1 R sym w n-1 , and now if w n-1 had a successor w n , then by using Φ 10 we could prove that there should be a node x such that w n-1 R succ x R sym w n , which isn't possible by assumption that w n-1 was the last letter of w. So w and w are of the same length.

Finally, thanks to Φ 8 we can prove that for 0 ≤ i < n, (w i ) = w i , so t does represent a solution to our PCP problem.

H.2 Reducing from PCP using Node Tests

The encoding above can be easily adapted for a restricted version of CoreXPath 2.0 with only the downward axes, by replacing the data joins by node tests using is. Here is how one can transform the previous formulas to be in such a fragment:

(1) Since every data value is actually the @id key of a node, every data test of the form π /@foo eq π ′ can be transformed into π /id(@foo)/@id eq π ′ .

(2) Once all the data joins are of the form π /@id eq π ′ /@id, we can replace them by node tests of the form π is π ′ (since all the @id keys are unique). @succ @succ @succ @succ @succ @succ @succ @succ @succ @succ @succ @succ @succ @succ @succ @succ @sym @sym @sym @sym @sym @sym @sym @sym @sym This extension concerns VerticalXPath extended with variables, and EMSO 2 XPath.

When an occurrence of id() is applied at the end of an absolute path /Π, it is translated into a variable $x Π that will be forced to contain exactly the nodes to which the id() call would jump, using the following axioms:

• φ 1 ($x Π , Π) := not(/[(not(. eq $x/@id)) and . eq // * /@id])

• φ 1 ($x Π , Π) := not($x[not(@id eq /)])

We will eliminate the id occurrences by using a translation function T id taking two arguments: the first one is a residual path π , not containing any id() call, that will be used to axiomatise variables $x π , and the second one is the query that remains to be translated. In the following translation, whenever a formula denoted $x Π is used, the corresponding axioms φ 1 ($x Π , Π) and φ 2 ($x Π , Π) will be added at top level.

T id (π , π ′ /π id ) = T id (π /π ′ , π id ) (where π ' does not contain any id() call) T id (π , π id /π ′ id ) = T id (T id (π , π id ), π ′ id ) T id (π , id(π ′ )) = $x Π (where $x Π is fresh, and Π = π /π ′ ) T id (π , id(π id )) = T id (ε, id(T id (π , π id )))

T id (π , π ′ ) = π /π ′ (where π ' does not contain any id() call) T id (π , π id union π ′ id ) = T id (π , π id ) union T id (π , π ′ id ) T id (π , π ′ [φ]) = T id (π , π ′ )[T id (ε, φ)] T id (ε, φ and φ ′ ) = T id (ε, φ) and T id (ε, φ ′ ) T id (ε, φ or φ ′ ) = T id (ε, φ) or T id (ε, φ ′ ) T id (ε, not(φ)) = not(T id (ε, φ))

We denote by Ax all the axioms that must be added at top level:

Ax(T id (π , π )) = $x Π apprearing in T id (π, π ) (φ 1 ($x Π , Π) ∧ φ 2 ($x Π , Π))
And we note t, ϵ, n f ⊨ Ax T id (π , π ) when t, ϵ, n f ⊨ T id (π , π ) ∧ Ax(T id (π , π )) Proposition H.3. Let t be a data tree and let n f ∈ N . Let π and π be path formulas in our fragment extended with id. We have: t, ϵ, n f ⊨ Ax T id (π , π ) iff t, ϵ, n f ⊨ π / π Proof. We prove this theorem by induction on the lexicographic order over the number of occurrences of id() in π and the size of π , showing only the non trivial cases:

• case π = π id /π ′ id : t, ϵ, n f ⊨ Ax T id (π , π id /π ′ id )

⇐⇒ t, ϵ, n f ⊨ Ax T id (T id (π , π id ), π ′ id ) ⇐⇒ t, ϵ, n f ⊨ Ax T id (π , π id )/π ′ id ⇐⇒ ∃n ∈ N t, ϵ, n ⊨ Ax T id (π , π id ) and t, n, n f ⊨ π ′ id ⇐⇒ ∃n ∈ N t, ϵ, n ⊨ π /π id and t, n, n f ⊨ π ′ id ⇐⇒ t, ϵ, n f ⊨ π /π id /π ′ id • case π = id(π id ):

t, ϵ, n f ⊨ Ax T id (π , id(π id )) ⇐⇒ t, ϵ, n f ⊨ Ax T id (ε, id(T id (π , π id ))) ⇐⇒ t, ϵ, n f ⊨ Ax id(T id (π , π id )) ⇐⇒ ∃n id ∈ N , n f ↓ n id and ∃n ′ f ∈ N , δ (n id ) = δ (n ′ f ) and t, ϵ, n ′ f ⊨ Ax T id (π , π id ) ⇐⇒ ∃n id ∈ N , n f ↓ n id and ∃n ′ f ∈ N , δ (n id ) = δ (n ′ f ) and t, ϵ, n ′ f ⊨ π /π id ⇐⇒ ∃n id ∈ N , n f ↓ n id and ∃n ′ f ∈ N , δ (n id ) = δ (n ′ f ) and ∃n ∈ N , t, ϵ, n ⊨ π and t, n, n ′ f ⊨ π id ⇐⇒ ∃n ∈ N t, ϵ, n ⊨ π and t, n, n f ⊨ id(π id ) ⇐⇒ t, ϵ, n f ⊨ π /id(π id )

• case π = id(π ′ ) (with no occurrence of id() in π ′ ):

t, ϵ, n f ⊨ Ax T id (π , id(π ′ )) ⇐⇒ t, ϵ, n f ⊨ Ax $x, where $x is a fresh variable axiomatised at top level with: (1) φ 1 := not(/π /π ′ [(. eq $x/@id) and . eq // * /@id]) (2) φ 2 := not($x[not(@id eq /π /π ′ )]) The formula φ 1 ensures that /π /id(π ′ ) ν P ⊆ $x ν P , and φ 2 ensures that $x ν P ⊆ /π /id(π ′ ) ν P . Hence, the equivalence is true. □

In addition, for the EMSO 2 XPath fragment, we can use a second-order variable to remember the starting point. In the translation of a query in an EMSO 2 formula, if the initial node is denoted by a first-order variable x, we can axiomatise a second-order variable X st ar t this way:

x ∈ X st ar t ∧ ∀y, y ∈ X st ar t ⇒ y = x Then, if an id() is used in a non-rooted path, we can handle it by adapting the previous axiomatisation and testing for X st ar t instead of testing for the root:

(1) not($X start /[(not(. eq $x/@id)) and . eq // * /@id]) (2) not($x[not(@id eq $X start /)]) But we must be careful not to allow such occurrences of id() in a node expression, as the example H.4 shows. In that sense, we must provide our grammar with a new starting symbol:

π ′ ::= π | π id
Example H.4. The formula /child::a/id(@x) can be translated to $x, or equivalently /child::a/$x if we want to simulate the path it follows more accurately, where the variable $x axiomatised by:

(1) not(/child::a/@x[not(. eq $x/@id) and . eq // * /@id]) (2) not($x[not(@id eq /child::a/@x)]) However, even though the translation will selects the same nodes as the original query, the variable $x will do a global jump directly to all the results, no matter what the current node is (cf. Fig. 14). Because of this, we cannot allow the use of id in a test: a test of the form [id(@x)] will be satisfied if a jump id(@x) can be done from the current node, but a test of the form [$x] will be satisfied if the variable $x is not empty, no matter what the current node is (cf. Fig. 15). Counter example of a formula using id in a node test: the query child::a[id(@x)] would only select the leftmost child of the root, but the query child::a[$x] with $x axiomatised as above would select all the children labelled by a, since $x would be non empty.

Figure 2 :

 2 Figure 2: Distribution of query sizes.

Figure 3 :

 3 Figure 3: A data tree; labels from Σ are shown in the nodes, data from D in violet next to them.

Figure 4 :

 4 Figure 4: The semantics of XPath axes.

Figure 5 :

 5 Figure 5: The semantics of XPath path expressions and node expressions.

  α ::= • • • | attribute and five node tests τ ::= attribute() | comment() | element() | text()

4. 1 . 1

 11 Positive XPath. Some of the earliest-studied fragments of XPath are based on tree patterns[START_REF] Hidders | Satisfiability of XPath expressions[END_REF]. Geerts and Fan[START_REF] Geerts | Satisfiability of XPath queries with sibling axes[END_REF] Thm. 4]

Figure 6 :

 6 Figure 6: Inclusions and complexities of the fragments of Sec. 4.

Proposition 5 . 1 .

 51 Satisfiability in ForwardXPath extended with root navigation is undecidable.

Proposition 5 . 4 .

 54 Data tests can be polynomially encoded in Core-XPath 1.0, CoreXPath 2.0, VerticalXPath, DownwardXPath, Forward-XPath, and EMSO 2 XPath.

Proposition 5 . 5 .

 55 Positive joins are expressible in CoreXPath 1.0, CoreXPath 2.0 and EMSO 2 XPath. 5.2.5 last(): Positional Predicates. The typical use of last() in XPath is through a positional predicate π [position() = last()]

Proposition 5 . 6 .

 56 The expression last(ancestor::a) [child::b] is not expressible in VerticalXPath.

Proposition 5 . 7 .

 57 Satisfiability in DownwardXPath extended with last(descendant-or-self:: * ) and notlast (descendant-or-self:: * ) is ACKERMANN-hard.

Figure 7 :

 7 Figure 7: Coverage of the XSLT sources.

Figure 8 :

 8 Figure 8: Coverage of the XQuery sources.

Figure 9 :

 9 Figure 9: Chord graph of the difference matrix of Tab. 5; we omitted DownwardXPath and ForwardXPath.

Proposition 5 . 7 .

 57 Satisfiability in DownwardXPath extended with last(descendant-or-self:: * ) and notlast (descendant-or-self:: * ) is ACKERMANN-hard.

Proposition 5 . 4 .

 54 Data tests can be polynomially encoded in CoreXPath 1.0, CoreXPath 2.0, VerticalXPath, DownwardXPath, ForwardXPath, and EMSO 2 XPath.

  (φ) D and not or d ∈D, a,b ∈Σ //a d ne //b d and not or a,b ∈Σ or c c ′ ∈C D //a c eq //b c ′

  there exists a mapping f : D → D which maps, for any c ∈ C D , data values occurring in nodes with tag Σ × {c} to distinct data values in [c]

  ns(a) def = 0 ns(α:: * ) def = 1 (where α ∈ {parent, child, ancestor, descendant})ns(φ or φ ′ ) def = ns(φ or φ ′ ) def = max{ns(φ), ns(φ ′ )} ns(not(φ)) def = ns(φ) ns(.[φ]) def = ns(φ)ns(π /π ′ ) def = ns(π ) + ns(π )

G. 2 . 1 4 c c 2n- 4 b b 2n- 3 a a 2n- 3 c c 2n- 3 a a 2n- 2 c c 2n- 2 b b 2n- 1 aFigure 10 :

 214433322110 Figure 10: n-bisimulation inside ℓ n (a double edge represents a chain of n c nodes)

1 0Figure 11 :

 111 Figure 11: Zoom around the starting points

pos 1 (

 1 parent:: * [φ]) ≡ parent:: * [φ] pos 1 (self:: * [φ]) ≡ self:: * [φ] pos 1 (child:: * [φ]) ≡ child:: * [φ and not (preceding-sibling:: * [φ])] pos 1 (preceding-sibling:: * [φ]) ≡ preceding-sibling:: * [φ and not (preceding-sibling:: * [φ])] pos 1 (following-sibling:: * [φ]) ≡ (next-sibling:: * [not(φ)]) * /next-sibling:: * [φ] pos 1 (ancestor:: * [φ]) ≡ ancestor:: * [φ and not (ancestor:: * [φ])] pos 1 (descendant:: * [φ]) ≡ (child:: * [φ and descendant:: * [φ] and not(preceding-sibling:: * /descendant-or-self:: * [φ]) ]) * /child:: * [φ and not(preceding-sibling:: * / descendant-or-self:: * [φ])] pos 1 (following:: * [φ]) ≡ ancestor-or-self:: * [following:: * [φ] and not(parent:: * /following:: * [φ])]/ pos 1 (following-sibling:: * [descendant-or-self:: * [φ]])/ (.[φ] union .[not(φ)]/pos 1 (descendant:: * [φ])) pos 1 (preceding:: * [φ]) ≡ ancestor-or-self:: * [preceding:: * [φ] and not(parent:: * /preceding:: * [φ])]/ pos 1 (preceding-sibling:: * [descendant-or-self:: * [φ]])/ (.[φ] union .[not(φ)]/pos 1 (descendant:: * [φ]))

Example H. 2 .

 2 Let's consider the following PCP problem, where Σ = {a, b}. (u 1 , v1 ) = (a, b aa), (u 2 , v2 ) = (ab, āa), (u 3 , v3 ) = (bba, bb). The sequence (3, 2, 3, 1) is a solution, and its encoding is represented in Fig. 13.

Figure 13 :

 13 Figure 13: Example of the encoding of a PCP solution.

Figure 14 :

 14 Figure14:The paths followed by the query /child::a/id(@x) in yellow, and by the query /child::a/$x in violet. r

Figure 15 :

 15 Figure 15: Counter example of a formula using id in a node test: the query child::a[id(@x)] would only select the leftmost child of the root, but the query child::a[$x] with $x axiomatised as above would select all the children labelled by a, since $x would be non empty.

Table 1 :

 1 The benchmark's composition.

	Sources Queries			Coverage
				XPath 1.0 XPath 2.0 XPath 3.0 XPath 3.0 std
	XSLT	14,675	98.4%	100.0%	100.0%	91.3%
	XQuery	6,466	76.1%		87.4%	99.8%	46.7%
	Total		21,141	91.6%		96.1%	99.9%	77.7%
	occurrences (logscale)	1 10 100 1,000	0	100	200	300	400 0% 20% 40% 60% 80% 100%	accumulated % of occurrences
					rank
		Figure 1: Occurrences of function calls.

Table 2 :

 2 Occurrence counts of the syntactic extensions of Sec. 5 in the entire benchmark.

		Basic			Advanced
	/π	$x	π △ + d π △ π last() id()
	272 12,476 4,791	853	1,203	31
	the corresponding satisfiability problems. As seen in Tab. 2, we
	consider first 'basic' extensions with considerable impact on the
	benchmark coverage in sections 5.2.1 to 5.2.3, and then 'advanced'
	ones with smaller impact in sections 5.2.4 to 5.2.6.

Table 3 :

 3 Number of new queries captured by the extensions of Sec. 5.2 in each fragment.

			basic π △ π last() id()
		Positive	7,653
		Core 1.0	7,895	+243	+54
		Core 2.0	4,309	+266
		Downward 1,993		+12
		Vertical	7,974		+25	+0
		Forward	2,053		+26
		EMSO 2	4,760	+241	+11
		NonMixing	136
		100%
					+extras
					extended
	percentage of queries	20% 40% 60% 80%			baseline
		0%
		P o s i t i v e C o r e 1 . 0 C o r e 2 . 0 D o w n w V e r t i c a l F o r w a r M S O d E a r d	2 N o n M i x i n g

Table 4 :

 4 Combined coverage of the extended fragments by query size.

	sizes	1-4	5-8 9-12 13-16 17-20 21-24 25-28 29-32 33-36 37-40 41-44 45-48 ≥ 49
	queries	5,146 5,661 3,359 1,996 1,330	806	590	503	283	231	117	131	988
	coverage 97.9% 58.7% 42.0% 44.2% 54.8% 44.9% 53.0% 42.7% 40.9% 47.6% 35.8% 46.5% 25.7%

Table 5 :

 5 Difference matrix for the extended fragments.

		Positive Core 1.0 Core 2.0 Downward Vertical Forward EMSO 2 NonMixing
	Positive	0	4	0	6,283	300	6,159	23	331
	Core 1.0	889	0	0	6,917	469	6,765	124	681
	Core 2.0	942	57	0	6,974	526	6,822	181	689
	Downward	251	0	0	0	0	0	12	83
	Vertical	746	30	30	6,478	0	6,478	73	671
	Forward	279	0	0	152	152	0	26	85
	EMSO 2	796	12	12	6,817	400	6,679	0	639
	NonMixing	584	49	0	6,368	478	6,218	119	0

Table 6 :

 6 The benchmark's list of sources.

	Source	Queries			Coverage
			XPath 1.0 XPath 2.0 XPath 3.0 XPath 3.0 Core 2.0
						std	extended
	DocBook	7,620	100.0%	100.0%	100.0%	95.6%	79.3%
	http://docbook.sourceforge.net/
	TEIXSL	6,303	96.4%	100.0%	100.0%	86.1%	70.8%
	https://github.com/TEIC/Stylesheets
	HTMLBook	752	100.0%	100.0%	100.0%	92.0%	66.4%
	https://github.com/oreillymedia/HTMLBook
	Total (XSLT)	14,675	98.4%	100.0%	100.0%	91.3%	75.0%

The output XQueryX representations of a handful of queries do not validate against XPath

3.0, due to out-of-bounds constant numerals; this is a very marginal effect.

Bojańczyk et al. [12] actually also allow joins of the form @a △ α :: * /@b, but this is subject to a semantic condition.

These assumptions are not met in the actual XPath model where comparisons are undefined between numeric and arbitrary string values, but this problem can be avoided e.g. when the type of attributes is known from a schema.

Cell (i, j ) shows the number of queries covered by fragment i but not fragment j.

ACKNOWLEDGMENTS

Work funded by ANR-14-CE28-0005 prodaq.

B EXAMPLE PARSER OUTPUT

Here is an XQuery snippet from the file functx.xqy of HisTEI: module namespace f u n c t x = " h t t p : / / www. f u n c t x . com " ; d e c l a r e function f u n c t x : i d -from-e l e m e n t ( $ e l e m e n t as e l e m e n t ( ) ? ) as x s : s t r i n g ? { d a t a ( ( $ e l e m e n t /@ * [ i d ( . ) i s . . ] ) [START_REF] Parosh | Norn: An SMT solver for string constraints[END_REF] ) } ;

The identifies 'data (( $element/@ * [id (.) is ..]) [START_REF] Parosh | Norn: An SMT solver for string constraints[END_REF])' as an XPath query inside this program, and returns the following information (note the normalisation of some of the syntactic sugar, like '@ * ' and ' .. '), including the syntax tree in XQueryX format [START_REF] Melton | XQueryX 3.0. W3C Recommendation[END_REF] inside the <ast> element: <?xml v e r s i o n = " 1 . 0 " ? > <benchmark > < x p a t h column = " 45 " f i l e n a m e = " benchmark / exampleh i s t e i . xqy " l i n e = " 4 " > < q u e r y > d a t a ( ( $ e l e m e n t / a t t r i b u t e : : * [ ( i d ( . ) i s p a r e n t : : n o d e ( ) ) ] ) [START_REF] Parosh | Norn: An SMT solver for string constraints[END_REF] ) < / q u e r y > < a s t s i z e = " 30 " > < x q x : f u n c t i o n C a l l E x p r x m l n s : x q x = " h t t p : / /www. w3 . o r g / 2 0 0 5 / XQueryX " > < x q x : f u n c t i o n N a m e > d a t a < / x q x : f u n c t i o n N a m e > < x q x : a r g u m e n t s > < x q x : p a t h E x p r > < x q x : s t e p E x p r > < x q x : f i l t e r E x p r > < x q x : s e q u e n c e E x p r > < x q x : p a t h E x p r > < x q x : s t e p E x p r > < x q x : f i l t e r E x p r > < x q x : v a r R e f > < xqx:name > e l e m e n t < / xqx:name > < / x q x : v a r R e f > < / x q x : f i l t e r E x p r > < / x q x : s t e p E x p r > < x q x : s t e p E x p r > < x q x : x p a t h A x i s > a t t r i b u t e < / x q x : x p a t h A x i s > < x q x : W i l d c a r d / > < x q x : p r e d i c a t e s > < x q x : i s O p > < x q x : f i r s t O p e r a n d > < x q x : f u n c t i o n C a l l E x p r > < x q x : f u n c t i o n N a m e > i d < / x q x : f u n c t i o n N a m e > < x q x : a r g u m e n t s > < x q x : c o n t e x t I t e m E x p r / > < / x q x : a r g u m e n t s > < / x q x : f u n c t i o n C a l l E x p r > < / x q x : f i r s t O p e r a n d > < x q x : s e c o n d O p e r a n d > < x q x : p a t h E x p r > < x q x : s t e p E x p r > < x q x : x p a t h A x i s > p a r e n t < / x q x : x p a t h A x i s > < x q x : a n y K i n d T e s t / > < / x q x : s t e p E x p r > < / x q x : p a t h E x p r > < / x q x : s e c o n d O p e r a n d > < / x q x : i s O p > < / x q x : p r e d i c a t e s > < / x q x : s t e p E x p r > < / x q x : p a t h E x p r > < / x q x : s e q u e n c e E x p r > < / x q x : f i l t e r E x p r > < x q x : p r e d i c a t e s > < x q x : i n t e g e r C o n s t a n t E x p r > < x q x : v a l u e >1 < / x q x : v a l u e > < / x q x : i n t e g e r C o n s t a n t E x p r > < / x q x : p r e d i c a t e s > < / x q x : s t e p E x p r > < / x q x : p a t h E x p r > < / x q x : a r g u m e n t s > < / x q x : f u n c t i o n C a l l E x p r > < / a s t > < / x p a t h > < / benchmark > The translation actually works over marked φ + expressions. Given a query φ + , we can annotate each occurrence of a data join with a unique mark m from a finite set M. For example, c[@a eq @b[. ne preceding:: * /@b]] might be annotated using M = {m, n} as

Then, given a valuation α: M → D, we define the translation (φ + α as follows, showing only the key cases:

Continuing the previous example with α (m) = d and α (n) = d ′ , we have:

d eq @b[. eq d ′ and d ′ ne preceding::

Note that this formula is satisfiable iff d = d ′ . Obviously, t, p |= (φ + ) α implies t, p |= φ + for any α. Conversely, if t, p |= φ + , we show that there exists α such that t, p |= (φ + ) α . Roughly, α is chosen to assign to each m the data value that made the corresponding join pass. We conclude the argument by observing that there are only finitely (but exponentially) many (φ + ) α up to satisfiability, hence or α (φ + ) α is well-defined and equisatisfiable with φ + .

As for variables, the encoding proposed here is not polynomial, but the added feature does not bring any complexity jump. We can actually use fragment-specific encodings that avoid the explicit constants of (φ) α : this can be achieved either by using second-order variables when available or similarly, in CoreXPath 1.0, thanks to the ability to have multiple propositional variables satisfied at a node in the decision procedure.

Lemma F.1. For any t, p, φ + and α we have that t, p |= (φ + ) α implies t, p |= φ + (and similarly for path expressions).

Proof. This follows easily by induction on φ + . Consider for instance the case where φ + = π + ne m π ′ + , we have t, p, q |= (π + ) α and t, p, q ′ |= (π ′ + ) α with δ (q) ∼ α (m) and α (m) δ (q ′ ). By induction hypothesis we have we have t, p, q |= π + and t, p, q ′ |= π ′ + , and the data has not changed, which allows us to conclude. By construction of the φ + fragment, data joins can only occur under "positive" constructs, hence all other cases go well. For instance, consider (in fragment where it is relevant) the case where φ + = π + except π . We have t, p, q |= (π + ) α for some q for which t, p, q ̸ |= π . By induction hypothesis, we obtain t, p, q |= π + which allows us to conclude. □

We did not use the unicity of marks in φ + . This comes into play in the next lemma.

Lemma F.2. For any t, p and φ + such that t, p |= φ + , there exists α over the marks of φ + such that t, p |= (φ + ) α (and similarly for path expressions).

Proof. We proceed again by induction on expressions. Consider the case where φ + = π 1 + △ m π 2 + . We have t, p, q 1 |= π 1 + and t, p, q 2 |= π 2 + , with δ (q 1 ) and δ (q 2 ) related according to △. By induction hypotheses we obtain t, p, q 1 |= (π 1 + ) α 1 and t, p, q 2 |= (π 2 + ) α 2 . Moreover, α 1 and α 2 have disjoint domains. We set α = α 1 ⊎ α 2 ⊎ {m → δ (q 1 )} and conclude easily that t, p |= (φ + ) α . Other cases are similar. □

We are ready to conclude. Proof. Given an initial query φ + in any of these fragments, there are infinitely many (φ + ) α , but we shall see that only finitely many of these formulas is enough for our purpose.

Let D(φ + ) be the data values occurring in data tests against constants in φ + . Let M be the finite set of marks that occur in φ + , and let D M be a subset of D of cardinal |M | and disjoint from D(φ + ). We claim that if φ + is satisfiable, then there is α with images in D M ∪ D(φ + ) such that (φ + ) α is satisfiable. Starting with a model t ′ of φ + , it suffices to take α ′ provided by the previous proposition, transform the model t ′ into t by rename values in the image of α ′ and outside the desired range, to obtain a suitable t and α.

Given two valuations α and In this section, we show that the satisfiability problem is undecidable for DownwardXPath+id. This will entail undecidability for ForwardXPath+id and VerticalXPath+id as well.

Let Σ be an alphabet, and let {(u i , v i ) | 0 ≤ i ≤ n} ⊆ (Σ + ) 2 be a PCP problem over Σ. We note Σ = {a | a ∈ Σ}, and we give ourselves a fresh symbol # that will mark the start of a PCP domino. We will encode a potential solution to this PCP problem as a branch in a data tree over Σ ∪ Σ for which the corresponding word will belong to {#u i v i | 0 ≤ i ≤ n} + . Since we are working with the DownwardXPath fragment, we cannot prevent the models from having other branches, but we will be able to force all the branches to be identical.

We will use the id links to move around in this encoding: let w be the word corresponding to our encoding branch of the tree, and let w (resp. w) be the longest subword of w in Σ (resp. Σ). Every node w i will have an attribute @succ for which the datum will match the @id key of the node w i+1 , and an attribute @sym for which the datum will match the @id key of the node w i . The nodes w i will also have attributes @succ and @sym playing similar roles. Such a word w will be the encoding of a solution of our PCP problem if and only if w = w.

Hence, we need to find formulas that will force this encoding to be respected. At the end, a data tree will satisfy this set of formulas if and only if it encodes a solution to our PCP problem.

Let's start by forcing all the branches from the root to be identical:

• Ψ 1 := not(//*[@id eq descendant:: * /@id]) (the @id keys are unique along a branch).

• Ψ 2 := and a b ∈Σ∪Σ∪{#} not(//*[id(@id)/child::a and id(@id)/child::b]) (if two nodes share the same @id key, then all their children are labelled by the same letter). • Ψ 3 := not(//*[id(@id)/child:: * /@id ne id(@id)/child:: * /@id]) (if two nodes share the same @id key, then all their children have the same @id key). • Ψ 4 := not(//*[(id(@id)/@sym ne id(@id)/@sym) or (id(@id)/@succ ne id(@id)/@succ)]) (if two nodes share the same @id key, then they have the same @sym data value and the same @succ data value).