Diego Figueira

Leonid Libkin

Pattern Logics and Auxiliary Relations

Keywords: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic-Computational logic First-order logic, pattern, finite model theory, locality, homomorphism preservation theorem, data trees, XML, decidability

A common theme in the study of logics over finite structures is adding auxiliary predicates to enhance expressiveness and convey additional information. Examples include adding an order or arithmetic for capturing complexity classes, or the power of real-life declarative languages. A recent trend is to add a data-value comparison relation to words, trees, and graphs, for capturing modern data models such as XML and graph databases.

Such additions often result in the loss of good properties of the underlying logic. Our goal is to show that such a loss can be avoided if we use pattern-based logics, standard in XML and graph data querying. The essence of such logics is that auxiliary relations are tested locally with respect to other relations in the structure. These logics are shown to admit strong versions of Hanf and Gaifman locality theorems, which are used to prove a homomorphism preservation theorem, and a decidability result for the satisfiability problem. We discuss applications of these results to pattern logics over data forests, and consequently to querying XML data.

Introduction

A common theme in the study of logics over finite structures is adding auxiliary relations and investigating the extra expressiveness they provide. Such auxiliary relations may serve several purposes. They may provide information about presentations of structures that is otherwise not available (for instance, an ordering of graph vertices). They may provide operations on the underlying domain to make logics closer to practical features that they are modeling (for instance, arithmetic operations are a common feature of real-life database query languages). And sometimes they provide extra features as models evolve (an example of this is the study of data trees as a better abstraction of XML data than trees themselves). We now illustrate these in more detail.

• In the study of logics capturing complexity classes (cf. [START_REF] Grädel | Finite Model Theory and its Applications[END_REF][START_REF] Immerman | Descriptive Complexity[END_REF][START_REF] Libkin | Elements of Finite Model Theory[END_REF]), one usually adds an auxiliary relation that specifies an ordering of the domain. The goal is to bridge the gap between machine models, that can talk about a particular presentation, and logics, that cannot distinguish isomorphic structures. • In the study of embedded finite models (cf. [START_REF] Grädel | Finite Model Theory and its Applications[END_REF]), one adds arbitrary auxiliary relations, for instance arithmetic operations. The goal is usually to simulate the expressiveness of real-life query languages over finite databases, as those use extra operations on the domain. • In the study of data models underlying modern database applications -such as XML and graph data -one distinguishes the basic structure (e.g., a tree for XML) and data that such basic structures carry. The latter is often modeled by a predicate expressing the property that two vertices carry the same data items, i.e., a data equality predicate, resulting in data words, data trees, and data graphs [7, 14-16, 34, 41].

With such auxiliary relations, one usually tries to control the power of the resulting logic. In the case of adding orderings, one does this by insisting on invariance of definable properties: they need not depend on a particular ordering that is used. Still, the mere presence of an order or a successor relation enhances the power of logic [START_REF] Libkin | Elements of Finite Model Theory[END_REF][START_REF] Rossman | Successor-invariant first-order logic on finite structures[END_REF]. At the same time, one can establish useful properties of definable queries, for instance, locality [START_REF] Anderson | Locality of queries definable in invariant first-order logic with arbitrary built-in predicates[END_REF][START_REF] Grohe | Locality of order-invariant first-order formulas[END_REF], or bounds on their expressiveness [START_REF] Benedikt | Towards a characterization of orderinvariant queries over tame graphs[END_REF][START_REF] Fagin | On monadic NP vs. monadic co-NP[END_REF][START_REF] Niemistö | On locality and uniform reduction[END_REF][START_REF] Schwentick | On winning Ehrenfeucht games and monadic NP[END_REF]. For embedded finite models, the spirit of the restrictions is similar: invariance under one-to-one mappings of the domain of structure. A typical result would state that adding arbitrary auxiliary relations yields no more power than adding an order under such invariance, cf. [START_REF] Grädel | Finite Model Theory and its Applications[END_REF].

In the case of adding the data equality predicate, restrictions guaranteeing good behavior of logics are of a different nature. The study of such predicates started with words and trees, on which first-order logic (FO) and monadic second-order logic (MSO) are undecidable, which explains the interest in preserving decidability (and connection with automata) in the presence of data. The standard restriction guaranteeing decidability is to the two-variable fragment, FO 2 , see [START_REF] Bojańczyk | Two-variable logic on data words[END_REF][START_REF] Bojańczyk | Twovariable logic on data trees and XML reasoning[END_REF], or extensions thereof [START_REF] Bojańczyk | Automata for data words and data trees[END_REF][START_REF] Tan | An automata model for trees with ordered data values[END_REF].

We are interested in different types of restrictions guaranteeing good properties of logics with auxiliary relations. Our primary motivation comes from studying logics over advanced data models such as XML and graph data, where auxiliary relations capture the notion of adding data values. A concrete example is shown in Fig. 1. In this tree, nodes have labels from a finite alphabet {a, b, c}, and they also come equipped with data values from an infinite set, in this case, N. One represents such a tree as a structure that has the usual child relation, unary labeling predicates for alphabet letters, and the data equality predicate for data values (instead of infinitely many unary predicates); we write x ∼ y if nodes x and y have the same data value (as shown by the dashed lines in the figure).

Restrictions such as invariance are simply not relevant in this setting (and invariant properties cannot say anything interesting about data values). Using FO 2 makes the logic too weak: many languages studied in the context of XML with data [START_REF] Amer-Yahia | Tree pattern query minimization[END_REF][START_REF] Björklund | Conjunctive query containment over trees[END_REF][START_REF] Marx | Conditional XPath[END_REF][START_REF] Miklau | Containment and equivalence for a fragment of XPath[END_REF][START_REF] Vianu | A Web odyssey: From Codd to XML[END_REF] or graphs with data [START_REF] Barceló | Querying graph databases[END_REF][START_REF] Libkin | Regular path queries on graphs with data[END_REF] need to go beyond the two-variable fragment.

Thus, we would like to find restrictions on logics with auxiliary relations that, while sufficiently expressive, do not impose too severe restrictions. The idea of such restrictions is motivated by practical languages for XML and graph data. A key notion in many of them is that of a pattern: essentially a small subgraph, or a subtree, that needs to be matched in a large data set. These often provide the basis for language constructors, for instance, for the navigational language XPath [START_REF] Marx | Conditional XPath[END_REF][START_REF] Miklau | Containment and equivalence for a fragment of XPath[END_REF], more general XML query languages [START_REF] Amer-Yahia | Tree pattern query minimization[END_REF][START_REF] Björklund | Conjunctive query containment over trees[END_REF][START_REF] David | Containment of pattern-based queries over data trees[END_REF], or path queries over graphs [START_REF] Barceló | Querying graph databases[END_REF][START_REF] Fan | Graph pattern matching revised for social network analysis[END_REF]. Patterns also provide a standard abstraction of incomplete data in relational, XML, and graph models [START_REF] Abiteboul | Foundations of Databases[END_REF][START_REF] Abiteboul | Representing and querying XML with incomplete information[END_REF][START_REF] Barceló | XML with incomplete information[END_REF][START_REF] Barceló | Querying regular graph patterns[END_REF][START_REF] Imielinski | Incomplete information in relational databases[END_REF].

An example of a pattern in a tree is a node labeled a that has an a-child with the same data value and a b-child with a different data value; this is clearly matched in the data tree in Fig. 1 by the root and its two children.

Patterns are highly useful as query language constructors for at least two different data models, and at the same time, patternbased logical languages provide a restriction on the use of auxiliary relations that makes it possible to recover nice properties of the underlying logic. The restriction imposed by patterns is that the use of auxiliary relations becomes local: we check those predicates for elements of the domain that are close to each other in the structure. In the above example, we check data equality of a node and its child, which are at distance one in the tree.

Our goal is to show that pattern-based logics with auxiliary relations behave well without imposing very restrictive conditions such as invariance or two-variable limitation. In fact, this good behavior is due to the local nature of auxiliary predicates.

The particular questions we investigate are inspired by applications of logical formalisms with data equality predicate in querying XML and graph data. These questions are split into three groups. The first one concerns the expressiveness of logics, which is a standard subject for investigation. The second one has to do with the homomorphism preservation theorem. This choice is motivated by both the importance of the result in finite model theory ( [START_REF] Rossman | Homomorphism preservation theorems[END_REF] proved that it holds over the class of all finite structures, solving a long-standing open problem; it also holds for several well-behaved classes of finite structures [START_REF] Atserias | On preservation under homomorphisms and unions of conjunctive queries[END_REF][START_REF] Dawar | Homomorphism preservation on quasi-wide classes[END_REF]) and its applications in the data management field (e.g., in handling incomplete information in databases [START_REF] Gheerbrant | When is naïve evaluation possible? In PODS[END_REF], in characterizing classes of schema mappings in data exchange [START_REF] Cate | Structural characterizations of schemamapping languages[END_REF], and in rewritability of ontologymediated queries [START_REF] Bienvenu | Ontology-based data access: a study through disjunctive datalog, CSP, and MMSNP[END_REF]). The third group deals with the basic decidability question, which in fact motivated two-variable restrictions for logics over data words and data trees.

Our main contributions are as follows. 1) Motivated by logics used for querying XML and graph data, we define a pattern logic with auxiliary relations, and an equally expressive logic: FO with local auxiliary relations.

2) When it comes to the expressiveness of the logic, we prove analogs of Hanf and Gaifman locality properties [START_REF] Gaifman | On local and non-local properties[END_REF][START_REF] Hanf | Model-theoretic methods in the study of elementary logic[END_REF] (see also [START_REF] Ebbinghaus | Finite Model Theory[END_REF][START_REF] Libkin | Elements of Finite Model Theory[END_REF]), with neighborhoods defined without using the auxiliary relations. These stronger versions of well known locality theorems give us easy tools to prove expressivity bounds for pattern logics.

3) We prove a homomorphism preservation theorem for pattern logics. It works over classes of structures that include, among others, ranked data trees. Crucially, such classes are defined without mentioning auxiliary relations: for instance, we can specify classes of trees so that the homomorphism preservation theorem would hold on them when the data equality predicate is added. Ranked data trees provide just one example of a class of structures for which the result holds; we state the condition in terms of closure and structural properties of the class. We also discuss applications of this result in querying XML data.

Note that such a result does not follow from Rossman's theorem [START_REF] Rossman | Homomorphism preservation theorems[END_REF], since trees are not FO-definable, nor from other results on homomorphism preservation [START_REF] Atserias | On preservation under homomorphisms and unions of conjunctive queries[END_REF][START_REF] Dawar | Homomorphism preservation on quasi-wide classes[END_REF] which impose restrictions that are violated by adding the data equality relation. Homomorphism preservation results in the finite [START_REF] Atserias | On preservation under homomorphisms and unions of conjunctive queries[END_REF][START_REF] Dawar | Homomorphism preservation on quasi-wide classes[END_REF][START_REF] Rossman | Homomorphism preservation theorems[END_REF] are rather hard to obtain, and our result requires a considerable effort too, crucially relying on the revised form of Gaifman locality theorem. 4) We show a decidability result for pattern logics. It is given for classes of structures which include data words and ranked data trees; we further show that the logic continues to be decidable when one adds the sibling ordering and other relations (for instance, other equivalence relations).

