Polynomial Rewritings for Linear Existential Rules

1 Introduction

This paper considers the well-known setting of ontologybased query answering (OBQA), where an ontology is used to enrich the extensional dataset with intensional knowledge. A database D is combined with an ontology Σ, while an input query is answered against the logical theory (D ∪Σ). In this setting, Description Logics (DLs) and existential rules are popular ontology languages, while conjunctive queries (CQs) is the main querying tool. Thus, efficient procedures for CQ answering under such languages are of great importance.

Among KR researchers there is a clear consensus that the required level of scalability in OBQA can only be achieved via query rewriting, which attempts to reduce OBQA into the problem of evaluating a query over a relational database. Two query languages are usually considered: first-order queries, which can be translated into standard SQL, and non-recursive Datalog queries, which can be translated into SQL with view definitions (SQL DDL). Therefore, query rewriting allows for the exploitation of existing technology provided by standard RDBMSs. The main approaches to query rewriting are the pure approach [Calvanese et al., 2007] and the combined approach [Lutz et al., 2009]:

Pure Approach: An ontologyΣ can be combinedwith a CQ q into a database query qΣ, such that, for every database D, qΣ over D yields exactly the same result as q evaluated against (D∪Σ). This approach applies only to languages for which the data complexity of CQ answering is below PTIME; thus, useful formalisms with PTIMEhard data complexity are immediately excluded.

Combined Approach: A refined approach to query answering, which overcomes the above shortcoming, is the combined approach that allows for the encoding of the consequences of the ontology in the given database. An ontology Σ can be incorporated together with a given CQ q into a database query qΣ, but also with a given database D into a database DΣ, such that qΣ over DΣ yields the same result as q evaluated over (D ∪ Σ).

Both approaches have been applied to DLs and classes of existential rules; see, e.g., [Calvanese et al., 2007; Lutz et al., 2009; Kontchakov et al., 2010; 2011; Cal`ı et al., 2012a; 2012b; Gottlob et al., 2014b]. However, they both suffer from a crucial weakness, which may revoke the key advantage of query rewriting, i.e., the use of RDBMSs: (pure or combined) rewriting algorithms may generate from a reasonably sized CQ an exponentially sized database query, which can be prohibitive for efficient execution by an RDBMS. This naturally leads to the polynomial version of the pure approach and the combined approach, where the rewriting algorithms are required to terminate after polynomially many steps.

The polynomial pure approach has been applied to DLLiteF [Kontchakov et al., 2010], one of the core languages of the DL-Lite family of DLs, and to unary inclusion dependencies [Kikot et al., 2011], that is, a small fragment of inclusion dependencies. The polynomial combined approach has been applied to ELHdr ⊥ [Lutz et al., 2009], an extension of the well-known DL EL, to DL-LiteNhorn [Kontchakov et al., 2010; 2011], one of the most expressive logic of the DL-Lite family, and only recently to the main guarded- and stickybased classes of existential rules [Gottlob et al., 2014b]. In this work, we are mainly concerned about existential rules.

Research Challenges. The problem of applying the polynomial pure and combined approach to existing classes of existential rules is relatively understood. Nevertheless, there are still basic open questions regarding the well-known formalism of linear (existential) rules, that is, assertions of the form ∀X∀Y(s(X,Y) → ∃Zp(X, Z)), where s(X,Y) and p(X,Z) are atomic formulas [Cal`ı et al., 2012a]. Despite their simplicity, linear rules are powerful enough for capturing prominent database dependencies, and in particular inclusion dependencies, as well as key DLs such as DL-LiteR and DLR-LiteR, the extension of DL-LiteR with n-ary roles. Evidently, linear rules form a central language that deserves our attention. As stated in [Gottlob et al., 2014b], a major open question is the following:

Can we apply the polynomial combined approach to the class of linear rules?

The answer to the above question is affirmative under the assumption that the arity of the underlying schema is bounded; implicit in [Gottlob et al., 2014a]. However, little is known for arbitrary linear rules, without any assumption on the underlying schema. Regarding the analogous question for the polynomial pure approach, it is well-known that the answer is negative; implicit in [Gottlob et al., 2014a]. Noticeably, this negative result cannot be transferred to full linear rules, i.e., linear rules without existential quantification. This gives rise to the following fundamental question:

