Mélanie König

Michel Leclère

Marie-Laure Mugnier

Michaël Thomazo

Sound, Complete and Minimal UCQ-Rewriting for Existential Rules

We address the issue of Ontology-Based Data Access, with ontologies represented in the framework of existential rules, also known as Datalog±. A wellknown approach involves rewriting the query using ontological knowledge. We focus here on the basic rewriting technique which consists of rewriting the initial query into a union of conjunctive queries. First, we study a generic breadth-first rewriting algorithm, which takes any rewriting operator as a parameter, and define properties of rewriting operators that ensure the correctness of the algorithm. Then, we focus on piece-unifiers, which provide a rewriting operator with the desired properties. Finally, we propose an implementation of this framework and report some experiments.

Introduction

We address the issue of Ontology-Based Data Access, which aims at exploiting knowledge expressed in ontologies while querying data. In this paper, ontologies are represented in the framework of existential rules [START_REF] Baget | On Rules with Existential Variables: Walking the Decidability Line[END_REF][START_REF] Krötzsch | Extending Decidable Existential Rules by Joining Acyclicity and Guardedness[END_REF], also known as Datalog± [START_REF] Calì | Taming the Infinite Chase: Query Answering under Expressive Relational Constraints[END_REF][START_REF] Calì | A general datalog-based framework for tractable query answering over ontologies[END_REF]. Existential rules allow one to assert the existence of new unknown individuals, which is a key feature in an open-world perspective, as for instance in incomplete databases [START_REF] Calì | On the Decidability and Complexity of Query Answering over Inconsistent and Incomplete Databases[END_REF]. These rules are of the form body → head, where the body and the head are conjunctions of atoms (without functions) and variables that occur only in the head are existentially quantified. They generalize lightweight description logics (DLs), which form the core of the tractable profiles of OWL2 [START_REF]OWL 2 Web Ontology Language: Document Overview[END_REF].

The general query answering problem can be expressed as follows: given a knowledge base (KB) K composed of a set of facts -or data-and an ontology (a set of existential rules here), and a query Q, compute the set of answers to Q in K. In this paper, we consider Boolean conjunctive queries (Boolean CQs or BCQs). Note however that all our results are easily extended to non-Boolean conjunctive queries as well as to unions of conjunctive queries. The fundamental problem, called BCQ entailment hereafter, can be recast as follows: given a KB K, composed of facts and existential rules, and a Boolean conjunctive query Q, is Q entailed by K? BCQ entailment is undecidable for general existential rules (e.g., [START_REF] Beeri | The implication problem for data dependencies[END_REF][START_REF] Chandra | Embedded implicational dependencies and their inference problem[END_REF], on the implication problem for tuple-generating dependencies, which have the same form as existential rules). There has been an intense research effort aimed at finding decidable subsets of rules that provide good tradeoffs between expressivity and complexity of query answering (see e.g., [START_REF] Mugnier | Ontological Query Answering with Existential Rules[END_REF] for a survey on decidable classes of rules). These decidable rule fragments overcome some of the limitations of DLs. In particular, they have unrestricted predicate arity, while DLs consider unary and binary predicates only, which allows one for a natural coupling with database schemas, in which relations may have any arity; moreover, adding information, such as data provenance, is made easier by the unrestricted predicate arity, since this information can be added as a new predicate argument.

There are two main approaches to solve BCQ entailment, which are linked to the classical paradigms for processing rules, namely forward and backward chaining, as illustrated by the next example.

Example 1 Let us consider data on movies, with unary relations movie and actor, and a binary relation play (intuitively, play(x, y) means that "x plays a role in y"). Let Q be a query asking if a given person, whose identifier is B, plays a role somewhere, i.e., Q = ∃y play(B, y). Let R be an existential rule expressing that "every actor plays a role in some movie", i.e., ∀x(actor(x) → ∃y(play(x, y) ∧ movie(y))). Assume that the data contain actor(B). If Q is asked on these data, the answer is no. However, the rule allows to infer that actor B plays in a movie, thus the answer to Q should be yes. Rule R can be used in a forward manner, i.e., it can be applied to the data: then, the knowledge ∃y 0 (play(B, y 0 ) ∧ movie(y 0 )) is added, where y 0 is a new variable. Query Q can be mapped to the enriched data, which allows to answer positively. Now, R can also be used in a backward manner, i.e., to rewrite Q, which yields the new query Q = actor(B). This query can be mapped to the (initial) data, which provides the positive answer.

Both approaches can be seen as ways of reducing the problem to a classical database query answering problem by eliminating the rules, see Figure 1. The first approach consists in applying the rules to the data, thus materializing entailed facts into the data. Then, Q is entailed by K if and only if it can be mapped to this materialized database. This approach is applicable either when the forward chaining procedure stops "naturally" (see [GHK + 13] for a survey on these cases), or when it stops by taking some parameters into consideration, typically the size of the query [START_REF] Calì | Taming the Infinite Chase: Query Answering under Expressive Relational Constraints[END_REF][START_REF] Leone | Efficiently computable datalog programs[END_REF]. The second approach consists in using the rules to rewrite the query into a first-order query (typically a union of conjunctive queries [CGL + 07, PUHM09, GOP11, VSS14, RMC12]) or a non-recursive Datalog program [START_REF] Rosati | Improving query answering over DL-Lite ontologies[END_REF][START_REF] Orsi | Optimizing query answering under ontological constraints[END_REF][START_REF] Gottlob | Rewriting Ontological Queries into Small Nonrecursive Datalog Programs[END_REF]. Then, Q is entailed by K if and only if the rewritten query is entailed by the initial database.

Materialization has the advantage of enabling efficient query answering but may be not appropriate for data size, data access rights or data maintenance reasons. Query rewriting has the advantage of avoiding changes in the data, however its drawback is that the rewritten query may be large, even exponential in the size of initial query, hence less efficiently processed, at least with current database techniques. Finally, techniques combining both approaches have been developed, in particular so-called combined approach [LTW09, KLT + 11] for lightweight description logics, as well as a similar algorithm for a large class of existential rules [START_REF] Thomazo | A generic querying algorithm for greedy sets of existential rules[END_REF].

In this paper, we focus on rewriting techniques, and more specifically on rewriting the initial conjunctive query Q into a union of conjunctive queries, that we will see as Figure 1: Forward / Backward Chaining a set of conjunctive queries. This set is called a rewriting set of Q and each element of a rewriting set is called a rewriting. While most previously cited work focuses on specific rule sublanguages (mostly DL-Lite, linear and sticky existential rules), we consider general existential rules. This means that our algorithm does not make any syntactic assumption on the input set of rules, but will terminate only in some cases (so-called finite unification sets of rules, see hereafter).

The goal is to compute a rewriting set both sound (if one of its elements maps to the initial database, then K entails Q) and complete (if K entails Q then there is an element that maps to the initial database). Minimality may also be a desirable property. In particular, let us consider the generalization relation (a preorder) induced on Boolean conjunctive queries by homomorphism: we say that Q 1 is more general than Q 2 if there is a homomorphism from Q 1 to Q 2 ; it is well-known that the existence of such a homomorphism is equivalent to the following property: for any set of facts F , if the answer to Q 2 in F is positive, then so is the answer to Q 1 . We point out that any sound and complete rewriting set of a query Q remains sound and complete when it is restricted to its most general elements. Since BCQ entailment is undecidable, there is no guarantee that such a finite set exists for a given query and general existential rules. A set of existential rules ensuring that a finite sound and complete set of most general rewritings exists for any query is called a finite unification set (fus) [START_REF] Baget | On Rules with Existential Variables: Walking the Decidability Line[END_REF]. The fus property is not recognizable [START_REF] Baget | On Rules with Existential Variables: Walking the Decidability Line[END_REF], but several easily recognizable fus classes have been exhibited in the literature: atomic-body rules [START_REF] Baget | Extending Decidable Cases for Rules with Existential Variables[END_REF], also known as linear TGDs [START_REF] Calì | A general datalog-based framework for tractable query answering over ontologies[END_REF], multi-linear TGDs [START_REF] Calì | A general Datalog-based framework for tractable query answering over ontologies[END_REF], sticky(-join) rules [START_REF] Calì | Query Answering under Non-guarded Rules in Datalog+[END_REF][START_REF] Gottlob | Ontological queries: Rewriting and optimization[END_REF], weakly-recursive rules [START_REF] Civili | A Broad Class of First-Order Rewritable Tuple-Generating Dependencies[END_REF] and sets of rules with an acyclic graph of rule dependencies [START_REF] Baget | Extending Decidable Cases for Rules with Existential Variables[END_REF]. By definition, the fus property is a specific case of firstorder rewritability, which means that the set of rules allows to rewrite any CQ into a (sound and complete) first-order query; it is suspected that both properties are actually equivalent, however, to the best of our knowledge, no proof of this result has been published.

Paper contributions. We start from a generic algorithm which, given a BCQ and a set of existential rules, computes a rewriting set. This task can be recast in terms of exploring a potentially infinite space of queries, composed of the initial conjunctive query and its (sound) rewritings, structured by the generalization preorder. The algorithm explores this space in a breadth-first way, with the aim of computing a complete rewriting set. It maintains a rewriting set Q and iteratively performs the following tasks: (1) generate all the one-step rewritings from unexplored queries in Q; (2) add these rewritings to Q and update Q in order to keep only incomparable most general elements. A rewriting operator is a function that, given a query and a set of rules, returns the one-step rewritings of this query. Note that it may be the case that the set of sound rewritings of the query is infinite while the set of its most general sound rewritings is finite. It follows that a simple breadth-first exploration of the rewriting space is not sufficient to ensure finiteness of the process, even for fus rules; one also has to maintain a set of the most general rewritings. This algorithm is generic in the sense that it is not restricted to a particular kind of existential rules nor to a specific rewriting operator (without guarantee of termination though).

This algorithmic scheme established, we then asked ourselves the following questions:

1. Assuming that the algorithm outputs a finite sound and complete set rewritings, composed of pairwise incomparable queries, is this set of minimal cardinality, in the sense that no sound and complete rewriting set produced by any other algorithm can be strictly smaller?

2. At each step of the algorithm, some queries are discarded, because they are more specific than other rewritings, even if they have not been explored yet. The question is whether this dynamic pruning of the search space keeps the completeness of the output. More generally, which properties have to be fulfilled by the operator to ensure the correctness of the algorithm and its termination for fus rules?

3. Finally, design a rewriting operator that fulfills the desired properties and leads to the effective computation of a sound and complete rewriting set.

With respect to the first question, we show that all sound and complete sets of rewritings, restricted to their most general elements, have the same cardinality, which is minimal with respect to the completeness property. Moreover, if we delete redundant atoms from the obtained CQs (which can be performed by a polynomial number of homomorphism tests for each query)1 , then we obtain a unique minimal sound and complete set of CQs of minimal size; uniqueness is of course up to a bijective variable renaming.