Thus, we retain decidability without such strong restrictions on expressiveness that the two-variable fragment imposes. In the case of unranked data trees, however, we show undecidability of the pattern logic. Organization. Basic definitions are given in Section 2. In Section 3 we define pattern logics and logics with local auxiliary relations. Section 4 proves locality theorems, and Section 5 shows the homomorphism preservation theorem and explains some of its application. In Section 6 we discuss decidability of pattern logics. Section 7 offers concluding remarks.

Preliminaries

Relational Structures A relational vocabulary σ is a finite set of relation symbols, each with a specified arity. A σ-structure A consists of a universe A (also called a domain) and an interpretation R A ⊆ A m of each R ∈ σ of arity m. We normally use A, B, . . . to denote the universe of A, B, . . ..

Let denote the disjoint union of sets (i.e., A B is

A ∪ B if A∩B = ∅). Let ⊕ denote the disjoint union of σ-structures, that is, A ⊕ B has universe A B and R A⊕B = R A R B for every R ∈ σ. A graph is a structure G = (V, E)
, where E is a binary relation that is symmetric and irreflexive. Thus, our graphs are undirected, loopless, and without parallel edges.

A σ-structure B is called a substructure of another σ-structure A if B ⊆ A and R B ⊆ R A for every R ∈ σ. In that case we write B ⊆ A. A substructure B is an induced substructure if R B = R A ∩ B m for every R ∈ σ of arity m. For A ⊆ A we write A| A for the induced substructure of A with domain A . For σ ⊆ σ, the σ -induced substructure of A, denoted by A| σ , is the restriction of A to the signature σ .

The Gaifman graph of a σ-structure A, denoted by G(A), is the undirected graph whose set of nodes is the universe of A, and whose edges are pairs (a, a ) of distinct elements of A that appear together in some tuple of a relation in σ.

Let G = (V, E) be a graph. Recall that the distance between two vertices u and v is the length of the shortest path from u to v. For a vertex u and an integer r ≥ 0, the r-neighborhood of u in G, denoted by N G r (u), is the set of vertices at distance at most r from u. In particular, N G 0 (u) = {u}. For a tuple ū = (u1, . . . , um), we let

N G r (ū) be {N G r (ui) | 1 ≤ i ≤ m}.
Where this causes no confusion, we also write N G r (ū) for the subgraph of G induced by this set of vertices.

For a structure A and a vector ā of elements of A, we define the r-neighborhood N A r (ā) as the induced substructure with the universe N G(A) r (ā) expanded with |ā| constant symbols interpreted as the elements of ā. In particular, if two neighborhoods N A r (ā) and N B r ( b) are isomorphic, which is denoted by

N A r (ā) ∼ = N B r ( b)
, it means that there is an isomorphism that sends ā to b.

Data trees and forests. These structures received much attention as of late, being an abstraction of XML documents with data. The structure of XML documents is normally modeled as a tree; in data trees, we add a data value from an infinite domain to each node. The usual way to represent this as a first-order structure is by means of an equivalence relation ∼ on nodes whose meaning is that two nodes carry the same data value, see Fig. 1.

We now give precise definition, generalizing slightly the standard ones from [START_REF] Bojańczyk | Automata for data words and data trees[END_REF][START_REF] Bojańczyk | Two-variable logic on data words[END_REF][START_REF] Bojańczyk | Twovariable logic on data trees and XML reasoning[END_REF][START_REF] Segoufin | Static analysis of XML processing with data values[END_REF]. For a vocabulary σ = τ {ch}, we say that a σ-structure A is a τ -tree if ch A is the child relation of a finite tree. Over τ -trees, we use "root", "parent", "child", "sibling", etc., to make reference to elements of the ch-induced tree. For any τ -tree A, we say that sib is a sibling order for A if it is the union, over all elements a in A, of total linear orders on sets of a's siblings {b ∈ A | (a, b) ∈ ch A }. We say that a τ -tree A is k-ranked if every element of A has at most k children. We write root(A) to denote the root element of A. Given a tree A and an element a ∈ A, by A a we denote the induced substructure given by the subtree rooted at a.

The class of data trees DT is the class of all τ -trees where τ has monadic relations and one binary equivalence relation ∼. The class of data forests DF is the class of disjoint unions of data trees, i.e., A1 ⊕ • • • ⊕ Am for m ∈ N such that A1, . . . , Am ∈ DT . By DF k we denote the class of data forests in which every data tree is k-ranked.

First-Order Logic (FO) Let σ be a relational vocabulary. Formulae of FO over σ are obtained by closing relational atomic formulae R(x1, . . . , xm), where R ∈ σ is of arity m, and atomic equality formulae x = y under conjunction ∧, disjunction ∨, negation ¬, existential ∃ and universal ∀ quantification. The semantics is standard. We write A |= ϕ(ā) if ϕ is true in A when its free variables are interpreted by the tuple of elements ā. The quantifier rank of a first-order formula is the maximum depth of quantifier nesting in it.

The class ∃Pos of existential-positive formulae is the closure of atomic formulae under conjunction, disjunction, and existential quantification. By substituting variables, one can eliminate equalities in ∃Pos formulae.

Locality. FO formulae are known to exhibit locality properties, most commonly formulated in terms of theorems by Hanf and Gaifman. Define (A, ā) r (B, b) for ā ∈ A n and b ∈ B n if there exists a bijection f : A → B such that N A r (āc) ∼ = N B r ( bf (c)) for every c ∈ A. Hanf's locality theorem states that for every FO formula ϕ(x), there exists a number r so that (A, ā) r (B, b) implies that A |= ϕ(ā) if and only if B |= ϕ( b). In fact r can be taken to be (3 k -1)/2, where k is the quantifier rank of ϕ. It was originally stated by Hanf in [START_REF] Hanf | Model-theoretic methods in the study of elementary logic[END_REF] for infinite models, and then restated for sentences over finite models in [START_REF] Fagin | On monadic NP vs. monadic co-NP[END_REF]; the present formulation is from [START_REF] Libkin | Elements of Finite Model Theory[END_REF].

To state Gaifman's theorem, note that for every integer r ≥ 0, there is an FO formula δ(x, y) ≤ r stating that the distance between x and y in the Gaifman graph is at most r. Let δ(x, y) > r be the negation of this formula. Note that δ(x, y) ≤ r could be expressed in ∃Pos, by a formula whose quantifier rank is bounded by r plus the maximum arity of a relation of σ (in fact it can even be logarithmic in r).

Define r-local formulae ψ r (x) as formulae in which all quantifiers are restricted to the r-neighborhood of x, i.e., formulae that are either of the form ∃y (δ(x, y) ≤ r ∧ . . .) or of the form

∀y (δ(x, y) ≤ r → . . .). A basic FO local sentence is ∃x1 . . . ∃xn 1≤i<j≤n δ(xi, xj) > 2r ∧ i≤n ψ r (xi) ,
where ψ r (x) is an r-local formula. Gaifman's theorem [START_REF] Gaifman | On local and non-local properties[END_REF] says that every FO sentence ϕ is equivalent to a Boolean combination of basic FO local sentences. Here r is exponential in the quantifier rank of ϕ.

Homomorphisms. A homomorphism between two structures A, B of the same vocabulary is a mapping

h : A → B so that for each relation symbol R in the vocabulary, if ū ∈ R A , then h(ū) ∈ R B .
Auxiliary relations. We often deal with a situation where the vocabulary is split into two kinds of relations: main and auxiliary ones. Throughout the paper we shall reserve τ for the vocabulary of auxiliary relations. If σ and τ are two disjoint vocabularies, we write στ as an abbreviation of σ τ . For instance, in data trees, we can treat the equal-value relation τ as the auxiliary relation. In the study of invariance, τ typically contains a single binary relation interpreted as a linear order or a successor.

Patterns and local auxiliary relations

As discussed in the introduction, logical languages for XML and graph data are largely based on patterns (either tree or graph patterns) [START_REF] Amer-Yahia | Tree pattern query minimization[END_REF][START_REF] Barceló | Querying graph databases[END_REF][START_REF] Barceló | Querying regular graph patterns[END_REF][START_REF] Björklund | Conjunctive query containment over trees[END_REF][START_REF] Fan | Graph pattern matching revised for social network analysis[END_REF][START_REF] Miklau | Containment and equivalence for a fragment of XPath[END_REF]. Such a pattern is a small subtree or a subgraph that needs to have a match in the large database. On top of it, one might impose data values [START_REF] Abiteboul | Representing and querying XML with incomplete information[END_REF][START_REF] Barceló | XML with incomplete information[END_REF][START_REF] Björklund | Optimizing conjunctive queries over trees using schema information[END_REF][START_REF] David | Containment of pattern-based queries over data trees[END_REF][START_REF] Libkin | Regular path queries on graphs with data[END_REF], for instance by means of the data equality predicate [START_REF] Bojańczyk | Automata for data words and data trees[END_REF][START_REF] Bojańczyk | Two-variable logic on data words[END_REF][START_REF] Bojańczyk | Twovariable logic on data trees and XML reasoning[END_REF][START_REF] Segoufin | Static analysis of XML processing with data values[END_REF]. An example of a pattern is the tree in Fig. 1. It has both the child and the data equality relations. Note that the tree (i.e., the reduct of the ch relation) is connected, but the data equality relation on it could be arbitrary: in that example, it has three connected components.

We now generalize this to arbitrary structures. Assume that we have, as before, two disjoint vocabularies σ and τ . A σ-pattern over στ is a στ -structure P so that the Gaifman graph of its σ-reduct is connected (i.e., the graph G(P|σ) is connected). We omit 'over στ ' if it is clear from the context.

Note that a σ-pattern over στ does include all the relations in τ as well, but it is only the σ-part of it that needs to be connected (like the tree in Fig. 1, where σ is the child relation).

Pattern logic. For an arbitrary structure A, let ∆ A denote its positive diagram, i.e., the conjunction of all relational atomic formulae true in A.

If |A| = n, then ∆ A has n free variables. For instance, if A is a graph with edges (v1, v2) and (v2, v3), then ∆ A (x1, x2, x3) = E(x1, x2) ∧ E(x2, x3).
Fix σ and τ . Formulae of σ-pattern logic FO PAT σ (στ ) are defined as follows:

ϕ, ψ := S(x) | x = y S ∈ σ | ∆ P (x) P is a σ-pattern | ϕ ∨ ψ | ϕ ∧ ψ | ¬ϕ | ∃xϕ | ∀xϕ .
That is, we restrict FO(στ ) by disallowing arbitrary atomic τformulae, and only allowing them as part of pattern formulae ∆ P , so that the σ-reduct of P is connected. The existential positive fragment (in which negation and universal quantification are disallowed) is denoted by ∃Pos PAT σ (στ ). Note that this is not the minimal definition of the logic: for instance, S(x) is a particular case of a formula ∆ P (x). In fact the logic can be compactly defined as

ϕ, ψ := (x = y) | ∆ P (x) | ϕ ∧ ψ | ¬ϕ | ∃xϕ.
The formula ∆ P (x) is a quantifier-free FO(στ ) formula; in particular its quantifier rank is zero. Note that if P has universe {v1, . . . , vn}, then A |= ∆ P (a1, . . . , an) if and only if the mapping f : vi → ai, for 1 ≤ i ≤ n, is a homomorphism from P to A.