Can we apply the polynomial pure approach to the class of full linear rules?

Our Results. It is the precise aim of the current work to give answers to the above open questions. In fact, we show that the answer to both questions is affirmative:

The class of linear existential rules is polynomially combined Q-rewritable, while full linear existential rules are polynomially (purely) Q-rewritable, where Q consists of first-order or non-recursive Datalog queries.

Since linear rules generalize DLR-LiteR, we immediately conclude that DLR-LiteR is also polynomially combined Qrewritable. These are non-trivial results that required novel techniques beyond the state of the art. In fact, all the formalisms for which the polynomial pure and combined approach have been applied, share a property that is crucial for the existing rewriting techniques: given a (Boolean) CQ q, a database D, and an ontology Σ, if q is entailed by (D ∪ Σ), then q admits a proof of polynomial size, i.e., q is already entailed by a polynomially sized subinstance of the underlying canonical model of D and Σ. However, the above property does not hold for (full) linear rules [Gottlob et al., 2014b]. Hence, by following the same principle as in existing techniques, i.e., to simulate the polynomially sized proof of the given query via a first-order or a non-recursive Datalog query, the obtained rewritings will unavoidably be of exponential size. Thus, our challenge is to simulate query proofs not necessarily of polynomial size via polynomially sized queries.

2 Preliminaries

Technical Definitions. Consider the following pairwise disjoint (infinite countable) sets: a set C of constants, a set N of labeled nulls, and a set V of variables. A term t is a constant, null, or variable. An atom has the form p(t1, . . . , tn), where p is an n-ary predicate, and t1, . . . , tn are terms. For an atom a, we denote dom(a), null(a) and var(a) the set of its terms, nulls, and variables, respectively; these extend to sets of atoms. Conjunctions of atoms are often identified with the sets of their atoms. An instance I is a (possibly infinite) set of atoms p(t), where t is a tuple of constants and nulls. A database D is a finite instance such that dom(D) ⊂ C. A homomorphism is a substitution h : C∪N∪V → C∪N∪V

that is the identity on C. We assume familiarity with conjunctive queries (CQs). We write q(I) for the answer to a CQ q over I. A Boolean CQ (BCQ) q has a positive answer over I, denoted I |= q, if () ∈ q(I).