To answer the second question, we define several properties that a rewriting operator has to satisfy and show that these properties actually ensure the correctness of the algorithm and its termination for fus rules. In particular, we point out that the fact that a query may be removed from the rewriting set before being explored may prevent the completeness of the output, even if the rewriting operator is theoretically able to generate a complete output. The prunability of the rewriting operator ensures that this dynamic pruning can be safely performed. Briefly, this property holds if, for all queries Q 1 and Q 2 , when Q 1 is more general than Q 2 then any one-step rewriting of Q 2 is less general than Q 1 itself or one of the one-step rewritings of Q 1 ; intuitively, this allows to discard the rewriting Q 2 even when its one-step rewritings have not been generated yet. Note that this kind of properties ties in with an issue raised in [START_REF] Imprialou | Benchmarking Ontology-Based Query Rewriting Systems[END_REF] about the gap between theoretical completeness of some methods and the effective completeness of their implementation, this gap being mainly due to algorithmic optimizations (here the dynamic pruning).

Concerning the third question, we proceed in several steps. First, we rely on a specific unifier, called a piece-unifier, that was designed for backward chaining with conceptual graph rules (whose logical translation is exactly existential rules [START_REF] Salvat | Sound and Complete Forward and Backward Chainings of Graph Rules[END_REF]). As in classical backward chaining, the rewriting process is based on a unification operation between the current query and a rule head. However, existential variables in rule heads induce a structure that has to be considered to keep soundness. Thus, instead of unifying a single atom of the query at once, our unifier processes a subset of atoms from the query. A piece is a minimal subset of atoms from the query that have to be erased together, hence the name piece-unifier. We present below a very simple example of piece unification (in particular, the head of the existential rule is restricted to a single atom).

Example 2 Let R = ∀x (q(x) → ∃y p(x, y)) and the BCQ Q = ∃u∃v∃w(p(u, v) ∧ p(w, v) ∧ r(u, w)). Assume we want to unify the atom p(u, v) from Q with p(x, y), for instance by a substitution {(u, x), (v, y)}.2 Since v is unified with the existential variable y, all other atoms from Q containing v must also be considered: indeed, simply rewriting Q into Q 1 = ∃w∃x∃y(q(x) ∧ p(w, y) ∧ r(x, w)) would be unsound: intuitively, the fact that the atoms p(u, v) and p(w, v) in Q share a variable would be lost in atoms q(x) and p(w, y); for instance F = q(a) ∧ p(b, c) ∧ r(a, b) would answer Q 1 despite Q being not entailed by F and R. Thus, p(u, v) and p(w, v) have to be both unified with the head of R, for instance by means of the following substitution:

µ = {(u, x), (v, y), (w, x)}. {p(u, v), p(w, v)} is called a piece. The corresponding rewriting of Q is ∃x(q(x) ∧ r(x, x)).
Piece-unifiers lead to a logically sound and complete rewriting method. As far as we know, it is the only method accepting any kind of existential rules, while staying in this fragment, i.e., without Skolemization of rule heads to replace existential variables with Skolem functions.

We show that the piece-based rewriting operator fulfills the desired properties ensuring the correctness of the generic algorithm, and its termination in the case of fus rules.

The next question was how to optimize the rewriting step. Indeed, the problem of deciding whether there is a piece-unifier between a query and a rule head is NPcomplete and the number of piece-unifiers can be exponential in the size of the query. To cope with these sources of complexity, we consider so-called single-piece unifiers, which unify a single-piece of the query at once (like µ in Example 2). When, additionally, the head of a rule R is restricted to an atom, which is a frequent case, each atom in a query Q belongs to at most one piece with respect to R; then, the number of (most general) single-piece unifiers of Q with the head of R is bounded by the size of Q.

We show that the single-piece based rewriting operator is able to generate a sound and complete rewriting set. However, as pointed out in several examples, it is not prunable. Hence, single-piece unifiers have to be combined to recover prunability. We thus define the aggregation of single-piece unifiers and show that the corresponding rewriting operator fulfills all desired properties and generates fewer queries than the piece-based rewriting operator. Detailed algorithms are given and first experiments are reported.

Paper organization. Section 2 recalls some basic notions about the existential rule framework. Section 3 defines sound, complete and minimal sets of rewritings. In Section 4, the generic breadth-first algorithm is introduced and general properties of rewriting operators are studied. Section 5 presents the piece-based rewriting operator. In Section 6, we focus on exploiting single-piece unifiers and introduce the rewriting operator based on their aggregation. Finally, Section 7 is devoted to detailed algorithms and experiments, as well as to further work. This is an extended version of papers by the same authors published at RR 2012 and RR 2013 (International Conference on Web Reasoning and Rule Systems).

Preliminaries

An atom is of the form p(t 1 , . . . , t k ) where p is a predicate with arity k, and the t i are terms, i.e., variables or constants. Given an atom or a set of atoms A, vars(A), consts(A) and terms(A) denote its sets of variables, constants and terms, respectively. In all the examples in this paper, the terms are variables (denoted by x, y, z, etc.). |= denotes the classical logical consequence. Two formulas f 1 and f 2 are said to be equivalent if

f 1 |= f 2 and f 2 |= f 1 .
A fact is an existentially closed conjunction of atoms.3 A conjunctive query (CQ) is an existentially quantified conjunction of atoms. When it is a closed formula, it is called a Boolean CQ (BCQ). Hence, facts and BCQs have the same logical form. In the following, we will see them as sets of atoms. A union of conjunctive queries (UCQ) is a disjunction of CQs, which will see as a set of CQs.

Given sets of atoms A and B, a homomorphism h from A to B is a substitution of vars(A) by terms(B) such that h(A) ⊆ B. We say that A is mapped to B by h. If there is a homomorphism from A to B, we say that A is more general than B, which is denoted A ≥ B.

Given a fact F and a BCQ Q, the answer to

Q in F is positive if F |= Q. It is well-known that F |= Q if and
only if there is a homomorphism from Q to F . If Q is a non-Boolean CQ, let x 1 . . . x q be the free variables in Q. Then, a tuple of constants (a 1 . . . a q ) is an answer to Q in F if there is a homomorphism from Q to F that maps x i to a i for each i. In other words, (a 1 . . . a q ) is an answer to Q in F if and only if the answer to the BCQ obtained from Q by substituting each x i with a i is positive.

In this paper, we consider only Boolean queries for simplicity reasons. This is not a restriction, since our mechanisms can actually process a CQ with free variables x 1 . . . x q by translating it into a BCQ with an added atom ans(x 1 . . . x q ), where ans is a special predicate not occurring in the knowledge base. Since ans can never be erased by a rewriting step, the x i can only be substituted and will not "disappear". We can thus compute the rewriting set of a CQ as a Boolean CQ with a special ans atom, then transform the rewritings into non-Boolean CQs by removing the ans atom and consider its arguments as free variables. Note that our the generic algorithm can accept as input a union of conjunctive queries as well, since it works exactly in the same way if it takes as input a set of CQs instead of a single CQ. In the following, we omit quantifiers in rules and queries, as there is no ambiguity. For instance, the rule R = ∀x (q(x) → ∃y p(x, y)) from Example 2 will be written q(x) → p(x, y).

A knowledge base (KB) K = (F, R) is composed of a fact F and a finite set of existential rules R. The BCQ entailment problem takes as input a KB K = (F, R) and a BCQ Q, and asks if F, R |= Q holds.

Desirable Properties of Rewriting Sets

Given a query Q and a set of existential rules R, rewriting techniques compute a set of queries Q, which we call a rewriting set hereafter. It is generally desired that such a set satisfies at least three properties: soundness, completeness and minimality.

Definition 2 (Sound and Complete set) Let R be a set of existential rules and Q be a BCQ. Let Q be a set of BCQs. Q is said to be sound w.r.t. Q and R if for all facts F , for all

Q ∈ Q, if Q can be mapped to F then F, R |= Q. Reciprocally, Q is said to be complete w.r.t. Q and R if for all facts F , if F, R |= Q then there is Q ∈ Q such that Q can be mapped to F .
We mentioned in the introduction that only the most general elements of a rewriting set need to be considered. Indeed, let Q 1 and Q 2 be two elements of a rewriting set such that Q 1 ≥ Q 2 . Then, for any fact F , the set of answers to Q 2 in F is included in the set of answers to Q 1 in F . Hence, removing Q 2 will not undermine completeness (and it will not undermine soundness either). The output of a rewriting algorithm should thus be a minimal set of incomparable queries that "covers" the set of all the sound rewritings of the initial query.

Definition 3 (Covering relation) Let Q 1 and Q 2 be two sets of BCQs. Q 1 covers Q 2 , which is denoted Q 1 ≥ Q 2 , if for all Q 2 ∈ Q 2 there is Q 1 ∈ Q 1 with Q 1 ≥ Q 2 .
Note that covering can also be defined in terms of classical database query containment, i.e.,

Q 1 covers Q 2 if and only if the UCQ Q 2 is included in the UCQ Q 1 . Definition 4 (Minimal set of BCQs, Cover) Let Q be a set of BCQs. Q is said to be minimal if there is no Q ∈ Q such that (Q \ {Q}) ≥ Q. A cover of Q is a minimal set Q c ⊆ Q such that Q c ≥ Q.
Since a cover is a minimal set, its elements are pairwise incomparable.

Example 3 Let Q = {Q 1 , . . . , Q 6 } and consider the following preorder over Q:

Q 1 ≥ Q 2 , Q 4 , Q 5 , Q 6 ; Q 2 ≥ Q 1 , Q 4 , Q 5 , Q 6 ; Q 3 ≥ Q 4 ; Q 5 ≥ Q 6 (note that Q 1 and Q 2 are equivalent). There are two covers of Q, namely {Q 1 , Q 3 } and {Q 2 , Q 3 }. See Figure 2.
A set of (sound) rewritings may have a finite cover even when it is infinite, as illustrated by Example 4.

Example 4 Let Q = t(u), R 1 = t(x) ∧ p(x, y) → r(y), R 2 = r(x) ∧ p(x, y) → t(y).
R 1 and R 2 have a head restricted to a single atom and no existential variable, hence the classical most general unifier can be used, which unifies the first atom in the query with the atom of a rule head. The rewriting set of Q with {R 1 , R 2 } is infinite. The first generated queries are the following (note that rule variables are renamed when needed):

Q 0 = t(u) Q 1 = r(x) ∧ p(x, y) // from Q 0 and R 2 with {(u, y)} Q 2 = t(x 0 ) ∧ p(x 0 , y 0 ) ∧ p(y 0 , y) // from Q 1 and R 1 with {(x, y 0 )} Q 3 = r(x 1 ) ∧ p(x 1 , y 1 ) ∧ p(y 1 , y 0 ) ∧ p(y 0 , y) // from Q 2 and R 2 with {(x 0 , y 1 )} Q 4 = t(x 2 ) ∧ p(x 2 , y 2 ) ∧ p(y 2 , y 1 ) ∧ p(y 1 , y 0 ) ∧ p(y 0 , y) // from Q 3 and
R 1 and so on . . . However, the set of the most general rewritings is {Q 0 , Q 1 } since any other query that can be obtained is more specific than Q 0 or Q 1 .

It can be easily checked that all covers of a given set have the same cardinality. We now prove that this property can be extended to the covers of all sound and complete finite rewriting sets of Q, irrespective of the rewriting technique used to compute these sets.

Theorem 1 Let R be a set of rules and Q be a BCQ. Any finite cover of a sound and complete rewriting set of Q with R is of minimal cardinality (among all sound and complete rewriting sets of Q).

Proof: Let Q 1 and Q 2 be two arbitrary sound and complete rewriting sets of

Q with R. Let Q c 1 (resp. Q c 2 ) be one of the finite covers of Q 1 (resp. Q 2 ). Q c 1 (resp. Q c
2 ) is also sound and complete, as well as smaller than or equal to Q 1 (resp. Q 2 ). We show that they have the same cardinality. Let