Patterns as those used for querying XML documents with data values are indeed such: one specifies a small connected part of the tree, and then adds an arbitrary data equality relation over it, see [START_REF] Barceló | XML with incomplete information[END_REF][START_REF] Björklund | Optimizing conjunctive queries over trees using schema information[END_REF][START_REF] David | Containment of pattern-based queries over data trees[END_REF][START_REF] Miklau | Containment and equivalence for a fragment of XPath[END_REF][START_REF] Segoufin | Static analysis of XML processing with data values[END_REF].

τ -local formulae. We now present a slightly different way of looking at the pattern logic, by allowing τ -predicates, but only in a "local" context. The resulting logic will be called FO LOC τ , expressing the fact that τ -predicates have been "localized". The idea of such local uses of predicates appeared previously not only in connection with patterns in data models, but also in connection with expressivity of logics in the finite [START_REF] Etessami | Reachability and the power of local ordering[END_REF].

To define it, we need an FO formula connσ(z) expressing that the σ-substructure induced by z is connected. That is, A |= connσ(ā) if and only if G((A|σ)|ā) has only one connected component. Note that while in general connectivity is not FO-definable, in this case we test for connectivity of a graph of a fixed size |z|. Thus, connσ(z) is an FO (in fact, positive, quantifier-free) formula: one simple takes the disjunctions of positive diagrams of all connected graphs with |z| vertices. Now we define FO LOC τ (στ ) as ϕ, ψ :

= S(x) | x = y S ∈ σ | T (x) ∧ connσ(x, ȳ) T ∈ τ | ϕ ∨ ψ | ϕ ∧ ψ | ¬ϕ | ∃xϕ | ∀xϕ
We write ∃Pos LOC τ (στ ) for the existential positive fragment, without ¬ and ∀.

Patterns and locality give us two different ways of looking at the same logic: Proposition 3.1. For all σ and τ , we have FO PAT σ (στ ) = FO LOC τ (στ ) and ∃Pos PAT σ (στ ) = ∃Pos LOC τ (στ ). Proof. For any σ-pattern formula ∆ P (x), let ϕ(x) ∈ ∃Pos PAT σ (στ ) be the formula that results from replacing every occurrence of T (ȳ) so that T ∈ τ with T (ȳ) ∧ connσ(ȳ, x) in ∆ P (x). Note that since the σ-reduct of the Gaifman graph of P is connected, we have that ∆ P (x) is equivalent to ϕ(x). Then, it follows that every FO PAT σ (στ ) formula is equivalent to a FO LOC τ (στ ) formula; and every ∃Pos PAT σ (στ ) formula is equivalent to a ∃Pos LOC τ (στ ) formula.

Conversely, any conjunctive quantifier-free ∃Pos LOC τ (στ ) formula ϕ(x) is equivalent to a finite disjunction of σ-pattern formulae i ∆ P i (x). Indeed, it is easy to see that the canonical structure

A ϕ of ϕ = ∃x.ϕ is a disjoint union P1 ⊕ • • • ⊕ Pn of structures Pi where G(Pi|σ) is connected for every i ∈ [1, n]
. This is a consequence of the syntactic restriction of FO LOC τ (στ ) requiring any two elements in a tuple of a relation T ∈ τ to be connected through σrelations. In other words, A ϕ is a disjoint union of σ-patterns over στ . Thus, ϕ(x) is equivalent to i∈[1,n] ∆ P i (ȳi), where ȳi, ranging over x, are the variables of the domain of Pi. Therefore, every ∃Pos LOC τ (στ ) formula is equivalent to a ∃Pos PAT σ (στ ) formula; and every FO LOC τ (στ ) formula is equivalent to a FO PAT σ (στ ). For a graph G, let G r stand for its r-step transitive closure, i.e., a graph in which we have an edge (u, v) if there is a path from u to v of length at most r in G. Given a στ -structure A, we say that it is (τ, r)-local if G(A|τ ) ⊆ G(A|σ) r . The (τ, r)-localization of A is its maximal (τ, r)-local substructure. It can be constructed as follows: look at all relations of τ , and remove all tuples ā from them that have two components a, a at distance greater than r in G(A|σ). Proposition 3.2. Let ϕ(x) be a formula of FO PAT σ (στ ) (or of FO LOC τ (στ )). There exists r ≥ 0 so that ϕ(ā) is true in A if and only if it is true in the (τ, r)-localization of A, for every tuple ā of elements of A.

Proof. Let ϕ(x1, . . . , xn) ∈ FO LOC τ with quantifier rank k, and let r = k + n. Suppose A is a στ -structure, R ∈ τ , and (b1, . . . , bm) ∈ R A , so that for some i, j ∈ [1, m], bi and bj are at distance > r, that is,

N A|σ r (bi) ∩ N A|σ r (bj) = ∅.
Let A be the structure resulting from removing (b1, . . . , bm) from R A in A. One can easily show by induction on the quantifier rank of ϕ that, for every a1, . . . , an ∈ A we have A |= ϕ(a1, . . . , an) ⇔ A |= ϕ(a1, . . . , an). This is because, by definition of FO LOC τ , ϕ can only test for R(x1, . . . , xm) in conjunction with connσ(x1, . . . , xm, y1, . . . , ys) for some y1, . . . , ys, which specifies that the elements denoted by x1, . . . , xm, y1, . . . , ys form a connected component, and thus that every pair xi, xj is at distance ≤ |{x1, . . . , xm, y1, . . . , ys}| ≤ n + k = r. By repeating this argument for all tuples b in a relation in τ which are not r-local, it follows that, for every structure A and a1, . . . , an in A, we have A |= ϕ(a1, . . . , an) if and only if  |= ϕ(a1, . . . , an), where  is the (τ, r)-localization of A.

It follows that if we define

τ -conn(A) as A|A 1 ⊕ • • • ⊕ A|A n ,
where the Ai's are the maximal connected components of G(A|σ), then A and τ -conn(A) agree on all FO PAT σ (στ ) formulae. Some (τ, r)-local relations always exist: for instance, if τ contains a single binary relation symbol S, then every structure A with a connected Gaifman graph has a (S, 3)-local successor relation; this follows from the fact that the cube of any connected graph is Hamiltonian [START_REF] Karaganis | On the cube of a graph[END_REF].

Locality of pattern logics

The goal of this section is to show strong locality results for the pattern logic: one can prove analogs of Hanf and Gaifman theorems for FO PAT σ (στ ) where neighborhoods are defined with respect to Gaifman graphs of σ-reducts only, i.e., τ -relations do not count for computing the distance between two elements. This makes neighborhoods smaller, and thus easier to make isomorphic; consequently it makes these versions of locality easier to apply. One particular application is the separation of FO PAT σ (στ ) from FO(στ ); others will be crucial for proving homomorphism preservation and decidability results.

For a στ -structure A, we use δσ(a, b) to denote the distance between a and b in G(A|σ), the Gaifman graph that takes into account only σ-relations. Note that δσ(x, y) ≤ r can be expressed as an existential-positive FO(σ) formula, and δσ(x, y) > r as its nega-tion. For ā = (a1, . . . , an), by N A|σ r (ā) we mean the substructure of A induced by the set {b | δσ(b, ai) ≤ r for some i ≤ n}, together with n additional constants, interpreted as the elements of ā. Note that while the elements of N

. Indeed, if (A, ā) τ d•r (B, b), then (A τ,r , ā) τ d•r (B τ,r , b) and therefore (A τ,r , ā) d (B τ,r , b), which means that A τ,r |= ϕ(ā) if and only if B τ,r |= ϕ( b). Since A τ,r |= ϕ(ā) ⇔ A |= ϕ(ā) and B τ,r |= ϕ(ā) ⇔ B |= ϕ(ā), it then follows that A |= ϕ(ā) iff B |= ϕ( b).
If τ has only unary predicates, then FO PAT σ (στ ) = FO LOC τ (στ ) = FO(στ ), since connσ(x) is true for each x. However, with a single non-unary predicate in τ , locality provides a separation result: This contradicts Theorem 4.1 and shows that ϕ is not definable in FO PAT σ (στ ). As a consequence of Hanf-τ -locality, we have the following condition, known as Gaifman locality for formulae with free variables [START_REF] Libkin | Elements of Finite Model Theory[END_REF] (except that we again only look at neighborhoods defined by σ-relations): where ψ is an FO(στ ) formula with one free variable, and ψ r,σ (x) stands for the relativization of ψ to N A|σ r (x); that is, the result of replacing in ψ every subformula of the form ∃yθ with ∃y(δσ(x, y) ≤ r ∧ θ), and every subformula of the form ∀yθ with ∀y(δσ(x, y) ≤ r → θ). The locality radius of a basic local sentence is r. Its width is n. The formula ψ is called the local condition.

While syntactically ( †) is not an FO PAT σ (στ ) sentence, it can be expressed in this logic. Indeed, it is easy to see that ( †) is definable in FO LOC τ (στ ): the first conjunct only refers to σ-relations, and in ψ r,σ (x), quantification is relativized to the r-neighborhood of x, with respect to σ. Thus, for any occurrence of a τ relation T (z1, . . . , z k ), we know that all the zi's must belong to the same connected component of G(A|σ), and in particular be at distance at most 2r from each other. Hence, each such atomic formula can be replaced by ∃ȳ (T (z) ∧ connσ(z, x, ȳ)), where ȳ has k • (r -1) variables witnessing paths from each of the zi's to x of length at most r. This turns ( †) into syntactically proper shape of an FO LOC τ (στ ) sentence, and thus by Proposition 3.1 it is also an FO PAT σ (στ ) sentence.

We now have an analog of Gaifman's theorem:

Theorem 4.4. Every FO PAT σ (στ ) sentence is equivalent to a Boolean combination of basic FO PAT σ (στ ) local sentences ( †). Proof. We make use again of Proposition 3.2, and of Gaifman's Theorem for FO. Given a FO PAT σ (στ ) sentence ϕ, by Gaifman's Theorem for FO it is equivalent to a Boolean combination of basic FO local sentences ψ1, . . . , ψn of the form ( †). In particular, it is equivalent to such a boolean combination on the class of (τ, r)localized structures, where r is as in Proposition 3.2. Over these structures, one can see that each basic FO local sentence ψi with locality radius ri is actually equivalent to a basic FO PAT σ (στ ) sentence with locality radius ≤ r • ri. We then have that over (τ, r)localized structures ϕ is equivalent to a Boolean combination of basic FO PAT σ (στ ) local sentences. Then, by Proposition 3.2, this generalizes to the class of all structures.

Note that, like for the analog of Hanf's theorem, we define distance with respect to σ relations only: formulae ψ r,σ can mention both σ and τ relations, but the radius of quantification is determined just by σ. This is different from formulae ψ r used in original Gaifman's theorem, which define neighborhoods with respect to all vocabulary predicates (and thus neighborhoods could be larger). In particular, it is easier to satisfy a basic FO LOC τ local sentence than a basic FO local sentence, which will make this version of Gaifman's theorem more valuable to us in the next sections.

Homomorphism preservation theorem

We now use locality results from the previous section to prove a homomorphism preservation theorem (hpt) for a large class of structures including ranked data forests. But first we explain the concept and its applications in computer science.

HPT and its applications

Preservation theorems relate semantic properties of FO sentences to their syntactic properties: for instance, a sentence is preserved under extensions if and only if it is equivalent to an existential sentence. A sentence ϕ is preserved under homomorphisms on a class C of structures if, whenever we have a homomorphism A → B between two structures of C, then A |= ϕ implies B |= ϕ. Then the hpt for C says that an FO sentence ϕ is preserved under homomorphisms on C structures if and only if it is equivalent to an existential positive sentence on C. It is very easy to check that ∃Pos sentences are preserved under homomorphisms; the crucial part is the reverse direction.