An existential rule (or simply rule) σ is a constant-free first-order formula ∀X∀Y(ϕ(X, Y) → ∃Z p(X, Z)), where (X∪Y∪Z) ⊂ V, ϕ is a conjunction of atoms; ϕ(X, Y) is the body of σ, while p(X, Z) is the head of σ. A class of existential rules that is of special interest for the current work consists of linear existential rules (or simply linear rules), that is, rules with only one body-atom [Cal`ı et al., 2012a]. More precisely, the class of linear rules, denoted LIN, is defined as the family of all possible sets of linear rules. Given a set Σ of rules, sch(Σ) is the set of predicates occurring in Σ. For brevity, we will omit the universal quantifiers. An instance I satisfies σ, written I |= σ, if the following holds: whenever there exists a homomorphism h such that h(p(X,Y)) ∈ I, then there exists h′ ⊇ h|X, where h|X is the restriction of h on X, such that h′ (p(X, Z)) ∈ I; I satisfies a set Σ of rules, denoted I |= Σ, if I satisfies each σ of Σ.

The models of a database D and a set Σ of rules, denoted mods(D,Σ), is the set {I | I ⊇ D and I |= Σ}. The answer to a CQ q w.r.t. D and Σ is defined as the set of tuples ans(q,D,Σ) = ⋂I∈mods(D,Σ){t | t ∈ q(I)}. The answer to a BCQ q is positive, denoted (D ∪ Σ) |= q, if ans(q, D, Σ) ̸= ∅. The problem of CQ answering is defined as follows: given a CQ q, a database D, a set Σ of rules, and a tuple of constants t, decide whether t ∈ ans(q,D,Σ). In case q is a BCQ, the above problem is called BCQ answering. These decision problems are LOGSPACE-equivalent, and we thus focus only on BCQ answering. For query answering purposes, we can assume, w.l.o.g., that both the query and the database contain only predicates of sch(Σ).

We assume familiarity with the chase procedure. Recall that the chase for a database D and a set Σ of rules, denoted chase(D, Σ), is a universal model of D and Σ, and thus (D∪ Σ) |= q iff chase(D,Σ) |= q, for each BCQ q. The chase graph for D and Σ, denoted CG(D, Σ), is a directed labeled graph (N,E, λ), where N is the set of nodes, λ is the node labeling function N → chase(D,Σ), and an edge (v, u) ∈ E iff λ(u) is obtained from λ(v) via a single chase step. It is easy to verify that, whenever Σ ∈ LIN, CG(D,Σ) is a directed forest.

Query Rewriting. For our purposes, we are going to consider two central query languages, namely first-order queries (FO), and non-recursive Datalog queries (NDL); see, e.g., [Abiteboul et al., 1995]). The formal definition of polynomial combined Q-rewritability, where Q ∈ {FO,NDL}, which is at the basis of the polynomial combined approach, is as follows; in the sequel, fix a class C of existential rules:

Definition 1 The class C is polynomially combined Qrewritable if, for every BCQ q, database D, and Σ ∈ C, we can rewrite in polynomial time: (i) q and Σ, independently of D, into qΣ ∈ Q, and (ii) D and Σ, independently of q, into a database DΣ, such that, (D ∪ Σ) |= q iff DΣ |= qΣ.

The rewriting of q and Σ is the query compilation phase, while the rewriting of D and Σ is the database compilation

(a)

Figure 1: Illustration of a proof generator.

phase. If the database compilation phase is dropped, then we get the notion of polynomial Q-rewritability.

Definition 2 The class C is polynomially Q-rewritable if, for every BCQ q, and Σ ∈ C, it is possible to rewrite in polynomial time: q and Σ into qΣ ∈ Q, such that, for every database D, (D∪Σ) |= q iff D |= qΣ.

3 Proof Generator

In this section, we introduce our main technical tool, called proof generator, which formalizes the intuitive idea that BCQ answering under linear rules can be realized as a reachability problem on the chase graph. Let us first illustrate the key ideas underlying the proof generator via a simple example.

Example 1 Let D = {p(a, b, c), p(b, c, d)}, and let Σ be the set of linear rules:

where b = p(X, Y, Z). Given the BCQ

as illustrated in Figure 1(a), there exists a homomorphism h (dashed arrows in the figure) that maps q to an initial segment of the chase graph of D and Σ, and thus (D ∪ Σ) |= q. It is interesting to observe that the nulls occurring in h(q), i.e., z1, z3, z4 and z5, form a rooted forest F , depicted in Figure 1(b), with the following properties; for brevity, let ν(z) be the atom in CG(D, Σ) where the null z is invented (see shaded atoms in Figure 1(a) for ν(z1), ν(z3), ν(z4) and ν(z5)): (i) for every root node z, ν(z) is reachable fromD; (ii) for every edge (z,w), ν(w) is reachable from ν(z); and (iii) for every atom a ∈ h(q), there exists a unique path π in F that contains all the nulls in a, and, assuming that the leaf node of π is z, a is reachable from ν(z). Indeed, it is easy to verify that ν(z1) and ν(z5) are reachable from D, ν(z3) and ν(z4) are reachable from ν(z1), and finally, h(p(A, a,B)) = p(z3, a, z1) is reachable from ν(z3), h(p(C,B, b)) = p(z4, z1, b) from ν(z4), and h(p(D, c, b)) = p(z5, c, b) from ν(z5).

Roughly speaking, the triple consisting of: (1) the homomorphism h, that maps q to the chase; (2) the function ν, that gives the atoms in the chase where the nulls occurring in h(q) were invented; and (3) the forest F, that encodes how the nulls of h(q) depend on each other, as well as the order of their generation, is what we call a proof generator for q w.r.t. D and Σ. The existence of such a triple, allows us to generate the part of the chase due to which the query is entailed, i.e., the proof of the query (hence the name "proof generator"). Therefore, for query answering purposes under linear rules, we simply need to check if such a proof generator exists. Let us now formalize the above intuitive ideas.

Rooted Forests. A rooted tree T on a set S is a tree with S be the node set of T, where one node, denoted root(T), has been designated the root, and the edges have an orientation away from the root. The tree-order of T is the (non-strict) partial order ⪯T over S such that v ⪯T u iff the unique path from the root to u passes through v. The corresponding strict partial order is given by: v ≺T u iff v ⪯T u and v ̸= u. A rooted forest F on a set S is a collection of rooted trees T1, . . . , Tn on S1, . . . , Sn, resp., where Si ∩ Sj = ∅, for 1 ⩽ i < j ⩽ n, and S = ⋃i∈[n] Si. We define root(F) = ⋃i∈[n] {root(Ti)}. The forest-order of F is the partial order ⪯F= ⋃i∈[n] ⪯Ti , while v ≺F u iff v ⪯F u and v ̸= u. Consider a set T ⊆ S such that, for each v, u ∈ T, v ⪯F u or u ⪯F v. It can be verified that there exists a unique v ∈ T, denoted greatestF (T), such that u ≺F v, for each u ∈ T.

Query Answering and Proof Generators. For technical clarity, we focus, w.l.o.g., on linear rules in normal form, i.e., linear rules with at most one occurrence of an existentially quantified variable; see, e.g., [Gottlob et al., 2014b]. Fix a BCQ q, a database D, and a set Σ ∈ LIN. As said above, a proof generator for q w.r.t. D and Σ is a triple consisting of a homomorphism h : var(q) → (dom(D) ∪N), a function ν : null(h(q)) → chase(D,Σ), and a rooted forest F on null (h(q)). Such a triple, in order to be a valid candidate for a proof generator, must satisfy certain properties. In particular, (1) the atoms of h(q), as well as the atoms where the nulls of h(q) were invented, do not contain incomparable (w.r.t. ⪯F ) nulls of h(q), and (2) for each z ∈ null(h(q)), z is the most recently generated null among the nulls in ν(z). The above properties are formalized via the proof generator scheme. In the sequel, for brevity, let U= null(h(q)).

Definition 3 A proof generator scheme for q w.r.t.D and Σ is a triple (h, ν, F), with h : var(q) → (dom(D) ∪N) be a mapping, ν : null(h(q)) → chase(D,Σ) be a (total) function, and F be a rooted forest on null (h(q)), such that:

1. For each a ∈ (h(q) ∪ {ν(z) | z ∈ U}), and for each z, w ∈ (null (a) ∩U), z ⪯F w or w ⪯F z; and

We are now ready to define the notion of the proof generator. Roughly, a proof generator is a proof generator scheme that gives rise to a proof of the given query, that is, a (finite) part of the chase due to which the query is entailed. The latter can be easily verified by applying some reachability checks on the chase graph. A path π = v1 . . . vn, where n > 1, in CG(D,Σ) = (N,E, λ) is called generating for a null z if, z ̸∈ null(λ(vi)), for each i ∈ [n- 1], and z ∈ null(λ(vn)). Given two (distinct) atoms a, b ∈ chase(D,Σ), we write a ⇝ b for the fact that b is reachable from a in CG(D,Σ). Furthermore, given a null z occurring in chase(D,Σ), we write a ⇝z b for the fact that b is reachable from a in CG(D, Σ) via a path that is generating for z.

Definition 4 A proof generator for q w.r.t. D and Σ is a proof generator scheme (h, ν, F) such that:

1. For each z ∈ root(F), there exists a ∈ D such that a ⇝z ν(z);
2. For each edge (z,w) of F, ν(z) ⇝w ν(w);
3. For each a ∈ h(q) with z = greatestF (null(a)), either a = ν(z) or ν(z) ⇝ a; and
4. For each a ∈ h(q) with null(a) = ∅, there exists b ∈ D such that b ⇝ a.

Our main technical lemma follows:

Lemma 5 (D∪Σ) |= q iff there exists a proof generator for q w.r.t. D and Σ.

4 Linear Existential Rules

In this section, we give a positive answer to our first research question regarding linear rules and the polynomial combined approach. More precisely, we show that:

Theorem 6 LIN is polynomially combined Q-rewritable, where Q ∈ {FO, NDL}.

To establish the above theorem, we heavily rely on the notion of the proof generator. For the rest of this section, fix a BCQ q, a database D, and a set Σ ∈ LIN. By Lemma 5, it suffices to construct in polynomial time a query qΣ ∈ Q (independently of D), and a database DΣ (independently of q), such that DΣ |= qΣ iff a proof generator for q w.r.t. D and Σ exists. Roughly, the query qΣ consists of three components: the first one guesses a triple (h, ν, F) as in Definition 3, the second component verifies that the guessed triple is a proof generator scheme, and finally, the third component verifies that the guessed triple is a proof generator for q w.r.t. D and Σ. The interesting part of qΣ is its third component, which applies the crucial reachability checks required by Definition 4. Although the path among two atoms in the chase graph may be of exponential size, its existence can be checked via Qqueries of polynomial size.

Let us make some assumptions that will simplify our task. Recall that Σ is in normal form, i.e., each rule has at most one occurrence of an existentially quantified variable. We further assume that the existentially quantified variable appears in the last position of the head-atom. Moreover, we assume that Σ contains only one predicate p of arity ω. As shown in [Gottlob et al., 2014b], the above assumptions can be made without affecting the generality of our proof. We finally assume that q is of the form ∃Z(p(t1)∧. . .∧p(tn)), where Z = Z1, . . . , Zℓ, and ti ∈ (dom(D) ∪ Z)ω , for each i ∈ [n].

4.1 First-Order Rewriting

We first focus on the case where Q = FO.

DATABASE COMPILATION PHASE. We define

where bit and star are auxiliary predicates not occurring in sch(Σ), while 0, 1 and ⋆ are fresh constants not in D. The purpose of 0 and 1 is, intuitively speaking, to encode in binary form the nulls that appear in the proof of the given query q. Note that those nulls cannot be explicitly encoded in DΣ, since in this case DΣ will depend on q, and such a rewriting will not be consistent with Definition 1. The purpose of ⋆ is to help us to indicate that a path in the chase graph does not need to be generating for some null. Clearly, DΣ does not depend on q, and it can be constructed on O(1) time.

QUERY COMPILATION PHASE. Let us now proceed with the definition of qΣ. As said above, qΣ consists of three components: guess a triple (h, ν, F), verify that is a proof generator scheme, and finally, verify that is a proof generator. Before giving the general shape of qΣ, let us introduce the variables, and their underlying meaning, that we will use in qΣ - assume, for the moment, that α is a sufficiently large integer such that all the nulls that may occur in the proof of q can be represented via tuples of the form {0, 1}α:

• For each i ∈ [ℓ], Zi = Z 1 i , ...,Z α i represents the term (constant or null) to which the query variable Zi is mapped to via the homomorphism h. Notice that such a term is encoded as a tuple of length α;
• For each i ∈ [ℓ], T1i , . . . ,Tωi , where each Tji is an αtuple, represents an atom in the chase where a null occurring in h(q) was invented. In other words, assuming that Tωi encodes the null z (the set Σ is in normal form, and thus an invented null appears at the last position), then T1i , . . . ,Tωi represents the atom ν(z); and
• For each i ∈ [ℓ - 1], the pair (Ai,Bi) represents an edge in the rooted forest F on null(h(q)); for brevity, let A = {A1, . . . , Aℓ-1} and B = {B1, . . . , Bℓ-1}

We define Q as the set that collects all the variables introduced above. Let us now comment on the key value α. It is well-known that, for query answering purposes under linear rules, it suffices to focus on an initial segment of the chase graph of depth δ = (n + 1) · (2ω)ω [Cal`ı et al., 2012a]. This implies that the maximum number of atoms that can appear in the proof of q is (n · δ), which in turn implies that the number of nulls in the proof of q is bounded by (n · δ · ω). Thus, it suffices to let α = ⌈log(n · δ · ω)⌉. It is important to say that α is polynomial w.r.t. q and Σ, and independent of D.

