Pablo Barceló
email: pbarcelo@dcc.uchile.cl

AND Diego Figueira
email: dfigueir@inf.ed.ac.uk

Leonid Libkin
email: libkin@inf.ed.ac.uk

Pablo Barcel Ó

P Barcel

Graph Logics with Rational Relations

Keywords: 1998 ACM Subject Classification: F.4.3 Formal Languages, H.2.3 Database languages, query languages, F.2 Analysis of algorithms and problem complexity Regular relations, Rational relations, Recognizable relations, intersection problem, RPQ, graph databases, non primitive recursive

come   L'archive ouverte pluridisciplinaire

Introduction

The motivation for the problems investigated in this paper comes from the study of logics for querying graphs. Such logics form the basis of query languages for graph databases, that have recently found numerous applications in areas including biological networks, social networks, Semantic Web, crime detection, etc. (see [START_REF] Angles | Survey of graph database models[END_REF] for a survey) and led to multiple systems and prototypes. In such applications, data is usually represented as a labeled graph. For instance, in social networks, people are nodes, and labeled edges represent different types of relationship between them; in RDF -the underlying data model of the Semantic Webdata is modeled as a graph, with RDF triples naturally representing labeled edges.

The questions that we address are related to the interaction of various classes of relations on words, for instance, rational relations (examples of those include subword and subsequence) or regular relations (such as prefix, or equality of words). An example of a question we are interested in is as follows: is it decidable whether a given regular relation contains a pair (w, w ) so that w is a subword/subsequence of w ? Problems like this are very basic and deserve a study on their own, but they are also necessary to answer questions on the power and complexity of querying graph databases. We now explain how they arise in that setting.

Logical languages for querying graph data have been developed since the late 1980s (and some of them became precursors of languages later used for XML). They query the topology of the graph, often leaving querying data that might be stored in the nodes to a standard database engine. Such logics are quite different in their nature and applications from another class of graph logics based on spatial calculi [START_REF] Cardelli | A spatial logic for querying graphs[END_REF][START_REF] Dawar | Expressiveness and complexity of graph logic[END_REF]. Their formulae combine various reachability patterns. The simplest form is known as regular path queries (RPQs) [START_REF] Cruz | A graphical query language supporting recursion[END_REF][START_REF] Consens | GraphLog: a visual formalism for real life recursion[END_REF]; they check the existence of a path whose label belongs to a regular language. Those are typically used as atoms and then closed under conjunction and existential quantification, resulting in the class of conjunctive regular path queries (CRPQs), which have been the subject of much investigation [START_REF] Calvanese | Containment of conjunctive regular path queries with inverse[END_REF][START_REF] Deutsch | Optimization properties for classes of conjunctive regular path queries[END_REF][START_REF] Florescu | Query containment for conjunctive queries with regular expressions[END_REF]. For instance, a CRPQ may ask for a node v such that there exist nodes v 1 and v 2 and paths from v to v i with the label in a regular language L i , for i = 1, 2.

The expressiveness of these queries, however, became insufficient in applications such as the Semantic Web or biological networks due to their inability to compare paths. For instance, it is a common requirement in RDF languages to compare paths based on specific semantic associations [START_REF] Anyanwu | ρ-Queries: enabling querying for semantic associations on the semantic web[END_REF]; biological sequences often need to be compared for similarity, based, for example, on the edit distance.

To address this, an extension of CRPQs with relations on paths was proposed [START_REF] Barceló | Expressive languages for path queries over graph-structured data[END_REF]. It used regular relations on paths, i.e., relations given by synchronized automata [START_REF] Elgot | On relations defined by generalized finite automata[END_REF][START_REF] Frougny | Synchronized rational relations of finite and infinite words[END_REF]. Equivalently, these are the relations definable in automatic structures on words [START_REF] Benedikt | Definable relations and first-order query languages over strings[END_REF][START_REF] Blumensath | Automatic structures. 15th Annual IEEE Symposium on Logic in Computer Science (LICS)[END_REF][START_REF] Bruyère | Logic and p-recognizable sets of integers[END_REF]. They include prefix, equality, equal length of words, or fixed edit distance between words. The extension of CRPQs with them, called ECRPQs, was shown to have acceptable complexity (NLogSpace with respect to data, PSpace with respect to query).

However, the expressive power of ECRPQs is still short of the expressiveness needed in many applications. For instance, semantic associations between paths used in RDF applications often deal with subwords or subsequences, but these relations are not regular. They are rational: they are still accepted by automata, but those whose heads move asynchronously. Adding them to a query language must be done with extreme care: simply replacing regular relations with rational in the definition of ECRPQs makes query evaluation undecidable! So we set out to investigate the following problem: given a class of graph queries, e.g., CRPQs or ECRPQs, what happens if one adds the ability to test whether pairs of paths belong to a rational relation S, such as subword or subsequence? We start by observing that this problem is a generalization of the intersection problem: given a regular relation R, and a rational relation S, is R ∩ S = ∅? It is well known that there exist rational relations S for which it is undecidable [START_REF] Berstel | Transductions and Context-Free Languages[END_REF]; however, we are not interested in artificial relations obtained by encoding PCP instances, but rather in very concrete relations used in querying graph data.

The intersection problem captures the essence of graph logics ECRPQs and CRPQs (for the latter, when restricted to the class of recognizable relations [START_REF] Berstel | Transductions and Context-Free Languages[END_REF][START_REF] Choffrut | Relations over words and logic: a chronology[END_REF]). In fact, query evaluation can be cast as the generalized intersection problem. Its input includes an m-ary regular relation R, a binary rational relation S, and a set I of pairs from {1, . . . , m}. It asks whether there is a tuple (w 1 , . . . , w m ) ∈ R so that (w i , w j ) ∈ S whenever (i, j) ∈ I. For m = 2 and I = {(1, 2)}, this is the usual intersection problem.

Another motivation for looking at these basic problems comes from verification of lossy channel systems (finite-state processes that communicate over unbounded, but lossy, FIFO channels). Their reachability problem is known to be decidable, although the complexity is not bounded by any multiply-recursive function [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF]. In fact, a "canonical" problem used in reductions showing this enormous complexity [START_REF] Chambart | Post embedding problem is not primitive recursive, with applications to channel systems[END_REF][START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF] can be restated as follows: given a binary rational relation R, does it have a pair (w, w ) so that w is a subsequence of w ? This naturally leads to the question whether the same bounds hold for the simpler instance of the intersection problem when we use regular relations instead of rational ones. We actually show that this is true. Summary of results. We start by showing that evaluating CRPQs and ECRPQs extended with a rational relation S can be cast as the generalized intersection problem for S with recognizable and regular relations respectively. Moreover, the complexity of the basic intersection problem is a lower bound for the complexity of query evaluation.

We then study the complexity of the intersection problem for fixed relations S. For recognizable relations, it is well known to be efficiently decidable for every rational S. For regular relations, we show that if S is the subword, or the suffix relation, then the problem is undecidable. That is, it is undecidable to check, given a binary regular relation R, whether it contains a pair (w, w ) so that w is a subword of w , or even a suffix of w . We also present a generalization of this result.

The analogous problem for the subsequence relation is known to be decidable, and, if the input is a rational relation R, then the complexity is non-multiply-recursive [START_REF] Chambart | Post embedding problem is not primitive recursive, with applications to channel systems[END_REF]. We extend this in two ways. First, we show that the lower bound remains true even for regular relations R. Second, we extend decidability to the class of all rational relations for which one projection is closed under subsequence (the subsequence relation itself is trivially such, obtained by closing the first projection of the equality relation).

In addition to establishing some basic facts about classes of relations on words, these results tell us about the infeasibility of adding rational relations to ECRPQs: in fact adding subword makes query evaluation undecidable, and while it remains decidable with subsequence, the complexity is prohibitively high.

So we then turn to the generalized intersection problem with recognizable relations, corresponding to the evaluation of CRPQs with an extra relation S. We show that the shape of the relation I holds the key to decidability. If its underlying undirected graph is acyclic, then the problem is decidable in PSpace for every rational relation S (and for a fixed formula the complexity drops to NLogSpace). In the cyclic case, the problem is undecidable for some rational relation S. For relations generalizing subsequence, we have decidability when I is a DAG, and for subsequence itself, as well as for suffix, query evaluation is decidable regardless of the shape of CRPQs.

Thus, under the mild syntactic restriction of acyclicity of comparisons with respect to rational relations, such relations can be added to the common class CRPQ of graph queries, without incurring a high complexity cost.

Organization. We give basic definitions in Section 2 and define the main problems we study in Section 3. Section 4 introduces graph logics and establishes their connection with the (generalized) intersection problem. Section 5 studies decidable and undecidable cases of the intersection problem. Section 6 looks at the case of recognizable relations and CRPQs and establishes decidability results based on the intersection pattern.

Preliminaries

Let N = {1, 2, . . . }, [i..j] = {i, i + 1, . . . , j} (if i > j, [i..j] = ∅), [i] = [1..i]. Given, A, B ⊆ N, an increasing function f : A → B is one such that f (i) ≥ f (j) whenever i > j. If f (i) > f (j) we call it strictly increasing.

Alphabets, languages, and morphisms. We shall use letters Σ, Γ to denote finite alphabets. The set of all finite words over an alphabet Σ is denoted by Σ * . We write ε for the empty word, w • w for the concatenation of two words, and |w| for the length of a word w. Given a word w ∈ Σ * , w[i..j] stands for the substring in positions [i..j], w[i] for w[i..i], and w[i..] for w[i..|w|]. Positions in the word start with 1.

If w = w • u • w , then • u is a subword of w (also called factor in the literature, written as u w),

• w is a prefix of w (written as w pref w), and • w is a suffix of w (written as w suff w). We say that w is a subsequence of w (also called subword embedding or scattered subword in the literature, written as w w) if w is obtained by removing some letters (perhaps none) from w, i.e., w = a 1 . . . a n , and

w = a i 1 a i 2 . . . a i k , where 1 ≤ i 1 < i 2 < . . . < i k ≤ n.
If Σ ⊂ Γ and w ∈ Γ * , then by w Σ we denote the projection of w on Σ. That is, if w = a 1 . . . a n and a i 1 , . . . , a i k are precisely the letters from Σ, with i 1 < . . . < i k , then

w Σ = a i 1 . . . a i k .
Recall that a monoid M = U, •, 1 has an associative binary operation • and a neutral element 1 satisfying 1x = x1 = x for all x (we often write xy for x • y). The set Σ * with the operation of concatenation and the neutral element ε forms a monoid Σ * , •, ε , the free monoid generated by Σ. A function f : M → M between two monoids is a morphism if it sends the neutral element of M to the neutral element of M , and if

f (xy) = f (x)f (y) for all x, y ∈ M . Every morphism f : Σ * , •, ε → M is uniquely determined by the values f (a), for a ∈ Σ, as f (a 1 . . . a n ) = f (a 1 ) • • • f (a n ). A morphism f : Σ * , •, ε → Γ * , •, ε is called alphabetic if f (a) ∈ Γ ∪ {ε},
and strictly alphabetic if f (a) ∈ Γ for each a ∈ Σ, see [START_REF] Berstel | Transductions and Context-Free Languages[END_REF].

A language L is a subset of Σ * , for some finite alphabet Σ. It is recognizable if there is a finite monoid M , a morphism f : Σ * , •, ε → M , and a subset M 0 of M such that

L = f -1 (M 0 ).
A language L is regular if there exists an NFA (non-deterministic finite automaton) A = Q, Σ, q 0 , δ, F such that L = L(A), the language of words accepted by A. We use the standard notation for NFAs, where Q is the set of states, q 0 is the initial state, F is the set of final states, and

δ ⊆ Q × Σ × Q is the transition relation.
A language is rational if it is denoted by a regular expression; such expressions are built from ∅, ε, and alphabet letters by using operations of concatenation (e • e ), union (e ∪ e ), and Kleene star (e * ). It is of course a classical result of formal language theory that the classes of recognizable, regular, and rational languages coincide.

Recognizable, regular, and rational relations. While the notions of recognizability, regularity, and rationality coincide over languages L ⊆ Σ * , they differ over relations over Σ, i.e., subsets of Σ * × . . . × Σ * . We now define those (see [START_REF] Berstel | Transductions and Context-Free Languages[END_REF][START_REF] Carton | Decision problems among the main subfamilies of rational relations[END_REF][START_REF] Choffrut | Relations over words and logic: a chronology[END_REF][START_REF] Elgot | On relations defined by generalized finite automata[END_REF][START_REF] Frougny | Synchronized rational relations of finite and infinite words[END_REF][START_REF] Thomas | Infinite trees and automaton-definable relations over ω-words[END_REF]).

Since Σ * , •, ε is a monoid, the product (Σ * ) n has the structure of a monoid too. We can thus define recognizable n-ary relations over Σ as subsets R ⊆ (Σ * ) n so that there exists a finite monoid M and a morphism f : (Σ * ) n → M such that R = f -1 (M 0 ) for some M 0 ⊆ M . The class of n-ary recognizable relations will be denoted by REC n ; when n is clear or irrelevant, we write just REC.

It is well-known that a relation R ⊆ (Σ * ) n is in REC n iff it is a finite union of the sets of the form L 1 × . . . × L n , where each L i is a regular language over Σ, see [START_REF] Berstel | Transductions and Context-Free Languages[END_REF][START_REF] Elgot | On relations defined by generalized finite automata[END_REF].

Next, we define the class of regular relations. Let ⊥ ∈ Σ be a new alphabet letter, and let Σ ⊥ be Σ ∪ {⊥}. Each tuple w = (w 1 , . . . , w n ) of words from Σ * can be viewed as a word over Σ n ⊥ as follows: pad words w i with ⊥ so that they all are of the same length, and use as the kth symbol of the new word the n-tuple of the kth symbols of the padded words. Formally, let = max i |w i |. Then w 1 ⊗ . . . ⊗ w n is a word of length whose kth symbol is (a 1 , . . . , a n ) ∈ Σ n ⊥ such that

a i = the kth letter of w i if |w i | ≥ k ⊥ otherwise.
We shall also write ⊗ w for w 1 ⊗ . . . ⊗ w n . We define

π i (u 1 ⊗ • • • ⊗ u k ) = u i for all i ∈ [k]. A relation R ⊆ (Σ * ) n is called a regular n-ary relation over Σ if there is a finite automaton A over Σ n ⊥ that accepts {⊗ w | w ∈ R}.
The class of n-ary regular relations is denoted by REG n ; as before, we write REG when n is clear or irrelevant.

Finally, we define rational relations. There are two equivalent ways of doing it. One uses regular expressions, which are now built from tuples ā ∈ (Σ ∪ {ε}) n using the same operations of union, concatenation, and Kleene star. Binary relations suff , , and are all rational: the expression a∈Σ (ε, a) Alternatively, n-ary rational relations can be defined by means of n-tape automata, that have n heads for the tapes and one additional control; at every step, based on the state and the letters it is reading, the automaton can enter a new state and move some (but not necessarily all) tape heads. The classes of n-ary relations so defined are called rational n-ary relations; we use the notation RAT n or just RAT, as before.

Relationships between classes of relations. While it is well known that REC 1 = REG 1 = RAT 1 , we have strict inclusions

REC k REG k RAT k
for every k > 1 (see for example [START_REF] Berstel | Transductions and Context-Free Languages[END_REF]). For instance

, pref ∈ REG 2 -REC 2 and suff ∈ RAT 2 -REG 2 .
The classes of recognizable and regular relations are closed under intersection; however the class of rational relations is not. In fact, one can find R ∈ REG 2 and S ∈ RAT 2 so that

R ∩ S ∈ RAT 2 . However, if R ∈ REC m and S ∈ RAT m , then R ∩ S ∈ RAT m .
Binary rational relations can be characterized as follows [START_REF] Berstel | Transductions and Context-Free Languages[END_REF][START_REF] Nivat | Transduction des langages de Chomsky[END_REF]. A relation R ⊆ Σ * × Σ * is rational iff there is a finite alphabet Γ, a regular language L ⊆ Γ * and two alphabetic morphisms f, g : Γ * → Σ * such that R = {(f (w), g(w)) | w ∈ L}. If we require f and g to be strictly alphabetic morphisms, we get the class of length-preserving regular relations, i.e., R ∈ REG 2 so that (w, w ) ∈ R implies |w| = |w |. Regular binary relations are then finite unions of relations of the form

{(w • u, w ) | (w, w ) ∈ R, u ∈ L} and {(w, w • u) | (w, w ) ∈ R, u ∈ L},
where R ranges over length-preserving regular relations, and L over regular languages.

Properties of classes of relations. Since relations in REC and REG are given by NFAs, they inherit all the closure/decidability properties of regular languages. If R ∈ RAT, then each of its projections is a regular language, and can be effectively constructed (e.g., from the description of R as an n-tape automaton). Hence, the nonemptiness problem is decidable for rational relations. However, testing nonemptiness of the intersection of two rational relations is undecidable [START_REF] Berstel | Transductions and Context-Free Languages[END_REF]. Also, for R, R ∈ RAT, the following are undecidable: checking whether R ⊆ R or R = R , universality (R = Σ * × Σ * ), and checking whether R ∈ REG or R ∈ REC [START_REF] Berstel | Transductions and Context-Free Languages[END_REF][START_REF] Carton | Decision problems among the main subfamilies of rational relations[END_REF][START_REF] Lisovik | The identity problem for regular events over the direct product of free and cyclic semigroups[END_REF].