Q 1 ∈ Q c 1 . There exists Q 2 ∈ Q c 2 such that Q 2 ≥ Q 1 . If not, Q would be entailed by F = Q 1 and R since Q c 1 is a sound rewriting set of Q (and Q 1 maps to itself), but no elements of Q c 2 would map to F : thus, Q c 2 would not be complete. Similarly, there exists Q 1 ∈ Q c 1 such that Q 1 ≥ Q 2 . Then Q 1 ≥ Q 1 , which implies that Q 1 = Q 1 by assumption on Q c 1 . For all Q 1 ∈ Q c 1 , there exists Q 2 ∈ Q c 2 such that Q 2 ≥ Q 1 and Q 1 ≥ Q 2 . Such a Q 2 is unique: indeed, two such elements would be comparable for ≥, which is not possible by construction of Q c 2 . The function associating Q 2 with Q 1 is thus a bijection from Q c 1 to Q c 2
, which shows that these two sets have the same cardinality.

Furthermore, the proof of the preceding theorem shows that, given any two sound and complete rewriting sets of Q, there is a bijection from any cover of the first set to any cover of the second set such that two elements in relation by the bijection are equivalent. However, these elements are not necessarily isomorphic (i.e., equal up to a variable renaming) because they may contain redundancies. Consider the preorder induced by homomorphism on the set of all BCQs definable on some vocabulary. It is well-known that this preorder is such that any of its equivalence classes possesses a unique element of minimal size (up to isomorphism), called its core (notion introduced for graphs 4 , but easily transferable to queries).

Every query can be transformed into its equivalent core by removing redundant atoms. We recall that a set of existential rules ensuring that a finite sound and complete set of most general rewritings exists for any query is called a finite unification set (fus). 5 By the remark above and Theorem 1, we obtain:

Corollary 2 Let R be a fus and Q be a BCQ. There is a unique finite sound and complete rewriting set of Q with R that has both minimal cardinality and elements of minimal size.

A Generic Rewriting Algorithm

We will now present a generic rewriting algorithm that takes as input a set of existential rules and a query, and as parameter a rewriting operator. The studied question is the following: which properties should this operator satisfy in order that the algorithm outputs a sound, complete, finite and minimal set?

Rewriting Algorithm

Definition 5 (Rewriting operator) A rewriting operator rew is a function which takes as input a BCQ Q and a set of rules R and outputs a set of BCQs denoted by rew(Q, R).

Since the elements of rew(Q, R) are BCQs, it is possible to apply further steps of rewriting to them. This naturally leads to the notions of k-rewriting and k-saturation.

Definition 6 (k-rewriting) Let Q be a conjunctive query, R be a set of rules and rew be a rewriting operator. A 1-rewriting of Q (w.r.t. rew and R) is an element of

rew(Q, R). A k-rewriting of Q, for k > 1, (w.r.t. rew and R) is a 1-rewriting of a (k -1)-rewriting of Q.
The term k-saturation is convenient to name the set of queries that can be obtained in at most k rewriting steps.

Definition 7 (k-saturation) Let Q be a BCQ, R be a set of rules and rew be a rewriting operator. We denote the set of k-rewritings of Q by rew k (Q, R). We call ksaturation, and denote by

W k (Q, R), the set of i-rewritings of Q for all i ≤ k. We denote W ∞ (Q, R) = k∈N W k (Q, R).
In the following, we extend the notations rew, rew k and W k to a set of BCQs

Q instead of a single BCQ Q: rew(Q, R) = Q∈Q rew(Q, R), rew k (Q, R) =
Algorithm 1 performs a breadth-first exploration of the rewriting space of a given query. 6 At each step, only the most general elements are kept thanks to a covering function, denoted by cover , that computes a cover of a given set.

Algorithm 1: A GENERIC REWRITING ALGORITHM

Data: A set of rules R, a BCQ Q Access: A rewriting operator rew , a covering function cover Result: A cover of the set of all the rewritings of Q

Q F ← {Q}; // resulting set Q E ← {Q}; // queries to be explored while Q E = ∅ do Q C ← cover(Q F ∪ rew(Q E , R)); // update cover Q E ← Q C \Q F ; // select unexplored queries Q F ← Q C ; return Q F
For termination reasons (see the proof of Property 6), already explored queries are preferred to non-explored queries in the computation of the cover. More precisely, if both Q c ∪ {q} and Q c ∪ {q } are covers of Q F ∪ rew(Q E , R), with q and q homomorphically equivalent and {q} belongs to Q F , then cover does not output Q c ∪ {q }. If rew fulfills some good properties (specified below), then, after the i th iteration of the while loop, the i-saturation of Q (with respect to R and rew) is covered by Q F , while Q E contains the queries that remain to be explored.

In the remainder of this section, we study the conditions that a rewriting operator must meet in order that: (i) the algorithm halts and outputs a cover of all the rewritings that can be obtained with this rewriting operator, provided that such a finite cover exists; (ii) the output cover is sound and complete.

Correctness and Termination of the Algorithm

We now define a property on the rewriting operator, called prunability. This property is sufficient to ensure that Algorithm 1 outputs a cover of W ∞ (Q, R). Intuitively, if an operator is prunable then, for every Q 1 more general than Q 2 , the one-step rewritings of Q 2 are covered by the one-step rewritings of Q 1 or by Q 1 itself. It follows that all the rewritings of Q 2 are covered by Q 1 and its rewritings. Hence, Q 2 can be safely removed from the current rewriting set.

Definition 8 (Prunable) A rewriting operator rew is said to be prunable if for any set of rules R and for all BCQs

Q 1 , Q 2 , Q 2 such that Q 1 ≥ Q 2 , Q 2 ∈ rew(Q 2 , R) and Q 1 ≥ Q 2 , there is Q 1 ∈ rew(Q 1 , R) such that Q 1 ≥ Q 2 .
The following lemma states that this can be generalized to k-rewritings for any k.

Lemma 3 Let rew be a prunable rewriting operator, and let

Q 1 and Q 2 be two sets of BCQs. If Q 1 ≥ Q 2 , then W ∞ (Q 1 , R) ≥ W ∞ (Q 2 , R). Proof: We prove by induction on i that W i (Q 1 , R) ≥ rew i (Q 2 , R). For i = 0, W 0 (Q 1 , R) = Q 1 ≥ Q 2 = rew 0 (Q 2 , R). For i > 0, for any Q 2 ∈ rew i (Q 2 , R), there is Q 2 ∈ rew i-1 (Q 2 , R) such that Q 2 ∈ rew(Q 2 , R). By induction hypothesis, there is Q 1 ∈ W i-1 (Q 1 , R) such that Q 1 ≥ Q 2 . rew is prunable, thus either Q 1 ≥ Q 2 or there is Q 1 ∈ rew(Q 1 , R) such that Q 1 ≥ Q 2 . Since W i-1 (Q 1 , R) and rew(Q 1 , R) are both included in W i (Q 1 , R), we can conclude.
This lemma would not be sufficient to prove the correctness of Algorithm 1, as will be discussed in Section 6.1. We need a stronger version, which checks that a query whose 1-rewritings are covered needs not to be explored.

Lemma 4 Let rew be a prunable rewriting operator, and let Q 1 and Q 2 be two sets of BCQs.

If (Q 1 ∪ Q 2 ) ≥ rew(Q 1 , R), then (Q 1 ∪ W ∞ (Q 2 , R)) ≥ W ∞ (Q 1 ∪ Q 2 , R). Proof: We prove by induction on i that Q 1 ∪ W i (Q 2 , R) ≥ rew i (Q 1 ∪ Q 2 , R). For i = 0, rew 0 (Q 1 ∪ Q 2 , R) = Q 1 ∪ Q 2 = Q 1 ∪ W 0 (Q 2 , R). For i > 0, for any Q i ∈ rew i (Q 1 ∪ Q 2 , R), there is Q i-1 ∈ rew i-1 (Q 1 ∪ Q 2 , R) such that Q i ∈ rew(Q i-1 , R). By induction hypothesis, there is Q i-1 ∈ Q 1 ∪ W i-1 (Q 2 , R) such that Q i-1 ≥ Q i-1 . Since rew is prunable, either Q i-1 ≥ Q i or there is Q i ∈ rew(Q i-1 , R) such that Q i ≥ Q i .
Then, there are two possibilities:

• either Q i-1 ∈ Q 1 : since Q 1 ∪ Q 2 ≥ rew(Q 1 , R), we have Q 1 ∪ Q 2 ≥ {Q i } and so Q 1 ∪ W i (Q 2 , R) ≥ {Q i }. • or Q i-1 ∈ W i-1 (Q 2 , R): then Q i ∈ W i (Q 2 , R).
Finally, the correctness of Algorithm 1 is based on the following loop invariants.

Property 5 (Invariants of Algorithm 1) Let rew be a rewriting operator. After each iteration of the while loop of Algorithm 1, the following properties hold:

1. Q E ⊆ Q F ⊆ W ∞ (Q, R); 2. Q F ≥ rew(Q F \ Q E , R); 3. if rew is prunable then (Q F ∪ W ∞ (Q E , R)) ≥ W ∞ (Q, R); 4. for all distinct Q, Q ∈ Q F , Q ≥ Q and Q ≥ Q.
Proof: Invariants are proved by induction on the number of iterations of the while loop.

Below Q i F and Q i E denote the value of Q F and Q E after i iterations. Invariant 1: Q E ⊆ Q F ⊆ W ∞ (Q, R). basis: Q 0 E = Q 0 F = {Q} = W 0 (Q, R) ⊆ W ∞ (Q, R). induction step: by construction, Q i E ⊆ Q i F and Q i F ⊆ Q i-1 F ∪ rew(Q i-1 E , R). For any Q ∈ Q i F we have: either Q ∈ Q i-1 F and then by induction hy- pothesis Q ∈ W ∞ (Q, R); or Q ∈ rew(Q i-1 E , R
) and then by induction hypothesis we have

Q i-1 E ⊆ W ∞ (Q, R), which implies Q ∈ W ∞ (Q, R). Invariant 2: Q F ≥ rew(Q F \ Q E , R). basis: rew(Q 0 F \ Q 0 E , R) = rew(∅, R) = ∅ and any set covers it. induction step: by construction, Q i F ≥ Q i-1 F ∪ rew(Q i-1 E , R); since by induc- tion hypothesis Q i-1 F ≥ rew(Q i-1 F \Q i-1 E , R), we have Q i F ≥ rew(Q i-1 F \ Q i-1 E , R) ∪ rew(Q i-1 E , R) = rew(Q i-1 F , R). Furthermore, by construc- tion, Q i E = Q i F \Q i-1 F ; thus Q i F \Q i E ⊆ Q i-1 F and so rew(Q i F \Q i E , R) ⊆ rew(Q i-1 F , R). Thus Q i F ≥ rew(Q i F \ Q i E , R). Invariant 3: if rew is prunable then (Q F ∪ W ∞ (Q E , R)) ≥ W ∞ (Q, R). basis: (Q 0 F ∪ W ∞ (Q 0 E , R)) = ({Q} ∪ W ∞ ({Q}, R)) = W ∞ (Q, R). induction step: we first show that (i): (Q i F ∪ W ∞ (Q i E , R)) ≥ W ∞ (Q i F , R), then we prove by induction that (ii): W ∞ (Q i F , R) ≥ W ∞ (Q, R): (i) by construction Q i E ⊆ Q i F , thus (Q i F \ Q i E ) ∪ Q i E = Q i F ,
and by Invariant 2, we have