The general shape of qΣ is as follows:

With the aim of simplifying the definition of qΣ, we make use of some useful shortcuts, given in Table 1. The employed shortcuts are self-explanatory, and thus we proceed with qΣ, without discussing their semantic meaning.

The real purpose of the subquery GuessTriple(Q) is to ensure that the guessed triple (h, ν, F) is valid, which means that ν : null(h(q)) → chase(D,Σ) is indeed a (total) function, and F is a rooted forest on null (h(q)). This can be easily done via a simple first-order query. In what follows, we present the formal definition of ProofGeneratorScheme(Q) and ProofGenerator (Q).

Proof Generator Scheme. We check whether the guessed triple is indeed a proof generator scheme. In fact, we simply need to check if the two conditions in Definition 3 hold. But let us first introduce some auxiliary notation. For each i ∈ [n], tti is defined as the tuple f(ti[1]), . . . , f(ti[w]), where f(t) = (t)α, if t ∈ C, and f(t) = t1 , . . . , tα, if t ∈ Z; recall that p(ti) is an atom of q. Moreover, for each j ∈ [ω], ttji = f(ti[j]). For example, if ω = 3, ti = c,Z3,Z1, and α = 2, then tti = c, c,Z 1 3 , Z 2 3 , Z 1 1 , Z 2 1 , while tt1i = c, c, tt2i = Z 1 3 , Z 2 3 and tt3i = Z 1 1 , Z 2 1 .

