On Bounded Positive Existential Rules Michel Leclère, Marie-Laure Mugnier, and Federico Ulliana University of Montpellier, LIRMM, Inria Abstract. We consider the existential rule framework, which generalizes Horn description logics. We study and compare several boundedness notions in this framework. Our main result states that (strongly-) bounded rules are exactly those at the intersection of two well-known abstract classes of existential rules, namely fes (finite expansion sets, which ensure the finiteness of the core chase) and fus (finite unification sets, which correspond to UCQ-rewritable rules). 1 Introduction Existential rules [6, 12, 21] are a fragment of first-order logic generalizing most onto- logical languages studied in ontology-mediated query answering (OMQA), in particular Horn description logics [13, 22, 23]. In the OMQA setting, databases (or fact bases) are added with an ontological layer, which allows to deduce new facts from incomplete datasources, thereby enriching answers to database queries. As OMQA can be directly implemented on top of relational database systems, many research efforts have been devoted to make the paradigm efficient. At the core of the techniques developed for existential rules, and to some extent for Horn description log- ics, we find the two classical paradigms for processing rules, namely forward chaining and backward chaining. In the OMQA setting, both approaches are recast as ways of reducing the problem to a classical database query answering problem, by embedding the rules into the facts or into the query. Forward chaining is decomposed into a mate- rialization step (applying the rules to the data, hence materializing inferences into the data) followed by the evaluation of the query against the enriched database. Backward chaining is decomposed into a query rewriting step (rewriting the query using the rules) followed by the evaluation of the rewritten query against the database, thereby leaving the data untouched. Both approaches rely on a fixpoint operator to cope with rule semantics. Indeed, materialization should continue until the point where only redundant facts are added to the dataset, while rewriting should continue until the point where only redundant queries are added to the rewriting set. It is understood that both processes may not terminate since entailment with existential rules is undecidable (e.g., [14]). Deciding halting of these processes is undecidable as well [17, 5]. Following the terminology introduced in [5], we say that a set of existential rules is a finite expansion set (fes) if it ensures that a finite sound and complete materialization can be computed for any fact base, and a finite unification set (fus) if it ensures that any conjunctive query can be rewritten into a finite sound and complete set of conjunctive queries (such a set being seen as a union of conjunctive queries). As concrete examples of fes rules, one can 2 Michel Leclère, Marie-Laure Mugnier, and Federico Ulliana cite (plain) datalog [1] and sets of rules satisfying various acyclicity conditions [16, 2]. Some prominent classes of fus rules are linear rules (which generalize some DL- Lite dialects [13, 12]), sticky rules [10] and more generally rules with the “backward shyness” property [25]. Note that [5] defines a third property ensuring decidability of OMQA, namely bounded-treewidth sets (which contains EL [23] and the family of guarded rules [9, 7]), however this class is out of the scope of this paper. To fes (resp. fus) rules is naturally associated a finite breadth-first materialization (resp. query rewriting) process, whose maximal number of steps generally depends not only on the set of rules but also on the data (resp. on the input query). In contrast, bounded rules are exactly those rules that can be evaluated without a fixpoint operator. A set of rules is said to be bounded if breadth-first materialization computes all conse- quences from a knowledge base (composed of a fact base and the rules) in a predefined number of steps k. More precisely, there is k independent from any fact base, such that the materialization of any fact base at step k 0 > k is equivalent to that obtained at step k. As relational database systems may lack a fixpoint operator (see for example MySQL), bounded rules form an interesting intersection point between databases and ontologies, because they can be seamlessly evaluated on any relational system, which is not the case in general. The goal of this work is to further investigate the properties of bounded existential rules, in particular the precise relationships between fes, fus and bounded sets of rules. Our contributions are more precisely the following: 1. We first define a breadth-first query rewriting technique which is precisely the dual of breadth-first materialization. Let K = (F, R) be any knowledge base, where F is a fact base and R a set of existential rules, and let q be a (Boolean) conjunctive query. From earlier work on existential rules, we know that K entails q iff there is k (depending on R and F ) such that F k , the saturation of F at step k, entails q (e.g., [11, 4]); equivalently, K entails q iff there is k 0 (depending on R and q) such that F entails Qk0 , the set of rewritings of q obtained at step k 0 (see [20, 18] for practical algorithms). We define a variant of the breadth-first query rewriting technique from [20] that fulfills the following property: for any i ≥ 0, F i entails q iff F entails Qi (Theorem 1), hence k = k 0 in the above sentence. 2. We point out that boundedness can also be defined in terms of query rewriting instead of materialization, and using Theorem 1, we obtain the same bound for both definitions: for any k, it holds that F k is equivalent to F k+1 for all F iff it holds that Qk is equivalent to Qk+1 for all q (Theorem 2). We also show that the notion of “bounded-depth derivation property” introduced in [12] is equivalent to fus, and define variants of this property corresponding to fes and boundedness respectively. 3. By definition, every bounded set of rules is both fes and fus. The question of whether the reciprocal statement holds was open. We show that, indeed, bounded rules are exactly those at the intersection of fes and fus (Theorem 3). On Bounded Positive Existential Rules 3 2 Preliminaries We consider a first-order setting with constants but no other function symbols. A term is either a constant or a variable. In the examples we will denote constants by letters at the beginning of the alphabet (a, b, ...,) and variables by letters at the end of the alphabet (v, w, x, y, z). An atom is of the form p(t1 , . . . , tk ) where p is a predicate of arity k and the ti are terms. Given an atom or set of atoms A, vars(A), consts(A) and terms(A) denote its set of variables, constants and terms, respectively. We denote by |= the classical logical consequence and by ≡ the logical equivalence. Given two sets of atoms A and A0 , a homomorphism h from A to A0 is a substitution of vars(A) by terms(A0 ) such that h(A) ⊆ A0 . If there is a homomorphism h from A to A0 , we say that A maps to A0 (by h), which is also denoted by A ≥ A0 . It is convenient to extend any substitution s to unchanged terms (we set s(t) = t for all considered constants and unchanged variables). A fact is an existentially closed conjunctions of atoms. We denote by F a fact base, that is a set of facts. Since a conjunction of facts is equivalent to a single fact, we also see a fact base as an existentially closed conjunction of atoms. A Boolean conjunctive query (in short CQ) is also an existentially closed conjunction of atoms. Next, fact bases and conjunctive queries will be seen as sets of atoms. The answer to a CQ q in a fact base F is true iff F |= q. It is well known that F |= q iff q ≥ F . A union of conjunctive queries (UCQ) Q = q1 ∨ q2 . . . ∨ qn is seen as a set of CQs Q = {q1 , . . . , qn }. The answer to Q in F is true iff F |= Q, i.e., F |= qi for some qi ∈ Q. An existential rule r = ∀x, y(B [x, y] → ∃z H [x, z]) is a closed formula where B is a conjunction of atoms constituting the body of the rule, H is a conjunction of atoms for the head of the rule, x and y are sets of universally quantified variables, and z is the set of existentially quantified variables of the rule. The variables in x, i.e., those shared by B and H , are called the frontier variables of the rule. In the following we will refer to a rule as a pair of sets of atoms (B , H ), interpreting their common variables as the frontier. In the examples, we will use the simplified notation B → H , for instance the rule ∀x(q(x) → ∃y (p(x, y) ∧ q(y))) will be written q(x) → p(x, y), q(y). A set of rules is denoted by R. We implicitly assume that all rules employ disjoint sets of variables. A knowledge base (KB) K = (F, R) is a pair where F is a fact base and R is a set of rules. The conjunctive query entailment problem consists in deciding for given KB K and CQ q whether K |= q (where K is seen as the first order theory associated with F ∪ R). It has long been shown that this problem is undecidable (this follows e.g., from [14]). A rule r = (B , H ) is applicable to a fact base F if there is a homomorphism h such that h(B ) ⊆ F . The application of r to F with respect to a homomorphism h is denoted by α(F, r, h) and defined as α(F, r, h) = F ∪ hsafe (H ) where hsafe is a safe extension of h to H , i.e., it substitutes existential variables from H with fresh variables (not used elsewhere). It holds that F, R |= q iff there is a fact base F 0 derived from F with rules in R, 1 such that F 0 |= q. 1 i.e., F 0 is obtained by a sequence of fact bases F (= F0 ), F1 , . . . , Fk (= F 0 ) such that, for all i > 0, Fi = α(Fi−1 , ri , h) with ri ∈ R and h a homomorphism from the body of ri to Fi−1 . 4 Michel Leclère, Marie-Laure Mugnier, and Federico Ulliana We now define fact materialization by (breadth-first) forward chaining, a useful tool, also known as saturation or (breadth-first) chase. 2 The one-step saturation of F with R, denoted by α(F, R), is defined as α(F, R) = F ∪(r,h) hsafe (H) for all r = (B, H) ∈ R and h homomorphism from B to F . The k-saturation of F with R, denoted by αk (F, R), is inductively defined as follows: α0 (F, R) = F and, for any k > 0, αk (F, R) = α(αk−1 (F, R), R). Next, when R is fixed, we will denote the set αk (F, R) by F k . Saturation is sound and complete, i.e., for all F , R and Q, F, R |= Q iff F k |= Q for some positive integer k (see e.g., [11, 4]). A set of rules R is said to be a fes (finite expansion set) if for all fact base F there exists a positive constant k such that F k |= F k+1 (hence F k ≡ F k+1 ) [6]. Note that k generally depends on F . It follows that when R is fes, the saturation process is finite, hence it can be used to decide if F, R |= Q. The following example illustrate the fes property. Example 1 (fes). Let K = (F, R) with F = {p(a, b)} and R = {r : p(x, y) → p(y, z), p(z, y)}. Then F 0 = F , F 1 = F ∪ {p(b, z0 ), p(z0 , b)}, F 2 = F 1 ∪ {p(z0 , z1 ), p(z1 , z0 ) , p(b, z2 ), p(z2 , b) , p(b, z00 ), p(z00 , b)} (the rule applications corresponding to homomorphisms already found at the preceding step are written in gray font, next we will omit them). We have F 2 ≡ F 1 (note that there is no k such that F k = F k+1 , even by considering only new homomorphisms at each step, which shows the importance of checking equivalence and not only equality). Actually it holds that F 2 ≡ F 1 for any F , hence R is fes (and even bounded, see Sect. 4). Let us consider R0 = {r : p(x, y) → p(y, z)}. Then F 0 = F , F 1 = F ∪ {p(b, z0 )}, F 2 = F 1 ∪ {p(z0 , z1 ), p(b, z2 )} and so on. There is no k such that F k ≡ F k+1 , hence R0 is not fes. Backward chaining is a dual approach to deciding conjunctive query entailment, which involves rewriting the input query using the rules. The key operation is unifica- tion between (a subset of) a query and (a subset of) a rule head, which requires particular care due to the presence of existential variables in the rules. For this reason, we use the notion of a piece-unifier (introduced in [6]). Given a subquery q 0 ⊆ q, we call sepa- rating variables of q 0 the variables occurring in both q 0 and (q \ q 0 ); the other variables from q 0 are called non-separating. The definition of piece-unifier below ensures that, q 0 being the unified part of q, only non-separating variables from q 0 can be unified with an existential variable of the rule. Definition 1 (Piece Unifier) Let q be a query and r = (B , H ) a rule. A piece-unifier of q with r is a triple µ = (q 0 , H 0 , u) where q 0 6= ∅, q 0 ⊆ q, H 0 ⊆ H , and u is a substitution of T = terms(q 0 ∪ H 0 ) by T such that (i) u(q 0 ) = u(H 0 ) and (ii) for all existential variable x ∈ vars(H 0 ) and t ∈ T , with t 6= x, if u(x) = u(t), then t is a non-separating variable from q 0 . Given a CQ q, a rule r = (B , H ) and a piece-unifier µ = (q 0 , H 0 , u) the direct rewriting of q with r and µ, denoted by β(q, r, µ), is the CQ usafe (B ) ∪ u(q \ q 0 ), where usafe is a safe extension of u to B substituting variables in vars(B ) \ vars(H 0 ) with fresh variables. 2 Several chase variants have been defined, see the last section. On Bounded Positive Existential Rules 5 Example 2 (Piece Unifier). Let r = r(x) → p(x, y) and q1 = {p(w, v), s(v)}. There is no piece-unifier of q1 with r since, with q10 = {p(w, v)}, v is a separating variable of q10 , hence cannot be unified with the existential variable y. Let q2 = {s(z), p(z, v), p(w, v), t(w)}. The triple µ = (q 0 , H 0 , u) with q 0 = {p(z, v), p(w, v)}, H 0 = {p(x, y)} and u = {x 7→ z, y 7→ v, w 7→ z} is a piece-unifier of q2 with r, which yields the direct rewriting {r(z), s(z), t(z)}. It holds that F, R |= q iff there is a rewriting q 0 of q with rules in R, 3 such that F |= q 0 . A set of rewritings Q of q (with R) is said to be sound and complete if for any F it holds that F, R |= q iff there is q 0 ∈ Q such that F |= q 0 . When Q is finite it can be seen as a UCQ, hence the previous condition can then be recast as follows: F, R |= q iff F |= Q. The set R is said to be fus (finite unification set) if for any q, there is a finite sound and complete set of rewritings of q with R [6, 20]. Similarly in spirit to saturation, one can consider breadth-first query rewriting: start- ing from the UCQ Q = {q}, at each step we compute all the direct rewritings of CQs in the current UCQ. Formally: the one-step rewriting of a UCQ Q with R is β(Q, R) = Q ∪(q,r,µ) {β(q, r, µ)} where q ∈ Q, r ∈ R and µ is a piece-unifier of q with r. Then, the (breadth-first) k-rewriting of Q with R, denoted by βk (Q, R), is inductively defined as follows: β0 (Q, R) = Q, and for all k > 0, βk (Q, R) = β(βk−1 (Q, R), R). It holds that F, R |= q iff F |= βk ({q}, R) for some positive integer k (follows from [4]). This property yields an alternative characterization of fus: a set of rules is fus iff for all q, there is k such that βk ({q}, R) ≡ βk+1 ({q}, R). 4 Example 3 (fus). Let r = p(x, y), p(y, z) → p(z, t). Let q 0 = {p(v, a)}, where a is a constant: since t is an existential variable, there is no piece-unifier of q 0 with r. Let q 00 = {p(a, v)}. β1 ({q 00 }, {r}) = {q 00 } ∪ {{p(x0 , y0 ), p(y0 , a)}}; β2 ({q 00 }, {r}) = β1 ({q 00 }, {r}) ∪ {{p(x00 , y00 ), p(y00 , a)}}, where the last CQ corre- sponds to the piece-unifier already found in the preceding step. Hence, β2 ({q 00 }, {r}) = β1 ({q 00 }, {r}) if we restrict the computation to new piece-unifiers. Finally, let q = {p(v, w)}. β1 ({q}, {r}) = {q} ∪ {q1 = {p(x0 , y0 ), p(y0 , v)}}. β2 ({q}, {r}) = β1 ({q}, {r}) ∪ {{p(x1 , y1 ), p(y1 , y0 ), p(x0 , y0 )}} (we consider only new piece-unifiers). Since existential variables can only be unified with non-separating variables, there is only one new piece-unifier ({p(x0 , v)}, {p(z, t)}, {z 7→ y0 , t 7→ v}), which yields q1 . β3 ({q}, {r}) = β2 ({q}, {r}) ∪ {{p(x2 , y2 ), p(y2 , y1 ), p(x1 , y1 )}}, where the new the piece-unifier is ({p(x0 , y0 ), p(y1 , y0 )}, {p(z, t)}, {z 7→ y1 , x0 7→ y1 , t 7→ y0 }). And so on. There is no k such that βk = βk+1 (up to bijective variable renaming), however any UCQ βi is equivalent to q. As these examples suggest it, {r} is indeed fus. 3 i.e., q 0 is obtained by a sequence of direct rewritings q(= q0 ), q1 , . . . , qk (= q 0 ) such that, for all i > 0, qi = β(qi−1 , ri , µ) with ri ∈ R and µ a piece-unifier of qi−1 with ri . 4 The breadth-first rewriting algorithm in [20] builds β(βi (Q, R), R) by considering only queries that are not contained in a query from βi (Q, R); in this case the fus condition be- comes: there is k such that βk+1 (Q, R) = βk (Q, R). 6 Michel Leclère, Marie-Laure Mugnier, and Federico Ulliana Note that there is k such that F |= βk ({q}, R) if and only if there is k 0 such that k0 α (F, R) |= q. However, the above breadth-first rewriting is not exactly the dual of breadth-first saturation, in the sense that α(F, R) |= q does not imply F |= β({q}, R). In other words, a single step of breadth-first rewriting is not able to “simulate” a step of saturation. Let us illustrate this observation with a simple example. Example 4 (Saturation vs rewriting step). Let K = (F, R) with F = {p0 (a), q0 (a)} and R = {rp : p0 (x) → p1 (x); rq : q0 (x) → q1 (x)}. Let q = {p1 (u), q1 (u)}. A single saturation step α(F, R) = {p0 (a), q0 (a), p1 (a), q1 (a)} allows to entail q. However, a single rewriting step β1 ({q}, R) = {{p1 (u), q1 (u)}, {p0 (u), q1 (u)}, {p1 (u), q0 (u)}} does not allow to prove that K |= q, i.e., F 6|= β1 ({q}, R). The trouble is that each direct rewriting is performed with respect to a single rule, hence the desired CQ {p0 (u), q0 (u)}, which requires to rewrite q with both rp and rq , is obtained only at the second rewriting step (from {p0 (u), q1 (u)} or from {p1 (u), q0 (u)}). 3 A New Breadth-First Query Rewriting In order to obtain the precise dual of saturation, we define another breadth-first rewrit- ing mechanism able to unify a CQ with several rules from R at once. Instead of a piece-unifier, we consider an “aggregated unifier” (as introduced in [19] for algorithmic purposes), which aggregates several piece-unifiers of a CQ with rules from R, pro- vided that these piece-unifers are compatible (briefly, they involve disjoint subsets of the query and unify common variables in a way that does not lead to unify different con- stants together). To avoid technical developments, we will consider here an alternative way of defining exactly the same kind of rewriting by modifying the set of rules instead of the unifier (this alternative definition is not practically relevant but it is suitable for our study). Let R0 = {r1 , . . . , rl } be a set of rules with each ri = (Bi , Hi ). We recall that distinct rules have disjoint sets of variables. The aggregated rule assigned to R0 , denoted by r1  . . .  rl , is defined as B1 ∧ . . . ∧ Bl → H1 ∧ . . . Hl . Let R be the (infinite) set of aggregated rules assigned to multisubsets of R (i.e., an aggregated rule may involve several “copies” of the same rule from R, with a safe renaming of variables in each copy). Then, for any UCQ Q, β  (Q, R) = Q ∪(q,r,µ) {β(q, r, µ)}, where q ∈ Q, r = r1  . . .  rl ∈ R with l ≤ |q|, and µ is a piece-unifier of q with r. We denote by βk (Q, R) the associated breadth-first k-rewriting. 5 Example 5. Consider again Ex. 4. We have β1 ({q}, R) = β1 ({q}, R)∪{{p0 (u), q0 (u)}}, where the additional query is obtained by unifying q with the aggregated rule r1  r2 = p0 (x0 ), q0 (x1 ) → p1 (x0 ), q1 (x1 ). We now prove that the new breadth-first rewriting fulfills the desired properties. Lemma 1 For all F, R and q, it holds that α(F, R)|= q iff F |=β  ({q}, R). 5 We could state β  (Q, R) = β(Q, R ), however it must be clear that, for each CQ, only a finite subset of R needs to be considered. On Bounded Positive Existential Rules 7 Proof:(Sketch) (⇒) Let F 1 = α(F, R). As F 1 |= q there is h such that h(q) ⊆ F 1 . Let q0 be the largest subset of q such that h(q0 ) ⊆ F and {q1 , . . . , ql } be the partition of q \ q0 such that each qi (0 < i ≤ l) maps to the atoms produced by the application of a rule ri = (Bi , Hi ) ∈ R to F with a homomorphism hi , i.e., h(qi ) ⊆ hsafe i (Hi ) 0 (and F ∪ hsafe 1 (H 1 ) ∪ . . . ∪ hsafe l (H l ) ⊆ F 1 ). For each i > 0, let H i ⊆ H i denote the 0  useful part of Hi , i.e., h(qi ) = hsafe i (H i ). If q 0 = q, i.e., F |= q, then F |= β ({q}, R) since q ∈ β  ({q}, R). Otherwise, let r = r1  . . .  rl and µ be the piece-unifier of q with r naturally associated with the homomorphisms h and h1 ∪ . . . ∪ hl (i.e., µ = (q1 ∪ . . . ∪ ql , H10 ∪ . . . ∪ Hl0 , u) where for all terms e and e0 in the domain of u, u(e) = u(e0 ) iff (h ∪ hsafe 1 ∪ . . . ∪ hsafe l )(e) = (h ∪ hsafe 1 ∪ . . . ∪ hsafe l )(e0 )). We    easily check that F |= β(q, r , µ). Since β(q, r , µ) ∈ β ({q}, R), we obtain that F |= β  ({q}, R). (⇐) If F |= q then α(F, R) |= q. Otherwise, we know there is q1 6= q in β1 ({q}, R) s.t. F |= q1 where q1 is obtained by rewriting q 0 ⊆ q with an aggregated rule r = r1  . . .  rl and a piece-unifier (q 0 , H10 ∪ . . . ∪ Hl0 , u). Let h0 be a homomorphism from q1 to F . For each ri = (Bi , Hi ) composing r , h0 ◦ usafe is a homomorphism from Bi to F . Hence, (h0 ◦ u)safe (Hi ) ⊆ α(F, R). We build the following homomorphism h from q to α(F, R): for all x ∈ vars(q), if x ∈ vars(q) \ vars(q 0 ) then h(x) = h0 (x), otherwise, let any e ∈ Hi0 such that u(x) = u(e), then h(x) = (h0 ◦ usafe )safe (e).  Theorem 1. For all F, q, R and k ≥ 0, it holds that αk (F, R)|= q iff F |=βk ({q}, R) Proof: The proof is by induction on k. For k = 0, the property is trivially true. As- sume the property holds for any k < n. First note that, for any i ≥ 1, αi (F, R) = αi−1 (α(F, R), R) and βi ({q}, R) = βi−1  (β  ({q}, R), R), which directly follows n from the definitions. We have α (F, R)|= q iff αn−1 (α(F, R), R)|= q iff  α(F, R)|=βn−1 ({q}, R) (by induction hypothesis) iff   F |=β (βn−1 ({q}, R), R) (by Lemma 1) iff F |=βn ({q}, R). Hence, αk (F, R)|= q iff F |=βk ({q}, R) holds for any k ≥ 0.  This correspondence between αk and βk allows us to rely on the soundness and completeness of breadth-first forward chaining to establish the soundness and com- pleteness of breadth-first rewriting: Corollary 1. It holds that F, R |= q iff F |= βk ({q}, R) for some positive integer k. Breadth-first rewriting yields an alternative definition of fus. Proposition 1 A set of rules R is fus iff for all query q there is a positive constant k such that βk ({q}, R) ≡ βk+1  ({q}, R). From now on, for a UCQ Q and a fixed set of rules R, we will denote the set βk (Q, R) simply by Qk . 8 Michel Leclère, Marie-Laure Mugnier, and Federico Ulliana 4 Several Notions of Boundedness We now define bounded rules and clarify their relationships with other properties found in the literature. Two meaningful notions of boundedness can be provided, with the bound being based on fact saturation or on query rewriting. Definition 2 A set of existential rules R is (saturation-bounded) if there exists k ∈ N such that for all F , F k ≡ F k+1 . (rewriting-bounded) if there exists k ∈ N such that for all Q, Qk ≡ Qk+1 . We first show that these two notions precisely coincide. Theorem 2. Any set of existential rules R is saturation-bounded iff it is rewriting- bounded. Moreover, the bound is the same, i.e., for all F and all Q, for all k, F k ≡ F k+1 iff Qk ≡ Qk+1 . Proof: (⇒) Assume that R is saturation-bounded and let k be the bound. Then for all Q and F it holds that F, R |= Q iff F k |= Q. Let q be any query in Qk+1 . Since q |= Qk+1 , by soundness of rewriting, it holds that q, R |= Q; since R is saturation- bounded, {q}k |= Q hence, by Th. 1, q |= Qk . Since this holds for any query q ∈ Qk+1 , we have Qk+1 |= Qk . Furthermore, by definition, Qk |= Qk+1 . Thus Qk ≡ Qk+1 . (⇐) Assume that R is rewriting-bounded and let k be the bound. Then for all Q and F it holds that F, R |= Q iff F |= Qk . By soundness of forward chaining, it holds that F, R |= F k+1 ; since R is rewriting-bounded, F |= (F k+1 )k hence, by Th. 1, F k |= F k+1 . Furthermore, by definition, F k+1 |= F k . Thus F k ≡ F k+1 .  In light of this, next we will simply say bounded rules. In [12], Calı̀ et al. introduced the notion of bounded-depth derivation property for existential rules, for which the number of saturation steps is bounded for all query (in short, Q-BDDP). We define the analogous of the bounded-depth derivation property for facts (F-BDDP), as well as a natural property issued from both from (Q-BDDP) and (F-BDDP), we call strong bounded-depth derivation property (strong BDDP). We show that these three properties coincide with the classes fus, fes and bounded. Definition 3 (Bounded-Derivation Properties) Let R be a set of existential rules. Then, R enjoys the property (F-BDD) if for all F there is k ∈ N such that for all Q: F, R |= Q iff F k |= Q (Q-BDD) if for all Q there is k ∈ N such that for all F : F, R |= Q iff F k |= Q (strong BDD) if there is k ∈ N such that for all F and Q: F, R |= Q iff F k |= Q. We now show that these notions respectively correspond to fes, fus and boundedness. 6 Proposition 2 Any set of existential rules is fes iff it has the F-BDD Property. 6 The three following propositions were first proven by J.-F. Baget and M.-L. Mugnier and presented in a seminar at Oxford University in December 2012. On Bounded Positive Existential Rules 9 Proof: (⇒) Let R be fes: for all F , there is k such that F k ≡ F k+1 . By soundness and completeness of forward chaining, for any Q we have F, R |= Q iff there is n such that F n |= Q. For any F and such n, it holds that F k |= F n . Hence, F k |= Q. (⇐) Assume R has the F-BDD Property and set Q = {F k+1 } (where k is the bound of the F-BDD Property). We thus have F, R |= F k+1 iff F k |= F k+1 . Forward chaining is sound, so F, R |= F k+1 . Hence F k |= F k+1 . By definition, F k+1 |= F k . Therefore, F k ≡ F k+1 .  Proposition 3 Any set of existential rules is fus iff it has the Q-BDD Property. Proof: (⇒) Let R be fus: for all Q, there is k such that Qk ≡ Qk+1 . By soundness and completeness of breadth-first rewriting (Corollary 1), for any F , we have F, R |= Q iff F |= Qk . Equivalently, by Th. 1, F k |= Q. (⇐) Assume R has the Q-BDD Property. For any q ∈ Qk+1 (where k is the bound of the Q-BDD Property), let us set F = q: we have q, R |= Q iff (q)k |= Q. Breadth-first rewriting is sound, so q, R |= Q. Hence q |= Qk . Since this holds for any q ∈ Qk+1 , we have Qk+1 |= Qk . Since Qk is included in Qk+1 , we also have Qk |= Qk+1 . Therefore, Qk ≡ Qk+1 .  Proposition 4 Any set of existential rules is bounded iff it has the strong BDD Property. Proof: The proof goes like that of Prop. 2. (⇒) Let R be saturation-bounded and let k such that for all F , F k ≡ F k+1 . By soundness and completeness of forward chaining, for any F and Q, we have F, R |= Q iff F k |= Q. (⇐) Assume R has the strong BDD Property and set Q = {F k+1 } (where k is the bound of the strong BDD Property). We thus have F, R |= F k+1 iff F k |= F k+1 . Forward chaining is sound, so F, R |= F k+1 . Hence F k |= F k+1 . By definition, F k+1 |= F k . Therefore, F k ≡ F k+1 .  5 Boundedness = fes ∩ fus We now prove that bounded rules are exactly those at the intersection of fes and fus classes. Theorem 3. R is fes and fus iff R is bounded. One direction of the proof (⇐) is straightforward, and follows by Prop.s 2 and 3, simply picking the k of the bound. We dedicate the remaining of this section to the formal development of the other direction. We first consider the set of all objects of the form (B̄ , H̄ ) where B̄ is a rewriting of a rule body in R and H̄ is the saturation of B̄ with R. When R is fes, such objects correspond to rules (i.e., each H̄ can be made finite). When moreover R is fus, the set of all rewritings to be considered is finite, hence the set of all rules of interest is finite. Definition 4 (Rule Completion) Let R = {r1 , . . . , rn } be a fes and fus set of rules of the form ri = (Bi , Hi ). We define the set CR as follows: 10 Michel Leclère, Marie-Laure Mugnier, and Federico Ulliana 1. For any ri = (Bi , Hi ), let ki be the smallest integer such that βki (Bi , R) ≡ βki +1 (Bi , R) (such a ki exists since R is fus). 2. For any qij ∈ βki (Bi , R), let kij be the smallest integer such that αkij (qij , R) ≡ αkij +1 (qij , R) (such a kij exists since R is fes). 3. Then: CR = {(B̄ , H̄ ) | ri = (Bi , Hi ) ∈ R, B̄ ∈ βki (Bi , R), H̄ = αkij (B̄ , R) } The bound associated with R is dR = maxri ∈R,qij ∈βk (Bi ,R) (kij ). i Note that CR is finite and unique (up to bijective variable renaming). Most impor- tantly, its size depends solely on R. Proposition 5 For any fes and fus set of rules R, it holds that CR ≡ R. Proof: The direction CR |= R holds since, for each rule ri = (Bi , Hi ) ∈ R, Bi ∈ βki (Bi , R), hence there is a rule r̄ = (B̄ , H̄ ) ∈ CR with Bi = B̄ and Hi ⊆ H̄ . Direction R |=CR follows from the soundness and completeness of saturation. Indeed, for each rule (B̄ , H̄ ) ∈ CR , let (B̄ 0 , H̄ 0 ) be obtained by replacing each frontier variable with a distinct fresh constant (i.e., that does not occur in R). By definition of CR , we have B̄ 0 , R |= H̄ 0 , and equivalently R |= B̄ → H̄ .  We now show that each saturation step with CR can be computed by a bounded number of saturation steps with R (again with a bound independent from any fact base, Prop. 6). Next, we will show that a single saturation step with CR is actually sufficient to saturate any fact base (Prop. 7), therefore it is equivalent to a bounded number of saturation steps with R. Proposition 6 Let R be fes and fus and CR be the associated completion set. Then: for any fact base F , αdR (F, R) |= α(F, CR ) (where dR is the bound introduced in Def. 4). Proof: (Sketch) Let F 0 = αdR (F, R). We show that for each rule r̄ = (B̄ , H̄ ) ∈ CR and each homomorphism h from B̄ to F , F 0 |= α(F, r̄, h) holds, which suffices to prove that F 0 |= α(F, CR ) since all rules are applied “in parallel” in a single saturation step. Consider the sequence S of rule applications leading from B̄ to H̄ . The choice of dR implies that αdR (B̄ , R) ≡ H̄ . Let h from B̄ to F . The sequence S can be applied “similarly” to F (i.e., each homomorphism hi associated with a rule application is replaced by h◦hi ), yielding S(F ) with S(F ) |= h(H̄ ). Since H̄ is obtained in at most dR breadth-first steps, this is also true for S(F ), hence F 0 |= S(F ). Since F ⊆ F 0 , we obtain F 0 |= F ∪ hsafe (H̄ ) = α(F, r̄, h).  Proposition 7 Let R be a set of rules both fes and fus. For any fact base F , it holds that α(F, CR ) ≡ αk (F, CR ) for all k≥1. Proof: (Sketch) We focus on proving that α(F, CR ) |= α(α(F, CR ), R) which suffices to derive the thesis. Indeed, we know that for any F 0 and R0 if F 0 |= α(F 0 , R0 ) then On Bounded Positive Existential Rules 11 F 0 |= αk (F 0 , R0 ), for all k ∈ N. Hence α(F, CR ) ≡ αk (α(F, CR ), R), in particular for k = dR . Moreover, as R is both fes and fus by Prop. 6 we have that α(F, CR ) |= α(α(F, CR ), CR ). Let r = (B , H ) be any rule of R. If r is applicable to α(F, CR ) with a homomor- phism h, then h(B ) ⊆ α(F, CR ). By Prop. 6 we thus have αdR (F, R) |= h(B ). By Th. 1, we get that F |= βdR ({h(B )}, R), so there exists h(B )rew ∈ βdR ({h(B )}, R) such that F |= h(B )rew . Any rewriting sequence from h(B) to h(B )rew can be per- formed “similarly” from B yielding Brew ∈ βdR ({B }, R) with Brew ≥ h(B )rew . Besides, by definition of CR , we know there exists r̄ = (B̄ , H̄ ) ∈ CR with B̄ = Brew and H̄ ≡ αdR (Brew , R). We show that any derivation sequence from B̄ to H̄ can be applied to h(B )rew to entail h(B ). Since r = (B , H ) ∈ R and this sequence is applied until saturation, h(H ) is also entailed. We conclude that α(F, CR ) |= h(H ).  Proof: [Proof of Th. 3] We now prove that if R is fes and fus then it is bounded. For any fact base F and any CQ q, F, R |= q iff F, CR |= q (Prop. 5). From Prop. 7, F, CR |= q iff α(F, CR ) |= q. Hence, F, R |= q iff α(F, CR ) |= q. It remains to show that there is k independent from F and q such that αk (F, R) ≡ α(F, CR ). From Prop. 6, we have a constant k (k = dR ) independent from F and q such that αk (F, R) |= α(F, CR ); moreover, since F, R |= αk (F, R) for any k, we have α(F, CR ) |= αk (F, R). We conclude that R is bounded.  6 Concluding Remarks In this paper, we provide several results that clarify the relationships between funda- mental properties of existential rule sets, namely fes, fus and boundedness. The main result is that bounded rule sets are exactly those that are both fes and fus. Recognizing if a set of rules is bounded is a difficult problem, which is already un- decidable for plain datalog [1], hence for many fes classes of existential rules. A signif- icant exception are monadic datalog programs, for which boundedness is recognizable [15]. An open question is whether boundedness is recognizable for specific classes of existential rules, in particular those known to be fus. Whether restricting predicate arity to two could have an impact on the problem decidability is also an interesting issue. Besides, the halting condition for the saturation process considered here relies on logical equivalence (i.e., F k ≡ F k+1 ). This condition corresponds exactly to the halt- ing of the chase variant known as the core chase [17]. Other chase variants have been proposed in the literature, in particular the restricted chase [8], the skolem chase [24] and the oblivious chase [9], which are known to halt in (increasingly) fewer cases (see, e.g., [3] for examples illustrating the differences between these mechanisms). With each of these variants could be associated a different boundedness notion. Note however that all the chase variants collapse on rules without existential variables (i.e., plain datalog), hence the undecidability of boundedness recognition in plain datalog applies to all these potential variants of boundedness. Acknowledgments. This work was partially supported by project PAGODA (ANR-12- JS02-007-01). 12 Michel Leclère, Marie-Laure Mugnier, and Federico Ulliana References 1. Abiteboul, S., Hull, R., Vianu, V. (eds.): Foundations of Databases: The Logical Level. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1st edn. (1995) 2. Baget, J., Garreau, F., Mugnier, M., Rocher, S.: Extending acyclicity notions for existential rules (long version). CoRR abs/1407.6885 (2014), http://arxiv.org/abs/1407.6885 3. Baget, J., Garreau, F., Mugnier, M., Rocher, S.: Revisiting chase termination for existential rules and their extension to nonmonotonic negation. CoRR abs/1405.1071 (2014), http: //arxiv.org/abs/1405.1071, proc. of NMR 2014 4. Baget, J.F., Leclère, M., Mugnier, M.L., Salvat, E.: On Rules with Existential Variables: Walking the Decidability Line. Artificial Intelligence 175(9-10), 1620–1654 (2011) 5. Baget, J., Leclère, M., Mugnier, M.: Walking the decidability line for rules with existential variables. In: KR 2010 (2010) 6. Baget, J., Leclère, M., Mugnier, M., Salvat, E.: Extending decidable cases for rules with existential variables. In: IJCAI 2009. pp. 677–682 (2009) 7. Baget, J., Mugnier, M., Rudolph, S., Thomazo, M.: Walking the complexity lines for gener- alized guarded existential rules. In: IJCAI 2011. pp. 712–717 (2011) 8. Beeri, C., Vardi, M.Y.: A proof procedure for data dependencies. J. ACM 31(4), 718–741 (1984) 9. Calı̀, A., Gottlob, G., Kifer, M.: Taming the infinite chase: Query answering under expressive relational constraints. In: KR’08. pp. 70–80 (2008) 10. Calı̀, A., Gottlob, G., Pieris, A.: Query answering under non-guarded rules in datalog+/-. In: RR’10. pp. 1–17 (2010) 11. Calı̀, A., Gottlob, G., Kifer, M.: Taming the infinite chase: Query answering under expressive relational constraints. J. Artif. Intell. Res. (JAIR) 48, 115–174 (2013) 12. Calı̀, A., Gottlob, G., Lukasiewicz, T.: A general datalog-based framework for tractable query answering over ontologies. In: PODS 2009. pp. 77–86 (2009) 13. Calvanese, D., Giacomo, G.D., Lembo, D., Lenzerini, M., Rosati, R.: DL-Lite: Tractable description logics for ontologies. In: AAAI. pp. 602–607 (2005) 14. Chandra, A.K., Vardi, M.Y.: The implication problem for functional and inclusion depen- dencies is undecidable. SIAM J. Comput. 14(3), 671–677 (1985) 15. Cosmadakis, S.S., Gaifman, H., Kanellakis, P.C., Vardi, M.Y.: Decidable optimization prob- lems for database logic programs (preliminary report). In: ACM Symposium on Theory of Computing. pp. 477–490 (1988) 16. Cuenca Grau, B., Horrocks, I., Krötzsch, M., Kupke, C., Magka, D., Motik, B., Wang, Z.: Acyclicity notions for existential rules and their application to query answering in ontologies. J. Art. Intell. Res. (JAIR) 47, 741–808 (2013) 17. Deutsch, A., Nash, A., Remmel, J.B.: The chase revisited. In: PODS. pp. 149–158 (2008) 18. Gottlob, G., Orsi, G., Pieris, A.: Query rewriting and optimization for ontological databases. ACM Trans. Database Syst. 39(3), 25:1–25:46 (2014) 19. König, M., Leclère, M., Mugnier, M., Thomazo, M.: On the exploration of the query rewrit- ing space with existential rules. In: Web Reasoning and Rule Systems - RR 2013. pp. 123– 137 (2013) 20. König, M., Leclère, M., Mugnier, M., Thomazo, M.: Sound, complete and minimal ucq- rewriting for existential rules. Semantic Web 6(5), 451–475 (2015) 21. Krötzsch, M., Rudolph, S.: Extending decidable existential rules by joining acyclicity and guardedness. In: Proc. of IJCAI. pp. 963–968 (2011) 22. Krötzsch, M., Rudolph, S., Hitzler, P.: Complexity boundaries for Horn description logics. In: Proc. of AAAI. pp. 452–457. AAAI Press (2007) On Bounded Positive Existential Rules 13 23. Lutz, C., Toman, D., Wolter, F.: Conjunctive query answering in the description logic EL using a relational database system. In: Proc. of IJCAI. pp. 2070–2075 (2009) 24. Marnette, B.: Generalized schema-mappings: from termination to tractability. In: PODS. pp. 13–22 (2009) 25. Thomazo, M.: Conjunctive Query Answering Under Existential Rules - Decidability, Com- plexity, and Algorithms. Ph.D. thesis, Université Montpellier II (2013), https://tel. archives-ouvertes.fr/tel-00925722