(Q i F \ Q i E ) ∪ Q i E ≥ rew(Q i F \ Q i E , R). Lemma 4 then entails that ((Q i F \ Q i E ) ∪ W ∞ (Q i E , R)) ≥ W ∞ ((Q i F \ Q i E ) ∪ Q i E , R) and we can conclude since Q i F = (Q i F \ Q i E ) ∪ Q i E . (ii) by construction, we have Q i F ≥ Q i-1 F ∪rew(Q i-1 E , R); so, by Lemma 3, we have W ∞ (Q i F , R) ≥ W ∞ (Q i-1 F ∪ rew(Q i-1 E , R), R) = W ∞ (Q i-1 F , R) ∪ W ∞ (rew(Q i-1 E , R), R). Moreover, Q i-1 E ⊆ Q i-1 F ⊆ W ∞ (Q i-1 F , R), thus W ∞ (Q i F , R) ≥ Q i-1 F ∪ Q i-1 E ∪ W ∞ (rew(Q i-1 E , R), R) = Q i-1 F ∪ W ∞ (Q i-1 E , R). Using (i), we have W ∞ (Q i F , R) ≥ W ∞ (Q i-1 F , R
) and conclude by induction hypothesis.

Invariant 4: for all distinct Q, Q ∈ Q F , Q ≥ Q and Q ≥ Q. Trivially satisfied
thanks to the properties of cover .

The next property states that if rew is prunable then Algorithm 1 halts for each case where W ∞ (Q, R) has a finite cover.

Property 6 Let rew be a rewriting operator, R be a set of rules and Q be a BCQ. If W ∞ (Q, R) has a finite cover and rew is prunable then Algorithm 1 halts.

Proof: Let Q be a finite cover of W ∞ (Q, R) and let m be the largest k for a k-rewriting in Q.

We thus have

W m (Q, R) ≥ Q ≥ W ∞ (Q, R).
Since the operator is prunable, we have

Q i F ≥ W i (Q, R) for all i ≥ 0 (proved with a straightforward induction on i). Thus Q m F ≥ W ∞ (Q, R). Thus, rew(Q m E , R) is covered by Q m F
, and since already explored queries are taken first for the computation of a cover, we have that

Q m+1 E = ∅.
Hence Algorithm 1 halts.

Theorem 7 Let rew be a rewriting operator, R be a set of rules and Q be a BCQ. If W ∞ (Q, R) has a finite cover and rew is prunable then Algorithm 1 outputs this cover (up to query equivalence).

Proof: By Property 6, Algorithm 1 halts. By Invariant 3 from Property 5,

(Q f F ∪ W ∞ (Q f E , R)) ≥ W ∞ (Q, R) where Q f F and Q f E denote the final values of Q F and Q E in Algorithm 1. Since Q f E = ∅ when Algorithm 1 halts, we have Q f F ≥ W ∞ (Q, R
). Thanks to Invariants 1 and 4 from Property 5 we conclude that

Q f F is a cover of W ∞ (Q, R).

Preserving Soundness and Completeness

We consider two further properties of a rewriting operator, namely soundness and completeness, with the aim of ensuring the soundness and completeness of the obtained rewriting set within the meaning of Definition 2.

Definition 9 (Soundness/completeness of a rewriting operator) Let rew be a rewriting operator. rew is sound if for any set of rules R, for any BCQ Q, for any Q ∈ rew(Q, R), for any fact F , F |= Q implies that F, R |= Q. rew is complete if for any set of rules R, for any BCQ Q, for any fact

F such that F, R |= Q, there exists Q ∈ W ∞ (Q, R) such that F |= Q .
Property 8 If rew is sound, then the output of Algorithm 1 is a sound rewriting set of Q and R.

Proof: Direct consequence of Invariant 1 from Property 5.

Perhaps surprisingly, the completeness of the rewriting operator is not sufficient to ensure the completeness of the output rewriting set. Examples are provided in Section 6.1. This is due to the dynamic pruning performed at each step of Algorithm 1. Therefore the prunability of the operator is also required.

Property 9 If rew is prunable and complete, then the output of Algorithm 1 is a complete rewriting set of Q and R.

Proof: Algorithm 1 returns Q F when Q E is empty. By Invariant 3 of Property 5, we know that (Q F ∪ W ∞ (∅, R)) ≥ W ∞ (Q, R). Since W ∞ (∅, R)) = ∅, we obtain that Q F ≥ W ∞ (Q, R).
Finally, as stated by the next theorem, when the rewriting operator is sound, complete and prunable, Algorithm 1 is correct and terminates for any finite unification set of rules. We remind that expressive classes of fus rules are known (see the introduction). In particular, the main members of DL-Lite family are generalized by the simple class of linear existential rules. See also Section 7 for examples of such ontologies.

Theorem 10 If rew is a sound, complete and prunable operator, and R is a finite unification set of rules, then for any BCQ Q, Algorithm 1 outputs a minimal (finite) sound and complete rewriting set of Q with R.

Proof: If R is a fus and rew is a sound and complete operator then W ∞ (Q, R) has a finite cover. The claim then follows from Properties 8 and 9 and Theorem 7.

Piece-Based Rewriting

As mentioned in the introduction (and illustrated in Example 2), existential variables in rule heads induce a structure that has to be taken into account in the rewriting mechanism. Hence the classical notion of a unifier is replaced by that of a piece-unifier [START_REF] Baget | On Rules with Existential Variables: Walking the Decidability Line[END_REF]. A piece-unifier "unifies" a subset Q of Q with a subset H of head(R), in the sense that the associated substitution u is such that u(Q ) = u(H ). Given a piece-unifier, Q is partitioned into "pieces", which are minimal subsets of atoms that must be processed together. More specifically, the cutpoints are the variables from Q that are not unified with existential variables from H (i.e., they are unified with frontier variables or constants); then a piece in Q is a minimal non-empty subset of atoms "glued" by variables other than cutpoints, i.e., connected by a path of variables that are not cutpoints. We recall below the definition of pieces given in [START_REF] Baget | On Rules with Existential Variables: Walking the Decidability Line[END_REF] (where T corresponds to the set of cutpoints).

Definition 10 (Piece) [START_REF] Baget | On Rules with Existential Variables: Walking the Decidability Line[END_REF] Let A be a set of atoms and T ⊆ vars(A). A piece of A according to T is a minimal non-empty subset P of A such that, for all a and a in A, if a ∈ P and (vars(a) ∩ vars(a )) ⊆ T , then a ∈ P .

In this paper, we give a definition of a piece-unifier based on partitions rather than substitutions, which simplifies subsequent proofs. For any substitution u from a set of variables E 1 to a set of terms E 2 associated with a piece-unifier, it holds that E 1 ∩E 2 = ∅. Thus, u can be associated with a partition P u of E 1 ∪ E 2 such that two terms are in the same class of P u if and only if they are merged by u; more specifically, we consider the equivalence classes of the symmetric, reflexive and transitive closure of the following relation ∼: t ∼ t if u(t) = t . Conversely, given a partition on a set of terms E, such that no class contains two constants, we can consider a substitution u obtained by selecting an element of each class with priority given to constants: if {e 1 . . . e k } is a class in the partition and e i is a selected element, then for all e j with 1 ≤ j = i ≤ k, we set u(e j ) = e i . If we consider a total order on terms, such that constants are smaller than variables, then a unique substitution is obtained by taking the smallest element in each class. We call admissible partition a partition such that no class contains two constants.

The set of all partitions over a given set is structured in a lattice by the "finer than" relation (given two partitions P 1 and P 2 , P 1 is finer than P 2 , denoted by P 1 ≥ P 2 , if every class of P 1 is included in a class of P 2 ). 7 The join of several partitions is the partition obtained by making the union of their non-disjoint classes. The join of two admissible partitions may be a non-admissible partition. We say that several admissible partitions are compatible if their join is an admissible partition. Note that if the concerned partitions are relative to the same set E, then their join is their greatest lower bound in the partition lattice of E.

The following property makes a link between comparable partitions and comparable substitutions.

Property 11 Let P 1 and P 2 be two admissible partitions over the same set such that P 1 ≥ P 2 , with associated substitutions u 1 and u 2 respectively. Then there is a substitution s such that u 2 = s • u 1 (i.e., u 1 is "more general" than u 2 ).

Proof: The substitution s is built as follows: for any class C i ∈ P 1 , let C j ∈ P 2 be the class such that C i ⊆ C j . Let e i (resp. e j ) be the selected element in C i (resp. C j ); if e i = e j (in this case, e i is necessarily a variable), then s(e i ) = e j . It can be immediately checked that u 2 = s • u 1 .

In the following definition of a piece-unifier, we assume that Q and R have disjoint sets of variables. Given Q ⊆ Q, we call separating variables from Q , and denote by sep(Q ), the variables occurring in both Q and

(Q \ Q ): sep(Q ) = vars(Q ) ∩ vars(Q \ Q ). Definition 11 (Piece-Unifier, Cutpoint) A piece-unifier of Q with R is a triple µ = (Q , H , P u ), where Q = ∅, Q ⊆ Q, H ⊆ head(R
) and P u is a partition on terms(Q ) ∪ terms(H ) satisfying the following three conditions:

1. P u is admissible; 2. if a class in P u contains an existential variable (from H ) then the other terms in the class are non-separating variables from Q ;

3. u(H ) = u(Q ), where u is a substitution associated with P u .

Figure 3: Piece-unifier

The cutpoints of µ, denoted by cutp(µ), are the variables from Q that are not unified with existential variables from H (i.e., they are unified with frontier variables or constants):

cutp(µ) = {x ∈ vars(Q ) | u(x) ∈ fr(R) ∪ consts(Q ) ∪ consts(H )}.
Given a query Q and a set of rules R, the piece-based rewriting operator computes the set of one-step piece-rewritings of Q according to all piece-unifiers of Q with a rule R ∈ R. We are now able to show that this operator fulfills the desired properties introduced in Section 4.

Theorem 16 Piece-based rewriting operator is sound, complete and prunable; this property is still true if only most general piece-unifiers are considered.

Proof: Soundness and completeness follow from Theorem 12. Prunability follows from Lemma 15. Thanks to Property 14, the proof remains true if most general pieceunifiers are considered.

Exploiting Single-Piece Unifiers

We are now interested in the efficient computation of piece-based rewritings. We identify several sources of combinatorial explosion in the computation of the piece-unifiers between a query and a rule:

1. The problem of deciding whether there is a piece-unifier of a given query Q with a given rule R is NP-complete in the general case. NP-hardness is easily obtained by considering the case of a rule with an empty frontier: then, there is a piece-unifier between Q and R if and only if there is a homomorphism from Q to H = head(R), which is an NP-complete problem, Q and H being any sets of atoms.

2. The number of most general piece-unifiers can be exponential in |Q|, even if the rule head H is restricted to a single atom. For instance, assume that each atom of Q unifies with H and forms its own piece; then there may be 2 |Q| piece-unifiers obtained by considering all subsets of Q.

3. The same atom in Q may belong to distinct pieces according to distinct unifiers, as illustrated by the next example.