The first condition in Definition 3, namely "for each a ∈ (h(q)∪{ν(z) | z ∈ U}), and for each z, w ∈ (null (a)∩U), z ⪯F w or w ⪯F z", can be verified via PGS1(Q):

The second condition, which asks that "for each z ∈ U, z = greatest F (null (ν(z)) ∩U)", can be checked via PGS 2(Q):

Notice that PGS2(Q) assumes the following: for each tuple b of bits in the image of Z1, . . . , Zℓ, there exists i ∈ [ℓ] such that Tωi is mapped to b. This is enforced by the subquery of GuessTriple(Q), which checks whether ν : null(h(q)) → chase(D,Σ) is a total function. Consequently, the query ProofGeneratorScheme(Q) is (PGS1(Q) ∧ PGS2(Q)).

Proof Generator. We proceed to check if the guessed triple is a proof generator for q w.r.t. D and Σ, or whether the four conditions in Definition 4 are fulfilled. Let us assume, for the moment, that we have access to the subqueries π and πG. Intuitively, π(X, Y), where X and Y are collections of tuples of variables representing some tuples in the chase, let say tX

and tY, respectively, means that p(tX) ⇝ p(tY). Analogously, πG(X, Y), assuming that Y[ω] represents the null z, is equivalent to p(tX ) ⇝z p(tY). Both π and πG are formally defined below.