Remark. We defined recognizable, regular, and rational relations over the same alphabet, i.e., as subsets of (Σ * ) n . Of course it is possible to define them as subsets of Σ 1 × . . . × Σ n , with the Σ i 's not necessarily distinct. Technically, there are no differences and all the results will continue to hold. Indeed, one can simply consider a new alphabet Σ as the disjoint union of Σ i 's, and enforce the condition that the ith projection only use the letters from Σ i (this is possible for all the classes of relations we consider). In fact, in the proofs we shall be using both types of relations.

Well-quasi-orders. A well-quasi-order ≤ ⊆ A × A is a reflexive and transitive relation such that for every infinite sequence (a i ) i∈N over A there are i < j with a i ≤ a j . We will make use of the following two lemmas. Lemma 2.1 (Higman's Lemma [START_REF] Higman | Ordering by divisibility in abstract algebras[END_REF]). For every alphabet Σ, the subsequence relation ⊆ Σ * × Σ * is a well quasi-order. Lemma 2.2 (Dickson's Lemma [START_REF] Dickson | Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors[END_REF]). For every well-quasi-order ≤ ⊆ A × A, the product order

≤ k ⊆ A k × A k (where (a 1 , . . . , a k ) ≤ k (a 1 , . . . , a k ) iff a i ≤ a i for all i ∈ [k]
) is a well-quasi-order.

Generalized intersection problem

We now formalize the main technical problem we study. Let R be a class of relations over Σ, and S a class of binary relations over Σ. We use the notation [m] for {1, . . . , m}. If R is an m-ary relation, S is a binary relation, and I ⊆ [m] 2 , we write R ∩ I S for the set of tuples (w 1 , . . . , w m ) in R such that (w i , w j ) ∈ S whenever (i, j) ∈ I.

The generalized intersection problem (R ∩ I S)

?
= ∅ is defined as:

Problem: (R ∩ I S) ? = ∅ Input: an m-ary relation R ∈ R, a relation S ∈ S, and I ⊆ [m] 2 Question: is R ∩ I S = ∅?
If S = {S}, we write S instead of {S}. We write GenInt S (R) for the class of all problems (R ∩ I S) ? = ∅ where S is fixed, i.e., the input consists of R ∈ R and I. As was explained in the introduction, this problem captures the essence of evaluating queries in various graph logics, e.g., CRPQs or ECRPQs extended with rational relations S. The classes R will typically be REC and REG.

If m = 2 and I = {(1, 2)}, the generalized intersection problem becomes simply the intersection problem for the classes R and S of binary relations:

Problem: (R ∩ S) ? = ∅ Input: R ∈ R and S ∈ S Question: is R ∩ S = ∅?
The problem (REC ∩ S) ? = ∅ is decidable for every rational relation S, simply by constructing R ∩ S, which is a rational relation, and testing its nonemptiness. However, (REG ∩ S) ? = ∅ could already be undecidable (we shall give one particularly simple example later).

Graph logics and the generalized intersection problem

In this section we show how the (generalized) intersection problems provide us with upper and lower bounds on the complexity of evaluating a variety of logical queries over graphs. We start by recalling the basic classes of logics used in querying graph data, and show that extending them with rational relations allows us to cast the query evaluation problem as an instance of the generalized intersection problem. The key observations are that:

• the complexity of GenInt S (REC) and (REC ∩ S) ? = ∅ provide an upper and a lower bound for the complexity of evaluating CRPQ(S) queries; and • for ECRPQ(S), these bounds are provided by the complexity of GenInt S (REG) and of (REG ∩ S) ? = ∅. The standard abstraction of graph databases [START_REF] Angles | Survey of graph database models[END_REF] is finite Σ-labeled graphs G = V, E , where V is a finite set of nodes, or vertices, and

E ⊆ V × Σ × V is a set of labeled edges. A path ρ from v 0 to v m in G is a sequence of edges (v 0 , a 0 , v 1 ), (v 1 , a 1 , v 2 ), • • • , (v m-1 , a m-1 , v m ) from E, for some m ≥ 0. The label of ρ, denoted by λ(ρ), is the word a 0 • • • a m-1 ∈ Σ * .
The main building blocks for graph queries are regular path queries, or RPQs [START_REF] Cruz | A graphical query language supporting recursion[END_REF]; they are expressions of the form x L → y, where L is a regular language. We normally assume that L is represented by a regular expression or an NFA. Given a Σ-labeled graph G = V, E , the answer to an RPQ above is the set of pairs of nodes (v, v ) such that there is a path ρ from v to v with λ(ρ) ∈ L.

Conjunctive RPQs, or CRPQs [START_REF] Calvanese | Containment of conjunctive regular path queries with inverse[END_REF][START_REF] Calvanese | View-based query processing and constraint satisfaction[END_REF][START_REF] Consens | GraphLog: a visual formalism for real life recursion[END_REF] are the closure of RPQs under conjunction and existential quantification. Formally, they are expressions of the form

ϕ(x) = ∃ȳ m i=1 (u i L i -→ u i ) (4.1)
where variables u i , u i s come from x, ȳ. The semantics naturally extends the semantics of RPQs: ϕ(ā) is true in G iff there is a tuple b of nodes such that for every i ≤ m and every v i , v i interpreting u i and u i , respectively, we have a path ρ i between v i and v i whose label

λ(ρ i ) is in L i .
CRPQs can further be extended to compare paths. For that, we need to name path variables, and choose a class of allowed relations on paths. The simplest such extension is the class of CRPQ(S) queries, where S is a binary relation over Σ * . Its formulae are of the form

ϕ(x) = ∃ȳ m i=1 (u i χ i :L i -→ u i ) ∧ (i,j)∈I S(χ i , χ j ) (4.2)
where I ⊆ [m] 2 . We use variables χ 1 , . . . , χ m to denote paths; these are quantified existentially. That is, the semantics of G |= ϕ(ā) is that there is a tuple b of nodes and paths ρ k , for k ≤ m, between v k and v k (where, as before, v k , v k are elements of ā, b interpreting u k , u k ) such that (λ(ρ i ), λ(ρ j )) ∈ S whenever (i, j) ∈ I. For instance, the query ∃y, y (x

χ:Σ * a -→ y) ∧ (x χ :Σ * b -→ y ) ∧ χ χ
finds nodes v so that there are two paths starting from v, one ending with an a-edge, whose label is a subsequence of the other one, that ends with a b-edge.

The input to the query evaluation problem consists of a graph G, a tuple v of nodes, and a query ϕ(x); the question is whether G |= ϕ(v). This corresponds to the combined complexity of query evaluation. In the context of query evaluation, one is often interested in data complexity, when the typically small formula ϕ is fixed, and the input consists of the typically large graph (G, v). We now relate it to the complexity of GenInt S (REC). Lemma 4.1. Fix a CRPQ(S) query ϕ as in (4.2). Then there is a DLogSpace algorithm that, given a graph G and a tuple v of nodes, constructs an m-ary relation R ∈ REC so that the answer to the generalized intersection problem (R ∩ I S)

? = ∅ is 'yes' iff G |= ϕ(v).
Proof. Given a Σ-labeled graph G = V, E and two nodes v, v , we write A(G, v, v ) for G viewed as an NFA with the initial state v and the final state v (that is, the set of states is V , the transition relation is E, and the alphabet is Σ). The language of such an automaton, L(A(G, v, v )), is the set of labels of all paths between v and v . Now consider a CRPQ(S) query ϕ(x) given by

∃ȳ m i=1 (u i χ i :L i -→ u i ) ∧ (i,j)∈I S(χ i , χ j ) ,
as in (4.2). Suppose we are given a graph G as above and a tuple of nodes v, of the same length as the length of x. The DLogSpace algorithm works as follows.

First we enumerate all tuples b of nodes of G of the same length as ȳ; since ϕ is fixed, this can be done in DLogSpace. For each b, we construct an m-ary relation Rb in REC as follows. Let n i and n i be the interpretations of u i and u i , when x is interpreted as v and ȳ as b. Then

Rb = m i=1 (L(A(G, n i , n i )) ∩ L i ).
Note that it can be constructed in DLogSpace; indeed each coordinate of Rb is simply a product of the automaton A(G, n i , n i ) and a fixed automaton defining L i . Next, let R = b Rb. This is constructed in DLogSpace too. Now it follows immediately from the construction that R ∩ I S = ∅ iff for some b, there exist paths ρ i between n i , n i , for i ≤ m, such that (λ(ρ l ), λ(ρ j )) ∈ S whenever (l, j) ∈ I, i.e., iff G |= ϕ(v).

Conversely, the intersection problem for recognizable relations and S can be encoded as answering CRPQ(S) queries. Lemma 4.2. For any given binary relation S, there is a CRPQ(S) query ϕ(x, x ) and a DLogSpace algorithm that, given a relation R ∈ REC 2 , constructs a graph G and two nodes v, v so that

G |= ϕ(v, v ) iff R ∩ S = ∅. Proof. Let R be in REC 2 . It is given as n i=1 (L i × K i )
, where the L i s and the K i s are regular languages over Σ. These languages are given by their NFAs which we can view as Σ-labeled graphs. Let V i , E i be the underlying graph of the NFA defining L i , such that v i 0 is the initial state, and F i is the set of final states. Likewise, let W i , H i be the underlying graph of the NFA defining K i , such that w i 0 is the initial state, and C i is the set of final states.