Example 7 Let Q = r(u, v) ∧ q(v) and R = p(x) → r(x, y) ∧ r(y, x) ∧ q(y). Atom r(u, v) belongs to two single-piece unifiers: ({r(u, v), q(v)}, {r(x, y), q(y)}, {{u, x}, {v, y}}) and ({r(u, v)}, {r(y, x)}, {{u, y}, {v, x}}). For an additional example, see Example 6, where p(u, v) and p(v, w) both belong to µ 1 and µ 2 .

To cope with this complexity, an idea is to rely on single-piece unifiers, i.e., pieceunifiers of the form (Q , -, -) where Q is a single piece of Q. This section is devoted to the properties of rewriting operators exploiting this notion. We show that the rewriting operator based on single-piece (most general) unifiers is sound and complete. However, perhaps surprisingly, it is not prunable, which prevents to use it in the generic algorithm. To recover prunability, we will define the aggregation of singlepiece unifiers, which provides us with a new rewriting operator, which has all the desired properties and generates rewriting sets with fewer components than the standard piece-unifier. Note, however, that this will not completely remove the second complexity source (i.e., the exponential number of unifiers to consider) since the number of aggregations of single-piece unifiers can still be exponential in the size of Q, even with atomic-head rules.

Single-Piece Based Operator

As expressed by the following theorem, (most general) single-piece unifiers provide a sound and complete operator.

Theorem 17 Given a BCQ Q and a set of rules R, the set of rewritings of Q obtained by considering exclusively most general single-piece unifiers is sound and complete.

Proof: See Appendix.

The proof of this theorem is given in Appendix since it is not reused hereafter. Indeed, the restriction to single-piece unifiers is not compatible with selecting most general rewritings at each step, as performed in Algorithm 1. We present below some examples that illustrate this incompatibility. Example 8 (Basic example) Let Q = p(y, z) ∧ p(z, y) and R = r(x, x) → p(x, x). There are two single-piece unifiers of Q with R, µ 1 = ({p(y, z)}, {p(x, x)}, {{x, y, z}}) and µ 2 = ({p(z, y)}, {p(x, x)}, {{x, y, z}}), which yield the same rewriting, e.g. Q 1 = r(x, x)∧p(x, x). There is also a two-piece unifier µ = (Q, {p(x, x)}, {{x, y, z}}), which yields e.g. Q = r(x, x). A query equivalent to Q can be obtained from Q 1 by a further single-piece unification. Now, assume that we restrict unifiers to single-piece unifiers and keep most general rewritings at each step. Since Q ≥ Q 1 , Q 1 is not kept, hence Q will never be generated, whereas it is incomparable with Q.

Concerning the preceding example, given u 1 and u 2 the substitutions respectively associated with µ 1 and µ 2 , one may argue that u 1 (Q) is redundant and the same holds for u 2 (Q); hence, the problem would be solved by computing u 1 (Q)\u 1 (Q ) instead of u 1 (Q \ Q ) and making u 1 (Q) non-redundant (i.e., equal to p(x, x)) before computing u 1 (Q) \ u 1 (Q ), which would then be empty. However, the problem goes deeper, as illustrated by the next two examples.

Example 9 (Ternary predicates) Let Q = r(u, v, w) ∧ r(w, t, u) and R = p(x, y) → r(x, y, x). Again, there are two single-piece unifiers of Q with R: µ 1 = ({r(u, v, w)}, {r(x, y, x)}, {{u, w, x}, {v, y}}) and µ 2 = ({r(w, t, u)}, {r(x, y, x)}, {{u, w, x}, {t, y}}). One obtains two rewritings more specific than Q, e.g., Q 1 = p(x, y) ∧ r(x, v, x), and Q 2 = p(x, y) ∧ r(x, t, x), which are isomorphic. There is also a two-piece unifier (Q, {r(x, y, x)}, {{u, w, x}, {v, t, y}}), which yields p(x, y). If we remove Q 1 and Q 2 , no query equivalent to p(x, y) can be generated. Example 10 (Very simple rule) This example has two interesting characteristics: (1) it uses unary/binary predicates only (2) it uses a very simple rule expressible with any lightweight description logic, i.e., a linear existential rule where no variable appears twice in the head or the body. Let Q = r(u, v) ∧ r(v, w) ∧ p(u, z) ∧ p(v, z) ∧ p(v, t) ∧ p(w, t) ∧ p 1 (u) ∧ p 2 (w) (see Figure 4) and R = b(x) → p(x, y). Note that Q is not redundant. There are two single-piece unifiers of Q with R, say µ 1 and µ 2 , with pieces Q 1 = {p(u, z), p(v, z)} and Q 2 = {p(v, t), p(w, t)} respectively. The obtained queries are pictured in Figure 4. These queries are both more specific than Q. The removal would prevent the generation of a query equivalent to r(x, x)∧p 1 (x)∧p 2 (x)∧ b(x), which could be generated from Q with a two-piece unifier.

Property 18 The single-piece-based operator is not prunable.

Proof: Follows from the above examples.

By Theorem 5 and Property 24, one can show that the conclusion of Lemma 3 (Section 4.2) is valid for single-piece unifiers, even though they are not prunable. This justifies that Lemma 3 is not enough to prove the correctness of Algorithm 1.

Nevertheless, single-piece unifiers can still be used as an algorithmic brick to compute more complex piece-unifiers, as shown in the next subsection.

Aggregated-Piece Based Operator

We first explain the ideas that underline aggregated single-piece unifiers. Let us consider the set of single-piece unifiers naturally associated with a piece-unifier µ. If we successively apply each of these underlying single-piece unifiers, we may obtain a CQ strictly more general than β(Q, R, µ), as illustrated by the next example.

Example 11 Let R = p(x, y) → q(x, y) and Q = q(u, v) ∧ r(v, w) ∧ q(t, w). Let µ = (Q , H , P u ) be a piece-unifier of Q with R with Q = {q(u, v), q(t, w)}, H = {q(x, y)} and P u = {{u, t, x}, {v, w, y}}. β(Q, R, µ) = p(x, y) ∧ r(y, y). Q has two pieces w.r.t. µ: P 1 = {q(u, v)} and P 2 = {q(t, w)}. If we successively compute the rewritings with the underlying single-piece unifiers µ P1 and µ P2 , we obtain Q s = β(β(Q, R, µ P1 ), R, µ P2 ) = β(p(x, y)∧r(y, w)∧q(t, w), R, µ P2 ) = p(x, y)∧r(y, y )∧ p(x , y ), which is strictly more general than β(Q, R, µ).

Given a set U of "compatible" single-piece unifiers of a query Q with a rule (the notion of "compatible" will be formally defined below), we can thus distinguish between the usual piece-unifier performed on the union of the pieces from the unifiers in U and an "aggregated unifier" that would correspond to a sequence of applications of the unifiers in U. This latter unifier is more interesting than the piece-unifier because, as illustrated by Example 11, it avoids generating some rewritings which are too specific. We will thus rely on the aggregation of single-piece unifiers to recover prunability.

Note that, in this paper, we combine single-piece unifiers of the same rule whereas in [START_REF] König | On the Exploration of the Query Rewriting Space with Existential Rules[END_REF] we consider the possibility of combining unifiers of distinct rules (and thus compute rewritings from distinct rules in a single step). We keep below the definitions introduced in [KLMT13], while pointing out that, in the context of this paper, the rules R 1 . . . R k in the definitions are necessarily copies of the same rule R. Intuitively, an aggregated unifier of R is a piece-unifier of a new rule built by aggregating copies of R (as formally expressed by next Property 19).

Definition 14 (Aggregation of a set of rules) Let R = {R 1 . . . R k } be a set of rules, with pairwise disjoint sets of variables. The aggregation of R, denoted by R

1 . . . R k , is the rule body(R 1 ) ∧ . . . ∧ body(R k ) → head(R 1 ) ∧ . . . ∧ head(R k ).
Definition 15 (Compatible set of piece-unifiers, Aggregated unifier)

Let U = {µ 1 = (Q 1 , H 1 , P 1 ) . . . µ k = (Q k , H k , P k )} be a set of piece-unifiers of Q with rules R 1 . . . R k respectively
, where the rules have pairwise disjoint sets of variables (in particular, for all 1 ≤ i, j ≤ k, i = j, it holds that vars(H i ) ∩ vars(H j ) = ∅).

• Set U is said to be compatible if (1) all Q i and Q j are pairwise disjoint; (2) the join of P 1 . . . P k is admissible.

• Given such a compatible set U, an aggregated unifier

of Q with R 1 . . . R k w.r.t. U is µ = (Q , H , P ) where: (1) Q = Q 1 ∪ . . . ∪ Q k ; (2) H = H 1 ∪ . . . ∪ H k ;
(3) P is the join of P 1 . . . P k . It is said to be single-piece if all the piece-unifiers in U are single-piece. It is said to be most general if all the piece-unifiers in U are most general.

Property 19 Let Q be a BCQ and

U = {µ 1 = (Q 1 , H 1 , P 1 ) . . . µ k = (Q k , H k , P k )} be a compatible set of piece-unifiers of Q with R 1 . . . R k .
Then, the aggregated unifier of U is a piece-unifier of Q with the aggregation of {R 1 . . . R k }.

Proof: We show that the aggregated unifier µ = (Q , H , P u ) of U satisfies the conditions of the definition of a piece-unifier (Definition 11). Condition 1 is fulfilled since, by definition of compatibility, the join of P 1 . . . P k is admissible. Condition 2 is satisfied as well, because, since P 1 . . . P k satisfy it, so does their join. Indeed, if a class contains an existential variable, it cannot be merged with another by aggregation because its other terms are non-separating variables, hence do not appear in other classes. Concerning the last condition, for all 1 ≤ i ≤ k, we have

u i (H i ) = u i (Q i )
, where u i is a substitution associated with

P i . Since Q = k i=1 Q i and H = k i=1
H i we know that, for any substitution u associated with P u , we have u(H ) = u(Q ).

According to this property, the rewriting associated with an aggregated unifier µ can be defined as β(Q, R 1 . . . R k , µ). It corresponds to the rewriting obtained by applying the piece-unifiers associated with the R i one after the other, as illustrated by the next example.

Example 12 Consider again Example 11. Let R = p(x , y ) → q(x , y ) be a copy of R. The aggregation R R is the rule p(x, y) ∧ p(x , y ) → q(x, y) ∧ q(x , y ).

Let U = {µ P1 , µ P2 } where µ P1 = ({q(u, v)}, {q(x, y)}, {{u, x}, {v, y}}) and µ P2 = ({q(t, w)}, {q(x , y )}, {{t, x }, {w, y }}) . The aggregated unifier of Q with R, R w.r.t. U is ({q(u, v), q(t, w)}, {q(x, y), q(x , y )}, {{u, x}, {v, y}, {t, x }, {w, y }}). The associated rewriting of Q is p(x, y) ∧ r(y, y ) ∧ p(x , y ), which is equal to the rewriting Q s in Example 11.
The difference between a piece-unifier and an aggregated unifier of Q with R can also be explained as follows: to build a piece-unifier of Q with R, we consider partitions of terms(Q) ∪ terms(head(R)), while in the aggregation operation we consider partitions of terms(Q) ∪ k i=1 terms(head(R i )), where k is the number of considered single-piece unifiers, and each R i is safely renamed from R. In other words, if, in the definition of an aggregated unifier, we assumed that the R 1 . . . R k had been exactly R, instead of safely renamed copies of R, then the aggregation of R 1 . . . R k would have We conclude by showing that h is a homomorphism from β(Q, R , µ

) = u (body(R 1 )∪ . . . ∪ body(R k )) ∪ u (Q \ Q ) to β(Q, R, µ) = u(body(R)) ∪ u(Q \ Q ), with two points:
1. for all i, h(u (body(R i ))) = u(body(R)). Indeed, for any variable x ∈ vars(body(R i )):