The first condition in Definition 4, that is, "for each z ∈ root(F), there exists a ∈ D such that a ⇝z ν(z)", can be verified via the query PG1(Q), which is defined as:

The second condition, namely "for each edge (z,w) of F, ν(z) ⇝w ν(w)", can be checked via the query PG2(Q):

The third condition, that is, "for each a ∈ h(q) with z = greatestF (null(a)), either a = ν(z) or ν(z) ⇝ a", can be verified by the query PG3(Q):

Finally, the fourth condition, namely "for each a ∈ h(q) with null(a) = ∅, there exists b ∈ D such that b ⇝ a", can be checked via the query PG4(Q):

Consequently, ProofGenerator (Q) is defined as (PG1(Q)∧ PG2(Q) ∧ PG3(Q) ∧ PG4(Q)). To conclude the definition of qΣ, it remains to define the crucial subqueries π and πG.

The Subqueries π and πG. As said above, π(X , Y) is equivalent to p(tX) ⇝ p(tY), where tX and tY are tuples in the chase represented by X and Y, while πG(X, Y) means that p(tX) ⇝z p(tY), where Y[ω] represents the null z. Assume that we have access to an auxiliary subquery πi(X, Y,T), which states the following: if T = (⋆)α, then p(tY) is reachable from p(tX ) in CG(D, Σ) via some path of length at most 2i ; otherwise, if T = Y[ω], then p(tY) is reachable from p(tX) via a path of length at most 2i that is also generating for z. Then, the crucial subqueries can be defined as