When C is the class of all structures (finite and infinite), this is a textbook model theory result. For finite structures, it had remained an open problem for decades, before being confirmed by Rossman [START_REF] Rossman | Homomorphism preservation theorems[END_REF] a few years ago. The hpt is also known for some classes of well-behaved finite structures, for instance structures of bounded treewidth [START_REF] Atserias | On preservation under homomorphisms and unions of conjunctive queries[END_REF][START_REF] Dawar | Homomorphism preservation on quasi-wide classes[END_REF]. These are not consequences of Rossman's theorem (since such classes of structures are not FO-definable), and in fact versions of hpt in the finite tend to be quite hard results to show.

At the same time, these preservation results often find applications in computer science. The reason for this is the special importance of the class of ∃Pos, especially in databases and constraint satisfaction [START_REF] Abiteboul | Foundations of Databases[END_REF][START_REF] Grädel | Finite Model Theory and its Applications[END_REF]. In terms of their expressiveness, ∃Pos formulae are equivalent to unions of conjunctive queries, or positive relational algebra queries, cf. [START_REF] Abiteboul | Foundations of Databases[END_REF]. These are very common queries, that also play a special role in many contemporary applications of databases, for instance, data integration and exchange. In fact, hpt was used for determining classes of mappings between database schemas that one needs to use in data exchange applications [START_REF] Cate | Structural characterizations of schemamapping languages[END_REF] and for characterizing properties of the chase procedure under various types of mappings [START_REF] Fagin | Local transformations and conjunctive-query equivalence[END_REF]. In constraint satisfaction, hpt is needed to provide characterization of FO-definable CSP problems [START_REF] Atserias | On digraph coloring problems and treewidth duality[END_REF].

Another area where the hpt proved very useful is handling incomplete data [START_REF] Abiteboul | Foundations of Databases[END_REF][START_REF] Imielinski | Incomplete information in relational databases[END_REF]. Suppose we have an FO structure (i.e., a relational database) whose elements come from two sets: C of constants and V of variables (also called nulls in the database terminology). For instance, G = {(1, x), (x, y), (y, 2)} is a graph whose nodes are 1, 2 ∈ C and x, y ∈ V. We view variables as instances of incompleteness: we do not know what these nodes actually are. Another instance of incompleteness is that some edges may be missing altogether. Thus, one defines the semantics of an incomplete structure A as the set [[A]] of structures A over C so that there is a homomorphism f : A → A which is the identity on C. For instance, G = {(1, 3), [START_REF] Amer-Yahia | Tree pattern query minimization[END_REF][START_REF] Anderson | Locality of queries definable in invariant first-order logic with arbitrary built-in predicates[END_REF], (4, 2), (5, 3)} is in [[G]], as witnessed by the homomorphism x → 3, y → 4.

If we now have an FO sentence (query) ϕ, the standard way of answering it over an incomplete structure A is to find certain answers ϕ: that is, [START_REF] Abiteboul | Foundations of Databases[END_REF][START_REF] Imielinski | Incomplete information in relational databases[END_REF]). In general, for arbitrary FO formulae, checking if A |= ϕ is an undecidable problem, as it is a form of finite validity. However, if ϕ is an ∃Pos sentence, then