• either x ∈ vars(body(R i ))\vars(H i ), hence h(u (x)) = h(x) = h -1 i (x) = u(h -1
i (x)) (u does not substitute the variables from vars(body(R))\vars(H )),

• or x ∈ fr(R i ) ∩ vars(H i ), hence h(u (x)) = s(u (x)) = u(h -1 i (x)); 2. h(u (Q \ Q )) = u(Q \ Q ). Indeed, for any variable x ∈ vars(Q \ Q ): • either x ∈ vars(Q ), then h(u (x)) = s(u (x)) = u(h -1 i (x)) = u(x) (h -1
i does not substitute the variables from Q), andu do not substitute the variables from vars(Q) \ vars(Q )).

• or x ∈ vars(Q) \ vars(Q ), then h(u (x)) = h(x) = x = u(x) (u
We call single-piece aggregator the rewriting operator that computes the set of onestep rewritings of a query Q by considering all the most general single-piece aggregated unifiers of Q.

Theorem 21 The single-piece aggregator is sound, complete and prunable.

Proof: Soundness comes from Property 19 and from the fact that, for any set of rules R, let R be the aggregation of R, one has R |= R. Completeness and prunability rely on the fact that the piece-based rewriting operator fulfills these properties, and the fact that for any queries Q and Q and any rule R, if Q = β(Q, R, µ), where µ is a pieceunifier, then the query Q obtained with the single-piece aggregator corresponding to µ is more general than Q , as expressed by Property 20.

Detailed Algorithms and Experiments

In this section, we first detail on the computation of all the most general single-piece unifiers of a query Q with a rule R, and explain how we use them to compute all the single-piece aggregators. Then, we focus on the specific case of unification with atomic-head rules, for which the computation is simpler. Last, we report first experiments.

Computing single-piece unifiers and their aggregation

We first introduce the notion of a pre-unifier, which is weaker than a piece-unifier. To become a piece-unifier, a pre-unifier has to satisfy an additional constraint on the separating variables of the unified subset of Q.

Definition 16 (Valid Partition) Let Q be a BCQ, R be a rule, Q ⊆ Q, H ⊆ head(R), and P u be a partition on terms(Q ) ∪ terms(H ). P u is valid if no class of P u contains two constants, or two existential variables of R, or a constant and an existential variable of R, or an existential variable of R and a frontier variable of R.

Definition 17 (Pre-unifier) Let Q be a BCQ, R be a rule, Q ⊆ Q, H ⊆ head(R), and P u be a partition on terms(Q ) ∪ terms(H ). Then µ = (Q , H , P u ) is a preunifier of Q with R if (1) P u is valid, and (2) given a substitution u associated with P u , it holds that u(H ) = u(Q ).

The next definition introduces the notion of sticky variables, which are the variables of Q that prevent Q to be a piece.

Definition 18 (Sticky Variables) Let Q be a BCQ, R be a rule, Q ⊆ Q, H ⊆ head(R) and P u be a partition on terms(Q ) ∪ terms(H ). The sticky variables of Q in P u w.r.t. Q and R, denoted by sticky(Q , P u ), are the separating variables of Q that occur in a class of P u containing an existential variable of R.

The next property ensures that a pre-unifier without sticky variables is a pieceunifier, and reciprocally. Its proof follows from the definitions.

Property 22 Let Q be a BCQ, R be a rule, Q ⊆ Q, H ⊆ head(R), and P u be a partition on terms(Q ) ∪ terms(H ). Then µ = (Q , H , P u ) is a piece-unifier of Q with R iff µ is a pre-unifier and sticky(Q , P u ) = ∅.

The fact that we can first build pre-unifiers, then check the absence of sticky variables, suggests an incremental method to compute all the most general single pieceunifiers of Q with R.

The first step consists in computing all the most general pre-unifiers of an atom a ∈ Q with an atom b ∈ head(R) with the same predicate. The partition on the terms of these atoms associated with their unification has to be valid. The next definition defines formally this notion of partition. Hence, the partition by position associated with {a, b} has to be valid. We denote by AP U the set of all the most general atomic pre-unifiers, i.e., AP U = {µ = ({a}, {b}, P ) | a ∈ Q, b ∈ head(R), and µ is a pre-unifier of Q with R }. Algorithm 2 details the computation of AP U .

We then use AP U to compute the set of all the most general single-piece unifiers of Q with R, denoted by SP U . Each atomic pre-unifier of AP U is incrementally extended in all possible ways with other atomic pre-unifiers of AP U , which contain "missing" atoms of Q with respect to sticky variables. Extending pre-unifier (Q 1 , H 1 , P 1 ) with pre-unifier (Q 2 , H 2 , P 2 ) consists in merging both pre-unifiers to obtain a new pre-unifier (Q 1 ∪ Q 2 , H 1 ∪ H 2 , join(P 1 , P 2 )); this extension can be performed if and only if the join of P 1 and P 2 is a valid partition; if the obtained pre-unifier has no sticky variable, it is a single piece-unifier.

Next algorithms 3, 4 and 5 detail the computation of SP U . Algorithm 3 is the main algorithm. It first uses Algorithm 2 to compute AP U , then, for each atomic pre-unifier µ ∈ AP U , it calls Algorithm 4, which computes the single-piece unifiers extending µ. Algorithm 4 first checks if µ contains sticky variables: if it it is the case, this singlepiece unifier is returned, otherwise the algorithm is recursively called, after a call to Algorithm 5 to obtain a set of candidate extensions of µ. Finally, the set of all the single-piece aggregators of Q with R is obtained by aggregating the unifiers from all non-empty compatible subsets of SP U . For optimisation reasons, this set is incrementally computed as follows:

1. Let U 1 = SP U = {µ 1 , . . . , µ k }; the µ i are called 1-unifiers.

2. For i = 2 to the greatest possible rank (i.e., as long as U i is not empty): let U i be the set of all i-unifiers obtained by aggregating an (i -1)-unifier from U i-1 and a single-piece unifier from U 1 .

3. Return the union of all the U i obtained.

The Specific Case of Atomic-Head Rules

Rules with an atomic head are often considered in the literature, specifically in logic programming or in deductive databases. One may ask if piece-unification become simpler in this specific case. In fact, considering atomic-head rules does not simplify the definition of a piece-unifier in itself, but its computation. Indeed, there is now a unique way of associating any atom from Q with the head of a rule. It follows that deciding whether there is a piece-unifier of Q with a rule can be done in linear time with respect to the size of Q (whereas it is NP-complete in the general case) and each atom belongs to a single piece, thus the set of all single-piece unifiers of Q with a rule can be computed in polynomial time.

More precisely, if a rule R has an atomic head, then every atom in Q participates in at most one most general single-piece unifier of Q with R (up to bijective variable renaming). This is is a corollary of the next property.

Property 23 Let R be an atomic-head rule and Q be a BCQ. For any atom a ∈ Q, there is at most one Q ⊆ Q such that a ∈ Q and Q is a piece for a piece-unifier of Q with R.

Proof: We prove by contradiction that two single-piece unifiers cannot share an atom of Q. Assume there are Q

1 ⊆ Q and Q 2 ⊆ Q such that Q 1 = Q 2 and Q 1 ∩ Q 2 = ∅, and µ 1 = (Q 1 , H, P 1 u ) and µ 2 = (Q 2 , H, P 2 u ) two single-piece-unifiers of Q with R, with H = head(R). Since Q 1 = Q 2 , one has Q 1 \ Q 2 = ∅ or Q 2 \ Q 1 = ∅. Assume Q 1 \ Q 2 = ∅. Let A = Q 1 ∩ Q 2 and B = Q 1 \ A.
There is at least one variable x ∈ vars(A) ∩ vars(B) such that there is an existential variable e of head(R) in the class of P 1 u containing x (otherwise µ 1 has more than one piece). Since H is atomic, there is a unique way of associating any atom with H, thus the class of P 2 u containing x contains e as well. It follows that Q 2 is not a piece since an atom of A and an atom of B share the variable x unified with an existential variable in µ 2 , while A is included in Q 2 and B is not.

The fact that an atom from Q participates in at most one most general single-piece unifier allows some algorithmic improvements. Indeed, when a piece-unifier of Q with head(R) is successfully built, all the atoms of Q can be removed from the set of atoms to be considered in the computation of the next piece-unifiers. Furthermore, there is a unique way of associating any atom from Q with head(R), hence there is only one pre-unifier of Q with head(R). Algorithm 6 exploits these specific aspects to compute all the single-piece unifiers of a query with an atomic-head rule.

Example 13 Let R = q(x) → p(x, y) and Q = p(u, v) ∧ p(v, t). Let us start from p(u, v): this atom is unifiable with head(R) and p(v, t) necessarily belongs to All tests reported here were performed on a DELL machine with a processor at 3.60 GHz and 16 GB of RAM, with 4 GB allocated to the Java Virtual Machine.

Table 1 reports the behavior of the rewriting algorithm on A vs AX and U vs UX with respect to three parameters: the runtime, the size of the output (number of CQs) and the number of generated CQs. The size of the output for AX and UX is before elimination of queries containing auxiliary predicates. The generated CQs are all the rewritings built during the rewriting process (excluding the initial query and possibly including some multi-occurrences of the same rewritings). We can see that avoiding rule decomposition makes a substantial difference. The gain is particularly striking with Q 5 on A / AX with respect to all three parameters (the runtime is 21 seconds for A and 1 hour and 36 minutes for AX, the size of the output is more than 52 times larger for AX before elimination of useless queries, and the number of generated queries is 89 times larger for AX). Moreover, we point out that only 29 / 102 rules in A and 5 / 77 rules in U have multiple heads, with only 2 atoms; we can reasonably expect that the gain increases with the proportion of multiple-head rules and the size of rule heads. Table 2: Generated queries with the single-piece aggregator Table 2 presents the size of the output, the number of generated CQs and the number of explored CQs for each ontology (as well as the runtime for information, see also Table 4). Note that, since subsumed rewritings are removed at each step of the breadthfirst algorithm, only some of the rewritings generated at a given step are explored at the next step. We can see that the number of generated queries can be large with respect to the cardinality of the output, which is less marked for explored queries. Table 3: Types of rules in the ontologies Our query rewriting tool is able to process any kind of existential rules. There is of course a price to pay for this expressivity, in terms of complexity of the involved mechanisms and time efficiency. We consider the algorithms presented in this paper as basic versions, which can be further improved in various ways, for instance by processing some specific kinds of rules in a specific way. Let us illustrate this with the example of rules expressing taxonomies. Indeed, a large part of currently available ontologies is actually composed of concept and role hierarchies. See Table 3: 71%, 31%, 47%, 91% and 53 % of the rules in ontologies A, S, U, V and G, respectively, express atomic concept or role inclusions.

We can compile these sets of rules as preorders on predicates. The detailed presentation of how to compute and process these preorders is out of the scope of this paper. Briefly said, the preorders are integrated into the rewriting process, which allows to generate a smaller rewriting set, this set being unfolded at the end to produce the expected UCQ. Our purpose here is just to illustrate the fact that some improvements of the basic version can dramatically decrease the runtime, while still relying on the same fundamental mechanisms. Table 4 allows to compare these two versions: PURE9 denotes the basic version of our tool and PURE H is the version with compiled hierarchical rules (note that compilation is performed offline, hence the algorithm takes as input the preorder and the non-hierarchical rules).

We also compared to two other query rewriting tools, Nyaya and Rapid. Nyaya is a tool dedicated to UCQ rewriting with linear and sticky existential rules, which implements the techniques presented in [START_REF] Gottlob | Ontological queries: Rewriting and optimization[END_REF], in particular an optimization for linear rules (which include DL-Lite ontologies). Table 4 shows that our tool is generally faster on the considered benchmark, even in its basic version, specially on Ontology A. This difference could be due to the fact that Nyaya does not directly process multiplehead rules, hence has to decompose them into atomic-head rules. For the large ontology G, Nyaya seemed to be still in a preprocessing step after several hours. Note that the very latest version of Nyaya includes parallel rewriting, which we did not consider here, since our tool does include this kind of optimization.

As far as we know, Nyaya is the only other tool able to process existential rules beyond lightweight DLs. We think that comparing to DL rewriting tools is not very relevant, since these systems make use of specific features, like predicate arity bounded by two, or the tree-model property. Tools tailored for DL-Lite exploit even further the very specific form of DL-Lite axioms. However, we compared to one of these tools, namely Rapid, to obtain an order of magnitude. Rapid is one of the fastest tools dedicated to DL-Lite ontologies [START_REF] Chortaras | Optimized Query Rewriting for OWL 2 QL[END_REF]. In Table 4, we can see that Rapid is indeed generally faster than our tool, the difference being less pronounced on the version with rule compilation.

Current work includes processing specific kinds of rules in a specific way, while Table 4: Runtime (ms) with several query rewriting tools keeping a system able to process any set of existential rules. Other optimizations could be implemented, such as exploiting dependencies between rules to select the rules to be considered at each step. Moreover, the form of the considered output itself, i.e., a union of conjunctive queries, leads to combinatorial explosion. Considering semiconjunctive queries instead of conjunctive queries as in [START_REF] Thomazo | Compact Rewriting for Existential Rules[END_REF] can save much with respect to both the running time and the size of the output, without compromising the efficiency of query evaluation; in [START_REF] Thomazo | Compact Rewriting for Existential Rules[END_REF] the piece-based rewriting operator is combined with query factorization techniques. We did not consider generating Datalog queries yet. Finally, further experiments should be performed on more complex ontologies. However, even if slightly more complex ontologies could be obtained by translation from description logics, real-world ontologies that would take advantage of the expressiveness of existential rules, as well as associated queries, are currently lacking.

Definition 1 (

 1 Existential rule) An existential rule (or simply a rule) is a formula R = ∀ x∀ y(B[ x, y] → ∃ zH[ y, z]), where x, y and z are tuple of variables, B = body(R) and H = head(R) are conjunctions of atoms, resp. called the body and the head of R. The frontier of R, denoted by fr(R), is the set vars(B) ∩ vars(H) = y. The set of existential variables in R is the set vars(H) \ fr(R) = z.

Figure 2 :

 2 Figure 2: Cover (Example 3)

Figure 4 :

 4 Figure 4: The queries in Example 10

Definition 19 (

 19 Partition by Position) Let A be a set of atoms with the same predicate p. The partition by position associated with A, denoted by P p (A), is the partition on terms(A) such that two terms of A occurring in the same position i (1 ≤ i ≤ arity(p)) are in the same class of P p (A).

  Algorithm 2: COMPUTATION OF AP U , THE SET OF THE MOST GENERAL = predicate(b) and P p ({a, b}) is valid then AP U ← AP U ∪ {({a}, {b}, P p ({a, b})}

	ATOMIC PRE-UNIFIERS
	Data: A BCQ Q and a rule R
	Result: The set of the most general pre-unifiers of an atom of Q with an atom of
	head(R)
	begin
	AP U ← ∅;
	foreach a ∈ Q do
	foreach b ∈ head(R) do
	if predicate(a) return AP U
	Algorithm 3: COMPUTATION OF SP U , THE SET OF THE MOST GENERAL
	SINGLE-PIECE UNIFIERS

Data: A BCQ Q and a rule R Result: The set of most general single-piece unifiers of

Q with R begin SP U ← ∅; AP U ← computeAPU(Q, R) ; // see

Algorithm 2 while AP U = ∅ do choose and remove ({a}, {b}, P ) from AP U ; SP U ← SP U ∪ SPUext({a}, {b}, P ); // see Algorithm 4 return SP U ;

  , H , P )} // it is a single-piece unifier elseQ add ← {a ∈ Q \ Q | vars(a) ∩ sticky(Q , P ) = ∅}; Ext ← Extend((Q , H , P ), Q add , AP U ) ; // see Algorithm 5 EP U ← ∅; foreach (Q ext , H ext , P ext ) ∈ Ext do EP U ← EP U ∪ SPUext(Q ext ,H ext , P ext ); // recursive call to Algorithm 4 return EPU ;

	Algorithm 4: COMPUTATION OF THE MOST GENERAL SINGLE-PIECE UNI-
	FIERS EXTENDING A GIVEN PRE-UNIFIER
	Access: Q, R and AP U declared in the calling algorithm 3
	Data: (Q , H , P ) a pre-unifier of Q with R
	Result: The set of the most general single-piece unifiers extending (Q , H , P )
	begin
	if sticky(Q , P ) = ∅ then
	return {(Q

See e.g.[START_REF] Chein | Graph-based Knowledge Representation and Reasoning-Computational Foundations of Conceptual Graphs[END_REF], Section

2.6, on basic conceptual graphs. The algorithm can even by made linear, noticing that an atom needs to be considered only once.

A substitution is given as a set of pairs, where a pair (x, e) means that x is substituted by e.

We generalize the classical notion of a fact in order to take existential variables into account.

Q∈Q rew k (Q, R) and W k (Q, R) = i≤k rew i (Q, R).4 See for instance[START_REF] Hell | The core of a graph[END_REF], where the notion of a core is traced back to the late sixties.5 The notion of a finite unification set was first introduced in [BLMS09] and defined with respect to pieceunifiers. However, since piece-unifiers provide a sound and complete rewriting operator (see Section 5) and all the covers of a given set have the same cardinality, the two definitions are equivalent.

Note that a depth-first exploration would not ensure termination for fus rules.

Usually, the notation ≤ is used to denote the relation "finer than". We adopt the converse convention, which is more in line with substitutions and the ≥ preorder on CQs.

Piece Unification based REwriting

Acknowledgments. We thank Giorgio Orsi for providing us with rule versions of ontologies A, S, U and V, as well as the version of Nyaya used for the experiments (October 2013 version). This work was partially funded by the ANR project PAGODA (ANR-12-JS02-007-01).

Condition 2 in the piece-unifier definition ensures that a separating variable in Q is necessarily a cutpoint. It follows that Q is composed of pieces: indeed, an existential variable from H is necessarily unified with a non-separating variable from Q , say x, which ensures that all atoms from Q in which x occurs are also part of Q . Figure 5 illustrates these notions.

We provide below some examples of piece-unifiers.

Example 5 Let R = q(x) → p(x, y) and Q = p(u, v) ∧ p(w, v) ∧ p(w, t) ∧ r(u, w).

Let H = {p(x, y)}. They are three piece-unifiers of Q with R: µ 1 = (Q 1 , H , P 1 u ) with Q 1 = {p(u, v), p(w, v)} and P 1 u = {{x, u, w}, {y, v}} µ 2 = (Q 2 , H , P 2 u ) with Q 2 = {p(w, t)} and P 2 u = {{x, w}, {y, t}} µ 3 = (Q 3 , H , P 3 u ) with Q 3 = {p(u, v), p(w, v), p(w, t)} and P 3 u = {{x, u, w}, {y, v, t}} Note that Q 1 and Q 2 are each composed of a single piece; Q 3 = Q 1 ∪ Q 2 and P 3 u is the join of P 1 u and P 2 u .

In the previous example, R has an atomic head, thus a piece-unifier of Q with R actually unifies the atoms from Q and the head of R into a single atom. In the general case, a piece-unifier unifies Q and a subset H of head(R) into a set of atoms, as illustrated by the next example.

Example 6 Let R = q(x) → p(x, y) ∧ p(y, z) ∧ p(z, t) ∧ r(y) and Q = p(u, v) ∧ p(v, w) ∧ r(u). A piece-unifier of Q with R is µ 1 = (Q 1 , H 1 , P 1 u ) with Q 1 = {p(u, v), p(v, w)}, H 1 = {p(x, y), p(y, z)} and P 1 u = {{x, u}, {v, y}, {w, z}}. Another piece-unifier is µ 2 = (Q 2 , H 2 , P 2 u ) with Q 2 = Q, H 2 = {p(y, z), p(z, t), r(y)} and P 2 u = {{u, y}, {v, z}, {w, t}}. Note that µ 3 = (Q 3 , H 3 , P 3 u ) with Q 3 = {p(u, v)}, H 3 = {p(x, y)} and P 3 u = {{x, u}, {v, y}} is not a piece-unifier because the second condition in the definition of piece-unifier is not fulfilled: v is a separating variable and is matched with the existential variable y.

Then, the notions of a one-step rewriting according to a piece-unifier, and of a rewriting obtained by a sequence of one-step rewritings, are defined in the natural way.

Definition 12 (One-step Piece-Rewriting) Given a piece-unifier µ = (Q , H , P u ) of Q with R, the one-step piece-rewriting of Q according to µ, denoted by β(Q, R, µ), is the BCQ u(body(R)) ∪ u(Q \ Q ), where u is a substitution associated with P u .

We thus define inductively a k-step piece-rewriting as a (k -1)-step piece rewriting of a one-step piece-rewriting. For any k, a k-step piece-rewriting of Q is a piecerewriting of Q.

The next theorem states that piece-based rewriting is logically sound and complete.

Theorem 12 ([SM96, BLMS11]) Let K = (F, R) be a KB and Q be a BCQ. Then

It follows from Theorem 12 that a sound and complete rewriting operator can be based on piece-unifiers: we call piece-based rewriting operator, the rewriting operator that, given Q and R, outputs all the one-step piece-rewritings of Q according to a piece-unifier of Q with R ∈ R. We denote it by β(Q, R).

Actually, as detailed hereafter, only most general piece-unifiers are to be considered, since the other piece-unifiers produce more specific queries.

Definition 13 (Most General Piece-Unifier) Given two piece-unifiers defined on the same subsets of a query and a rule head,

) is called a most general piece-unifier if it is more general than all the piece-unifiers on Q and H .

Property 13 Let µ 1 and µ 2 be two piece-unifiers with µ 1 ≥ µ 2 . Then µ 1 and µ 2 have the same pieces.

Proof: µ 1 and µ 2 have the same pieces iff they have the same cutpoints. It holds that cutp(µ 1 ) ⊆ cutp(µ 2 ) since every class from P 1 u is included in a class from P 2 u : hence a variable from Q that is in the same class as a frontier variable or a constant in P 1 u also is in P 2 u . It remains to prove that cutp(µ 2 ) ⊆ cutp(µ 1 ). Let x be a cutpoint of µ 2 and P 2 u (x) be the class of x in P 2 u . Since x is a cutpoint of µ 2 , there is a term t in P 2 u (x) that is a constant or a frontier variable. Since P 1 u ≥ P 2 u , we know that P 1 u (x) ⊆ P 2 u (x). Let t be a term of H from P 1 u (x) (there is at least one term of H and one term of Q in each class since the partition is part of a unifier of H and Q ). We are sure that t is not an existential variable because t ∈ P 2 u (x) and an existential variable cannot be in the same class as t (Condition 2 in the definition of a piece-unifier), so t is a frontier variable or a constant, hence x is a cutpoint of µ 1 .

Proof: Let u 1 (resp. u 2 ) be a substitution associated with P 1 u (resp. P 2 u ). Since P 1 u ≥ P 2 u , there is a substitution s such that

The following lemma expresses that piece-based rewriting operator is prunable.

u ) be a pieceunifier of Q 2 with R, and let u 2 be a substitution associated with P 2 u . We consider two cases:

Let P 1 u be the partition on terms(H 1 ) ∪ terms(Q 1 ) such that two terms are in the same class of P 1 u if these terms or their images by h are in the same class of P 2 u (i.e., for a term t, we consider

u fulfills all the conditions of the piece-unifier definition since P 2 u fulfills these conditions.

Let u 1 be a substitution associated with P 1 u . For each class P of P 1 u (resp. P 2 u ), we call selected element the unique element t of P such that u 1 (t) = t (resp. u 2 (t) = t). We build a substitution s, from the selected elements of the classes in P 1 u which are variables, to the selected elements of the classes in P 2 u , as follows: for any class P of P 1 u , let t be the selected element of

by considering three cases according to the part of β(Q 1 , R, µ 1 ) in which the variable occurs, i.e., in Q 1 but not in Q 1 , in body(R) but not in H 1 , or in the remaining part corresponding to the images of sep(Q 1 ) by u 1 :

with two points:

1. h (u 1 (body(R))) = u 2 (body(R)). Indeed, for any variable x of body(R):

we point out that, for any variable

been exactly R after removal of duplicate atoms, and the aggregated unifier would have been the usual piece-unifier.

The next property shows that, from any piece-unifier µ, one can build a most general single-piece aggregated unifier, which produces a rewriting more general than the one produced by µ.

Property 20 For any piece-unifier µ of Q with R, there is a most general singlepiece aggregated unifier

Proof: Let Q 1 , . . . , Q k be the pieces of Q according to µ = (Q , H , P u ) and let u be a substitution associated with P u . Let R 1 . . . R k be safely renamed copies of R. Let h i denote the variable renaming used to produce R i from R.

} be a set of piece-unifiers of Q with R 1 , . . . , R k built as follows for all i:

• H i is the image by h i of the subset of H unified by u with Q i • let h i (P u ) be the partition built from P u by replacing each x ∈ vars(H ) by h i (x); then, P i u is obtained from h i (P u ) by (1) restricting it to the terms of Q i and H i , and (2) refining it as much as possible while keeping the property that

, where u i is a substitution associated with the partition.

For any µ i = (Q i , H i , P i u ) we immediately check that:

1. µ i is a most general piece-unifier.

2. µ i is a single-piece unifier.

3. for all µ j ∈ U, with µ i = µ j , µ j and µ i are compatible.

Let µ = (Q , H , P u ) be the aggregated unifier of Q with R 1 , . . . , R k w.r.t. U. Note that Q = Q . The above properties fulfilled by any µ i from U ensure that µ is a most general single-piece aggregated unifier.

We note R = R 1 . . . R k . It remains to prove that β(Q, R , µ ) ≥ β(Q, R, µ). Let u be a substitution associated with P u . For each class P of P u (resp. P u ), we call selected element the unique element t of P such that u(t) = t (resp. u (t) = t).

We build a substitution s, from the selected elements in P u which are variables, to the selected elements in P u , as follows: for any class P of P u , let t be the selected element of

Note that for any term t in P u , there is a variable renaming h i such that s(u (t)) = u(h -1 i (t)) (if t is a constant or a variable from vars(Q) then any h i can be chosen).

We build now a substitution h from vars(β(Q, R , µ )) to terms(β(Q, R, µ)), by considering three cases according to the part of β(Q, R , µ ) in which the variable occurs, i.e., in Q but not in Q , in body(R i ) but not in H i , or in the remaining part corresponding to the images of sep(Q ) by u : It should be noted that any existential rule can be decomposed into an equivalent set of rules with atomic head by introducing a new predicate, which gathers the variables of the original head (e.g. [START_REF] Calì | Taming the Infinite Chase: Query Answering under Expressive Relational Constraints[END_REF][START_REF] Baget | Extending Decidable Cases for Rules with Existential Variables[END_REF]). Hence, the restriction to atomic-head rules can be made without loss of expressivity. Now, the question is whether it is more efficient to directly process rules with complex heads, or to decompose them into atomic-head rules and benefit from a simpler computation of piece-unifiers. The experiments reported below clearly show that the former choice is better.

Experiments and Perspectives

The query rewriting algorithm, instantiated with the rewriting operator described in the preceding section, has been implemented in Java. Since benchmarks dedicated to existential rules are not available yet, first experiments were carried out with sets of existential rules obtained by translation from ontologies expressed in the description logic DL-Lite R , namely ADOLENA (A), STOCKEXCHANGE (S), UNIVERSITY (U) and VICODI (V). This benchmark was introduced in [PUHM09] and then used in several papers, e.g., [START_REF] Gottlob | Ontological queries: Rewriting and optimization[END_REF][START_REF] Chortaras | Optimized Query Rewriting for OWL 2 QL[END_REF][START_REF] Imprialou | Benchmarking Ontology-Based Query Rewriting Systems[END_REF][START_REF] König | A Sound and Complete Backward Chaining Algorithm for Existential Rules[END_REF]. Ontologies A and U contain some rules with multiple heads; the ontologies obtained by decomposing rules into

and there is a pre-unifier (Q , head(R), P ) and

atomic-head rules are respectively known as AX and UX. Additionally, we considered the translation of a larger ontology, the DL-Lite version of OpenGalen2 8 (G), which contains more than 50k rules. Each ontology is provided with five handcrafted queries.

In [START_REF] König | A Sound and Complete Backward Chaining Algorithm for Existential Rules[END_REF], we compared with other systems concerning the size of the output and pointed out that none of the existing systems output a complete set of rewritings. However, beside the fact that these systems have evolved since then, one can argue that the size of the rewriting set should not be a decisive criterion (indeed, assuming that the systems are sound and complete, a minimal rewriting set can be obtained by selecting most general elements, see Theorem 1). Therefore, other criteria have to be taken into account, such as the runtime or the total number of CQs generated during the rewriting process.

Appendix: Proof of Theorem 17

To prove the completeness of the single-piece based operator, we first prove the following property:

Property 24 For any piece-unifier µ of Q with R, there is a sequence of rewritings of Q with R using exclusively most general single-piece unifiers and leading to a BCQ

Proof: We first introduce some notations. Given a partition P and x a term occurring in P , P (x) is the class of P that contains x. Let P and P be two partitions such that the terms of P are included in the terms of P and any class of P is included in a class of P : then we say that P is a subpart of P (note that if P and P are defined on the same set, it means that P is finer than P ) Let P c 1 , . . . , P c n be the pieces of Q according to µ = (Q , H , P u ) and let u be a substitution associated to

and u i is a substitution associated with P i u with: • R i is a safely renamed copy of R by a variable renaming h i .

• H i is the image by h i of the subset of H unified by u with P c i • P i u is obtained from partition h i (P u ) (built from P u by applying h i ) by ( 1) restricting it to the terms of Q i and H i (2) refining it as much as possible while keeping the property that it is associated with a unifier of H i and Q i . Note that P i u is a subpart of h i (P u ).

u be the partition assigned to u • i . We know that P i• u is the join of P 1 u , . . . P i u , thus P i• u is a subpart of P h u , the join of the h i (P u ) for 1 ≤ i ≤ n. Indeed, for each i, P i u is a subpart of h i (P u ) and the following property is easily checked: let s 1 and s 2 be substitutions with disjoint domains, and P 1 s , P 2 s be their associated partitions; then, the partition assigned to s 1 • s 2 (and to s 2 • s 1 ) is exactly the join of P 1 s and P 2 s .

• Q 1 = P c 1 and for i > 1, Q i = u • i-1 (P c i ). We ensure the property than ∀i,

For similar reasons, we ensure the property that ∀i, ∀j > i, u

We now show that:

1. µ i is a piece-unifier 2. µ i is a most general piece-unifier 3. µ i is a single-piece unifier For the first point:

• P i u satisfies the conditions of a piece-unifier because P u satisfies them and P i u is a subpart of h i (P u ).

For the second point, since P i u is the finest partition associated with a piece-unifier of H i and Q i , we are sure that µ i is a most general piece-unifier.

For the third point, note that each atom of Q i corresponds to at least one atom of P c i . Thus if P c i is composed of a unique atom, so is H i which thus forms a singlepiece. Otherwise, P c i is a single-piece from more than one atom; each atom a of P c i contains a variable x such that P u (x) contains an existential variable y which comes from the subset of H unified by u with P c i . Thus the corresponding atom u

At the end of the sequence,

.n (u n (. . . u j (body(R j )))) and the terms of P n• u are the same as the terms of P h u . Since P n• u is a subpart of P h u , we can say that P n• u is finer than P h u so, there is a substitution s such that

Let h be the substitution obtained by making the union of the inverses of the h i , then h(u

Then we can prove that for all j, 1 ≤ j ≤ n, h(s(u n (. . . u j (body(R j ))))) = u(body(R)). Indeed, u n (. . . u j (body(R j ))) = u n (. . . u 1 (body(R j ))) since the terms of body(R j ) do not appear in u i (i < j).

To conclude the proof, we have h(s(Q n )) ⊆ u(body(R))∪u(Q\Q

Theorem 17 Given a BCQ Q and a set of rules R, the set of rewritings of Q obtained by considering exclusively most general single-piece unifiers is sound and complete.

Proof: Soundness holds trivially since a single-piece unifier is a piece-unifier. For completeness, thanks to Theorem 12, we just have to show by induction on k, the length of the rewriting sequence leading from Q to a k-piece-rewriting of Q, that: for any k-piece-rewriting Q r of Q, there exists Q s a piece-rewriting of Q obtained by using exclusively most general single-piece unifiers such that Q s ≥ Q r . For k = 0 the property is trivially satisfied. For k ≥ 1, one has Q r = β(Q r , R, µ), with Q r being a piece-rewriting of Q obtained by a piece-rewriting sequence of length k -1. By induction hypothesis, there exists Q s a piece-rewriting of Q obtained by using exclusively single-piece unifiers such that Q s ≥ Q r . By Lemma 15, either Q s ≥ Q r , or there is a piece-unifier µ of Q s with R such that β(Q s , R, µ ) ≥ Q r . In this latter case, thanks to Property 24, there is a sequence of rewritings of Q s with R using only single-piece unifiers and leading to a CQ Q s such that Q s ≥ β(Q s , R, µ ).