where 2λ is the maximum size of a path among two atoms in the proof of q. Recall that, for query answering purposes under linear rules, it suffices to focus on an initial segment of the chase graph of depth δ = (n + 1) · (2ω)ω [Cal`ı et al., 2012a]. Therefore, 2λ ⩽ δ; hence, for our purposes, it suffices to set λ = ⌈log δ⌉. It is crucial for our construction that λ is polynomial w.r.t. q and Σ, and independent of D.

Let us now proceed with the formal definition of πi. To this end, we need an effective way to check if a tuple is obtained from some other tuple during the chase by applying a certain linear rule. This is achieved via the subquery ̂ σ(X , T), where X is a sequence of tuples (of variables) of length 2ω, which has the following intuitive meaning: if T = (⋆)α, then the tuple in the chase graph represented by X [ω + 1], . . . , X [2ω] can be obtained from X[1], . . . ,X[ω] by applying σ; otherwise, if T = X[2ω], then in addition we need that the null represented by T is invented in the generated atom - the formal definition of ̂ σ follows.

Assume that σ is a linear rule of the form p(t1, . . . , tω) → p(tω+1, . . . , t2ω). We define the function ξ : [2ω] → [2ω] in such a way that, for each i ∈ [2ω]: if ti /∈ {ti+1, . . . , t2ω}, then ξ(i) = i; otherwise, ξ(i) is the smallest j > i such that ti = tj and ti ̸∈ {ti+1, . . . , tj-1}. In words, given the position i of a variable V occurring in σ, ξ(i) is the next position (from left-to-right) where the same variable V (if any) occurs in σ. For example, if σ is the rule p(X1,X1,X2) → p(X2,X1,X3), we have that ξ(1) = 2, ξ(2) = 5, ξ(3) = 4, ξ(4) = 4, ξ(5) = 5, ξ(6) = 6.

We proceed by considering the following two cases where σ contains or not an existentially quantified variable:

• If σ contains an existentially quantified variable, which implies {tω+1, . . . , t2ω-1} ⊆ {t1, . . . , tω} and t2ω ̸∈ {t1, . . . , tω}, then ̂ σ(X,T) is defined as

• If σ does not contain an existentially quantified variable, then ̂ σ(X,T) is defined as

We have now all the ingredients to define πi. This is done inductively as follows: π0(X, Y,T) is defined as

while πi+1(X, Y,T) is defined as (calligraphic letters, as usual, denote sequences of α-tuples of variables)

One may claim that the definition of πi+1(X, Y,T) can be simplified by exploiting the query ̂ πi+1(X , Y, T) defined as

with ̂ π0(X, Y,T) = π0(X, Y,T). However, in this case, the size of ̂ πλ will be exponential in λ, and thus exponential in ω. The construction of qΣ is now complete, and the next key result can be established:

Proposition 7 The following hold:

1. DΣ is constructible in O(1) time, independently of q;
2. qΣ ∈ FO, and is constructible in polynomial time, independently of D; and
3. DΣ |= qΣ iff there exists a proof generator for q w.r.t. D and Σ.

Note that the actual size of qΣ is O(|Σ|α2n5ω5 ). Clearly, Proposition 7 and Lemma 5 imply Theorem 6 when Q = FO.

4.2 Non-Recursive Datalog Rewriting

Let us now focus on the case where Q = NDL. To avoid notational clutter, in what follows we will refer to the database DΣ and the FO-query qΣ defined above by DFO Σ and qFO Σ , respectively. Starting from qFO Σ , we can construct in polynomial time (independently of D) a query qΣ ∈ NDL such that DFO Σ |= qFO Σ iff DΣ |= qΣ, where DΣ is defined as

which in turn implies Theorem 6 when Q = NDL. Let us briefly explain how qΣ is constructed.

It is interesting to observe that qFO Σ can "almost" be transformed into a positive existential first-order query. To achieve this we need to overcome two difficulties: (1) π(X, Y) and πG(X, Y) are defined via a formula that involves universal quantification; and (2) qFO Σ uses negation. To overcome difficulty (1), let us assume, for the moment, that we have access to the auxiliary predicates R and RG (R stands for reachable) that store all the pairs (X, Y) that make the subqueries π(X, Y) and πG(X, Y), respectively, true. Then, in qFO Σ , we replace π(X, Y) and πG(X, Y) with the atomic formula R(X, Y) and RG(X, Y), respectively; this gives us the query [qFO Σ ]R. It is easy to verify that [qFO Σ ]R can be transformed in polynomial time into negation normal form, where each negated atom is of the form ¬(X = Y ) or ¬bit(X). Since DΣ gives us access to the relation neq, we can replace ¬(X = Y ) with neq(X, Y ). Moreover, we can replace ¬bit(X) with the equivalent formula (dom(X) ∨ star(X)). After applying the above replacements, we obtain the positive existential query [qFO Σ ]+R .

It is well-known that each positive existential query can be effectively rewritten as a non-recursive Datalog query. Thus, [qFO Σ ]+R can be transformed in polynomial time into an NDLquery [qΣ]R. In order to obtained the desired NDL-query qΣ, it remains to show that the crucial predicates R and RG can be defined via a non-recursive Datalog query of polynomial size. Assuming that we have access to the predicate Rλ that holds all the triples (X , Y, T) that make the subquery πλ(X , Y, T) true, the desired predicates are defined via the rules

Finally, the predicate Rλ can be defined via the polynomially sized NDL-query obtained after transforming the "almost"

positive existential FO-query ̂ πλ into an exponentially more succinct non-recursive Datalog query - recall that ̂ πλ is the naive implementation of πλ via a query of exponential size (given at the end of Section 4.1).

It is interesting to observe that, when the target query language is FO, the database compilation phase is feasible in constant time, while for NDL rewritings it takes polynomial time. This is because FO-queries are powerful enough to express inequalities, which is not the case for NDL-queries.

5 Dropping Existential Quantifiers

We proceed to give a positive answer to our second research question regarding the class of full linear rules and the polynomial pure approach. Recall that full linear rules are linear rules without existential quantification, and the corresponding class is denoted FLIN. We show that:

Theorem 8 FLIN is polynomially Q-rewritable, where Q ∈ {FO, NDL}.

The above result can be shown via simplified versions of the rewriting procedures presented above. Fix a BCQ q, and a set Σ ∈ FLIN, under the same assumptions as in Section 4. We first focus on the case where Q = FO, and we are going to construct an FO-query qFO Σ . Since Σ is full, for every database D, chase(D,Σ) does not contain null values. Therefore, qFO Σ can be obtained from the FO-query qΣ defined in Section 4.1, by keeping only PG4(Q), which checks if "for each a ∈ h(q) with null(a) = ∅, there exists b ∈ D such that b ⇝ a". Since there are no nulls in the chase, we do not need anymore to represent the terms in the chase via α-tuples. Thus, Q = Z1, . . . , Zℓ, and qFO Σ is defined as

where λ = ⌈logωω ⌉. The crucial subquery πλ is defined inductively as follows: π0(X,Y) is

while πi+1(X,Y) is

The actual size of the obtained query is O(|Σ|nω2 logω). Having the first-order query qFO Σ in place, it is easy to construct an equivalent NDL-query qNDL Σ , in the same way as discussed in Section 4.2, and Theorem 8 follows.

6 Discussion and FutureWork

The results of this work are, for the moment, of theoretical nature and we do not claim that they will directly lead to better practical algorithms. We believe that a smart implementation of the proposed techniques can lead to more efficient rewriting procedures; this will be the subject of future research. We are also planning to optimize the proposed rewriting algorithms, with the aim of constructing queries of optimal size. For example, after a more refined analysis, one can show that the bound α can be reduced from polynomial to logarithmic.

Acknowledgements. G. Gottlob was supported by the EPSRC Programme Grant EP/M025268/ "VADA: Value Added Data Systems - Principles and Architecture". M. Manna was supported by the MIUR project "SI-LAB BA2KNOW - Business Analitycs to Know", and by Regione Calabria, programme POR Calabria FESR 2007-2013, projects "ITravel PLUS" and "KnowRex: Un sistema per il riconoscimento e l'estrazione di conoscenza". A. Pieris was supported by the Austrian Science Fund (FWF): P25207-N23 and Y698.