A |= ϕ iff A |= ϕ for each A ∈ [[A]] (see
A |= ϕ ⇔ A |= ϕ (1)
(cf. [START_REF] Imielinski | Incomplete information in relational databases[END_REF]). This says that to evaluate ϕ with certainty over an incomplete database, we just have to use the standard query evaluation engine and simply evaluate ϕ itself. This is a very desirable property, and thus it is natural to ask how far it extends. With the help of hpt in the finite one can answer this: if (1) holds for an FO sentence ϕ, then ϕ is equivalent to an ∃Pos sentence [START_REF] Libkin | Incomplete information and certain answers in general data models[END_REF]. Thus, unions of conjunctive queries are the maximal class of FO queries for which certain answers can be found by straightforward query evaluation. The connection between hpt and query evaluation does not stop here: it extends to other relational semantics of incompleteness and other notions of homomorphisms [START_REF] Gheerbrant | When is naïve evaluation possible? In PODS[END_REF]. What is more problematic is extending it to XML with incomplete information [START_REF] Abiteboul | Representing and querying XML with incomplete information[END_REF][START_REF] Barceló | XML with incomplete information[END_REF]. Even though the underlying structure of XML documents is that of trees, adding arbitrary data-equality predicates destroys their small treewidth and all other properties for which the hpt is known [START_REF] Atserias | On preservation under homomorphisms and unions of conjunctive queries[END_REF][START_REF] Dawar | Homomorphism preservation on quasi-wide classes[END_REF].

Thus, in addition to the general interest in hpt results in finite model theory, they come with concrete applications, and there are open problems related to them, in particular in the context of XML with data values. One of those will be settled in the next section.

HPT for the pattern logic

We first state formally what it means for a logic to satisfy the hpt over a class C. Suppose we have a logic L that has an existential positive fragment ∃PosL (for instance, FO, or FO PAT σ , or FO LOC τ ). A sentence ϕ of L is preserved under homomorphisms on C if for every two structures A, B ∈ C such that there is a homomorphism h : A → B, we have that A |= ϕ implies B |= ϕ. Then the homomorphism preservation theorem (hpt) holds for L over C if the following two conditions are equivalent for a sentence ϕ of L:

• ϕ is preserved under homomorphisms on C;

• ϕ is equivalent to an ∃PosL sentence on C.

We now state an hpt result for the pattern logic. Let C be a class of στ -structures. Given a structure A, we say that a set X ⊆ A is r-scattered if δ(x, y) > 2r for all distinct x, y ∈ X, and it is σ, r-scattered if δσ(x, y) > 2r for all distinct x, y ∈ X. We say that C is σ-wide if for all r, m > 0, there exists a number n so that each A ∈ C with |A| > n has a σ, r-scattered set of size m. An example is the class of structures whose σ-reducts have degree bounded by a fixed number k.

Theorem 5.1. Let C be a class of finite στ -structures that is closed under disjoint unions and induced substructures, and is σ-wide. Then the homomorphism preservation theorem holds for FO PAT σ (στ ) over C. Before we outline the proof of this theorem, we mention a few applications. We start with the class of data forests. Recall that in this case, σ contains the child relation ch, while τ contains unary labeling predicates and the binary data equality predicate ∼ (actually, it makes no difference whether the unary predicates belong to σ or to τ ). Note that the class of data forests DF is closed under disjoint unions and induced substructures. Thus, the hpt holds for every wide class of data forests with respect to the child relation. Clearly, the class of ranked data forests is such, and hence we get: Corollary 5.2. The hpt holds for the pattern logic over DF k , for every k > 0.

We can further extend this using the notion of moderate degree, or degree bounded by n o (1) , from [START_REF] Schwentick | On winning Ehrenfeucht games and monadic NP[END_REF]. We say that a class C of σstructures is of moderate degree if all the degrees in their Gaifman graphs are bounded by n o (1) for all sufficiently large structures. That is, for every ε > 0, there exists N > 0 so that for every structure A ∈ C of size n ≥ N , the maximum degree in G(A) is less than n ε . A class C of data forests is of moderate degree if the class of its ch-reducts (i.e., the trees themselves) is.

One can show that the class of data forests of moderate degree is ch-wide. Thus: Proposition 5.3. The hpt holds for the pattern logic over data forests of moderate degree.

Proof. Let C be a class of forests of moderate degree; assume that f (n) is the maximum degree in a forest having n nodes. We show that C is ch-wide; that will suffice to conclude the corollary.

Fix r, m > 0. Let d = (2r + 2)m, and let ε = 1 d+1 . Then, for all n ≥ m d+1 , we have d n/m ≥ n ε . Thus, for some N0 depending on m and r, we have for all n ≥ N0:

n m ≥ f (n) d . (2)
Indeed, otherwise we would have n m < f (n) d for arbitrarily large n, and thus f (n) > n m 1/d ≥ n ε for arbitrarily large n, which is impossible since C is of moderate degree.

Suppose we have a forest of size n for n > N0. Assume that it has m or more connected components. Then it clearly has an rscattered set of size m. So assume it has fewer than m connected components (trees); then at least one of them, t, is of size at least n/m. We know that if we we have a tree of branching factor at most k and size at least k d , then it has a branch of length at least d. Since |t| ≥ n m ≥ f (n) d , by [START_REF] Barceló | XML with incomplete information[END_REF], we see that t0 has a branch of length d = (2r + 2)m. Therefore, this branch alone has an r-scattered set of size m. This has direct implications for evaluating queries over XML documents with incomplete information. Such documents are modeled as forests where each node is assigned a data value from either a set C of constants or a set V of variables; one can think of them as direct analogs of incomplete relational databases. We refer to them as XML forests. These provide the actual model of incomplete XML that is abstracted as data forests; in the latter, instead of having a potentially infinite set of data values, we only have the data equality predicate. Some models of incomplete XML deal with more complex structural incompleteness than the forest structure [START_REF] Abiteboul | Representing and querying XML with incomplete information[END_REF][START_REF] Barceló | XML with incomplete information[END_REF], but we do not consider them here as they quickly lead to intractability of query evaluation [START_REF] Barceló | XML with incomplete information[END_REF].

Query languages considered for incomplete XML documents are usually pattern logics [START_REF] Abiteboul | Representing and querying XML with incomplete information[END_REF][START_REF] Barceló | XML with incomplete information[END_REF][START_REF] Björklund | Conjunctive query containment over trees[END_REF][START_REF] David | Containment of pattern-based queries over data trees[END_REF] or their fragments. As explained in section 5.1, it is crucial for us to know when checking A |= ϕ is equivalent to checking A |= ϕ, i.e., when finding certain answers can be replaced by straightforward query evaluation. In the database terminology, one says that naïve evaluation works for ϕ. While this is known for relational databases [START_REF] Libkin | Incomplete information and certain answers in general data models[END_REF], for XML the problem is open. We can now settle it for child-pattern queries and the class of XML documents whose branching degree is not very large.

Corollary 5.4. Let ϕ be a FO PAT ch sentence and C a class of XML incomplete documents of fixed or moderate degree. Then naïve evaluation works for ϕ over C if and only if ϕ is equivalent to an ∃Pos PAT ch sentence over C. This follows from Corollary 5.2 and Proposition 5.3, and the result from [START_REF] Gheerbrant | When is naïve evaluation possible? In PODS[END_REF] showing the equivalence of naïve evaluation on a class C and preservation under homomorphisms on the same class.

Proof of Theorem 5.1

Due to Proposition 3.1, it suffices to prove the result for FO LOC τ . As before, we omit the στ vocabulary from notations when it is clear from the context. That each formula of ∃Pos LOC τ is preserved under homomorphisms is immediate by a straightforward induction on the structure of the formula. Thus, we prove the opposite direction.

We say that B is a segregated substructure of A if there are pairwise disjoint subsets A1, . . . , An of A so that B = A|A 1 ⊕ • • • ⊕ A|A n . We write seg for the segregated substructure relation. Note that a class of structures C is closed under disjoint unions and induced substructures if and only if it is closed under disjoint unions and segregated substructures.

For a sentence ϕ preserved under homomorphisms on a class of structures C, we say that A ∈ C is a seg-minimal model of ϕ in C if A |= ϕ and for every proper substructure

B seg A, A seg B such that B ∈ C, we have B |= ϕ.
The term conjunctive query [START_REF] Abiteboul | Foundations of Databases[END_REF] denotes formulae of the form ∃x1, . . . , xn θ, where θ is a conjunction of atomic formulae. Every finite structure A with n elements gives rise to a canonical conjunctive query ϕ A , which is the existential closure of its positive diagram, i.e., ϕ A = ∃x∆ A (x), where x is the set of all variables used in ∆ A . Conversely, every conjunctive query ϕ = ∃x1, . . . , xn θ gives rise to a canonical structure Aϕ with n elements, known as its tableau [START_REF] Abiteboul | Foundations of Databases[END_REF], where the elements of A are the variables x1, . . . , xn, and the relations of A consist of the tuples of variables in the conjuncts of θ. The following is well known (cf. [START_REF] Abiteboul | Foundations of Databases[END_REF][START_REF] Grädel | Finite Model Theory and its Applications[END_REF]). If A and B are two finite structures, then

∃ homomorphism A → B ⇔ B |= ϕ A ⇔ ϕ B |= ϕ A . (3)
Not all structures have a canonical conjunctive query that is a formula of FO LOC τ . Nevertheless, those structures A so that A = τ -conn(A) do have a canonical FO LOC τ conjunctive query. Lemma 5.5. For every A so that A = τ -conn(A), the canonical conjunctive query ϕ A is definable in FO LOC τ .

Indeed, note that any two elements a, b of A related by a relation T ∈ τ belong to the same connected component, and thus δσ(a, b) ≤ n for n = |A|. It is then immediate that ϕ A is definable in FO LOC τ . Also, from the definition of FO LOC τ we have that for every structure A and FO LOC τ sentence ϕ,

A |= ϕ ⇔ τ -conn(A) |= ϕ. (4)
Lemma 5.6. Let C be a class of finite στ -structures closed under segregated substructures and let ϕ be a FO LOC τ sentence that is preserved under homomorphisms on C. Then the following are equivalent:

1. ϕ has finitely many seg-minimal models in C up to isomorphism. 2. ϕ is equivalent on C to a ∃Pos LOC τ sentence.

Proof of the lemma. For the 1. ⇒ 2. direction, take any seg- minimal model A of ϕ. Note that A must be so that τ -conn(A) = A, since otherwise τ -conn(A) would be a strict segregated substructure of A where τ -conn(A) |= ϕ, by [START_REF] Barceló | Querying graph databases[END_REF]. Indeed, τ -conn(A) ∈ C by the hypothesis, and hence A would not be seg-minimal. Let ϕ A be the canonical conjunctive FO LOC τ query of A (it is definable in FO LOC τ due to Lemma A.1). We define the existential positive formula ψ as the disjunction of all ϕ A for each seg-minimal model A of ϕ. We next show that ψ and ϕ are equivalent.

Note that, by ( 6), we have that B |= ϕ A iff there is a homomorphism from A to B. If B |= ψ then B |= ϕ A for some disjunct ϕ A of ψ, and hence there is a homomorphism from A to B, by [START_REF] Atserias | On preservation under homomorphisms and unions of conjunctive queries[END_REF]. Since A |= ϕ and ϕ is closed under homomorphisms, then B |= ϕ. Conversely, if B |= ϕ there must be some seg-minimal A seg B so that A |= ϕ. Hence, ψ contains ϕ A as a disjunct, meaning that A |= ψ.

For the 2. ⇒ 1. direction, by propagating disjunctions, we can convert every existential-positive ∃Pos LOC τ formula ϕ is equivalent to a finite disjunction m i=1 ψi, where each ψi is a conjunctive query. For each such conjunctive query ψi, let Ai be the canonical finite structure associated with ψi, 1 ≤ i ≤ m. Note that such a canonical structure Ai need not be a member of C. Nonetheless, it is easy to see that every seg-minimal model B of ϕ in C is equal to a homomorphic image h(Ai) of one of the canonical finite structures Ai, 1 ≤ i ≤ m. Thus, the cardinality of every seg- minimal model of ϕ in C is less than or equal to the maximum cardinality of the canonical finite structures Ai, 1 ≤ i ≤ m, which implies that ϕ has finitely many seg-minimal models in C. This proves the lemma.

The proof is based on the fact that ∃Pos LOC τ sentence is a union of conjunctive queries (i.e., the ∃, ∧ fragment of FO LOC τ ), and that the canonical conjunctive query ϕ A of a structure A (i.e., the existential closure of the positive diagram of A) is definable in FO LOC τ as long as A = τ -conn(A).

The main consequence of Lemma 5.6 is that in order to establish that C has the homomorphism preservation property, it suffices to establish an upper bound on the size of the seg-minimal models. This is done by: Proposition 5.7. Let C be a class of στ -structures that is closed under disjoint unions and induced substructures. For every FO LOC τ sentence ϕ that is preserved under homomorphisms, there are r, m ∈ N such that if A is a seg-minimal model of ϕ, then A does not contain a σ, r-scattered set of size m.

The idea of the proof is as follows. Suppose ϕ is an FO LOC τ sentence preserved under homomorphisms. Let Σ = {ϕ1, . . . , ϕs} be a collection of basic local sentences of the form ( †) such that ϕ is equivalent to a Boolean combination of them. It exists by Theorem 4.4. For each i ≤ s, let ti be the locality radius, ni the width and ψ t i ,σ i (x) the local condition of ϕi. Also, let t = maxi ti and n = maxi ni. We take r = 2t and m = 2 s+|στ | + 1. For each i, we write θi(y) for the formula ∃x δσ(x, y) ≤ ti ∧ ψ t i ,σ i (x) . By means of contradiction, suppose that A is a model of ϕ so that A contains an σ, r-scattered set {c1, . . . , cm} of size m. Then, by definition N A|σ r (ci) ∩ N A|σ r (cj) = ∅ for i = j. Furthermore, since m > 2 s+|στ | , there are i and j with i = j such that

• for all l, A |= θ l (ci) if, and only if, A |= θ l (cj); and

• for all S ∈ στ , (ci, . . . , ci) ∈ S A if, and only if, (cj, . . . , cj) ∈ S A .

We then prove that there is some relation R ∈ στ so that there is some tuple ē ∈ R A so that ē includes ci and some other element a = ci. This implies that B = A| A\{c i } ⊕ A| {c i } is a proper segregated substructure of A, and thus B ∈ C. Take Bn to be the disjoint union of n copies of B. We then prove

A ⊕ Bn |= ϕ iff Bn |= ϕ. (5)
To prove this, we show that no ϕ l distinguishes between A ⊕ Bn and Bn. By symmetry, we restrict our attention to the case l = 1.

[⇐] Since Bn is isomorphic to an induced substructure of A ⊕ Bn, A ⊕ Bn satisfies ϕ1 if Bn does.

[⇒] We suppose that (A⊕Bn)|σ has a σ, 2t1-scattered subset X of cardinality n1 such that N (A⊕Bn)|σ t 1 (x) |= ψ1(x) for all x ∈ X and prove that Bn has such a subset X as well. The case n1 > 1 is easy. In this case, the t1-neighborhood of some x ∈ X does not contain any of the tuples of Ec i . Then, N B|σ t 1 (x) = N A|σ t 1 (x) and therefore each of the n summands of Bn has a t1-neighborhood isomorphic to N A|σ t 1 (x). Since n ≥ n1, we can take n1 distinct elements {x1, . . . , xn 1 } = X from Bn so that for every j ∈ Suppose then that n1 = 1 and let x be the only element of X. It suffices to prove that A contains an element y such that N A|σ t 1 (y) does not contain any of the tuples of Ec i and N A|σ t 1 (y) |= ψ1(y). If N A|σ t 1 (x) does not contain any of the tuples of Ec i , we have finished; so suppose that N A|σ t 1 (x) contains ē ∈ Ec i . Then δσ(ci, x) ≤ t1 and therefore N A|σ 2t 1 (ci) satisfies θ1(ci). Recall that ci is equivalent to cj and δσ(ci, cj) > 2r ≥ 4t1. Hence N A|σ 2t 1 (cj) satisfies θ1(cj) and does not contain any of the tuples of Ec i . Hence there exists y ∈ A such that N A|σ t 1 (y) |= ψ1(y) and N A|σ t 1 (y) is included in N A|σ 2t 1 (cj) and therefore does not contain any of the tuples of Ec i . This concludes the proof of (5).

Since ϕ is preserved under homomorphisms, and by assumption A |= ϕ, the existence of a homomorphism A → A ⊕ Bn implies A ⊕ Bn |= ϕ. By (5), we get Bn |= ϕ, and since we have a homomorphism Bn → B, we conclude B |= ϕ. As B is a proper segregated substructure of A in C, we have that A is not a seg- minimal model of ϕ. This contradiction proves the proposition.

We now conclude the proof. Let ϕ ∈ FO LOC τ be preserved under homomorphisms on C. By Proposition 5.7, there are r, m > 0 so that any seg-minimal model A of ϕ does not have a σ, r-scattered set of size m. Since the class is σ-wide, this implies that there is n > 0 so that every seg-minimal model A of ϕ has size at most n. Thus, up to isomorphism, there are finitely many seg- minimal models A of ϕ in C. This, by Lemma 5.6, implies that ϕ is equivalent to a ∃Pos LOC τ sentence.

Decidability of pattern logics

The main initial direction in the study of the data equality predicate for tree-like structures was to extend decidability results of logics for words and trees to those that admit data values as well [START_REF] Bojańczyk | Automata for data words and data trees[END_REF][START_REF] Bojańczyk | Two-variable logic on data words[END_REF][START_REF] Bojańczyk | Twovariable logic on data trees and XML reasoning[END_REF][START_REF] Segoufin | Static analysis of XML processing with data values[END_REF]. The motivation for this is static analysis of XML queries. The well known correspondence of XML structural properties and tree automata (cf. [START_REF] Vianu | A Web odyssey: From Codd to XML[END_REF]) gives us many decidable static analysis tasks, but the connection with automata fails when data values from an infinite set are added. Indeed, FO is undecidable over data trees (even data words). Hence, it was necessary to impose restrictions. The usual way of doing so is by restricting the number of variables: [START_REF] Bojańczyk | Twovariable logic on data trees and XML reasoning[END_REF] showed that FO 2 , first-order logic with two variables, is decidable over data trees, while FO 3 is not. Similar results hold for data words even in the presence of an order [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], and some extensions, of more automata-theoretic flavor, have been proposed as well [START_REF] Bojańczyk | Automata for data words and data trees[END_REF][START_REF] Tan | An automata model for trees with ordered data values[END_REF].

The problem with FO 2 is that it is quite restricted for XML querying. While some useful queries, in particular some fragments of XPath, can be captured by it [START_REF] Marx | Conditional XPath[END_REF], more expressive fragments of XPath, and crucially, more expressive queries that can use more complex patterns [START_REF] Amer-Yahia | Tree pattern query minimization[END_REF][START_REF] David | Containment of pattern-based queries over data trees[END_REF][START_REF] Marx | Conditional XPath[END_REF][START_REF] Miklau | Containment and equivalence for a fragment of XPath[END_REF][START_REF] Vianu | A Web odyssey: From Codd to XML[END_REF] are not captured at all by restricting the number of variables. At the same time, many such querying mechanisms are based on patterns, so perhaps one can recover decidability using pattern logics?

Decidability of pattern logics

By decidability of course we mean decidability of the satisfiability problem. A logic L is decidable on a class C if the following problem is decidable: given a sentence ϕ of L, check whether there exists A ∈ C so that A |= ϕ.

Our results show that in particular, the pattern logic is decidable on the class of ranked data trees. In fact we prove a more general result that allows other auxiliary relations on trees, not just the data equality predicate (e.g., other equivalence relations or linear orders).

Recall that by τ -trees we mean {ch} τ -structures where ch is interpreted as a child relation of a tree. Thus, we deal with the pattern logic FO PAT ch ({ch} τ ) over τ -trees. We now define conditions on τ that make it decidable. Those will go beyond having a single data-equality predicate ∼ in τ (i.e., beyond data trees).

Recall that root(A) stands for the root of a τ -tree, and A a is the {ch} τ -substructure induced by the subtree rooted at a. For τ -trees A1, . . . , Am ∈ C we define Σ C (A1, . . . , Am) as the set {A ∈ C | root(A) has exactly m children a1, . . . , am, and for all i ≤ m we have A ai = Ai}.

We say that C is an effective inductive class of τ -trees if three conditions hold:

1. Testing whether a structure A is in C is decidable; 2. C is closed under subtrees, i.e., for every A ∈ C and a ∈ A, the structure A a is in C;

3. for each r ≥ 0 and structures A1, . . . , Am ∈ C, the set • the sibling order relation sib,

{N A|σ r (root(A)) | A ∈ Σ C (A1, . . . , Am)} is computable from {N A i |σ r (root(Ai)) | 1 ≤ i ≤ m}.
• n equivalence relations ∼1, . . . , ∼n,

• m linear orders ≤1, . . . , ≤m, and

• l partial orders 1, . . . , l . This is an extension of the class of data trees, since one of the equivalence relations can be viewed as the data equality predicate. Corollary 6.2. The pattern logic FO PAT ch is decidable on ranked data trees, even expanded with a sibling order and an arbitrary number of equivalence relations and partial and linear orders.

The satisfiability problem for FO PAT ch is not affected by adding a prefix of existential monadic second order quantifiers: the proof goes through as before, with extra unary relations. Thus, if we define ∃MSO PAT σ (στ ) as formulae of the form ∃X1 . . . Xn ϕ, where ϕ is an FO PAT σ (σ τ {X1, . . . , Xn}) formula and X1, . . . , Xn are unary predicates, then we obtain: Corollary 6.3. The logic ∃MSO PAT ch is decidable on ranked data trees even with a sibling order and an arbitrary number of equivalence relations and partial and linear orders.

The reason Corollary 6.3 is useful is that many static analysis tasks for XML are considered with respect to a regular tree language [START_REF] Segoufin | Static analysis of XML processing with data values[END_REF], as regular languages provide a standard abstraction of XML schema languages [START_REF] Vianu | A Web odyssey: From Codd to XML[END_REF]. Thus, satisfiability of a logic L relative to a tree automaton is the following problem: given a tree automaton TA, and a formula ϕ of L, is there a tree (with extra relations such as the data equality relation) that satisfies ϕ and is accepted by TA?

Since encoding a tree automaton on a ranked tree is expressible in ∃MSO over vocabulary {ch, sib}, with references to sib local (i.e., restricted to ch-neighborhoods of radius 2), we obtain: Corollary 6.4. If C is an effective inductive class of ranked τtrees, then the satisfiability problem for FO PAT ch ({ch} τ ) relative to a tree automaton is decidable on C.

In particular, it is decidable whether a data tree satisfying a FO PAT ch sentence exists in a given regular tree language. Sketch of the proof of Theorem 6.1. The decidability result is another consequence of Gaifman locality theorem for the pattern logic. Let σ = {ch}, and let ϕ be a FO PAT σ (στ ) sentence, where τ is as in the statement of the theorem. In the proof we assume that τ contains a sibling order relation sib. This is without any loss of generality, since it can be shown that any effective inductive class of ranked trees continues to be effective inductive if we add the sibling order relation. By Theorem 4.4, ϕ is equivalent to a Boolean combination of basic FO PAT σ local sentences. Let r be the bound on the locality radius and let n be the bound on the width of these basic FO PAT σ local sentences.

The sibling number of an element a of a tree A is one plus the number of previous siblings it has in the order sib (note that the sibling number of the root is 1). Given two elements a, a from a tree A so that a is an ancestor of a , we write path(a, a ) ∈ N * to denote the string representing the path between a and a :

• if a = a then path(a, a ) = ε, the empty string,

• otherwise, path(a, a ) = path(a, a ) • i where i is the sibling number of a , and a is the parent of a .

For any k-ranked ordered τ -tree A with root a, consider the function ξ A with domain [1, r] × [1, n], so that for every r ∈ [1, r] and n ∈ [1, n], its value ξ A (r, n) is the set of all n-tuples (N A|σ r (a1), p1), . . . , (N A|σ r (a n), p n) so that a1, . . . , a n ∈ A, the distance δσ(ai, aj) is greater than 2 • r whenever i = j, and pi is defined as path(a, ai) if δσ(a, ai) ≤ 2 • r and as ∞ otherwise, for all i ≤ n. Note that there can be at most one i ∈ [1, n] so that |pi| ≤ r in each tuple (if there were two, they must be at distance ≤ 2 • r from each other). Note also that the sizes of N A|σ r (ai) are bounded by a function on k and r since C contains only k-ranked trees. Thus, it follows that once r and n are fixed, Ξ def = {(ξ A , N A|σ 2r (root(A))) | A ∈ C} is finite (assuming, of course, that we do not distinguish isomorphic structures). We will call (ξ A , N A|σ 2r (root(A))) the neighborhood description of A. Note that by Gaifman locality, whether A |= ϕ holds is determined by ξ A (and there is an effective procedure to verify this). We now show how to compute Ξ.

The key property to do this is the following lemma.

Lemma 6.5. Let a be the root of A ∈ C and let a1, . . . , am, for m ≤ k, be the children of a. Then ξ A is computable from ξ A a 1 , . . . , ξ A am and N A|σ 2r (a). Using the lemma, we can show that the following is the correct procedure to compute Ξ:

1. Let Ξ0 contain all (ξ A , A) such that A ∈ C and A is a singleton. 7. Repeat steps 3-6 until there is no change to Ξ. Now the decision procedure is simple: to verify whether ϕ is satisfiable, it suffices to test whether there is a neighborhood description in Ξ of a structure in which ϕ holds. Due to Gaifman locality theorem, whether A |= ϕ depends only on the neighborhood description of A and ϕ, and thus the theorem follows.

Undecidability results

A natural question is whether the decidability result continues to hold if trees need not be ranked. The answer to this is negative. We start with a simple observation that gives us undecidability for pattern logics with the next-sibling order relation sib.

Corollary 6.6. The pattern logic FO PAT ch,sib is undecidable on unranked data trees, even of height 1. This is a consequence of the undecidability of FO on data words [START_REF] Bojańczyk | Two-variable logic on data words[END_REF], since the entire tree of height one becomes a radiusone neighborhood of the root, and in the presence of the sibling ordering, it contains full FO on the data word of the root's children.

But even without the sibling order, the pattern logic is undecidable once the restriction to ranked trees is removed. Theorem 6.7. The logic FO PAT ch is undecidable over arbitrary data trees.

The proof is by encoding of 2-counter Minsky machines and reduction from the undecidability of their emptiness problem.

Conclusions

We have shown that pattern logics over structures with auxiliary relations behave quite well and preserve several properties of the underlying logic. We showed strong versions of Hanf and Gaifman locality theorems that do not use auxiliary relations in defining vertices of neighborhoods. We established a general homomor-phism preservation theorem that covers classes of structures not covered by previously known homomorphism preservation results. Finally, we proved decidability of the pattern logic for a large class of data trees. Note that the very notion of pattern logic is directly inspired by querying modern data models such as XML and graph databases. In fact our results can be applied to querying XML and graph data with incomplete information and to reasoning about XML with data values.

A few questions remain. The best homomorphism preservation result that we have is for unranked trees of moderate degree. We do not yet know if this restriction can be lifted. For instance, we do not know if the homomorphism preservation theorem holds if the σ-reduct has bounded treewidth, nor do we know what happens on unranked trees with the sibling order/successor. We also would like to explore connections between our results and those on invariance, in particular, we would like to see whether our techniques can be used to provide new results on the behavior of invariant queries. The fact that some common auxiliary relations (e.g., successor) can be defined locally, suggests that this might be a possible route for establishing new results in a notoriously hard area.

Figure 1 .

 1 Figure 1. Example of a data tree.

  A|σ r (ā) are those at distance ≤ r from ā in G(A|σ), the structure N A|σ r (a) contains all the induced relations of σ and τ . Given two στ -structures A and B, we write (A, ā) τ d (B, b) for ā ∈ A n and b ∈ B n if there exists a bijection f : A → B such that for every c ∈ A, N A|σ d (āc) ∼ = N B|σ d ( bf (c)). We say that a formula ϕ(x) is Hanf-τ -local if there exists a number d so that (A, ā) τ d (B, b) implies that A |= ϕ(ā) if and only if B |= ϕ( b).

Theorem 4 . 1 .

 41 Every formula of FO PAT σ (στ ) is Hanf-τ -local. Proof. This can be seen as a consequence of Proposition 3.2 and Hanf-locality of FO. Given a FO PAT σ (στ ) formula ϕ(x), let d be so that (A, ā) d (B, b) implies that A |= ϕ(ā) if and only if B |= ϕ( b). It exists by Hanf-locality of FO. Let r be the radius yielded by Proposition 3.2, so that A |= ϕ(ā) iff A τ,r |= ϕ(ā), where A τ,r is the (τ, r)-localization of A. We then have that d • r is the necessary radius

Corollary 4 . 2 .

 42 FO PAT σ (στ ) FO(στ ) if and only if τ has at least one relation of arity > 1. Proof. Let τ have a relation T of arity m > 1. Let ϕ say that T is nonempty, i.e., ∃x1, . . . , xm T (x1, . . . , xm). Assume ϕ is definable in FO PAT σ (στ ), and let d witness its Hanf-τ -locality. Take A to be a structure on an m-element universe {a1, . . . , am} in which all σ and τ relations are empty, and let B with the universe {b1, . . . , bm} be like A except that T B contains a single tuple (b1, . . . .bm). Since each neighborhood N A|σ r (a) is a singleton with all relations empty (and likewise for B), the map f : ai → bi, i ≤ m witnesses A τ d B. However, A |= ¬ϕ while B |= ϕ.

Corollary 4 . 3 .

 43 For every FO PAT σ (στ ) formula ϕ(x), there is a number r ≥ 0 so that N A|σ r (ā1) ∼ = N A|σ r (ā2) implies that ā1 and ā2 are indistinguishable by ϕ, i.e., A |= ϕ(ā1) ↔ ϕ(ā2). We can also show a strengthening of Gaifman's theorem for sentences. A basic FO PAT σ (στ ) local sentence is of the form ∃x1 . . . xn 1≤i<j≤n δσ(xi, xj) > 2r ∧ i≤n ψ r,σ (xi) , ( †)

[ 1 ,

 1 n1], xj is in the jth summand of Bn and N B|σ t 1 (xj) = N A|σ t 1 (x) (and therefore satisfies ψ1).

Theorem 6 . 1 .

 61 Let C be an effective inductive class of k-ranked τ -trees. Then FO PAT ch ({ch} τ ) is decidable on C. Before sketching the proof, we give a few corollaries. An example of an effective inductive class is the class of trees with

2 .

 2 Set Ξ := Ξ0.3. Let (ξ1, A1), . . . , (ξm, Am) ∈ Ξ for some m ∈ [1, k]. Thus, there are structuresA i ∈ C so that Ai = N A i |σ 2r (root(A i )) and ξi = ξ A i for all i ∈ [1, m].

4 .

 4 Let A ∈ {N A|σ 2r (root(A)) | A ∈ Σ C (A1, . . . , Am)}. All such A can be computed, since C is effective inductive and Ai = N

  A i |σ 2r (root(A i )) for each i ≤ m. 5. Compute ξ from {ξi} i∈[1,m] and A as in Lemma 6.5.6. Add (ξ , A ) to Ξ.

Acknowledgments We are very grateful to anonymous reviewers for their comments, especially for pointing out the current simple proofs of locality theorems in Section 4. Work supported by EP-SRC grant J015377.

A. Complete Proofs

Proofs from Section 3 Proof of Proposition 3.1

For any σ-pattern formula ∆ P (x), let ϕ(x) ∈ ∃Pos PAT σ (στ ) be the formula that results from replacing every occurrence of T (ȳ) so that T ∈ τ with T (ȳ) ∧ conn σ (ȳ, x) in ∆ P (x). Note that since the σ-reduct of the Gaifman graph of P is connected, we have that ∆ P (x) is equivalent to ϕ(x). Then, it follows that every FO PAT σ (στ ) formula is equivalent to a FO LOC τ (στ ) formula; and every ∃Pos PAT σ (στ ) formula is equivalent to a ∃Pos LOC τ (στ ) formula. Conversely, any conjunctive quantifier-free ∃Pos LOC τ (στ ) formula ϕ(x) is equivalent to a finite disjunction of σ-pattern formulae i ∆ Pi (x). Indeed, it is easy to see that the canonical structure A ϕ of ϕ = ∃x.ϕ is a disjoint union P 1 ⊕ • • • ⊕ P n of structures P i where G(P i | σ ) is connected for every i ∈ [1, n]. This is a consequence of the syntactic restriction of FO LOC τ (στ ) requiring any two elements in a tuple of a relation T ∈ τ to be connected through σ-relations. In other words, A ϕ is a disjoint union of σ-patterns over στ . Thus, ϕ(x) is equivalent to i∈ [1,n] ∆ Pi (ȳ i ), where ȳi , ranging over x, are the variables of the domain of P i . Therefore, every ∃Pos LOC τ (στ ) formula is equivalent to a ∃Pos PAT σ (στ ) formula; and every FO LOC τ (στ ) formula is equivalent to a FO PAT σ (στ ). Proof of Proposition 3.2 Let ϕ(x 1 , . . . , x n ) ∈ FO LOC τ with quantifier rank k, and let r = k + n. Suppose A is a στ -structure, R ∈ τ , and (b 1 , . . . , b m ) ∈ R A , so that for some i, j ∈ [1, m], b i and b j are at distance > r, that is, N A|σ r (b i ) ∩ N A|σ r (b j ) = ∅. Let A be the structure resulting from removing (b 1 , . . . , b m ) from R A in A. One can easily show by induction on the quantifier rank of ϕ that, for every a 1 , . . . , a n ∈ A we have A |= ϕ(a 1 , . . . , a n ) ⇔ A |= ϕ(a 1 , . . . , a n ). This is because, by definition of FO LOC τ , ϕ can only test for R(x 1 , . . . , x m ) in conjunction with conn σ (x 1 , . . . , x m , y 1 , . . . , y s ) for some y 1 , . . . , y s , which specifies that the elements denoted by x 1 , . . . , x m , y 1 , . . . , y s form a connected component, and thus that every pair x i , x j is at distance ≤ |{x 1 , . . . , x m , y 1 , . . . , y s }| ≤ n + k = r. By repeating this argument for all tuples b in a relation in τ which are not r-local, it follows that, for every structure A and a 1 , . . . , a n in A, we have A |= ϕ(a 1 , . . . , a n ) if and only if  |= ϕ(a 1 , . . . , a n ), where  is the (τ, r)-localization of A.

Proofs from Section 5

Proof of Theorem 5.1

Due to Proposition 3.1, it suffices to prove the result for FO LOC τ . As before, we omit the στ vocabulary from notations when it is clear from the context.

That each formula of ∃Pos LOC τ is preserved under homomorphisms is immediate by a straightforward induction on the structure of the formula. Thus, we show the opposite direction.

We say that B is a segregated substructure of A if there are pairwise disjoint subsets A 1 , . . . , A n of A so that B = A| A1 ⊕ • • • ⊕ A| An . We write for the substructure relation, ind for the induced substructure relation, and seg to the segregated substructure relation. Note that an induced substructure is a segregated substructure, and a segregated substructure is a substructure. Note also that any class of structures that is closed under disjoint unions and induced substructures is also closed under segregated substructures.

Note that a class of structures C is closed under disjoint unions and induced substructures iff it is closed under disjoint unions and segregated substructures.

For a sentence ϕ preserved under homomorphisms on a class of structures C, we say that A ∈ C is a minimal model of ϕ in C if A |= ϕ and for every proper substructure B A such that B ∈ C, we have B |= ϕ.

We will occasionally use the term conjunctive query [START_REF] Abiteboul | Foundations of Databases[END_REF] to denote both formulae of the form ∃x 1 , . . . , x n θ, where θ is a conjunction of atomic formulae. Every finite structure A with n elements gives rise to a canonical conjunctive query ϕ A , which is the existential closure of its positive diagram, i.e., ϕ A = ∃x∆ A (x), where x is the set of all variables used in ∆ A . Conversely, every conjunctive query ϕ = ∃x 1 , . . . , x n θ gives rise to a canonical structure A ϕ with n elements, known as its tableau [START_REF] Abiteboul | Foundations of Databases[END_REF], where the elements of A are the variables x 1 , . . . , x n , and the relations of A consist of the tuples of variables in the conjuncts of θ.

The following well known result (cf. [START_REF] Abiteboul | Foundations of Databases[END_REF][START_REF] Grädel | Finite Model Theory and its Applications[END_REF]) will be useful for us. If A and B are two finite structures, then

Not all structures have a canonical conjunctive query that is a formula of FO LOC τ . Nevertheless, those structures A so that A = τ -conn(A) do have a canonical FO LOC τ conjunctive query.

Lemma A.1. For every A so that A = τ -conn(A), the canonical conjunctive query ϕ A is definable in FO LOC τ .

Proof. Note that any two elements a, b of A related by a relation T ∈ τ belong to the same connected component, and thus

Before showing the following easy Lemma, we notice that, from the definition of FO LOC τ we have that for every structure A and FO LOC τ sentence ϕ,

Lemma 5.6. Let C be a class of finite στ -structures closed under segregated substructures and let ϕ be a FO LOC τ sentence that is preserved under homomorphisms on C. Then the following are equivalent:

(1) ϕ has finitely many seg -minimal models in C.

(2) ϕ is equivalent on C to a ∃Pos LOC τ sentence.

Proof.

(1) ⇒ (2) Take any seg -minimal model A of ϕ. Note that A must be so that τ -conn(A) = A, since otherwise τ -conn(A) would be a strict segregated substructure of A where τ -conn(A) |= ϕ, by [START_REF] Barceló | Querying graph databases[END_REF]. Indeed, τ -conn(A) ∈ C by the hypothesis, and hence A would not be seg -minimal. Let ϕ A be the canonical conjunctive FO LOC τ query of A (it is definable in FO LOC τ due to Lemma A.1). We define the existential positive formula ψ as the disjunction of all ϕ A for each seg -minimal model A of ϕ. We next show that ψ and ϕ are equivalent.

Note that, by ( 6), we have that

and hence there is a homomorphism from A to B, by [START_REF] Atserias | On preservation under homomorphisms and unions of conjunctive queries[END_REF]. Since A |= ϕ and ϕ is closed under homomorphisms, then B |= ϕ. Conversely, if B |= ϕ there must be some seg -minimal A seg B so that A |= ϕ. Hence, ψ contains ϕ A as a disjunct, meaning that A |= ψ.

(2) ⇒ (1) By propagating disjunctions, we can convert every existential-positive ∃Pos LOC τ formula ϕ is equivalent to a finite disjunction m i=1 ψ i , where each ψ i is a conjunctive query. For each such conjunctive query ψ i , let A i be the canonical finite structure associated with ψ i , 1 ≤ i ≤ m. Note that such a canonical structure A i need not be a member of C. Nonetheless, it is easy to see that every seg -minimal model B of ϕ in C is equal to a homomorphic image h(A i ) of one of the canonical finite structures A i , 1 ≤ i ≤ m. Thus, the cardinality of every seg -minimal model of ϕ in C is less than or equal to the maximum cardinality of the canonical finite structures A i , 1 ≤ i ≤ m, which implies that ϕ has finitely many seg -minimal models in C.

The main consequence of this lemma is that in order to establish that C has the homomorphism preservation property, it suffices to establish an upper bound on the size of the seg -minimal models. To be precise, we aim to prove that for any ϕ there is an N such that no seg -minimal model of ϕ is larger than N . Proposition 5.7. Let C be a class of στ -structures that is closed under disjoint unions and induced substructures. For every FO LOC τ sentence ϕ that is preserved under homomorphisms, there are r, m ∈ N such that if A is a segminimal model of ϕ, then A does not contain a σ, r-scattered set of size m.

Proof. Suppose ϕ is an FO LOC τ sentence of quantifier rank q that is preserved under homomorphisms. Let Σ = {ϕ 1 , . . . , ϕ s } be a collection of basic FO LOC τ local sentences (obtained by Theorem 4.4) such that ϕ is equivalent to a Boolean combination of them. For each i, let t i be the radius of locality, n i the width and ψ i (x) the local condition of ϕ i . Also, let t = max i t i and n = max i n i . We take r = 2t and m = 2 s+|στ | + 1. For each i, we write θ i (y) for the following formula

By means of contradiction, suppose that A is a model of ϕ so that A| σ contains an σ, r-scattered set {c 1 , . . . , c m } of size m. Then, by definition

there are i and j with i = j such that (a) for all l, A |= θ l (c i ) if, and only if, A |= θ l (c j ); and (b) for all S ∈ στ , (c i , . . . , c i ) ∈ S A if, and only if, (c j , . . . , c j ) ∈ S A . We first show that there is some relation R ∈ στ so that there is some tuple ē ∈ R A so that ē includes c i and some other element a = c i . Assume towards a contradiction that there is no such relation R ∈ στ . Let B be the induced substructure of A obtained by removing c i . Note that there is a homomorphism from A to B identifying c i with c j and being the identity on all other elements from A \ {c i }, thanks to condition (b). Since ϕ is preserved under homomorphisms, it follows that B is a model of ϕ, and thus that A is not seg -minimal. This is in contradiction with our hypothesis.

Hence, B = A| A\{ci} ⊕ A| {ci} is a proper segregated substructure of A, and thus B ∈ C. Let E ci be the set of all tuples removed from A in order to obtain B. Note that all of them contain c i in one component. Take B n to be the structure that is the disjoint union of n copies of B, and take A ⊕ B n to be the disjoint union of A and B n . We show that the structures A ⊕ B n and B n must agree on the sentence ϕ.

Proof. We show that no ϕ l distinguishes between A ⊕ B n and B n . By symmetry, we restrict our attention to the case l = 1.

[⇐] Since B n is isomorphic to an induced substructure of

for all x ∈ X and prove that B n has such a subset X as well. The case n 1 > 1 is easy. In this case, the t 1 -neighborhood of some x ∈ X does not contain any of the tuples of E ci . Then, N Since ϕ is preserved under homomorphisms, and there are homomorphisms from A to A ⊕ B n and from B n to B, it follows that if A is a model of ϕ, so is B. Thus, since B is a proper segregated substructure of A in C, the latter is not a seg -minimal model of ϕ.

We now conclude the proof. Let ϕ ∈ FO LOC τ be preserved under homomorphisms on C. By Proposition 5.7, there are r, m > 0 so that a seg -minimal model A of ϕ has an σ, r-scattered set of size m in G(A| σ ). Since the class is σ-wide, this implies that there is n > 0 so that every seg -minimal model A of ϕ has size at most n. Thus, up to isomorphism, there are finitely many seg -minimal models A of ϕ in C. This, by Lemma 5.6, implies that ϕ is preserved under homomorphisms on C.

Proof of Corollary ??

Let C be a class of forests of moderate degree; assume that f (n) is the maximum degree in a forest having n nodes. We show that C is ch-wide; that will suffice to conclude the corollary.

Fix r, m > 0. Let d = (2r + 2)m, and let ε = 1 d+1 . Then, for all n ≥ m d+1 , we have n m

Thus, for some N 0 depending on m and r, we have for all n ≥ N 0 :

Indeed, otherwise we would have n m < f (n) d for arbitrarily large n, and thus f (n) > n m 1/d ≥ n ε for arbitrarily large n, which is impossible since C is of moderate degree. Suppose we have a forest of size n for n > N 0 . Assume that it has m or more connected components. Then it clearly has an r-scattered set of size m. So assume it has fewer than m connected components (trees); then at least one of them, t, is of size at least n/m. We know that if we we have a tree of branching factor at most k and size at least k d , then it has a branch of length at least d. Since

, we see that t 0 has a branch of length d = (2r + 2)m. Therefore, this branch alone has enough elements to have an r-scattered set of size m.

Proofs from Section 6

Proof of Theorem 6.1

The decidability result is another consequence of Gaifman locality theorem for the pattern logic. Let σ = {ch}, and let ϕ be a FO PAT σ (στ ) sentence, where τ is as in the statement of the theorem. In the proof we assume that τ contains a sibling order relation sib. This is without any loss of generality, since it can be shown that any effective inductive class of ranked trees continues to be effective inductive if we add a sibling order relation. By Theorem 4.4, ϕ is equivalent to a Boolean combination of basic FO PAT σ local sentences. Let r be the bound on the locality radius and let n be the bound on the width of these basic FO PAT σ local sentences. The sibling number of an element a of a tree A is one plus the number of previous siblings it has in the order sib (note that the sibling number of the root is 1). Given two elements a, a from a tree A so that a is an ancestor of a , we write path(a, a ) ∈ N * to denote the Dewey-style string representing the path between a and a :

• if a = a then path(a, a ) = ε, the empty string,

• otherwise, path(a, a ) = path(a, a ) • i where i is the sibling number of a , and a is the parent of a .

For any k-ranked ordered τ -tree A with root a, consider the function ξ A with domain [1, r] × [1, n], so that for every r ∈ [1, r] and n ∈ [1, n], its value ξ A (r, n) is the set of all n-tuples (N A|σ r (a 1 ), p 1 ), . . . , (N A|σ r (a n), p n) so that a 1 , . . . , a n ∈ A, the distance δ σ (a i , a j ) is greater than 2 • r whenever i = j, and

for all i (see Figure 2 for an example). Note that there can be at most one i ∈ [1, n] so that |p i | ≤ r in each tuple (if there were two, they must be at distance ≤ 2 • r from each other). Note also that the sizes of N A|σ r (a i ) are bounded by a function on k and r since C contains only k-ranked trees. Thus, it follows that once r and n are fixed,

Henceforward we will call (ξ A , N A|σ 2r (root(A))) the neighborhood description of A. Note that by Gaifman locality, whether A |= ϕ holds is determined by ξ A (and there is an effective procedure to verify this). We now show how to compute Ξ.

The key property to do this is the following.

Idea of the abstraction of a tuple of ξ A , for n = 3. Gray balls represent non-intersecting neighborhoods of three elements a1, a2, a3. a1 is so that δσ(a, a1) ≤ 2 • r, whereas a2 and a3 are at distance more than 2 • r from a.

Proof. It is easy to construct, for all r ∈ [1, r] and n ∈ [1, n], all n-tuples of ξ A (r, n) of the form

for every i, based solely on the information contained in ξ A a1 (r, n), . . . , ξ A am (r, n). Indeed, it suffices to take any n elements (A 1 , j 1 • p 1 ), . . . , (A n, j n • p n) so that

• there are tuples t j1 ∈ ξ A aj 1 , . . . , t jn ∈ ξ A aj n ,

• every (A i , p i ) appears in a component k i of t ji , and • there are no two i = i with k i = k i and j i = j i (i.e., we don't repeat twice the same component).

We must then show how to build the tuples containing some (N A|σ r (c i ), p i ) where δ σ (a, c i ) ≤ r (or, in other words, where |p i | ≤ r). Note that any such c i is in N Let us first assume that (a) holds, and let us fix (N A|σ r (c), l • p ) as a component of an n-tuple we want to output. The remaining n -1 components are chosen to be (A 1 , p 1 ), . . . , (A n-1 , p n-1 ) so that

• for some t l ∈ ξ A al (r, n), k p ∈ [1, n], and A we have that (A , p ) is in the k p -component of t l ,

• for every i ∈ [1, n -1] there exists j i ∈ [1, m],

• for every i ∈ [1, n -1] there exists a tuple t ji ∈ ξ A aj i (r, n) and a component k i ∈ [1, n] of t ji (if j i = l, the tuple t l is the one described in the previous item), • for every i ∈ [1, n -1] we have that (A i , p i ) appears in the k i -component of t ji , and either p i = p i = ∞ or p i = j i • p i and |p | + δ σ (a l , a ji ) + |p i | > 2 • r, that is, the distance between c and the element denoted by p i is greater than 2 • r. (Note that this condition can only be true if j i = l.) • There are no repeated elements, that is, there are no i = i so that j i = j i and k i = k i .

The remaining case (b) is only easier.

Notice that this gives a method for computing all n-tuples of r-neighborhood descriptions of A. It then follows that ξ A is computable from ξ A a1 , . . . , ξ A am and N A|σ 2r (a). Using the Lemma above, the procedure to compute Ξ is as follows:

1. Let Ξ 0 contain all (ξ A , A) such that A ∈ C and A is a singleton. [1,m] and A as in Lemma 6.5.

Set

6. Add (ξ , A ) to Ξ.

7. Repeat steps 3-6 until there is no change to Ξ.

First note that all the neighborhood descriptions in the algorithm output Ξ correspond to neighborhood descriptions of structures from C. This is because Ξ is initialized by neighborhood descriptions of all the singletons of C (note that C contains singletons because it is closed under subtrees), and every (ξ , A ) added to Ξ is so that A is the 2r-neighborhood of some tree A ∈ C due to effective inductiveness, and ξ = ξ A due to Lemma 6.5.

On the other hand, we show that Ξ contains all the neighborhood descriptions of the elements of C. Due to steps 1-2, Ξ contains all the neighborhood descriptions of trees of height 0. Suppose now that Ξ contains all the neighborhood descriptions of trees of height h, and let A be a tree of height h + 1 with m children of the root a 1 , . . . , a m . Since C is closed under subtrees, A a 1 , . . . , A a m ∈ C, and thus (ξ 1 , A 1 ), . . . , (ξ m , A m ) ∈ Ξ where

(a i ) and ξ i = ξ Ai for all i ∈ [1, m]. By steps 3-6, and due to C being effective inductive, it follows that (ξ A , N A|σ 2r (root(A))) ∈ Ξ. Now the decision procedure is very simple. To verify whether ϕ is satisfiable, it suffices to test whether there is a neighborhood description in Ξ of a structure in which ϕ holds. As already mentioned, due to Gaifman locality theorem, whether A |= ϕ depends only on the neighborhood description of A and ϕ, and thus the theorem follows.

Proof of Theorem 6.7

The proof goes by reduction from the emptiness problem for 2-counter Minsky machine M. An accepting run of M is a sequence (q 0 , t 0 , q 1 ), (q 1 , t 1 , q 2 ), . . . , (q n-1 , t n , q n ) of transitions from its set δ of transitions, so that q 0 is the initial state, q n the final state and for every i, (q i , t i , q i+1 ) is a transition of the machine, where t i ∈ {inc, dec, zero} × {1, 2}.

In the conditions below we make reference to "uncles" and "nephews" of nodes, meaning the siblings of the parent and the children of siblings of the parent respectively. One can code this run in a data trees as follows:

• There are |δ| + 6 monadic predicates, one for every transition in δ and also the predicates:

• At every node there is exactly one monadic predicate that holds, that we call "label".

• There is exactly one branch whose every node has a label from δ. This branch starts at the root and ends at a leaf. Further, the root's label starts with the initial state and the leaf's label ends with a final state. For every non-leaf node of this branch, the ending state is equal to the starting state of the child's node. Every other node not belonging to this branch is a leaf. The idea is that the number of siblings labeled c 1 (resp. c 2 ) code the value of counter 1 (resp. counter 2) at that point of the run.

• For every node labeled with some (q, t, q ), all its siblings have pairwise distinct data values. If t = (inc, 1) then it has exactly one child labeled c + 1 (if it is not a leaf), otherwise it has no children labeled c + 1 . If t = (dec, 1) then it has exactly one uncle labeled c - 1 , otherwise it has no uncles labeled c - 1 . A similar condition holds for (inc, 2)/(dec, 2) and c + 2 /c - 2 . In other words, a node labeled c + i contains a new data value that enforces that the counter i has one more sibling than in the previous step. On the other hand, a node labeled c - i contains a data value that does not appear in the coding of counter i of the next step of the run, thus ensuring that counter i decrements by one its encoded value.

• For every node labeled c 1 there is a nephew labeled c 1 with the same data value, unless it has no nephews (idem with c 2 ).

• For every node labeled c 1 there is an uncle labeled c 1 with the same data value, unless it has no uncles (idem with c 2 ).

• Every node labeled c + 1 has no uncles with the same data values (idem with c + 2 ). • Every node labeled c - 1 has no nephews with the same data value (idem with c 2 ). It is easy to see that all these properties can be expressed in FO LOC τ , and that there is a data tree satisfying these properties if, and only if, M has an accepting run. Note that this reduction uses necessarily the fact that the data tree is unranked, as otherwise, as we have seen in Theorem 6.1, it would be decidable.