We now construct the graph G. Its labeling alphabet is the union of Σ and {#, $, !}. Its set of vertices is the disjoint union of all the V i s, W i s, as well as two distinguished nodes start and end. Its edges include all the edges from E i s and H i s, and the following:

• #-labeled edges from start to each initial state, i.e., to each v 0 i and w 0 i for all i ≤ n. • $-labeled edges between the initial states of automata with the same index, i.e., edges (v i 0 , $, w i 0 ) for all i ≤ n. • !-labeled edges from final states to end, i.e., edges (v, !, end), where v ∈ i≤n F i ∪ i≤n C i . We now define a CRPQ(S) query ϕ(x, y) (omitting path variables for paths that are not used in comparisons):

∃x 1 , x 2 , z 1 , z 2         x # → x 1 ∧ x # → x 2 ∧ x 1 $ → x 2 ∧ x 1 χ:Σ * → z 1 ∧ x 2 χ :Σ * → z 2 ∧ z 1 ! → y ∧ z 2 ! → y ∧ S(χ, χ )        
The query says that from start, we have #-edges to the initial states v i 0 and w i 0 : they must have the same index since there is a $-edge between them. From there we have two paths, ρ and ρ , corresponding to the variables χ and χ , which are Σ-labeled, and thus are paths in the automata for L i and K i , respectively. From the end nodes of those paths we have !-edges to end, so they must be final states; in particular, λ(ρ) ∈ L i and λ(ρ ) ∈ K i . We finally require (λ(ρ), λ(ρ )) ∈ S, i.e., (λ(ρ), λ(ρ )) ∈ (L i ×K i )∩S. Hence, if G |= ϕ(start, end) then for some i ≤ n we have two words (w, w ) that belong to (L i × K i ) ∩ S, i.e., R ∩ S = ∅. Conversely, if R ∩ S = ∅, then (L i × K i ) ∩ S = ∅ for some i ≤ n, and the witnessing paths of the nonemptiness of (L i × K i ) ∩ S will witness the formula ϕ(start, end) (together with initial states of the automata of L i and K i and some of their final states).

Combining the lemmas, we obtain: Theorem 4.3. Let K be a complexity class closed under DLogSpace reductions. Then:

(1) If the problem GenInt S (REC) is in K, then data complexity of CRPQ(S) queries is in K; and (2) If the problem (REC ∩ S) ? = ∅ is hard for K, then so is data complexity of CRPQ(S) queries.

We now consider extended CRPQs, or ECRPQs, which enhance CRPQs with regular relations [START_REF] Barceló | Expressive languages for path queries over graph-structured data[END_REF], and prove a similar result for them, with the role of REC now played by REG. Formally, ECRPQs are expressions of the form

ϕ(x) = ∃ȳ m i=1 (u i χ i :L i -→ u i ) ∧ k j=1 R j ( χj ) (4.3)
where each R j is a relation from REG, and χj a tuple from χ 1 , . . . , χ m of the same arity as R j . The semantics of course extends the semantics of CRPQs: the witnessing paths ρ 1 , . . . , ρ m should also satisfy the condition that for every atom R(ρ i 1 , . . . , ρ i l ) in (4.3), the tuple (λ(ρ i 1 ), . . . , λ(ρ i l )) is in R. Finally, we obtain ECRPQ(S) queries by adding comparisons with respect to a relation S ∈ RAT, getting a class of queries ϕ(x) of the form

∃ȳ m i=1 (u i χ i :L i -→ u i ) ∧ k j=1 R j ( χj ) ∧ (i,j)∈I S(χ i , χ j ) (4.4)
Similarly to the case of CRPQs, we can establish a connection between data complexity of ECRPQ(S) queries and the complexity of the generalized intersection problem: Theorem 4.4. Let K be a complexity class closed under DLogSpace reductions. Then:

(1) If the problem GenInt S (REG) is in K, then data complexity of ECRPQ(S) queries is in K; and (2) If the problem (REG∩S) ? = ∅ is hard for K, then so is data complexity of ECRPQ(S) queries.

Similarly to the proof of Theorem 4.3, the result will be an immediate consequence of two lemmas. First, evaluation of ECRPQ(S) queries is reducible to the generalized intersection problem for regular relations. Lemma 4.5. Fix an ECRPQ(S) query ϕ as in (4.4). Then there is a DLogSpace algorithm that, given a graph G and a tuple v of nodes, constructs an m-ary relation R ∈ REG so that the answer to the generalized intersection problem (R ∩ I S)

? = ∅ is 'yes' iff G |= ϕ(v).
Conversely, the intersection problem for regular relations and S can be encoded as answering ECRPQ(S) queries. Lemma 4.6. For each binary relation S, there is an ECRPQ(S) query ϕ(x, x ) and a DLogSpace algorithm that, given a relation R ∈ REG 2 , constructs a graph G and two nodes v, v so that

G |= ϕ(v, v ) iff (R ∩ S) = ∅.
The proof of Lemma 4.5 is almost the same as the proof of Lemma 4.1: as before, we enumerate tuples b, construct relations Rb and R = b Rb, but this time we take the product of this recognizable relation with regular relations mentioned in the query. Since the query is fixed, and hence we take a product with a fixed number of fixed automata, such a product construction can be done in DLogSpace. The result is now a regular m-ary relation. The rest of the proof is exactly the same as in Lemma 4.1.

We now prove Lemma 4.6. Let R ∈ REG 2 be given by an NFA over

Σ ⊥ × Σ ⊥ whose underlying graph is G R = V R , E R , where E R ⊆ V R × (Σ ⊥ × Σ ⊥ ) × V R . Let v 0 be
its initial state, and let F be the set of final states.

We now define the graph G. Its labeling alphabet Γ is the disjoint union of Σ ⊥ × Σ ⊥ , the alphabet Σ itself, and a new symbol #. Its nodes V include all nodes in V R and two extra nodes, v f and v . The edges are:

• all the edges in E R ;

• edges (v, #, v f ) for every v ∈ F ;

• edges (v , a, v ) for every a ∈ Σ. We now define two regular relations over Γ. The first, R 1 , consists of pairs (w, w ), where w ∈ (Σ ⊥ × Σ ⊥ ) * and w ∈ Σ * . Furthermore, w is of the form w ⊗ w for some w ∈ Σ * . It is straightforward to check that this relation is regular. The second one, R 2 , is the same except w is of the form w ⊗ w . In other words, the first component is w 1 ⊗ w 2 , and the second is either w 1 or w 2 , for R 1 or R 2 , respectively.

Next, we define the ECRPQ(S) ϕ(x, y):

∃x 1 , y 1 , x 2 , y 2 , z    x χ:Σ ⊥ ×Σ ⊥ → z ∧ z # → y ∧ x 1 χ 1 :Σ * → y 1 ∧ x 2 χ 2 :Σ * → y 2 ∧ R 1 (χ, χ 1 ) ∧ R 2 (χ, χ 2 ) ∧ S(χ 1 , χ 2 )   
Note that when this formula is evaluated over G, with x interpreted as v 0 and y interpreted as v f , the paths χ 1 and χ 2 can have arbitrary labels from Σ * . Paths χ can have arbitrary labels over Σ ⊥ × Σ ⊥ ; however, since they start in v 0 and must be followed by an #-edge, they end in a final state of the automaton for R, and hence labels of these paths are precisely words in Σ ⊥ ×Σ ⊥ of the form w 1 ⊗w 2 , where (w 1 , w 2 ) ∈ R. Now R 1 ensures that the label of χ 1 is w 1 and that the label of χ 2 is w 2 . Hence the labels of χ 1 and χ 2 are precisely the pairs of words in R, and the query asks whether such a pair belongs to S. Hence,

G |= ϕ(v 0 , v f ) iff R ∩ S = ∅.
It is straightforward to check that the construction of G can be carried out in DLogSpace. This proves the lemma and the theorem. Thus, our next goal is to understand the behaviors of the generalized intersection problem for various rational relations S which are of interest in graph logics; those include subword, suffix, subsequence. In fact to rule out many undecidable or infeasible cases it is often sufficient to analyze the intersection problem. We do this in the next section, and then analyze the decidable cases to come up with graph logics that can be extended with rational relations.

The intersection problem: decidable and undecidable cases

We now study the problem (REG ∩ S) ? = ∅ for binary rational relations S such as subword and subsequence, and for classes of relations generalizing them. The input is a binary regular relation R over Σ, given by an NFA over Σ ⊥ × Σ ⊥ . The question is whether R ∩ S = ∅. We also derive results about the complexity of ECRPQ(S) queries. For all lower-bound results in this section, we assume that the alphabet contains at least two symbols.

As already mentioned, there exist rational relations S such that (REG ∩ S)

?
= ∅ is undecidable. However, we are interested in relations that are useful in graph querying, and that are among the most commonly used rational relations, and for them the status of the problem was unknown.

Note that the problem (REC ∩ S)

?
= ∅ is tractable: given R ∈ REC, the relation R ∩ S is rational, can be efficiently constructed, and checked for nonemptiness. 5.1. Undecidable cases: subword and relatives. We now show that even for such simple relations as subword and suffix, the intersection problem is undecidable. That is, given an NFA over Σ ⊥ × Σ ⊥ defining a regular relation R, the problem of checking for the existence of a pair (w, w ) ∈ R with w suff w or w w is undecidable. As an immediate consequence of this, we obtain: Corollary 5.2. The query evaluation problem for ECRPQ( suff ) and ECRPQ( ) is undecidable.

Thus, some of the most commonly used rational relations cannot be added to ECRPQs without imposing further restrictions.

We skip the proof of Theorem 5.1 for the time being and concentrate first on how to obtain a more general undecidability result out of it. As we will see below, the essence of the undecidability result is that relations such as suff and can be decomposed in a way that one of the components of the decomposition is a graph of a nontrivial strictly alphabetic morphism. More precisely, let R • R be the binary relation

{(w • w , u • u ) | (w, u) ∈ R and (w , u ) ∈ R }. Let Graph(f ) be the graph of a function f : Σ * → Σ * , i.e., {(w, f (w)) | w ∈ Σ * }.
Proposition 5.3. Let R 0 , R 1 be binary relations on Σ such that R 0 is recognizable and its second projection is Σ * . Let f be a strictly alphabetic morphism that is not constant (i.e. the image of f contains at least two letters). Then, for

S = R 0 • Graph(f ) • R 1 , the problem (REG ∩ S) ? = ∅ is undecidable.
Note that both suff and are of the required shape: suffix is ({ε}

× Σ * ) • Graph(id) • ({ε} × {ε}), and subword is ({ε} × Σ * ) • Graph(id) • ({ε} × Σ * )
, where id is the identity alphabetic morphism.

Proofs of Theorem 5.1 and Proposition 5.3. We present the proof for the suffix relation suff . The proofs for the subword relation, and more generally, for the relations containing the graph of an alphabetic morphism follow the same idea and will be explained after the proof for suff . The proof is by encoding nonemptiness for linearly bounded automata (LBA). Recall that an LBA A has a tape alphabet Γ that contains two distinguished symbols, α and β, which are the left and the right marker. The input word w ∈ (Γ -{α, β}) * is written between them, i.e., the content of the input tape is α • w • β. The LBA behaves just like a Turing machine, except that when it is reading α or β, it cannot rewrite them, and it cannot move left of α or right of β. The problem of checking whether the language of a given LBA is nonempty is undecidable.

We encode this as follows. The alphabet Σ is the disjoint union of the tape alphabet Γ of the LBA A, the set of its states Q, and the designated symbol $ (we assume, of course, that these are disjoint). A configuration C of the LBA consists of the tape content a 0 . . . a n , where a 0 = α and a n = β, and all the a i s, for 0 < i < n, are letters from Γ -{α, β}, the state q, and the position i, for 0 ≤ i ≤ n, that the head is pointing to. We encode this as a word w C = $a 0 . . . a i-1 qa i . . . a n $ ∈ Σ * of length n + 4. Of course if the head is pointing to α, the configuration is $qa 0 . . . a n $. Note that if we have a run of the LBA with configurations C 0 , C 1 , . . ., then the lengths of all the w C i s are the same.

Next, note that the relation

R A imm = {(w C , w C ) | C is an immediate successor of C} is regular (in fact
such a relation is well-known to be regular even for arbitrary Turing machines [START_REF] Benedikt | Definable relations and first-order query languages over strings[END_REF][START_REF] Blumensath | Automatic structures. 15th Annual IEEE Symposium on Logic in Computer Science (LICS)[END_REF][START_REF] Bruyère | Logic and p-recognizable sets of integers[END_REF]). Since all configurations are of the same length, we obtain that the relation

R A = {(w C 0 w C 1 . . . w Cm , w C 1 . . . w C m ) | C i+1 is an immediate successor of C i for i < m}
is regular too (since only one configuration in the first projection does not correspond to a configuration in the second projection). By taking the product with a regular language that ensures that the first symbol from Q in a word is q 0 , and the last such symbol is from F , we have a regular relation

R A = (w C 0 w C 1 . . . w Cm , w C 1 . . . w C m ) C i+1 is an immediate successor of C i for i < m; C 0 is an initial configuration ; C m is a final configuration
which can be effectively constructed from the description of the LBA. Now assume that R A ∩ suff is nonempty. Then, since all encodings of configurations are of the same length, it must contain a pair (w

C 0 w C 1 . . . w Cm , w C 1 . . . w Cm ) such that C i+1
is an immediate successor of C i for all i < m. Since C 0 is an initial configuration and C m is a final configuration, this implies that the LBA has an accepting computation. Conversely, if there is an accepting computation with a sequence of configurations C 0 , C 1 , . . . , C m of the LBA, then the pair (w C 0 w C 1 . . . w Cm , w C 1 . . . w Cm ) is both in R A and in the suffix relation. Hence, R A ∩ suff is nonempty iff there is an accepting computation of the LBA, proving undecidability.

The proof for the subword relation is practically the same. We change the definition of relation R A so that there is an extra $ symbol inserted between w C 0 and w C 1 , and two extra $ symbols after w Cm in the first projection; in the second projection we insert extra two $ symbols before w C 1 and after w C m . Note that the relation remains regular: even if the components are not fully synchronized, at every point there is a constant delay between them (either 2 or 1), and this can be captured by simply encoding one or two alphabet symbols into the state. Since in each word there are precisely two places where the subword $$$ appears, the subword relation in this case becomes the suffix relation, and the previous proof applies.

The same proof can be applied to deduce Proposition 5.3. Note that we can encode letters of alphabet Σ within the alphabet {0, 1} so that the encodings of each letter of Σ will have the same length, namely log 2 (|Γ| + |Q| + 1) . Then the same proof as before will apply to show undecidability over the alphabet {0, 1}, since the encodings of configurations still have the same length.

Since R 0 is regular, it is of the form i L i × K i , and by the assumption, i K i = Σ * . Thus, the encoding of the initial configuration will belong to one of the K i s, say K j . We then take a fixed word w 0 ∈ L j and assume that the second component of the relation starts with w 0 (which can be enforced by the regular relation). Likewise, we take a fixed pair (w 1 , w 2 ) ∈ R 1 , and assume that w 1 is the suffix of the first component of the relation, and w 2 is the suffix of the second. This too can be enforced by the regular relation. Now if we have a non-constant alphabetic morphism f , we have two letters, say a and b, so that f (a) = f (b). We now simply use these letters, with a playing the role of 0, and b playing the role of 1 in the first projection of relation R, and f (a), f (b) playing the roles of 0 and 1 in the second projection, to encode the run of an LBA as we did before. The only difference is that instead of a sequence of $ symbols to specify the positions of the encoding we use a (fixed-length) sequence that is different from w 0 , w 1 , w 2 above, to identify its position uniquely. Then the proof we have presented above applies verbatim. 5.2. Decidable cases: subsequence and relatives. We now show that the intersection problem is decidable for the subsequence relation and, much more generally, for a class of relations that do not, like the relations considered in the previous section, have a "rigid" part. More precisely, the problem is also decidable for any relation so that its projection on the first component is closed under subsequence. However, the complexity bounds are extremely high. In fact we show that the complexity of checking whether (R ∩ ) = ∅, when R ranges over REG 2 , is not bounded by any multiply-recursive function. This was previously known for R ranging over RAT 2 , and was viewed as the simplest problem with non-multiply-recursive complexity [START_REF] Chambart | Post embedding problem is not primitive recursive, with applications to channel systems[END_REF]. We now push it further and show that this high complexity is already achieved with regular relations. Some of the ideas for showing this come from a decidable relaxation of the Post Correspondence Problem (PCP), namely the regular Post Embedding Problem, or PEP reg , introduced in [START_REF] Chambart | Post embedding problem is not primitive recursive, with applications to channel systems[END_REF]. An instance of this problem consists of two morphisms σ, σ : Σ * → Γ * and a regular language L ⊆ Σ * ; the question is whether there is some w ∈ L such that σ(w) σ (w) (recall that in the case of the PCP the question is whether σ(w) = σ (w) with L = Σ + ). We call w a solution to the instance (σ, σ , L). The PEP reg problem is known to be decidable, and as hard as the reachability problem for lossy channel systems [START_REF] Chambart | Post embedding problem is not primitive recursive, with applications to channel systems[END_REF] which cannot be bounded by any primitive-recursive function -in fact, by any multiply-recursive function (a generalization of primitive recursive functions with hyper-Ackermannian complexity, see [START_REF] Rose | Subrecursion: Functions and Hierarchies[END_REF]). More precisely, it is shown in [?] to be precisely at the level F ω ω of the fast-growing hierarchy of recursive functions [START_REF] Löb | Hierarchies of number theoretic functions[END_REF][START_REF] Rose | Subrecursion: Functions and Hierarchies[END_REF]. 1 1 In this hierarchy-also known as the Extended Grzegorczyk Hierarchy-, the classes of functions Fα are closed under elementary-recursive reductions, and are indexed by ordinals. Ackermannian complexity corresponds to level α = ω, and level α = ω ω corresponds to some hyper-Ackermannian complexity.

The problem PEP reg is just a reformulation of the problem (RAT ∩ ) ? = ∅. Indeed, relations of the form {(f (w), g(w)) | w ∈ L}, where L ⊆ Σ * ranges over regular languages and f, g over morphisms Σ * → Γ * are precisely the relations in RAT 2 [START_REF] Berstel | Transductions and Context-Free Languages[END_REF][START_REF] Nivat | Transduction des langages de Chomsky[END_REF]. Hence, (RAT ∩ ) ? = ∅ is decidable, with non-multiply-recursive complexity.

Proposition 5.4 ([13]). (RAT ∩ )

? = ∅ is decidable, non-multiply-recursive.
We show that the lower bound already applies to regular relations.

Theorem 5.5. The problem (REG ∩ ) ? = ∅ is decidable, and its complexity is not bounded by any multiply-recursive function.

The proof of the theorem above will be shown further down, after some preparatory definitions and lemmas are introduced.

It is worth noticing that one cannot solve the problem (REG∩ ) ?

= ∅ by simply reducing to nonemptiness of rational relations due to the following. Proposition 5.6. There is a binary regular relation R such that (R ∩ ) is not rational.

Proof. Let Σ = {a, b}, and consider the following regular relation,

R = {(a m , b m • a m ) | m, m ∈ N}. Note that the relation R ∩ is then {(a m , b m • a m ) | m, m ∈ N, m ≥ m}.
We show that R ∩ is not rational by means of contradiction. Suppose that it is, and let A be an NFA over {a, b, ε} × {a, b, ε} that recognizes R ∩ . Suppose Q is the set of states of A, and |Q| = n.

Consider the following pair

(a n+1 , b n+1 • a n+1 ) ∈ R ∩ .
Then there must be some u ∈ ({a, b, ε} × {a, b, ε}) * such that

(π 1 (u), π 2 (u)) = (a n+1 , b n+1 • a n+1 )
and u ∈ L(A). Let ρ A : [0..|u|] → Q be the accepting run of A on u, and let 1

≤ i 1 < • • • < i n+1 ≤ |u| be such that π 2 (u[i j ]) = a for all j ∈ [n + 1]. Clearly, among ρ A (i 1 ), . . . , ρ A (i n+1 )
there must be two repeating elements by the pigeonhole principle. Let 1 ≤ j 1 < j 2 ≤ n + 1 be such elements, where ρ

A (i j 1 ) = ρ A (i j 2 ). Hence u = u[1..i j 1 -1] • u[i j 2 ..] ∈ L(A), and therefore π 1 (u ), π 2 (u ) ∈ R ∩ . Notice that π 2 (u ) = b n+1 • a n+1-(j 2 -j 1 )
. But by definition of R ∩ we have that π 1 (u ) = a n+1 with n + 1 -(j 2j 1 ) ≥ n + 1, which is clearly false. The contradiction comes from the assumption that R ∩ is rational.

As already mentioned, the decidability part of Theorem 5.5 follows from Proposition 5.4. We prove the lower bound by reducing PEP reg into (REG ∩ ) ? = ∅. This reduction is done in two phases. First, we show that there is a reduction from PEP reg into the problem of finding solutions of PEP reg with a certain shape, which we call a strict codirect solutions (Lemma 5.7). Second, we show that there is a reduction from the problem of finding strict codirect solutions of a PEP reg instance into (REG ∩ ) ? = ∅ (Proposition 5.8). Both reductions are elementary and thus the hardness result of Theorem 5.5 follows.

In the next section we define the strict codirect solutions for PEP reg , showing that we can restrict to this kind of solutions. In the succeeding section we show how to reduce the problem into (REG ∩ ) ? = ∅.

5.2.1.

Codirect solutions of PEP reg . There are some variations of the PEP reg problem that result being equivalent problems. These variations restrict the solutions to have certain properties. Given a PEP reg instance (σ, σ , L), we say that w ∈ L with |w| = m is a codirect solution if there are (possibly empty) words v 1 , . . . , v m such that 1.

v k σ (w[k]) for all 1 ≤ k ≤ m, 2. σ(w[1..m]) = v 1 • • • v m , and 3. |σ(w[1..k])| ≥ |v 1 • • • v k | for all 1 ≤ k ≤ m. If furthermore 4. |σ(w[1..k])| > |v 1 • • • v k | for all 1 ≤ k < m,
we say that it is a strict codirect solution. In this case we say that the solution w is witnessed by v 1 , . . . , v m . In [START_REF] Chambart | Post embedding problem is not primitive recursive, with applications to channel systems[END_REF] it has been shown that the problem of whether an instance of the PEP reg problem has a codirect solution is equivalent to the problem of whether it has a solution. Moreover, it can be shown that this also holds for strict codirect solutions.

Lemma 5.7. The problem of whether a PEP reg instance has a strict codirect solution is as hard as whether a PEP reg instance has a solution.

Proof. We only show how to reduce from finding a codirect solution problem to finding a strict codirect solution problem. The other direction is trivial, since a strict codirect solution is in particular a solution. Let (σ, σ , L) be a PEP reg instance, and w ∈ L be a codirect solution with |w| = m, minimal in size, and witnessed by v 1 , . . . , v k . Let A = (Q, Σ, q 0 , δ, F ) be an NFA representing L, where |Q| = n. Let ρ : [0..m] → Q be an accepting run of A on w.

Let 0 ≤ k 1 < • • • < k t ≤ m be all the elements of {s ≥ 0 : |σ(w[1..s])| = |v 1 • • • v s |}.
Observe that k 1 = 0, and k t = m by condition 2. It is not difficult to show that by minimality of m there cannot be more than n indices. Proof. Suppose ad absurdum that t ≥ n + 1. Then, there must be two

k l < k l such that ρ(k l ) = ρ(k l ). Hence, w = w[1..k l ] • w[k l + 1..] ∈ L is also a codirect solution, contradicting that w is a minimal size solution.
Let L[q, q ] be the regular language denoted by the NFA (Q, Σ, q, δ, {q }). Claim 5.7.2. For every i < t, (σ, σ , L[ρ(k i ), ρ(k i+1 )]) has a strict codirect solution.

Proof. We show that for every i < t, w

[k i + 1..k i+1 ] is a solution for (σ, σ , L[ρ(k i ), ρ(k i+1 )]), witnessed by v k i +1 , . . . , v k i+1 .
Clearly, condition 1 still holds. Further, since

|σ(w[1..k i ])| = |v 1 • • • v k i | and |σ(w[1..k i+1 ])| = |v 1 • • • v k i+1 |, we have that |σ(w[k i + 1..k i+1 ])| = |v k i +1 • • • v k i+1 | and then σ(w[k i + 1..k i+1 ]) = v k i +1 • • • v k i+1 , verifying condition 2.
Finally, by the fact that k i and k i+1 are consecutive indices we cannot have some k

with k i + 1 < k < k i+1 so that |σ(w[k i + 1..k ])| = |v k i +1 • • • v k | since it would imply |σ(w[1..k ])| = |v 1 • • • v k |
and in this case k ≥ k i+1 . Then, conditions 3 and 4 hold. Therefore, we obtain the following reduction.

Claim 5.7.3. (σ, σ , L) has a codirect solution if, and only if, there exist {q 1 , . . . , q t } ⊆ Q with q 1 = q 0 and q t ∈ F , such that for every i, (σ, σ , L[q i , q i+1 ]) has a strict codirect solution.

This reduction being exponential is outweighed by the fact that we are dealing with a much harder problem.

With the help of Lemma 5.7 we prove Theorem 5.5 in the next section. 5.2.2. Proof of Theorem 5.5. Since decidability follows from Proposition 5.4, we only show the lower bound. To this end, we show how to code the existence of a strict codirect solution as an instance of (REG ∩ ) ? = ∅. Proposition 5.8. There is an elementary reduction from the existence of strict codirect solutions of PEP reg into (REG ∩ )

? = ∅.
Given a PEP reg instance (σ, σ , L), remember that the presence of a strict codirect solution enforces that if there is a pair (u, v) = (σ(w), σ (w)) with w ∈ L and u v, it is such that for every proper prefix u of u the smallest prefix v of v such that u v must be so that |v | > |u |. In the proof, we convert the rational relation R = {(σ(w), σ (w)) | w ∈ L} into a length-preserving regular relation R over an extended alphabet Γ ∪ {#}, defined as the set of all pairs (u, v)

∈ (Γ ∪ {#}) * × (Γ ∪ {#}) * so that |u| = |v| and (u Γ , v Γ ) ∈ R. If we now let R to be the regular relation R • {(ε, v) | v ∈ {#} * }, we obtain that: (i) if w ∈ R ∩ then w ∈ R ∩
, where w is the projection of w onto Γ * × Γ * ; and (ii) if there is some strict codirect solution w ∈ R ∩ , then there is some w ∈ R ∩ such that w is the projection of w onto Γ * × Γ * . Whereas (i) is trivial, (ii) follows from the fact that w is a strict codirect solution. If w = (u, v) ∈ R , where f (w) = (u) Γ , g(w) = (v) Γ , the complication is now that, since u ∈ Γ ∪ {#}, it could be that u v just because there is some # in u that does not appear in v. But we show how to build (u, v) such that whenever u[i] = # forces v[j] = # with j > i then we also have that u[j] = #. This repeats, forcing v[k] = # for some k > j and so on, until we reach the tail of v that has sufficiently many #'s to satisfy all the accumulated demands for occurrences of #.

Proof of Proposition 5.8. Let (σ, σ , L) be a PEP reg instance. For every a ∈ Σ, consider the binary relation R a consisting of all pairs (u, u )

∈ (Γ ∪ {#}) * × (Γ ∪ {#}) * such that u Γ = σ(a), u Γ = σ (a) and |u| = |u |. Note that R a is a length-preserving regular relation. Let R be the set of pairs (u 1 • • • u m , u 1 • • • u m )
such that there exists w ∈ L where |w| = m and (u i , u i ) ∈ R w[i] for all i. Note that R is still a length-preserving regular relation. Finally, we define R as the set of pairs (u, u • u ) such that (u, u ) ∈ R and u ∈ {#} * . R is no longer a length-preserving relation, but it is regular. Observe that if R ∩ = ∅, then (σ, σ , L) has a solution. Conversely, we show that if (σ, σ , L) has a strict codirect solution, then R ∩ = ∅.

Suppose that the PEP reg instance (σ, σ , L) has a strict codirect solution w ∈ L with |w| = m, witnessed by v 1 , . . . , v m . Assume, without any loss of generality, that σ and σ are alphabetic morphisms and that m > 1. We exhibit a pair (u, u ) ∈ R such that u u . We define (u, u

) = (u 1 • • • u m , u 1 • • • u m • u m+1 ), where (u i , u i ) ∈ R w[i]
for every i ≤ m, and u m+1 ∈ {#} * . In order to give the precise definition of (u, u ), we need to introduce some concepts first.

Let

σ # (a) ∈ Γ ∪ {#} be # if σ(a) = ,
[m] → [m] so that g(i) is the minimum j such that v 1 • • • v j = σ(w[1..i])
. Note that there is always such a j, since |σ(w[1..i])| > 0 by Claim 5.8.1. Now we show some easy properties of g, necessary to correctly define the witnessing pair (u, u ) ∈ R such that u u . Claim 5.8.2. g(i) > i for all 1 ≤ i < m, and g(m) = m.

Proof. Let g(i) = j and hence |σ(w[1..i])| = |v 1 • • • v j |. First, notice that |v 1 • • • v j | = |σ(w[1..i])| ≥ |v 1 • • • v i |
by condition 3 of codirectness, and then that j ≥ i.

If i < m, |v 1 • • • v i | < |σ(w[1..i])| by condition 4, and thus |v 1 • • • v i | < |v 1 • • • v j | which implies i < j. If i = m, then j = i by the fact that j ≥ i = m. Claim 5.8.3. g is increasing: g(i) ≥ g(j) if i ≥ j. Proof. Given m ≥ i ≥ j ≥ 1, we have that |v 1 • • • v g(i) | = |σ(w[1..i])| (by definition of g) ≥ |σ(w[1..j])| (since i ≥ j) = |v 1 • • • v g(j) |
(by definition of g) which implies that g(i) ≥ g(j).

Observation 5.9.

For all i ≤ m, if σ(w[i]) ∈ Γ then σ(w[i]) = σ (w[g(i)]).
The most important pairs of positions (i, j) ∈ [m] × [m] that witness u u , are those so that j = g(i) and σ(w[i]) = ε. Once those are fixed, the remaining elements in the definition of g are also fixed. Let us call G to this set, and let us state some simple facts for later use. Since our coding uses the letter # as some sort of blank symbol, it will be useful to define the factors ũ1 , ũ2 , . . . of u that contain exactly one letter from Γ. We then define ũi as the maximal prefix of u i • • • u m belonging to the following regular expression: Γ • {#} * .

G = {(i, g(i)) ∈ [m] × [m] | σ(w[i]) ∈ Γ} Observation 5.10. For every (i, j), (i , j ) ∈ G, if i = i then j = j . In
'₁ u'₂ u'₃ u'₄ u'₅ u'₆ u'₇ u'₈ u'₉ # a a b a b a c a # c b c # b a # u u' # # # # # # # # # # # # # # # # # a b # a c # # a b # a # # # # # # # # # # # # # # # # # # a b a c
We are now in good shape to define precisely u j , u j for every j ∈ [m]. For every j < m,

• if (i, j) ∈ G for some i, then

u j = ũi and u j = σ # (w[j]) • u j [2.
.]; and

• if there is no i so that (i, j) ∈ G, then (u j , u j ) = (σ # (w[j]), σ # (w[j])).
And on the other hand, (u

m , u m ) = (σ # (w[m]), σ # (w[m]
)) and u m+1 = # |u 1 •••um| . Figure 1 contains an example with all the previous definitions. Notice that the definition of u j makes use of ũj and the definition of ũj seems to make use of u j . We next show that in fact ũj does not depend on u j , and that the strings above are well defined.

Observation 5.11.

For i < m, ũi is a prefix of u i • • • u g(i)-1 .
Proof. By Claim 5.8.2 and Claim 5.10.1, σ(w[i..g(i)]) contains at least two elements and hence u i • • • u g(i) contains at least two elements from Γ, namely u i [START_REF] Angles | Survey of graph database models[END_REF] and u g(i) [START_REF] Angles | Survey of graph database models[END_REF]. Then, ũi cannot contain [START_REF] Angles | Survey of graph database models[END_REF]) as a prefix.

u i • • • u g(i)-1 • (u g(i)
By the above Observation 5.11, to compute ũi we only need u j 's and u j 's with j < i, and hence (u, u ) is well defined. Observation 5.12. All the u i 's, u i 's and ũi 's are of the form a

• # • • • # or # • • • #, for a ∈ Γ.
From the definition of (u, u ) we obtain the following.

Observation 5.13. For every n ≤ m,

(1) |(u 1 • • • u n ) Γ | = {i ∈ [n] | ∃j.(i, j) ∈ G} = |σ(w[1..n])|, and (2) |(u 1 • • • u n ) Γ | = {j ∈ [n] | ∃i.(i, j) ∈ G} = |σ (w[1..n])|.
We now show that (u, u ) ∈ R and that u u . Claim 5.13.1. (u, u ) ∈ R.

Proof. Note that u i = σ # (w[i]) for all i and then (u i ) Γ = σ(w[i]).
We also show that (

u i ) Γ = σ (w[i]). If u j is such that there is no (i, j) ∈ G, or j = m, then it is plain that (u j ) Γ = σ (w[j]
) by definition of u j . On the other hand, if u j = ũi for (i, j) ∈ G, then

(u j ) Γ = (ũ i ) Γ = (u i ) Γ = (u i [1]) Γ
(by Observation 5.12)

= (σ(w[i])) Γ (by def. of u i ) = σ(w[i]) (since σ(w[i]) ∈ Γ by def. of G) = σ (w[g(i)]) = σ (w[j]).
(by Observation 5.9)

Thus, every (u i , v i ) with i ≤ m is such that (u i ) Γ = σ(w[i]) and (u i ) Γ = σ (w[i]), meaning that (u i , v i ) ∈ R w[i] for every i ≤ m. Hence, we have that (u 1 • • • u m , u 1 • • • u m ) ∈ R and since u m+1 ∈ {#} * , (u, u ) ∈ R.
Next, we prove that u u , but before doing so, we need an additional straightforward claim. Let {i .k])|. This is in contradiction with condition 4 of strict codirectness. Hence, g(i j ) ≥ i j+1 .

1 < • • • < i |G| } = {i | (i, g(i)) ∈ G}. Note that i 1 =
Claim 5.13.3. u u .

Proof. We factorize u = û1 • • • û|G| and we show that each ûi is a substring of u that appears in an increasing order. We define ûj = u i j • • • u i (j+1) -1 for every j < |G|, and û|G| = u i |G| • • • u m . Hence, the ûi 's form a factorization of u. Indeed, this is the unique factorization in which each ûi is of the form b

• # • • • # for b ∈ Γ.
For every j < |G|, we show that ûj u g(i j ) . The following summarizes properties of subsequence-closed relations.

ûj = u i j • • • u i (j+1) -1 u i j • • • u g(i j )-1 (
Proposition 5.14.

(1) SCR RAT.

(2) SCR ⊆ REG and REG ⊆ SCR.

(

) A relation R is in SCR iff {w ⊗ w | (w, w ) ∈ R} is accepted by an NFA A = Q, Σ ⊥ × Σ ⊥ , q 0 , 3
δ, F such that (q, (a, b), q ) ∈ δ implies (q, (⊥, b), q ) ∈ δ for all q, q ∈ Q and a, b ∈ Σ ⊥ . We call an automaton with such property a subsequenceclosed automaton.

Note that (3) is immediate by definition of R , (1) is a consequence of (3), and ( 2) is due to the fact that is not regular and that, for example, the identity {(u, u) | u ∈ Σ * } is not a subsequence-closed relation.

When an SCR relation is given as an input to a problem, we assume that it is represented as a subsequence-closed automaton as defined in item (3) in the above proposition.

Note also that (SCR ∩ SCR)

? = ∅ is decidable in polynomial time: if R, R ∈ SCR and R ∩ R = ∅, then (ε, w) ∈ R ∩ R
for some w, and hence the problem reduces to simple NFA nonemptiness checking.

The main result about SCR relations generalizes decidability of (RAT ∩ )

? = ∅.
Theorem 5.15. The problem (RAT ∩ SCR)

?
= ∅ is decidable, with non-mutiply recursive complexity.

In order to prove Theorem 5.15 we use Lemmas 5.16 and 5.17, as shown below. But first we need to introduce some additional terminology. We say that (A 0 , A 1 ) is an instance of (RAT ∩ SCR)

? = ∅ over Σ, Γ if A 1 is a subsequence-closed automaton over Σ ⊥ × Γ ⊥ , and A 0 is a NFA over Σ ⊥ × Γ ⊥ . Given a (RAT ∩ SCR) ? = ∅ instance (A 0 , A 1 ) over Σ, Γ, we say that (w 1 , w 2 ) is a solution if w 1 , w 2 ∈ (Σ ⊥ × Γ ⊥ ) * , w 1 ∈ L(A 1 ), w 2 ∈ L(A 0 )
. We say that a solution (w 0 , w 1 ) of an instance (A 0 , A 1 ) over Σ, Γ is synchronized if π 2 (w 0 ) = π 2 (w 1 ). We write (RAT ∩ SCR) syn ?

= ∅ for the problem of whether there is a synchronized solution.

Lemma 5.16. There is a polynomial-time reduction from the problem (RAT ∩ SCR)

? = ∅ into (RAT ∩ SCR) syn ? = ∅.
Proof. We show that (RAT ∩ SCR)

?
= ∅ is reducible to the problem of whether there exists a synchronized solution of (RAT ∩ SCR) ? = ∅. Suppose that (A 0 , A 1 ) is an instance of (RAT ∩ SCR) ? = ∅ over the alphabets Σ, Γ. Consider the automata A 0 , A 1 as the result of adding all transitions (q, (⊥, ⊥), q) for every possible state q to both automata. It is clear that the relations recognized by these remain unchanged, and that A 0 is still a subsequenceclosed automaton. Moreover, this new instance has a synchronized solution if there is any, as stated in the following claim.

Claim 5.16.1. There is a synchronized solution for (A 0 , A 1 ) if, and only if, there is a solution for (A 0 , A 1 ).

The 'only if' part is immediate. For the 'if' part, let (w 0 , w 1 ) be a solution for (A 0 , A 1 ). Let

w 0 = w 0,1 • • • w 0,n , w 1 = w 1,1 • • • w 1,
n be factorizations of w 0 and w 1 such that for every i ∈ {0, 1}, π 2 (w i,1 ) is in {⊥} * ; and for each j > 1, i ∈ 0, 1, π 2 (w i,j ) is in Γ • {⊥} * . It is plain that there is always such factorization and that it is unique.

For every j ∈ [n], we define w 0,j = w 0,j • (⊥, ⊥) k and w 1,j = w 1,j • (⊥, ⊥) -k , with k = |w 1,j | -|w 0,j |, where we assume that (⊥, ⊥) m with m ≤ 0 is the empty string. We define

w 0 = w 0,1 • • • w 0,n , w 1 = w 1,1 • • • w 1,n . Note that (w 0 , w 1 ) is a solution of (A 0 , A 1 )
since it is the result of adding letters (⊥, ⊥) to (w 0 , w 1 ), which is also a solution of (A 0 , A 1 ). We have that π 2 (w 0 ) = π 2 (w 1 ), and therefore that (w 0 , w 1 ) is a synchronized solution for (A 0 , A 1 ). Lemma 5.17. There is a polynomial-time reduction from (RAT ∩ SCR) syn ?

= ∅ into (RAT ∩ )

? = ∅.
Proof. The problem of finding a synchronized solution for A 0 , A 1 can be then formulated as the problem of finding words v, u 0 , u 1 ∈ Σ * ⊥ with |v| = |u 0 | = |u 1 |, so that (u 0 ⊗v, u 1 ⊗v) is a solution. We can compute an NFA A over Σ 2 ⊥ ×Γ ⊥ from A 0 , A 1 , such that (u 0 , u 1 , v) ∈ L(A) if, and only if, u 0 ⊗ v ∈ L(A 1 ) and u 1 ⊗ v ∈ L(A 0 ). Consider now an automaton A over Σ 2

⊥ such that L(A ) = {(u 0 , u 1 ) | ∃v (u 0 , u 1 , v) ∈ L(A)}. It corresponds to the rational automaton of the projection onto the first and second components of the ternary relation of A, and it can be computed from A in polynomial time. We then deduce that there exists

u 0 ⊗ u 1 ∈ L(A ) so that (u 0 ) Σ (u 1 ) Σ if, and only if, there is v ∈ Γ * ⊥ with |v| = |u 0 | = |u 1 | so that u 0 ⊗ v ∈ L(A 0 ) and u 1 ⊗ v ∈ L(A 1 ), where (u 0 ) Σ (u 1 ) Σ . But this condition is in fact equivalent to R 0 ∩ R 1 = ∅ (where R i = {((u) Σ , (v) Σ ) | u ⊗ v ∈ L(A i )}), since • if ((u 1 ) Σ , (v) Σ ) ∈ R 1 and (u 0 ) Σ (u 1 ) Σ , then ((u 0 ) Σ , (v) Σ ) ∈ R 1 (since R 1 ∈ SCR) and hence ((u 0 ) Σ , (v) Σ ) ∈ R 0 ∩ R 1 ; and • if R 0 ∩ R 1 = ∅, then there exists a synchronized solution (u 0 ⊗ v, u 1 ⊗ v) of A 0 , A 1 ;
in other words, there are |v|

= |u 0 | = |u 1 | so that u 0 ⊗ v ∈ L(A 0 ), u 1 ⊗ v ∈ L(A 1 )
, and (u 0 ) Σ = (u 1 ) Σ .

We have thus reduced the problem to an instance of (RAT ∩ ) ? = ∅: whether there is (u, v) in the relation denoted by A so that u v.

Proof of Theorem 5.15. The decidability part of Theorem 5.15 follows as a corollary of Lemmas 5.16 and 5.17 Coming back to graph logics, we obtain: Corollary 5.18. The complexity of evaluation of ECRPQ( ) queries is not bounded by any multiply-recursive function.

Another corollary can be stated in purely language-theoretic terms.

Corollary 5.19. Let C be a class of binary relations on Σ * that is closed under intersection and contains REG. Then the nonemptiness problem for C is:

• undecidable if or suff is in C;

• non-multiply-recursive if is in C.

5.3.

Discussion. In addition to answering some basic language-theoretic questions about the interaction of regular and rational relations, and to providing the simplest yet problem with non-multiply-recursive complexity, our results also rule out logical languages for graph databases that freely combine regular relations and some of the most commonly used rational relations, such as subword and subsequence. With them, query evaluation becomes either undecidable or non-multiply-recursive (which means that no realistic algorithm will be able to solve the hard instances of this problem). This does not yet fully answer our questions about the evaluation of queries in graph logics. First, in the case of subsequence (or, more generally, SCR relations) we still do not know if query evaluation of ECRPQs with such relations is decidable (i.e., what happens with GenInt S (REG) for such relations S).

Even more importantly, we do not yet know what happens with the complexity of CRPQs (i.e., GenInt S (REC)) for various relations S. These questions are answered in the next section.

Restricted logics and generalized intersection problem

The previous section already ruled out some graph logics with rational relations as either undecidable or decidable with extremely high complexity. This was done merely by analyzing the intersection problem for binary rational and regular relations. We now move to the study of the generalized intersection problem, and use it to analyze the complexity of graph logics in full generality. We first deal with the generalization of the decidable case (SCR relations), and then consider the problem GenInt S (REC), corresponding to CRPQs extended with relations S on paths. 6.1. Generalized intersection problem and subsequence. We know that (REG∩ ) ? = ∅ is decidable, although not multiply-recursive. What about its generalized version? It turns out it remains decidable. Theorem 6.1. The problem GenInt (REG) is decidable. That is, there is an algorithm that decides, for a given m-ary regular relation R and

I ⊆ [m] 2 , whether R ∩ I = ∅. Proof. Let k ∈ N, I ⊆ [k] × [k]
and R ∈ REG k be an instance of the problem. Let us define G = {(w 1 , . . . , w k ) | ∀(i, j) ∈ I, w i w j }. We show how to compute if R ∩ G is empty or not. Let A = (Q, (Σ ⊥ ) k , q 0 , δ, F ) be a NFA over (Σ ⊥ ) k corresponding to R, for simplicity we assume that it is complete. Remember that every w

∈ L(A) is such that π i (w) is in Σ * ; {⊥} * for every i ∈ [k].
Given u, v ∈ Σ * , we define u \ v as u[i..], where i is the maximal index such that u[1..i -1] v. In other words, u \ v is the result of removing from u the maximal prefix that is a subsequence of v.

We define a finite tree t whose every node is labeled with

• a depth n ≥ 0, • k words w 1 , . . . , w k ∈ Σ n ⊥ ,
• for every (i, j) ∈ I, a word α ij ∈ Σ * , and • a state q ∈ Q. For a node x we denote these labels by x.n, x.w 1 , . . . , x.w k , x.α ij for every (i, j) ∈ I and x.q respectively. The tree is such that the following conditions are met.

• The root is labeled by x.n = 0, x.w 1 = • • • = x.w k = ε, for very (i, j) ∈ I, x.α ij = ε, and x.q = q 0 . • A node x has a child y in t if and only if

-y.n = x.n + 1, -x.w i = y.w i [1..y.x -1] for every i ∈ [k],
there is a transition (x.q, ā, y.q) ∈ δ with ā = (y.w i [y.n]) i∈[k] , and y.α ij = (w i ) Σ \ (w j ) Σ for every (i, j) ∈ I. • A node x is a leaf in t if and only if is final or saturated (as defined below). A node x is final if x.q ∈ F and x.α ij = ε for all (i, j) ∈ I. It is saturated if it is not final and there is an ancestor y = x such that y.q = x.q and y.α ij x.α ij for all (i, j) ∈ I. Lemma 6.2. The tree t is finite and computable.

Proof. The root is obviously computable, and for every branch, one can compute the list of children nodes of the bottom-most node of the branch. Indeed these are finite and bounded. The tree t cannot have an infinite branch. If there was an infinite branch, then as a result of Higman's Lemma cum Dickson's Lemma (and the Pigeonhole principle) there would be two nodes x = y, where x is an ancestor of y, x.q = y.q, and for all (i, j) ∈ I, x.α ij y.α ij . Therefore, y is saturated and it does not have children, contradicting the fact that x and y are in an infinite branch of t. Since all the branches are finite and the children of any node are finite, by Kőnig's Lemma, t is finite, and computable.

Lemma 6.3. If t has a final node, R ∩ G = ∅.
Proof. If a leaf x is final, consider all the x.n ancestors of x: x 0 , . . . , x n-1 , such that x i .n = i for every i ∈ [n-1]. Consider the run ρ : [0..x.n] → Q defined as ρ(x.n) = x.q and ρ(i) = x i .q for i < x.n. It is easy to see that ρ is an accepting run of A on x.w 1 ⊗. . .⊗x.w k and therefore that ((x.w 1 ) Σ , . . . , (x.w k ) Σ ) ∈ R. On the other hand, for every (i, j) ∈ I, (x.w i ) Σ (x.w j ) Σ since α ij = ε. Hence, ((x.w 1 ) Σ , . . . , (x.w k ) Σ ) ∈ G and thus R ∩ G = ∅. Lemma 6.4. If all the leaves of t are saturated, R ∩ G = ∅.

Proof. By means of contradiction suppose that there is w

= w 1 ⊗ • • • ⊗ w k ∈ (Σ k
⊥ ) * such w ∈ L(A) through an accepting run ρ : [0..n] → Q, and for every (i, j) ∈ I, (w i ) Σ (w j ) Σ . Let |w| = n be of minimal size.

By construction of t, the following claims follow.

Claim 6.4.1.

There is a maximal branch x 0 , . . . , x m in t such that x .n = , x .w j = w j [1.. ], x .q = ρ( ) for every ∈ [0..m] and j ∈ [k].

Claim 6.4.2. For every ∈ [0..m] and (i, j) ∈ I,

x .α ij • (w i [ + 1..]) Σ (w j [ + 1..]) Σ , (6.1)
(w i [1.. -|x .α ij |]) Σ (w j [1.. ]) Σ . (6.2)
Since we assume that all the leaves of t are saturated, in particular x m is saturated and there must be some m < m such that x m and x m verify the saturation conditions.

Consider the following word.

w = w[1..m ] • w[m + 1..]
The run ρ trimmed with the positions [m + 1..m] is still an accepting run on w (since ρ(m ) = ρ(m)), and therefore ((π 1 (w )) Σ , . . . , (π k (w )) Σ ) ∈ R.

For an arbitrary (i, j) ∈ I, we show that (π i (w )) Σ (π j (w )) Σ . First, note that by (6.2) we have that

(π i (w )[1..m -|x m .α ij |]) Σ = (w i [1..m -|x m .α ij |]) Σ (w j [1..m ]) Σ (by (6.2)) = (π j (w )[1..m ]) Σ .
Since x m and x m verify the saturation conditions, x m .α ij x m .α ij . Therefore, Hence, by Lemmas 6.2, 6.3 and 6.4, R ∩ G = ∅ if and only if t has a final node, which is computable. Corollary 6.5. The query evaluation problem for ECRPQ( ) queries is decidable.

(π i (w )[m -|x m .α ij | + 1..]) Σ = (π i (w )[m -|x m .α ij | + 1..m ]) Σ • (π i (w )[m + 1..]) Σ = x m .α ij • (w i [m + 1..]) Σ x m .α ij • (w i [m + 1..]) Σ (since x m .α ij x m .α ij ) (w j [m + 1..]
Of course the complexity is extremely high as we already know from Corollary 5.18. Note that while the intersection problem of with rational relations is decidable, as is GenInt (REG), we lose the decidability of GenInt (RAT) even in the simplest cases that go beyond the intersection problem (that is, for ternary relations in RAT and any I that does not force two words to be the same). Proposition 6.6. The problem (RAT ∩ I ) ? = ∅ is undecidable even over ternary relations when I is one of the following:

(1) {(1, 2), (2, 3)}, (2) {(1, 2), (1, 3)}, or (3) {(1, 2), (3, 2)}.
Proof. The three proofs use a reduction from the PCP problem. Recall that this is defined as follows. The input are two equally long lists u 1 , u 2 , . . . , u n and v 1 , v 2 , . . . , v n of strings over alphabet Σ. The PCP problems asks whether there exists a solution for this input, that is, a sequence of indices i 1 , i 2 , . . . , i k such that 1 2, 3)}: The proof goes by reduction from an arbitrary PCP instance given by lists u 1 , . . . , u n and v 1 , . . . , v n of strings over alphabet Σ. The following relation

≤ i j ≤ n (1 ≤ j ≤ k) and u i 1 u i 2 • • • u i k = v i 1 v i 2 • • • v i k . (1) {(1, 2), (
R = {(u i 1 • • • u im , v i 1 • • • v im , u i 1 • • • u im ) | m ∈ N and i 1 , . . . , i m ∈ [n]} is rational and R ∩ {(x, y, z) | x y
z} is non-empty if and only if the instance has a solution.

(2) {(1, 2), (1, 3)}: The proof again goes by reduction from an arbitrary PCP instance given by lists u 1 , . . . , u n and v 1 , . . . , v n of strings over alphabet Σ. For simplicity, and without any loss of generality, we assume that |u i |, |v i | ≤ 1 for every i. Let Σ = {â | a ∈ Σ}, and for every

w = a 1 • • • a ∈ Σ * , let ŵ = â1 • • • â . Consider R = {(x, y, z) | m ∈ N, i 1 , . . . , i m ∈ [n], w 1 , w 1 , . . . , w m+1 , w m+1 ∈ Σ * , x = u i 1 vi 1 u i 2 vi 2 • • • u im vim , y = w 1 ûi 1 w 2 • • • w m ûim w m+1 , z = ŵ1 v i 1 ŵ2 • • • ŵm v im ŵm+1 }
which is a rational relation. Note that there is some (x, y, z) ∈ R with x y if and only if there is some

v i 1 • • • v im u i 1 • • • u im .
Similarly for x z. Therefore, there is (x, y, z) ∈ R with x y, x z if and only if

v i 1 • • • v im = u i 1 • • • u im for some choice of i 1 , . . . , i m .
(3) {(1, 2), (3, 2)}: This is similar to [START_REF] Anyanwu | ρ-Queries: enabling querying for semantic associations on the semantic web[END_REF], but this time we consider the following rational relation.

R = {(x, y, z) | m ∈ N, i 1 , . . . , i m ∈ [n], w 1 , w 1 , . . . , w m+1 , w m+1 ∈ Σ * , y = u i 1 vi 1 u i 2 vi 2 • • • u im vim , x = w 1 ûi 1 w 2 • • • w m ûim w m+1 , z = ŵ1 v i 1 ŵ2 • • • ŵm v im ŵm+1 }
Analogously as before, there is (x, y, z) ∈ R with x y, z y if and only if the PCP instance has a solution. 6.2. Generalized intersection problem for recognizable relations. We now consider the problem of answering CRPQs with rational relations S, or, equivalently, the problem GenInt S (REC). Recall that an instance of such a problem consists of an m-ary recognizable relation R and a set I ⊆ [m] 2 . The question is whether R ∩ I S = ∅, i.e., whether there exists a tuple (w 1 , . . . , w m ) ∈ R so that (w i , w j ) ∈ S whenever (i, j) ∈ I. It turns out that the decidability of this problem hinges on the graph-theoretic properties of I. In fact we shall present a dichotomy result, classifying problems GenInt S (REC) into PSpace-complete and undecidable depending on the structure of I.

Before stating the result, we need to decide how to represent a recognizable relation R. Recall that an m-ary R ∈ REC is a union of relations of the form L 1 × . . . × L m , where each L i is a regular language. Hence, as the representation of R we take the set of all such L i s involved, and as the measure of its complexity, the total size of NFAs defining the L i s.

With a set I ⊆ [m] 2 we associate an undirected graph G I whose nodes are 1, . . . , m and whose edges are {i, j} such that either (i, j) ∈ I or (j, i) ∈ I. We call an instance of (REC ∩ I S) ? = ∅ acyclic if G I is an acyclic graph. Now we can state the dichotomy result. Theorem 6.7.

• Let S be a binary rational relation. Then acyclic instances of GenInt S (REC) are decidable in PSpace. Moreover, there is a fixed binary relation S 0 such that the problem (REC ∩ I S 0 ) ? = ∅ is PSpace-complete. • For every I such that G I is not acyclic, there exists a binary rational relation S such that the problem (REC ∩ I S)

? = ∅ is undecidable.
Proof. For PSpace-hardness we can do an easy reduction from nonemptiness of the intersection of m given NFA's, which is known to be PSpace-complete [START_REF] Kozen | Lower bounds for natural proof systems[END_REF]. Given m NFAs A 1 , . . . , A m , define the (acyclic) relation

I = {(i, i + 1) | 1 ≤ i < m}. Then i L(A i ) is nonempty if and only if i L(A i ) ∩ I S 0 = ∅, where S 0 is the regular relation {(w, w) | w ∈ Σ * }.
For the upper bound, we use the following idea: First we show how to construct, in exponential time, the following for each m-ary recognizable relation R, binary rational relation S and acyclic I ⊆ [m] 2 : An m-tape automaton A(R, S, I) that accepts precisely those w = (w 1 , . . . , w m ) ∈ (Σ * ) m such that w ∈ R and (w i , w j ) ∈ S, for each (i, j) ∈ I. Intuitively, A(R, S, I) represents the "synchronization" of the transducer that accepts R with a copy of the 2-tape automaton that recognizes S over each projection defined by the pairs in I. Such synchronization is possible since I is acyclic. Hence, in order to solve GenInt S (REC) we only need to check A(R, S, I) for nonemptiness. The latter can be done in PSpace by the standard "on-the-fly" reachability analysis. We proceed with the details of the construction below.

Recall that rational relations are the ones defined by n-tape automata. We start by formally defining the class of n-tape automata that we use in this proof. An n-tape automaton, n > 0, is a tuple

A = (Q, Σ, Q 0 , δ, F ), where Q is a finite set of control states, Σ is a finite alphabet, Q 0 ⊆ Q is the set of initial states, δ : Q × (Σ ∪ {ε}) n → 2 Q×([n]∪{[n]})
is the transition function with ε a symbol not appearing in Σ, and F ⊆ Q is the set of final states. Intuitively, the transition function specifies how A moves in a situation when it is in state q reading symbol ā ∈ Σ n : If (q , j) ∈ δ(q, ā), where j ∈ [n], then A is allowed to enter state q and move its j-th head one position to the right of its tape. If (q , [n]) ∈ δ(q, ā) then A is allowed to enter state q and move each one of its heads one position to the right of its tape.

Given a tuple w = (w 1 , . . . , w n ) ∈ (Σ * ) n such that w i is of length p i ≥ 0, for each 1 ≤ i ≤ n, a run of A over w is a sequence q 0 P 0 q 1 P 1 • • • q k-1 P k-1 q k , for k ≥ 0, such that:

(1)

q i ∈ Q, for each 0 ≤ i ≤ k, (2)
q 0 ∈ Q 0 , ( 3
) P i is a tuple in ([p 1 ] ∪ {0}) × • • • × ([p n ] ∪ {0}
), for each 0 ≤ i ≤ k -1 (intuitively, the P i 's represent the positions of the n heads of A at each stage of the run. In particular, the j-th component of P i represents the position of the j-th head of A in stage i of the run), (4) P 0 = (b 1 , . . . , b n ), where b i := 0 if w i is the empty word ε (that is, p i = 0) and b i := 1 otherwise (that is, the run starts by initializing each one of the n heads to be in the initial position of its tape, if possible), (5) P k-1 = (p 1 , . . . , p n ), that is, the run ends when each head scans the last position of its head, and (6) for each 0

≤ i ≤ k -1, if P i = (r 1 , . . . , r n ) and (π 1 ( w))[r 1 ], . . . , (π n ( w))[r n ] = (a 1 , . . . , a n ),
where we assume by definition that w[0] = ε, then δ(q i , (a 1 , . . . , a n )) contains a pair of the form (q i+1 , j) such that: (a) if i < k -1 then j ∈ [n] and P i+1 is the tuple (r 1 , . . . , r j-1 , r j + 1, r j+1 , . . . , r n ).

In such case we say that (q i+1 , P i+1 ) is a valid transition from (q i , P i ) over w in the j-th head, and (b

) if i = k -1 then j = [n]
. This is a technical condition that ensures that each head of A should leave its tape after the last transition in the run is performed. That is, each run is forced to respect the transition function δ when the n-tape automaton A is in state q reading the symbols in the corresponding positions of its n heads. Further, the positions of the n heads are updated in the run also according to what is allowed by δ. Notice that each transition in a run moves a single head, except for the last one that moves all of them at the same time. The run is accepting if q k ∈ F (that is, A enters an accepting state after each one of its heads scans the last position of its own tape).

Each n-tape automaton A defines the language L(A) ⊆ (Σ * ) n of all those w = (w 1 , . . . , w n ) ∈ (Σ * ) n such that there is an accepting run of A over w. It can be proved with standard techniques that languages defined by n-ary rational relations are precisely those defined by n-tape automata. Notice that there is an alternative, more general model of n-tape automata that allows each transition to move an arbitrary number of heads. It is easy to see that this model is equivalent in expressive power to the one we present here, as transitions that move an arbitrary number of heads can easily be encoded by a a series of single-head transitions. We have decided to use this more restricted version of n-tape automata here, as it will allow us simplifying some of the technical details in our proof. Now we continue with the proof that the problem GenInt S (REC) can be solved in PSpace if I is acyclic (that is, it defines an acyclic undirected graph). The main technical tool for proving this is the following lemma: Lemma 6.8. Let R be an m-ary relation in REC, S a binary rational relation, and I a subset of [m] × [m] that defines an acyclic undirected graph. It is possible to construct, in exponential time, an m-tape automaton A(R, S, I) such that the language defined by A(R, S, I) is precisely the set of words w = (w 1 , . . . , w m ) ∈ (Σ * ) m such that w ∈ R and (w i , w j ) ∈ S for all (i, j) ∈ I.

We start by proving the lemma. The intuitive idea is that A(R, S, I) is an m-tape automaton that at the same time recognizes R and represents the "synchronization" of the |I| copies of the 2-tape automaton S over the projections corresponding to the pairs in I. Since I is acyclic, such synchronization is possible.

Assume that |I| = . Let t 1 , . . . , t be an arbitrary enumeration of the pairs in I. Also, assume that the recognizable relation R is given as

i N i 1 × • • • × N im ,
where each N i j is an NFA over Σ (without transitions on the empty word). Assume that the set of states of N i j is U i j , its set of initial states is U 0 i j and its set of final states is U F i j . Further, assume that the 2-tape transducer S is given by the tuple

(Q S , Σ, Q 0 S , δ S , Q F S )
, where Q S is the set of states, the set of initial states is Q 0 S , the set of final states is Q F S , and δ S :

Q S × (Σ ∪ {ε}) × (Σ ∪ {ε}) → 2 Q×({1,2}∪{{1,2}}
) is the transition function. We take |I| = disjoint copies S 1 , . . . , S of S, such that S i , for each 1 ≤ i ≤ , is the tuple

(Q S i , Σ, Q 0 S i , δ S i , Q F S i ).
Without loss of generality we assume that if

t i = (j, j ) ∈ [m] × [m] then δ S i is a function from Q S i × (Σ ∪ {ε}) × (Σ ∪ {ε}) into 2 Q×(
{j,j }∪{{j,j }}) . We can do this because I is acyclic, and hence j = j .

The m-tape automaton A(R, S, I) is defined as the tuple (Q, Σ, Q 0 , δ, F ), where:

(1) The set of states

Q is i U i 1 × • • • × U im × Q S 1 × • • • × Q S .
(2) The initial states in Q 0 are precisely those in

i U 0 i 1 × • • • × U 0 im × Q 0 S 1 × • • • × Q 0 S .
(3) The final states in F are precisely those in

i U F i 1 × • • • × U F im × Q F S 1 × • • • × Q F S .
(4) The transition function δ :

Q × (Σ ∪ {ε}) m → 2 Q×([m]∪{[m]}
) is defined as follows on state q ∈ Q and symbol ā ∈ (Σ ∪ {ε}) m . Assume that q = (u i 1 , . . . , u im , q 1 , . . . , q ), where u i j ∈ U i j for each 1 ≤ j ≤ m, and q j ∈ Q S j for each 1 ≤ j ≤ . Further, assume that ā = (a 1 , . . . , a m ), where a j ∈ (Σ∪{ε}) for each 1 ≤ j ≤ m. Then δ(q, ā) consists of all pairs of the form (u i 1 , . . . , u im , q 1 , . . . , q ), j , for j ∈ [m], such that: (a)

u i k = u i k for each k ∈ [m] \ {j},
and there is a transition in N i j from u i j into u i j labeled a j ; and

(b) for each 1 ≤ k ≤ , if t k is the pair (k 1 , k 2 ) ∈ [m] × [m] then the following holds: (1) If j ∈ {k 1 , k 2 } then q k = q k , and (2) if j ∈ {k 1 , k 2 } then (q k , j) belongs to δ S k (q k , (a k 1 , a k 2 )
), plus all pairs of the form (u i 1 , . . . , u im , q 1 , . . . , q ), [m] such that: (a) for each 1 ≤ k ≤ m there is a transition in

N i k from u i k into u i k labeled a k ; and (b) for each 1 ≤ k ≤ , if t k is the pair (k 1 , k 2 ) ∈ [m] × [m] then (q k , {{k 1 , k 2 }}) belongs to δ S k (q k , (a k 1 , a k 2 )
). Intuitively, δ defines possible transitions of A(R, S, I) that respect the transition function of each one of the copies of S over its respective projection. Further, while scanning its tapes the automaton A(R, S, I) also checks that there is an i such that for each 1 ≤ j ≤ m the j-th tape contains a word in the language defined by N i j .

Clearly, A(R, S, I) can be constructed in exponential time from R, S and I. Notice, however, that states of A(R, S, I) are of polynomial size.

We prove next that for every w = (w 1 , . . . , w m ) ∈ (Σ * ) m it is the case that w is accepted by A(R, S, I) if and only if w belongs to the language of R and (w i , w j ) ∈ S, for each (i, j) ∈ I. =⇒) Assume first that w = (w 1 , . . . , w m ) ∈ (Σ * ) m is accepted by A(R, S, I). It is easy to see from the way A(R, S, I) is defined that, for some i, the projection of the accepting run of A(R, S, I) on each 1 ≤ j ≤ m defines an accepting run of N i j over w j . Further, for each (j, k) ∈ I it is the case that the projection of the accepting run of A(R, S, I) on (j, k) defines an accepting run of S over (w j , w k ). We conclude that w belongs to the language of R and (w j , w k ) ∈ S, for each (j, k) ∈ I. ⇐=) Assume, on the other hand, that w = (w 1 , . . . , w m ) ∈ (Σ * ) m belongs to the language of R and (w i , w j ) ∈ S, for each (i, j) ∈ I. Further, assume that the length of w i is p i ≥ 0, for each 1 ≤ i ≤ m. We prove next that w is accepted by A(R, S, I).

Since w ∈ R it must be the case that w is accepted by

N i 1 × • • • × N im , for some i. Let us assume that ρ i j := u i j ,0 (1)
u i j ,1 (2) • • • u i j ,p j -1 (p j ) u i j ,p j is an accepting run of the 1-tape automaton N i j over w j , for each 1 ≤ j ≤ m. Since for every t j (1 ≤ j ≤ ) of the form (k, k ) ∈ [m] × [m] it is the case that (w k , w k ) ∈ S,
there is an accepting run λ j := q j,0 P j,0 q j,1 P j,1 • • • q j,r j P j,r j q j,r j +1 of S j over (w k , w k ). We then inductively define a sequence

q0 P 0 q1 P 1 • • •
where each qj is a state of Q and each

P j is a tuple in ([p 1 ] ∪ {0}) × • • • × ([p m ] ∪ {0}), as follows:
(1) q0 := (u i 1 ,0 , . . . , u im,0 , q 1,0 , . . . , q ,0 ).

(2) P 0 = (b 1 , . . . , b m ), where b i := 0 if w i is the empty word and b i := 1 otherwise.

(3) Let j ≥ 0. Assume that qj = (u i 1 , . . . , u im , q 1 , . . . , q ), where each u i k is a state in N i k and each q k is a state in S k , and that

P j = (r 1 , . . . , r m ) ∈ ([p 1 ] ∪ {0}) × • • • × ([p m ] ∪ {0}).
If for every 1 ≤ k ≤ m it is the case that r k = p k then the sequence stops. Otherwise it proceeds as follows.

If for some 1 ≤ k ≤ m it is the case that u i k (r k ) is not a subword of the accepting run ρ i k , 2 or that for some 1

≤ k ≤ such that t k = (k 1 , k 2 ) ∈ [m] × [m] it is the case that q k (r k 1 , r k 2 )
is not a subword of the accepting run λ k , 3 then the sequence simply fails.

Otherwise check whether there is a 1 ≤ k ≤ m such that the following holds: (a) r k = p k .

2 Notice that ρi k is a word in the language defined by (Ui k • [p k ]) * • Ui k , and hence it is completely well-defined whether a word in Ui k • [p k ] is or not a subword of ρi k .

3 This is well-defined for essentially the same reasons given in the previous footnote.

(b) For each pair

t k 1 ∈ I of the form (k, k ) ∈ [m] × [m] it is the case that if q k 1 (r k , r k ) is the subword in Q S k 1 • ([p k ] × [p k ]) that immediately follows q k 1 (r k , r k ) in the run λ k 1 , 4 then r k = r k + 1, and r k = r k . (c) For each pair t k 1 ∈ I of the form (k , k) ∈ [m] × [m] it is the case that if q k 1 (r k , r k ) is the subword in Q S k 1 • ([p k ] × [p k ]
) that immediately follows q k 1 (r k , r k ) in the run λ k 1 , then r k = r k + 1, and r k = r k . Intuitively, this states that we can move the k-th head of A(R, S, I) and preserve the transitions on each run of the form λ k 1 such that S k 1 is a copy of S that has one of its components reading tape k.

If no such k exists the sequence fails. Otherwise pick the least 1 ≤ k ≤ m that satisfies the conditions above, and continue the sequence by defining the pair (q j+1 , P j+1 ) as

(u i 1 , • • • , u i k-1 , u i k , u i k+1 , • • • , u im , q 1 , • • • , q ), (r 1 , • • • , r k-1 , r k + 1, r k+1 , • • • , r m ) ,
where the following holds: (a)

u i k (r k + 1) is the subword in U i k • [p k ] that immediately follows u i k (r k ) in ρ i k . (b) For each pair t k 1 ∈ I of the form (k, k ) ∈ [m]×[m], it is the case that q k 1 satisfies that q k 1 (r k +1, r k ) is the subword in Q S k 1 •([p k ]×[p k ]) that immediately follows q k 1 (r k , r k ) in the run λ k 1 . (c) For each pair t k 1 ∈ I of the form (k , k) ∈ [m]×[m], it is the case that q k 1 satisfies that q k 1 (r k , r k +1) is the subword in Q S k 1 •([p k ]×[p k ]) that immediately follows q k 1 (r k , r k ) in the run λ k 1 . (d) For each pair t k 1 ∈ I of the form (k , k ) ∈ [m] × [m] such that k = k and k = k,
it is the case that q k 1 = q k 1 . In this case we say that (q j+1 , P j+1 ) is obtained from (q j , P j ) by performing a transition on the k-th head.

We first prove by induction the following crucial property of the sequence q0 P 0 q1 P 1 • • • : The sequence does not fail at any stage j ≥ 0. Clearly, the sequence does not fail in stage 0 given by pair (q 0 , P 0 ). Assume now by induction that the sequence has not failed until stage j ≥ 0 given by pair (q j , P j ), and, further, that the sequence does not stop in stage j. We prove next that the sequence does not fail in stage j + 1.

If the sequence stops in stage j + 1 it clearly does not fail. Assume then that the sequence does not stop in stage (j + 1). Also, assume that q j = (u i 1 , . . . , u im , q 1 , . . . , q ), where each u i k is a state in N i k and each q k is a state in S k . Further, assume that

P j = (r 1 , . . . , r m ) ∈ ([p 1 ] ∪ {0}) × • • • × ([p m ] ∪ {0}
). Since the sequence did not stop in stage j it must be the case that for every 1 ≤ k ≤ m the sequence u i k (r k ) is a subword of the accepting run ρ i k , and that for every 1

≤ k ≤ such that t k = (k 1 , k 2 ) ∈ [m] × [m] the sequence q k (r k 1 , r k 2
) is a subword of the accepting run λ k .

Assume that (q j+1 , P j+1 ) is obtained from (q j , P j ) by performing a transition on the k-th head, for 1 ≤ k ≤ m. Then the pair (q j+1 , P j+1 ) is of the form:

(u i 1 , • • • , u i k , • • • , u im , q 1 , • • • , q ), (r 1 , • • • , r k , • • • , r m ) ,
where the following holds: 4 Notice, since A(R, S, I) does not allow empty transitions, that q k 1 (r k , r k ) is well-defined since the subword q k 1 (r k , r k ) appears exactly once in the run λ k 1 and, further,

q k 1 (r k , r k ) is followed in λ k 1 by a subword in QS k 1 • ([p k ] × [p k ]) because r k = p k . (1) u i k = u i k , for each k ∈ [m] \ {k}, (2) u i k (r k + 1) is the subword in U i k • [p k ] that immediately follows u i k (r k ) in ρ i k , (3) r k = r k , for each k ∈ [m] \ {k}, (4) r k = r k + 1, (5) for each pair t k 1 ∈ I of the form (k, k ) ∈ [m] × [m], it is the case that q k 1 satisfies that q k 1 (r k + 1, r k ) is the subword in Q S k 1 • ([p k ] × [p k ]) that immediately follows q k 1 (r k , r k ) in the run λ k 1 , (6) for each pair t k 1 ∈ I of the form (k , k) ∈ [m] × [m], it is the case that q k 1 satisfies that q k 1 (r k , r k + 1) is the subword in Q S k 1 • ([p k ] × [p k ]
) that immediately follows q k 1 (r k , r k ) in the run λ k 1 , and (7) for each pair

t k 1 ∈ I of the form (k , k ) ∈ [m] × [m] such that k = k and k = k,
it is the case that q k 1 = q k 1 . Then, by inductive hypothesis, it is the case that for every k ∈ [m] \ {k} the sequence u i k (r k ) is a subword of the accepting run ρ i k . For the same reason, for every 1

≤ k ≤ such that t k = (k 1 , k 2 ) ∈ [m] × [m], k 1 = k and k 2 = k, it is the case that q k (r k 1 , r k 2 )
is a subword of the accepting run λ k . Further, simply by definition u i k (r k ) is a subword of the accepting run ρ i k . Also, by definition, for each pair

t k 1 ∈ I of the form (k , k) ∈ [m] × [m],
it is the case that q k 1 (r k , r k ) is a subword of the accepting run λ k 1 , and, similarly, for each pair

t k 1 ∈ I of the form (k, k ) ∈ [m] × [m]
, it is the case that q k 1 (r k , r k ) is a subword of the accepting run λ k 1 . Hence, in order to prove that the sequence does not fail in stage j + 1 it is enough to show that there is an 1 ≤ h ≤ m such that some pair of the form (q, P ), where q ∈ Q and P ∈ ([p 1 ] ∪ {0}) × • • • × ([p m ] ∪ {0}), can be obtained from (q j+1 , P j+1 ) by performing a transition on the h-th head.

Since the sequence does not stop in stage j + 1, the set H = {1 ≤ h ≤ m | r h = p h } must be nonempty. Let h 1 be the least element in H. Since the underlying undirected graph of I is acyclic, the connected component of I to which h 1 belongs is a tree T . Without loss of generality we assume that T is rooted at h 1 .

We start by trying to prove that there is pair of the form (q, P ), where q ∈ Q and

P ∈ ([p 1 ] ∪ {0}) × • • • × ([p m ] ∪ {0}
), that can be obtained from (q j+1 , P j+1 ) by performing a transition on the h 1 -th head. If this is the case we are done and the proof finishes. Assume otherwise. Then we can assume without loss of generality that there is a pair of the form

t k ∈ I of the form (h 1 , h 2 ) ∈ [m] × [m] such that the subword in Q S k • ([p h 1 ] × [p h 2 ]
) that immediately follows q k (r h 1 , r h 2 ) in the run λ k is of the form q k (r h 1 , r h 2 + 1). (That is, the run λ k continues from q k (r h 1 , r h 2 ) by moving its second head). The other possibility is that there is a pair of the form

t k ∈ I of the form (h 2 , h 1 ) ∈ [m] × [m] such that the subword in Q S k • ([p h 2 ] × [p h 1 ]
) that immediately follows q k (r h 2 , r h 1 ) in the run λ k is of the form q k (r h 2 + 1, r h 1 ). But this case is completely symmetric to the previous one.

We then continue by trying to show that there is pair of the form (q, P ), where q ∈ Q and P ∈

([p 1 ]∪{0})ו • •×([p m ]∪{0}
), that can be obtained from (q j+1 , P j+1 ) by performing a transition on the h 2 -th head. If this is the case then we are ready and the proof finishes. Assume otherwise. Then again we can assume without loss of generality that there is a pair of the form t k ∈ I of the form (h

2 , h 3 ) ∈ [m] × [m] such that the subword in Q S k • ([p h 2 ] × [p h 3 ]
) that immediately follows q k (r h 2 , r h 3 ) in the run λ k is of the form q k (r h 2 , r h 3 + 1). (That is, the run λ k continues from q k (r h 2 , r h 3 ) by moving its second head).

Since T is acyclic and finite, if we iteratively continue in this way from h 2 we will either have to find some h ∈ H such that there is pair of the form (q, P ), where q ∈ Q and

P ∈ ([p 1 ] ∪ {0}) × • • • × ([p m ] ∪ {0}
), that can be obtained from (q j+1 , P j+1 ) by performing a transition on the h-th head, or we will have to stop in some h ∈ H that is a leaf in T . But clearly for this h it must be possible to show that there is pair of the form (q, P ), where q ∈ Q and P ∈

([p 1 ] ∪ {0}) × • • • × ([p m ] ∪ {0}
), that can be obtained from (q j+1 , P j+1 ) by performing a transition on the h-th head. This shows that the sequence does not fail in stage j + 1.

We now continue with the proof of the first part of the theorem. Since the sequence does not fail, and from stage j into stage j + 1 the position of at least one head moves to the right of its tape, the sequence must stop in some stage j ≥ 0 with associated pair (q j , P j ). Then P j = (p 1 , . . . , p m ). Assume that qj = (u i 1 , . . . , u im , q 1 , . . . , q ), where each u i k is a state in N i k and each q k is a state in S k . Then, from the properties of the sequence, it must be the case that u i k (p k ) appears as a subword in the accepting run ρ i k , for each 1 ≤ k ≤ m, and for each 1

≤ k ≤ such that t k = (k 1 , k 2 ) ∈ [m] × [m] it is the case that q k (p k 1 , p k 2 )
appears as a subword in the accepting run λ k . Hence u i k = u i k ,p k -1 and q k = q k,r k .

It easily follows from the definition of the sequence (q 0 , P 0 )(q 1 , P 1 ) • • • and the transition function δ of A(R, S, I), that the following holds for each k < j: If (q k+1 , P k+1 ) is obtained from (q k , P k ) by performing a transition on the k -the head, 1 ≤ k ≤ m, then (q k+1 , P k+1 ) is a valid transition from (q k , P k ) over w in the k -th head. Further, assume that ā = (π 1 ( w))[p 1 ], . . . , (π n ( w))[p n ] , then δ(q j , ā) contains a pair of the form (q j+1 , {[m]}), where:

qj+1 := u i 1 ,p 1 , • • • , u im,pm , q 1,r 1 +1 , • • • , q ,r +1 .
Clearly, qj+1 ∈ F (that is, qj+1 is a final state of A(R, S, I)) and we conclude that q0 P 0 q1 P 1 • • • qj P j qj+1 is an accepting run of A(R, S, I) over w, which was to be proved.

We now explain how Theorem 6.7 follows from Lemma 6.8. The lemma tells us that in order to solve acyclic instances of GenInt S (REC) we can construct, from the m-ary recognizable relation R, the binary rational relation S and the acyclic I ⊆ [m] × [m], the m-tape automaton A(R, S, I), and then check A(R, S, I) for nonemptiness. The latter can be done in polynomial time in the size of A(R, S, I) by performing a simple reachability analysis in the states of A(R, S, I). This gives us a simple exponential time bound for the complexity of solving acyclic instances of GenInt S (REC). However, as we mentioned before, each state in A(R, S, I) is of polynomial size. Thus, checking whether A(R, S, I) is nonempty can be done in nondeterministic PSpace by using a standard "on-the-fly" construction of A(R, S, I) as follows: Whenever the reachability algorithm for checking emptiness of A(R, S, I) wants to move from a state r 1 of A(R, S, I) to a state r 2 , it guesses r 2 and checks whether there is a transition from r 1 to r 2 . Once this is done, the algorithm can discard r 1 and follow from r 2 . Thus, at each step, the algorithm needs to keep track of at most two states, each one of polynomial size. From Savitch's theorem, we know that PSpace equals nondeterministic PSpace. This shows that acyclic instances of GenInt S (REC) can be solved in PSpace.

The proof of the second part of the theorem is by an easy reduction from the PCP problem (e.g. in the style of the proof of the second part of Theorem 6.10). query of the form

ϕ(x) = ∃ȳ m i=1 (u i ρ i :L i -→ u i ) ∧ (i,j)∈I S(ρ i , ρ j ) .
Given a graph G and tuple ā of nodes, the algorithm constructs (using the proof of Lemma 4.1) in deterministic logarithmic space an acyclic instance of GenInt S (REC), given by recognizable relation R of fixed arity m (this follows from the fact that ϕ(x) is fixed), and fixed

I ⊆ [m] × [m],
such that the answer to this instance is 'yes' iff G |= ϕ(ā). Since the arity of R is fixed, our previous observation tells us that we can solve the instance of GenInt S (REC) given by R and I in NLogSpace. But NLogSpace reductions compose, and hence the data complexity of the query evaluation problem for CRPQ(S) queries is also NLogSpace. Thus, we get not only the possibility of extending CRPQs with rational relations but also a good complexity of query evaluation. The NLogSpace-data complexity matches that of RPQs, CRPQs, and ECRPQs [START_REF] Consens | GraphLog: a visual formalism for real life recursion[END_REF][START_REF] Cruz | A graphical query language supporting recursion[END_REF][START_REF] Barceló | Expressive languages for path queries over graph-structured data[END_REF], and the combined complexity matches that of first-order logic, or ECRPQs without extra relations.

The next natural question is whether we can recover decidability for weaker syntactic conditions by putting restrictions on a class of relations S. The answer to this is positive if we consider directed acyclicity of I, rather than acyclicity of the underlying undirected graph of I. Then we get decidability for the class of SCR relations. In fact, we have a dichotomy similar to that of Theorem 6.7. Theorem 6.10.

• Let S be a relation from SCR. Then (REC ∩ I S)

? = ∅ is decidable in NExptime if I is a directed acyclic graph.
• There is a relation I with a directed cycle and S ∈ SCR such that (REC ∩ I S) ? = ∅ is undecidable.

Proof. We start by proving the first item. In order to do that, we first prove a small model property for the size of the witnesses of the instances in (REC ∩ I S) ? = ∅, when S is a relation in SCR and I is a DAG. Let R be an m-ary recognizable relation, m > 0, and I ⊆ [m] × [m] that defines a DAG. Assume that both R and S are over Σ. Then the following holds: Assume R ∩ I S = ∅. There is w = (w 1 , . . . , w m ) ∈ (Σ * ) m of at most exponential size that is accepted by R and such that (w i , w j ) ∈ S, for each (i, j) ∈ I. We prove this small model property by applying usual cutting techniques.

Assume that R is given as

i N i 1 × • • • × N im ,
where each N i j is an NFA over Σ. Further, assume that S is given as one of the 2-tape NFAs used in the PSpace upper bound of Theorem 6.7. That is, S defined by the tuple

(Q S , Σ, Q 0 S , δ S , Q F S )
, where Q S is the set of states, the set of initial states is Q 0 S , the set of final states is Q F S , and δ S :

Q S × (Σ ∪ {ε}) × (Σ ∪ {ε}) → 2 Q×({1,2}∪{{1,2}}
) is the transition function. Assume also that there is ū = (u 1 , . . . , u m ) ∈ (Σ * ) m that is accepted by R such that (u i , u j ) ∈ S, for each (i, j) ∈ I. Then ū is accepted by

N i 1 × • • • × N im , for some i.
Since I is a DAG it has a topological order on [m]. We assume without loss of generality that such topological order is precisely the linear order on [m]. We prove the following invariant on 1 ≤ ≤ m: There exists w = (w 1 , . . . , w m ) ∈ (Σ * ) m such that (1) w is accepted by R, (2) (w j , w k ) ∈ S, for each (j, k) ∈ I, and (3) each w with ≤ is of at most exponential size. Clearly this proves our small model property on = m. The proof is by induction.

The basis case is = 1. We start from ū and "cut" its first component in order to satisfy the invariant. By using standard pumping techniques it is possible to show that there is a subsequence w 1 of u 1 of size at most O(|N i 1 |) that is accepted by N i 1 . Clearly the tuple (w 1 , u 2 , . . . , u m ) belongs to R. Further, for each pair of the form (1, j) in I it is the case that (w 1 , u j ) ∈ S. This is the case because (u 1 , u j ) ∈ S, u 1 w j and S ∈ SCR. Notice that we do not need to consider pairs of the form (j, 1) since we are assuming that the linear order on [m] is a topological order of I. This implies that (w 1 , u 2 , . . . , u m ) satisfies our invariant on = 1.

Assume now that the invariant holds for < m. Then there exists w = (w 1 , . . . , w m ) ∈ (Σ * ) m such that (1) w is accepted by R, (2) (w j , w k ) ∈ S, for each (j, k) ∈ I, and (3) each w with ≤ is of at most exponential size. We proceed to "cut" w +1 while preserving the invariant. Let I( + 1) be {1 ≤ j ≤ | (j, + 1) ∈ I}. Let ρ j be an accepting run of S over (w j , w +1 ), for each j ∈ I( + 1). Further, let P be the set of all positions 1 ≤ k ≤ |w +1 | such that for some j ∈ I( + 1) the accepting run ρ j contains a subword of the form q (k , k) q (k + 1, k), where q, q ∈ Q S and 1 ≤ k ≤ |w j |. That is, P defines the set of positions over w +1 , in which the accepting run ρ j of S over (w j , w +1 ), for some j ∈ I( + 1), makes a move on the head positioned over w j . Intuitively, these are the positions of w +1 that should not be "cut" in order to maintain the invariant. Notice that the size of P is bounded by s := Σ 1≤ ≤ |w |, and hence from the inductive hypothesis the size of P is exponentially bounded.

By using standard pumping techniques it is possible to show that there is a subsequence w +1 of w +1 of size at most

|N i +1 | • |P| • |I( + 1) • |Q S | • |Σ| + 2,
such that w +1 is accepted by N i +1 and (w j , w +1 ) is accepted by S, for each j ∈ I( + 1). Assume this is not the case, and that the shortest subsequence w +1 of w +1 that satisfies this condition is of length strictly bigger than

|N i +1 | • |P| • |I( + 1)| • |Q S | • |Σ| + 2.
Then there exist two positions 1 ≤ i < j ≤ |w +1 | such that (i) k ∈ P, for each i ≤ k ≤ j, (ii) the labels of i and j in w +1 coincide, (iii) the run ρ s assigns the same state to both i and j, for each s ∈ I( + 1), and (iv) some accepting run of N +1 assigns the same state to both i and j. Let w +1 be the subsequence of w +1 that is obtained by cutting all positions i ≤ k ≤ j -1. Clearly, w +1 is shorter than w +1 and is accepted by N +1 . Further, (w s , w +1 ) is accepted by S, for every s ∈ I( + 1). This is because (w s , w +1 ) is invariant with respect to the accepting run ρ s , for each s ∈ I( + 1), as the cutting does not include elements in P (that is, we only cut elements in which ρ s does not need to synchronize with the head positioned over w s ) and ρ s assigns the same state to both i and j, which have, in addition, the same label. This is a contradiction.

We claim that w = (w 1 , . . . , w , w +1 , w +2 , • • • , w m ) ∈ (Σ * ) m satisfies the invariant. Clearly, w is accepted by R since w +1 is accepted by N i +1 and, by inductive hypothesis, w j is accepted by N i j , for each j ∈ [m] \ { + 1}. Further, simply by definition it is the case that (w j , w +1 ) ∈ S, for each j ∈ I( +1). Moreover, (w +1 , w j ) ∈ S, for each ( +1, j) ∈ I, simply because w +1 It is now simple to prove the first part of the theorem using the small model property. In fact, in order to check whether R ∩ I S = ∅, for S ∈ SCR, we only need to guess an exponential size witness w, and then check in polynomial time that it satisfies R and each projection in I satisfies S. This algorithm clearly works in nondeterministic exponential time. Now we prove the second item. We reduce from the PCP problem. Assume that the input to PCP are two equally long lists a 1 , a 2 , . . . , a n and b 1 , b 2 , . . . , b n of strings over alphabet Σ. Recall that we want to decide whether there exists a solution for this input, that is, a sequence of indices i 1 , i 2 , . . . , i k such that 1 ≤ i j ≤ n (1 ≤ j ≤ k) and a i 1

a i 2 • • • a i k = b i 1 b i 2 • • • b i k .
Assume without loss of generality that Σ is disjoint from N. Corresponding to every input a 1 , a 2 , . . . , a n and b 1 , b 2 , . . . , b n of PCP over alphabet Σ, we define the following:

• An alphabet Σ(n) := Σ ∪ {1, 2, . . . , n};

• a regular language R a,n := ( 1≤i≤n a i • i) * ;

• a regular language R b,n := ( 1≤j≤n b j • j) * .

Consider a ternary recognizable relation R over alphabet Σ(n) ∪ { , †}, where and † are symbols not appearing in Σ(n), defined as

•Σ * × † •R a,n × † •R b,n .
Further, consider a binary relation S over (Σ(n) ∪ { , †}) * defined as the union of the following sets: Assume first that R ∩ I S = ∅. Hence there are words w 1 ∈ ( • Σ * ), w 2 ∈ ( † • R a,n ) and w 3 ∈ ( † • R b,n ), such that (w i , w j ) belongs to S , for each (i, j) ∈ I. Since (2, 3) ∈ I, it must be the case that (w 2 , w 3 ) belongs to S . Thus, since the first symbol of both w 2 and w 3 is †, it must be the case that (w 2 ) {1,...,n} (w 3 ) {1,...,n} . For the same reasons, and given that (3, 2) ∈ I, it must be the case that (w 3 ) {1,...,n} (w 2 ) {1,...,n} . We conclude that (w 2 ) {1,...,n} = (w 3 ) {1,...,n} .

Since (1, 2) ∈ I, it must be the case that (w 1 , w 2 ) belongs to S . Thus, since the first symbol of w 1 is and the first symbol of w 2 is †, it must be the case that (w 1 ) Σ (w 2 ) Σ . For the same reasons, and given that (2, 1) ∈ I, it must be the case that (w 2 ) Σ (w 1 ) Σ . We conclude that (w 1 ) Σ = (w 2 ) Σ .

Mimicking the same argument, but this time using the fact that {(1, 3), (3, 1)} ⊆ I, we conclude that (w 1 ) Σ = (w 3 ) Σ . But then (w 2 ) Σ = (w 3 ) Σ (because (w 1 ) Σ = (w 2 ) Σ ). The other direction, that is, that the fact that the instance of the PCP problem given by a 1 , . . . , a n and b 1 , . . . , b n has a solution implies that R ∩ I S = ∅, can be proved using the same arguments.

In particular, if we have a CRPQ(S) query of the form

∃ȳ m i=1 (u i χ i :L i -→ u i ) ∧ (i,j)∈I S(χ i , χ j ) ,
where I is acyclic (as a directed graph) and S ∈ SCR, then query evaluation has NExptime combined complexity.

The proof of this result is quite different from the upper bound proof of Theorem 6.7, since the set of witnesses for the generalized intersection problem is no longer guaranteed to be rational without the undirected acyclicity condition. Instead, here we establish the finite-model property, which implies the result. Also, as a corollary to the proof of Theorem 6.10, we get the following result: Proposition 6.11. Let S ∈ SCR be a partial order. Then GenInt S (REC) is decidable in NExptime.

Proof. As in the previous proof, we start by proving a small model property for the size of the witnesses of the instances in GenInt S (REC), for S a partial order in SCR. Let R be an m-ary recognizable relation, m > 0, and I ⊆ [m] × [m]. Assume that both R and S are over Σ. Then the following holds: Assume R ∩ I S = ∅. There is w = (w 1 , . . . , w m ) ∈ (Σ * ) m of at most exponential size that is accepted by R and such that (w i , w j ) ∈ S, for each (i, j) ∈ I. We prove this small model property by applying usual cutting techniques.

Assume that R is given as

i N i 1 × • • • × N im ,
where each N i j is an NFA over Σ. Further, assume that S is given as the 2-tape transducer S defined by the tuple (Q S , Σ, Q 0 S , δ S , Q F S ), where Q S is the set of states, the set of initial states is Q 0 S , the set of final states is Q F S , and δ S : Q S × (Σ ∪ {ε}) × (Σ ∪ {ε}) → 2 Q×({1,2}∪{{1,2}}) is the transition function. Assume also that there is ū = (u 1 , . . . , u m ) ∈ (Σ * ) m that is accepted by R and such that (u i , u j ) ∈ S, for each (i, j) ∈ I. Then ū is accepted by N i 1 × • • • × N im , for some i.

Let I + be the transitive closure of I. Notice, since S defines a partial order over Σ * , that (u j , u k ) ∈ S, for each (j, k) ∈ I + . Further, for every pair (j, k) ∈ [m] × [m] such that {(j, k), (k, j)} ⊆ I + we must have that u j = u k . We need to maintain such equality when applying our cutting techniques over ū. In order to do that we define an equivalence relation E I over [m] as follows: . Then it must be the case that (u 1 , . . . , u p ) ∈ (Σ * ) p belongs to R and (u j , u k ) ∈ S, for each (j, k) ∈ I([m]/E I ). Further, from every witness to the fact that R ∩ I([m]/E I ) S = ∅ we can construct in polynomial time a witness to the fact that R∩ I S = ∅. Hence, in order to prove our small model property it will be enough to prove the following: There is w = (w 1 , . . . , w p ) ∈ (Σ * ) p of at most exponential size (in R) that is accepted by R and such that (w j , w k ) ∈ S, for each (j, k) ∈ I([m]/E I ).

The latter can be done by mimicking the inductive proof of the first part of Theorem 6.10. We only have to deal now with the issue that some of the NFAs that define R may be exponential in the size of R. However, by following the inductive proof one observes that this is not a problem, and that the same exponential bound holds in this case.

It is now simple to prove the first part of the theorem using the small model property. In fact, in order to check whether R ∩ I S = ∅, for S a partial order in SCR, we only need to guess an exponential size witness w, and then check in exponential time that it satisfies R and each projection in I satisfies S. This algorithm clearly works in nondeterministic exponential time.

By applying similar techniques to those in the proof of Theorem 6.9 we obtain the following. Corollary 6.12. If S ∈ SCR is a partial order, then CRPQ(S) queries can be evaluated with NExptime combined complexity. In particular, CRPQ( ) queries have NExptime combined complexity.

We do not have at this point a matching lower bound for the complexity CRPQ( ) queries. Notice that an easy PSpace lower bound follows by a reduction from the intersection problem for NFAs, as the one presented in the proof of Theorem 6.7.

The last question is whether these results can be extended to other relations considered here, such as subword and suffix. We do not know the result for subword (which appears to be hard), but we do have a matching complexity bound for the suffix relation. Proposition 6.13. The problem GenInt suff (REC) is decidable in NExptime. In particular, CRPQ( suff ) queries can be evaluated with NExptime combined complexity.

Proof. We only prove that GenInt suff (REC) is decidable in NExptime. The fact that CRPQ( suff ) queries can be evaluated with NExptime combined complexity follows easily from this by applying the same techniques as in the proof of Theorem 6.9. query both topology and data have been proposed recently [START_REF] Grumberg | Variable automata over infinite alphabets[END_REF][START_REF] Libkin | Regular path queries on graphs with data[END_REF]. A natural question is to extend the positive results shown here to such a setting.

R

Theorem 5 . 1 .

 51 The problems (REG ∩ suff ) ? = ∅ and (REG ∩ ) ? = ∅ are undecidable.

Claim 5 .

 5 7.1. t ≤ n.

  or σ(a) otherwise; likewise for σ # . By definition of strict codirect solution, we have the following. Claim 5.8.1. σ(w[1]) ∈ Γ. Proof. Indeed, if σ(w[1]) = Γ, then σ(w[1]) = ε and |σ(w[1])| = 0, and then condition 4 of strict codirectness stating that |σ(w[1])| > |v 1 |, would be falsified. Let us define the function g :

Figure 1 :

 1 Figure 1: Exemplary reduction from PEP reg to (REG∩ ) ? = ∅, for the case σ(w) = abacaba, σ (w) = aababacacbcba.

  1 by Claim 5.8.1. Claim 5.13.2. i j+1 ≤ g(i j ) Proof. By means of contradiction, suppose g(i j ) < i j+1 . Then, |σ(w[1..g(i j )])| = |{i ∈ [g(i j )] | ∃j.(i, j) ∈ G}| (by Observation 5.13.1) = |{i ∈ [g(i j )] | ∃j.(i, j) ∈ G}| (since g(i j ) < i j+1 ) = |σ (w[1..g(i j )])|. (by Observation 5.13.2) In other words, there is some k < m such that |σ(w[1..k])| = |σ (w[1.

5 . 2 . 3 .

 523 by Claim 5.13.2) ũi j (by Observation 5.11) = ũg -1 (g(i j )) (by Observation 5.10) = u g(i j ) (by def. of u ) On the other hand, û|G| u g(i |G| ) • u m+1 = u m • u m+1 . By Claim 5.8.3, g is increasing. Hence, u u . By Claims 5.13.1 and 5.13.3, we conclude that R ∩ = ∅. Subsequence-closed relations. The next question is how far we can extend the decidability of (RAT ∩ ) ? = ∅. It turns out that if we allow one projection of a rational relation to be closed under taking subsequences, then we retain decidability. Let R ⊆ Σ * × Γ * be a binary relation. Define another binary relation R = {(u, w) | u u and (u , w) ∈ R for some u } Then the class of subsequence-closed relations, or SCR, is the class {R | R ∈ RAT}. Note that the subsequence relation itself is in SCR, since it is obtained by closing the (regular) equality relation under subsequence. That is, = {(w, w) | w ∈ Σ * } . Not all rational relations are subsequence-closed (for instance, subword is not).

  , and Proposition 5.4. Of course the complexity is non-multiplyrecursive, since the problem subsumes (REG ∩ ) ? = ∅ of Theorem 5.5.

  ) Σ (by (6.1)) = (π j (w )[m + 1..]) Σ Hence, we showed that there are some , such that (π i (w )[1.. ]) Σ (π j (w )[1.. ]) Σ and (π i (w )[ + 1..]) Σ (π j (w )[ + 1..]) Σ , for = m -|x m .α ij | and = m . Thus, (π i (w )) Σ (π j (w )) Σ .This means that ((π 1 (w )) Σ , . . . , (π k (w )) Σ ) ∈ G and thus ((π 1 (w )) Σ , . . . , (π k (w )) Σ ) ∈ R ∩ G. But this cannot be since |w | < |w| and w is of minimal length. The contradiction arises from the assumption that R ∩ G = ∅. Then, R ∩ G = ∅.

  w +1 and S ∈ SCR. The remaining pairs in I are satisfied by induction hypothesis. Finally, w +1 is of size at most O(|N i +1 | • |P| • |I( + 1)| • |Q S | • |Σ|), and hence, by inductive hypothesis, it is of size at most exponential. By inductive hypothesis, each w with ≤ is of size at most exponential.

( 1 )

 1 {(w, w ) ∈ ( † • (Σ(n)) * ) × ( † • (Σ(n)) * ) | w {1,...,n} w {1,...,n} }. (2) {(w, w ) ∈ ( † • (Σ(n)) * ) × ( • Σ * ) | w Σ w Σ }. (3) {(w, w ) ∈ ( • Σ * ) × ( † • (Σ(n)) * ) | w Σ w Σ }.The intuition is that S takes care that indices in the sequences are consistent. the It is easy to see that S is a rational relation. This implies that S is in SCR.From input a 1 , . . . , a n and b 1 , . . . , b n to the PCP problem, we construct an instance of GenInt S (REC) defined by the recognizable relation R andI = {(1, 2),(2, 1), (1, 3), (3, 1), (2, 3), (3, 2)}.We claim that R ∩ I S = ∅ if and only if the PCP instance given by lists a 1 , . . . , a n and b 1 , . . . , b n has a solution.

Assume (w 2 )

 2 {1,...,n} = (w 3 ) {1,...,n} = i1 i 2 • • • i n , where each i j ∈ [n]. Then from the fact that (w 2 ) Σ = (w 3 ) Σ we conclude that a i 1 a i 2 • • • a in = b i 1 b i 2 • • • b in ,and hence that the instance of the PCP problem given by a 1 , . . . , a n and b 1 , . . . , b n has a solution.

E

  I := {(j, k) ∈ [m] × [m] | j = k or {(j, k), (k, j)} ⊆ I + }. Hence E I contains all pairs (j, k) ∈ [m] × [m] such that I implies u j = u k . Take the quotient [m]/E I , and consider the restriction I([m]/E I ) of I over [m]/E I , defined in the expected way:([j] E I , [k] E I ) ∈ I([m]/E I ) if and only if (j , k ) ∈ I, for some j ∈ [j] E I and k ∈ [k] E I . Notice that I([m]/E I ) defines a DAG over [m]/E I .Consider now a new input to GenInt S (REC), given this time byI([m]/E I ) ⊆ ([m]/E I )× ([m]/E I ), and the recognizable relation R defined as[j] E I ∈[m]/E I M [j] E I i , where M [j] E I i = k∈[j] E I N i k .Notice that this new input may be of exponential size in the size of R.Assume that [m]/E I consists of p ≤ m equivalence classes and, without loss of generality, that these correspond to the first p indices of [m]. Hence each product in R is of the formM i 1 × • • • × M ip ,where M i j is defined as the intersection of all NFAs in the equivalence class [j] E I . Also, I([m]/E I ) is the restriction of I to [p] × [p]

Figure 2 :

 2 Figure 2: Complexity of the intersection and generalized intersection problems, and combined complexity of graph queries for subword ( ), suffix ( suff ), and subsequence ( ) relations. NMR stands for non-multiply-recursive lower bound.

This is the full version of the conference paper [3]. Partial support provided by Fondecyt grant 1110171, EPSRC grant G049165, and FET-Open Project FoX, grant agreement 233599.

6.3.

CRPQs with rational relations. The acyclicity condition gives us a robust class of queries, with an easy syntactic definition, that can be extended with arbitrary rational relations. Recall that CRPQ(S) queries are those of the form

S(χ i , χ j ) , see (4.2) in Sec. [START_REF] Barceló | Expressive languages for path queries over graph-structured data[END_REF]. We call such a query acyclic if G I , the underlying undirected graph of I, is acyclic. Theorem 6.9. The query evaluation problem for acyclic CRPQ(S) queries is decidable for every binary rational relation S. Its combined complexity is PSpace-complete, and data complexity is NLogSpace-complete.

Proof. We provide a nondeterministic PSpace algorithm that solves the query evaluation problem when we assume the query to be part of the input (i.e. combined complexity). Then the result will follow from Savitch's theorem, that states that PSpace equals nondeterministic PSpace.

Given a graph G, a tuple ā of nodes, and acyclic CRPQ(S) query of the form

the algorithm starts by guessing a polynomial size assignment b for the existentially quantified variables of ϕ(x), that is, the variables in ȳ. It then checks that

If this is the case the algorithm accepts and declares that G |= ϕ(ā). Otherwise it rejects and declares that G |= ϕ(ā). By using essentially the same techniques as in the proof of Lemma 4.1, one can show that there is a polynomial time translation that, given G and ψ(ā, b), constructs an acyclic instance of GenInt S (REC) such that the answer to this instance is 'yes' iff G |= ψ(ā, b). From Theorem 6.7 we know that acyclic instances of GenInt S (REC) can be solved in PSpace, and hence that the algorithm described above can be performed in nondeterministic PSpace.

With respect to the data complexity, we start with the following observation. Acyclic instances of GenInt S (REC) can be solved in NLogSpace for m-ary relations in REC, if we assume m to be fixed. The proof of this fact mimicks the proof of the PSpace upper bound in Theorem 6.7, but this time we assume the arity of R to be fixed. In such case A(R, S, I) is of polynomial size, and each one of its states is of logarithmic size. We can easily check A(R, S, I) for nonemptiness in NLogSpace in this case, by performing a standard "on-thefly" reachability analysis.

We provide an NLogSpace algorithm that solves the query evaluation problem when we assume the query to be fixed (i.e. data complexity). Consider a fixed acyclic CRPQ(S)

We start by proving a small model property for the size of the witnesses of the instances in GenInt suff (REC). Let R be an m-ary recognizable relation, m > 0, and

Assume that both R and suff are over Σ. Then the following holds: Assume it is the case that R ∩ I { suff } = ∅. There is w = (w 1 , . . . , w m ) ∈ (Σ * ) m of at most exponential size that is accepted by R and such that w i suff w j , for each (i, j) ∈ I. We prove this small model property by applying cutting techniques.

Assume that R is given as

where each N i j is an NFA over Σ. We assume, without loss of generality, that I defines a DAG over Assume then that there is ū = (u 1 , . . . , u m ) ∈ (Σ * ) m that is accepted by R and such that u i suff u j , for each (i, j) ∈ I. Then ū is accepted by

Assume that the length of u j is p j ≥ 0, for each 1 ≤ j ≤ m. Our goal is to "cut" ū in order to obtain an exponential size witness to the fact that R ∩ I { suff } = ∅.

We recursively define the set M k of marked positions in string u k , 1 ≤ k ≤ m, as follows:

• No position in u 1 is marked.

• For each 1 < k ≤ m the set M k of marked positions in u k is defined as the union of the marked positions in u k with respect to j, for each j < k such that (j, k) ∈ I, where the latter is defined as follows. Assume that M j is the set of marked positions in u j . Then the set M k of positions 1 ≤ ≤ p k that are marked in u k with respect to j is {r

and hence 1 ≤ r + p kp j ≤ p k for each r ∈ M j and for r = 1). Intuitively, M k consists of those positions 1 ≤ ≤ p k such that for some j < k with (j, k) ∈ I + , where I + is the transitive closure of I, it is the case that that

Or, in other words, the fact that u j suff u k starts to be "witnessed" at position of u k . We assume the M k 's to be linearly ordered by the restriction of the linear order 1 < 2 < • • • < m to M k . By a simple inductive argument it is possible to prove that the size of M k is polynomially bounded in m, for each 1 ≤ k ≤ m.

Since u j suff u k , for each (j, k) ∈ I, this implies that the labels in some positions of u j are preserved in the respective positions of u k that witness the fact that u j suff u k . The important thing to notice is that, since we are dealing with suff , the following holds: For each position p that is "copied" from u j into u k in order to satisfy u j suff u k , the distance from p to the last element of u j equals the distance from the copy of p in u k to the last position of u k . That is, distances to the last element of the string are preserved when copying positions (and labels) in order to satisfy I. We need to take care of this information when "cutting" ū in order to obtain an exponential size witness for the fact that R ∩ I { suff } = ∅. In order to do this we define for each 0

a binary relation r on {u 1 , . . . , u m } such that u j r u k if p jr > 0 and (j, k) ∈ I. This implies that position p jr of u j is "copied" as position p kr of u k in order to satisfy the fact that u j suff u k . But in order to consistently "cut" ū, we need to preserve the suffix relation both with respect to forward and backward edges of the graph defined by I. In order to do that we define r as ( r ∪ ( r ) -1 ). Further, since suff is a partial order over Σ * , and hence it defines a transitive relation, it is important for us also to consider the transitive closure ( r ) + of the binary relation r . Intuitively, u j ( r ) + u k , for 1 ≤ j, k ≤ m, if position p jr of u j has to be "copied" into position p kr of u k in order for ū to satisfy the pairs in I with respect to suff .

Let

We claim the following: There is w = (w 1 , . . . , w m ) ∈ (Σ * ) m such that: (1) w is accepted by R, (2) w i suff w j , for each (i, j) ∈ I, and (3) for each 1 ≤ k ≤ m the number of positions in w k between any two consecutive positions in M k is bounded by s • t • 2 m • |Σ| m . This clearly implies our small model property.

Assume that ū does not satisfy this. Then there exists 1 ≤ j ≤ m and two consecutive positions p and p in M j , such that the number of positions in u j between p and p is bigger than s • t • 2 m • |Σ| m . But this implies that there are two positions p jr and p jr (r > r ) between p and p in u j such that the following hold:

Intuitively, this says that the set of strings in which position p jr of u j is "copied" coincides with the set of strings in which position p jr of u j is "copied".

(2) For each k such that u j ( r ) + u k it is the case that neither p kr nor p kr is a marked position in M k , and there is no marked position in M k in between p kr and p kr in u k .

(3) The state assigned by the accepting run of N i j over u j to position p jr of u j is the same than the one assigned to position p jr . (4) The state assigned by the accepting run of N i k over u k to the "copy" p kr of position p jr over u k , for each k such that u j ( r ) + u k , is the same than the one assigned to the "copy" p kr of position p jr over u k .

(5) The symbol in position p jr of u j is the same as the symbol in position p jr of u j .

(6) For each k such that u j ( r ) + u k it is the case that the symbol in position p kr of u k is the same as the symbol in position p kr of u k . Intuitively, this states that if we "cut" the string u j from position p jr + 1 to p jr , and string u k from position p kr + 1 to p kr , for each k such that u j ( r ) + u k , then the resulting ū = (u 1 , . . . , u m ) ∈ (Σ) m satisfies the following: (1) ū is accepted by R, and (2) for each (j, k) ∈ I it is the case that u j suff u k . We formally prove this below. Notice for the time being that this implies our small model property. Indeed, if we recursively apply this procedure to ū we will end up with w = (w 1 , . . . , w m ) ∈ (Σ * ) m such that: (1) w is accepted by R, (2) w j suff w k , for each (j, k) ∈ I, and (3) for each 1 ≤ k ≤ m the number of positions in w k between any two consecutive positions in M k is bounded by

Let ū = (u 1 , . . . , u m ) ∈ (Σ) m be the result of applying once the cutting procedure described above to ū = (u 1 , . . . , u m ), starting from string ūj by cutting positions from p jr + 1 to p jr (r > r ). It is not hard to see that ū is accepted by R, since each u k has been cut in a way that is invariant with respect to the accepting run of N i k over u k . Assume that ( , k) ∈ I. We need to prove that u suff u k . If u = u and u k = u k then u suff u k by assumption. Assume then that at least one of u and u k has been cut. Suppose first that u has been cut from position pr + 1 to position pr in order to obtain u . Then u j ( r ) + u and u j ( r ) + u . Clearly, it is also the case that u r u k and u r u k , which implies that u j ( r ) + u k and u j ( r ) + u k . Thus, u k is also cut from position p kr + 1 to p kr in order to obtain u k , and hence u suff u k . Suppose, on the other hand, that u has not been cut but u k has been cut from position p kr + 1 to position p kr in order to obtain u k . We consider three cases:

(1) r > p j -1. Then clearly u k suff u j .

(2) r ≤ p j -1 and r > p j -1. This cannot be the case since then either p kr is a marked position in M k (when r = p j -1), or p kr and p kr have a marked position in M k in between (namely, p kp j + 1). Any of these contradicts the fact that a cutting of u k could be applied from position p kr to position p kr in order to obtain u k . (3) r < p j -1 and r ≥ p j -1. Similar to the previous one. We can finally prove the theorem using the small model property. In fact, in order to check whether R ∩ I { suff } = ∅ we only need to guess an exponential size witness w, and then check in polynomial time that it satisfies R and each projection in I satisfies suff . This algorithm clearly works in nondeterministic exponential time.

Conclusions

Motivated by problems arising in studying logics on graphs (as well as some verification problems), we studied the intersection problem for rational relations with recognizable and regular relations over words. We have looked at rational relations such as subword , suffix suff , and subsequence , which are often needed in graph querying tasks. The main results on the complexity of the intersection and generalized intersection problems, as well as the combined complexity of evaluating different classes of logical queries over graphs are summarized in Fig. 2. Several results generalizing those (e.g., to the class of SCR relations) were also shown. Two problems related to the interaction of the subword relation with recognizable relations remain open and appear to be hard.

From the practical point of view, as rational-relation comparisons are demanded by many applications of graph data, our results essentially say that such comparisons should not be used together with regular-relation comparisons, and that they need to form acyclic patterns (easily enforced syntactically) for efficient evaluation.

So far we dealt with the classical setting of graph data [START_REF] Angles | Survey of graph database models[END_REF][START_REF] Calvanese | Containment of conjunctive regular path queries with inverse[END_REF][START_REF] Calvanese | View-based query processing and constraint satisfaction[END_REF][START_REF] Consens | GraphLog: a visual formalism for real life recursion[END_REF][START_REF] Cruz | A graphical query language supporting recursion[END_REF] in which the model of data is that of a graph with labels from a finite alphabet. In both graph data and verification problems it is often necessary to deal with the extended case of infinite alphabets (say, with graphs holding data values describing its nodes), and languages that