The chase procedure is an indispensable tool for several database applications, where its termination guarantees decidability of these tasks. Most previous studies have focused on the skolem chase variant and its termination. It is known that the standard chase variant is more powerful in termination analysis provided a database is given. But all-instance termination analysis presents a challenge, since the critical database and similar techniques do not work. The interest of this paper is on the following question: How to devise a framework in which various known decidable classes of finite skolem chase can all be properly extended by the technique of standard chase? To address this question, we develop a novel technique to characterize the activeness of all possible cycles of a certain length in the standard chase procedure, which leads to the formulation of a parameterized class called k-SAFE(cycle), which guarantees all-instance, allpath termination, where the parameter takes a cycle function by which a concrete class of finite standard chase is instantiated. The approach applies to any class of finite skolem chase that is identified with a condition of acyclicity. More generally, we show how to extend the hierarchy of bounded rule sets under skolem chase without increasing the complexity of data and combined reasoning tasks.
The advent of emerging applications of knowledge representation and ontological reasoning have been the motivation of recent studies on existential rule languages, known as tuple-generating dependencies (TGDs [1], also called rules) or Datalog ± [2], which have been considered a powerful modeling language for applications in data exchange, data integration, ontological querying, and so on. A major advantage of this approach is that the formal semantics based on first-order logic facilitates reasoning in an application, where answering conjunctive queries over a database extended with a set of existential rules is a primary task, but unfortunately an undecidable one in general [3]. Chase procedure is a bottom-up algorithm that extends a given database by applying specified rules. If such a procedure terminates, given an input database D, a finite rule set Σ and a conjunctive query, we can answer the query against Σ and D by deciding whether the result of chase based on Σ and D entails the query.
Four variants of chase procedure have been considered in the literature, which are called oblivious, semi-oblivious (skolem), standard (aka restricted) and core chase. With oblivious chase being a weaker version of skolem chase and core chase as a parallel, wrapping procedure of standard chase (which indeed captures all universal models), the main interests have been on skolem [4] and standard chase [5]. In particular, given a rule set and a database, we know that whenever skolem chase terminates so does the standard chase, but the reverse does not hold in general. Thus, standard chase is more powerful in termination analysis.
In spite of existence of many notions of acyclicity in the literature, (cf. [6] for a comprehensive survey), there are natural examples from the real world ontologies that do not belong to any known class, but with terminating standard chase. However, finding any characterization to assure standard chase termination is a very challenging task, and in the last decade, to the best of our knowledge only one condition has been found [7], originally in the context of description logics. As shown in [8], the problem of checking all-instance termination of standard chase is not a recursively enumerable problem (i.e. in general, the set of all-instance terminating standard chase TGDs is not enumerable). The tools developed in this paper are the first of its kind to provide an effective enumeration algorithm to characterize all-instance terminating standard chase TGDs.
In this work, we provide a highly general theoretical framework to identify strict superclasses of all existing classes of finite chase that we are aware of.
The main contributions of this paper are as follows:
1. We introduce a novel characterization of derivations under standard chase. We show that, although there is no unique database for termination analysis under standard chase, there exist a collection of "critical databases" by which the non-termination behavior of a derivation sequence can be captured. This is shown in Theorem 1. 2. We define a hierarchy of decidable classes of finite standard chase, called k-SAFE(cycle), which, when given a definition of cycle, is instantiated to a concrete class of finite chase. This is achieved by our Theorem 3 based on which various acyclicity conditions under skolem chase can be generalized to introduce classes of finite chase beyond finite skolem chase. 3. We show that the entire hierarchy of δ-bounded rule sets under skolem chase [9] can be generalized by introducing δ-bounded sets under standard chase, and as shown in Theorem 8, this extension does not increase the reasoning complexity under skolem chase.
We assume the following pairwise disjoint sets of symbols: Const a countably infinite set of constants, N a countably infinite set of (labeled) nulls, and V a countably infinite set of variables. A schema is a finite set R of relation (or predicate) symbols, where each R ∈ R is assigned a positive integer as its arity which is denoted by arity(R). Let Dom = Const ∪ N. Terms are symbols in Dom ∪ V. Ground terms are terms involving no variables. An atom is an expression of the form R(t), where t ∈ (Const ∪ V) arity(R) and R is a predicate symbol from R. A general instance (or simply an instance) I is a set of atoms over the relational schema R; term(I) denotes the set of terms occurring in I. A database is a finite instance I where terms are constants from Const. Given two instances I and J over the same schema, a homomorphism h : I → J is a mapping on terms which is identity on constants and for every atom R(t) of I we have that R(h(t)) (which we may write alternatively by h(R(t))) is an atom of J such that h(I) ⊆ J.
A tuple-generating dependency (also called a rule) is a first-order sentence σ of the form: φ(x, y) → ∃zψ(x, z), where x and y are sets of universally quantified variables (with the quantifier omitted) and φ and ψ are conjunctions of atoms constructed from relation symbols from R, constants from Const, and variables from x ∪ y and x ∪ z respectively. The formula φ (resp. ψ) is called the body of σ, denoted body(σ) (resp. the head of σ, denoted head(σ)).
Given a rule σ, a skolem function f σ z is introduced for each variable z ∈ z where arity(f σ z ) = |x|. Terms constructed from skolem functions and constants are called skolem terms. In this paper, we will regard skolem terms as a special class of nulls. Ground terms in this context are constants from N or skolem terms. The functional transformation of σ, denoted sk(σ), is the formula obtained from σ by replacing each occurrence of z i ∈ z with f σ zi (x). The skolemized version of a rule set Σ is the union of sk(σ) for all rules σ ∈ Σ and is denoted sk(Σ).
We use var u (σ) and var ex (σ) to refer to the sets of universal and existential variables appearing in σ, and var(σ) refers to the set of all variables appearing in σ. We further define: a path (based on Σ) is a nonempty (finite or infinite) sequence of rules from Σ; a cycle C = (σ 1 , ..., σ n ) (n ≥ 1) is a finite path whose first and last elements coincide (i.e., σ 1 = σ n ); a k-cycle (k > 0) is a cycle in which at least one rule has k + 1 occurrences and all other rules have k + 1 or less occurrences. Given a path P , with Rules(P ), we denote the set of distinct rules used in P .
We assume all rules are standardized apart so that no variable is shared by more than one rule; given an instance I, term(I) denotes the set of all terms occurring in I; and for a set or a sequence Q, the cardinality |Q| is defined as usual.
Chase is a fixpoint construction that accepts as input a database D and a finite set Σ of rules and adds atoms to D.
This paper is concerned with the skolem and standard chase variants. Below, let D be a database and Σ a rule set over the same schema.
We define skolem chase based on a breadth-first fixpoint construction as follows: we let chase 0 sk (D, Σ) = D and, for all i > 0, let chase i sk (D, Σ) be the union of chase i−1 sk (D, Σ) and h(head(sk(σ)) for all rules σ ∈ Σ and all homomorphisms h such that h(body(σ)) ⊆ chase i−1 sk (D, Σ). Then, we let chase sk (D, Σ) be the union of chase i sk (D, Σ) for all i ≥ 0. Due to order sensitive derivations, standard chase is defined over paths. In this paper, when we define a homomorphism h : I → J, if I and J are clear from the context, we may define such a homomorphism as a mapping from variables to terms. Definition 1. Let P = (σ 1 , σ 2 , ...) be a path, where σ i ∈ Σ for all i ≥ 1, and H = (h 1 , h 2 , ...) homomorphisms such that |P | = |H|. A standard chase path based on Σ, denoted chase p std (D, P, H), expresses a sequence of chase steps that satisfy the following conditions: for all i ≥ 1,
where
). We also use chase p std (D, P, H) to denote the union of D i , ∀i ≥ 0.
By abuse of notation, we may say "chase p std (D, P, H) is a standard chase path" to mean that the sequence of chase steps on the path P using H, for the given database D, constitutes a standard chase path.
We say that a rule set Σ has finite standard chase, or is terminating under standard chase, if there are only finite standard chase paths based on Σ, for all databases.
The classes of rule sets whose chase terminates on all paths (all possible derivation sequences of chase steps) independent of given databases (thus all instances) is denoted by CT ∀∀ , where ∈ {sk, std} (sk for skolem chase and std for standard chase).
In skolem chase, the applied rule σ and the related homomorphism h form a trigger (σ, h), w.r.t. the conclusion set generated so far. If such a skolem chase step is also a standard chase step, (σ, h) is called an active trigger [10].
A conjunctive query (CQ) Q is a formula of the form Q(x) := ∃yΦ(x, y), where x and y are tuples of variables; Φ(x, y) is a conjunction of atoms with variables in x ∪ y. A boolean conjunctive query (BCQ) is a CQ of the form Q().
It is well-known that, for all boolean conjunctive queries (BCQs) q, D ∪ Σ |= q (under the semantics of first-order logic) if and only if chase sk (D, Σ) |= q and if and only if ∀P,H chase p std (D, P, H) |= q [11].
To illustrate the practical relevance of the standard chase, let us consider modeling a secure communication protocol where two different signal types can be transmitted: type A (or inter-zone) and type B (intra-zone). Let us consider a scenario where a transmitter from one zone requests to establish a secure communication with a receiver from another zone in this network. There are an unknown number of trusted servers. Before a successful communication between two users can occur, following a handshake protocol, the transmitter must send a type A signal to a trusted server in the same zone and receive an acknowledgment back. Then, that trusted server sends a type B signal to a trusted server in the receiver zone.
Below, we use existential rules to model the described communication (the modeling here does not include the actual process of transmitting signals).
Example 1. Consider the rule set Σ 1 below, where S(x, y) denotes a request to send a type A signal from x to y and D(x, y) q request to send a type B signal from x to y. Note that u and v are trusted servers in the zone where x and y are located, respectively.
where s 1 and s 2 are function symbols. With the database D 0 = {D(t, r)}, after applying σ 1 and σ 2 , we have:
Clearly, the path (σ 1 , σ 2 ) leads to a standard chase path, but (σ 1 , σ 2 , σ 1 ) does not, since the trigger for applying the last rule in the path is not active -the head can be satisfied by already derived atoms S(s 1 (t), t) and S(t, s 1 (t)). Now let us consider another rule set Σ 2 = {r 1 , r 2 }, where,
With the same input database D 0 , we can find out that any non-empty prefix of P = (r 1 , r 2 , r 1 , r 2 , r 1 ) leads to a standard chase path except P itself. Note that P is a 2-cycle.
Since skolem chase is based on triggers and standard chase applies active triggers, standard chase provides a more powerful tool for termination analysis for a given database. However, this does not extend to the case of all-instance termination, as the critical database technique [12] for skolem chase does not apply to standard chase. Recall that a critical database is one that contains a ground atom for each relation symbol filled with exactly one fresh constant. The above example is not at all a surprise, as the complexity of membership checking in the class of rule sets that have finite standard chase, CT std ∀∀ , is coRE-complete [8], which implies that in general, there exists no effectively computable (finite) set of databases which can simulate termination w.r.t. all input databases2 . What we can do is to identify an RE subset of CT std ∀∀ , whose size can grow asymptotically and, at the same time, whose finite subsets can be checked for standard chase termination.
One natural consideration draws attention to the notion of cycles since, firstly, cycles are recursively enumerable with increasing lengths, and secondly, it is these cycles that may cause non-termination. Thus, checking cycles for safety yields an RE set, which can be extended by checking more nested cycles. However, a challenging question is which databases to be checked against. In the following, we tackle this question.
Given a path, our goal is to simulate derivations under standard chase with an arbitrary database, by derivations with a collection of databases. If this simulation captures all derivations in the path with any database, by running this simulation we can determine whether the given rule set is terminating for some finite set of pre-specified paths, for all databases.
We only need to consider the type of paths that potentially lead to cyclic applications of chase in the sense that the last rule of the path depends on the first, possibly through some intermediate ones in between. Note that σ in Example 3 depends on itself based on the classic notion of unification. So, with the aim of ruling out similar examples, we need to consider a dependency notion under which the cycle P = (σ, σ) in the above example is not identified as a dangerous cycle. For this purpose, we consider the notion of rule dependencies as introduced in [13], which is based on piece unification [14]. Condition (a) gives a sufficient condition for rule dependency, but it may be an overestimate, which is constrained by condition (b). It can be easily observed that in Example 3, condition (a) holds (for B = {T (x, y)} and H = {T (y, z)} where θ = {x/y, y/z}) but condition (b) does not (since var ex (H) = {z} and z is unified with y which occurs in B and body(σ) \ B = {P (x, y)}). Therefore, based on Def. 2, no piece unifier of body(σ) and head(σ) exists. Definition 3. Given two rules σ 1 and σ 2 , we say that σ 2 depends on σ 1 , if there is a piece unifier of body(σ 2 ) with head(σ 1 ), and we say that σ 2 depends on σ 1 w.r.t. θ, if θ is such a piece unifier. Terminology: Given a vector V = (v 1 , ..., v n ) where n ≥ 2, a projection of V preserving end points, denoted V = (v 1 , ..., v m ), is a projection of V (as defined in usual way), with the additional requirement that the end points are preserved, i.e., v 1 = v 1 and v m = v n . By abuse of terminology, V above will simply be called a projection of V . Definition 4. Let Σ be a rule set, D a database, and P a path (σ 1 , ..., σ n ) with n ≥ 2. A vector of homomorphisms H = (h 1 , ..., h n ) is called chained for P if there is a projection H = (h 1 , ..., h m ) of H and the corresponding path projection P = (σ 1 , ..., σ m ) of P such that for all 1 ≤ i < m, σ i+1 depends on σ i w.r.t. h i .
With the aim of capturing condition (ii) of Def. 1 based on the notions that we introduced, in what follows, we define the notion of activeness. Definition 5. (Activeness) Let Σ be a rule set and D a database. A path P = (σ 1 , ..., σ n ) is said to be active w.r.t. D, if there exists a chained vector of homomorphisms H = (h 1 , ..., h n ) for P such that chase p std (D, P, H) is a standard chase path for D, P, H based on Σ. In this case, H = (h 1 , ..., h n ) is called a witness of the activeness of P w.r.t. D.
Intuitively, the definition says that a path P is active w.r.t. a database D if there is an active trigger for each rule application in the path, hence it is a standard chase path, and the last rule application depends on some earlier ones and eventually on the first on the path. In other words, if P is not active w.r.t. D we then know that P is either "terminating" w.r.t. D, or for each vector of homomorphisms H = (h 1 , ..., h n ) such that chase p std (D, P, H) is a standard chase path, H is not chained for P ; thus it does not pose as a "dangerous cycle" even in the case σ 1 = σ n .
Let H = (h 1 , ..., h n ) be a vector of homomorphisms such that chase p std (D, P, H) is a standard chase path. To determine if H is chained for P , O(n 2 ) checks are needed, 3where each h i (body(σ i )) is checked against every h j (head(σ j )), for all j < i, to determine if σ i depends on σ j w.r.t. h i ∪ h j .
We are now ready to address the issue of which databases to be checked against for termination analysis. First, let us define a mapping e i : V ∪ Const → V, i ∪ Const, for each i ∈ N, where constants in Const are mapped to themselves and each variable v ∈ V is mapped to v, i . Definition 6. Given a path P = (σ 1 , σ 2 , ...), we define
A pair x, i in D P is intended to name a fresh constant, based on the derivation step in P in which the variable x occurs. In this way, all these fresh constants are distinct. Note that D P is a set of atoms over these new constants (and the constants already appearing in rules) and is independent of any input database. Let us call these pairs indexed constants and use short hand v i for v, i .
Intuitively, atoms in D P are intended to simulate those in a derivation sequence where body atoms in an applied rule are satisfied by atoms from a given database. Since in general we don't know which body atoms are satisfied by a given database in each step of a derivation sequence, we need to test activeness using each subset of D P . This process is finite whenever P is.
Note that due to the structure of D P , application of each rule to D P may lead to a new trigger and therefore, without the notion of chained property, every path can be trivially active.
Example 4. Consider the rule set Σ of Example 3 and a path P = (σ, σ). We have: D P = {T (x 1 , y 1 ), P (x 1 , y 1 ), T (x 2 , y 2 ), P (x 2 , y 2 )}. We see that P is not active w.r.t. D P , as there does not exist any chained vector of homomorphisms H = (h 1 , h 2 ) for P .
Theorem 1. Let Σ be a rule set, and P = (σ 1 , ..., σ n ) a path. P is active w.r.t. some database if and only if P is active w.r.t. some database D * ⊆ D P . Definition 7. A k-cycle P = (σ 1 , ..., σ n ) is safe if for all databases D, P is not active w.r.t. D. A rule set Σ is said to be k-safe if all k-cycles of Σ are safe.
It then follows from Theorem 1, we have Corollary 2. Let Σ be a rule set. For any k-cycle P = (σ 1 , ..., σ n ), if for all subsets D * of D P , P is not active w.r.t. D * , then P is safe. E.g., it can be verified that the rule set Σ 1 in Example 1 is k-safe for any k ≥ 1. We now introduce a hierarchy of classes of finite standard chase based on the notion of k-safety. The idea is to introduce a parameter of cycle function to generalize various notions of acyclicity in the literature. Definition 8. Let Σ be a rule set and C the set of all finite cycles based on Σ. A cycle function is a mapping cycle Σ : C → {T, F }.
Let cycle be a binary function from rule sets and cycles of which cycle Σ is the projection function on its first parameter, i.e. cycle(Σ, C) = cycle Σ (C). By abuse of terminology, the function cycle, which in addition takes a rule set as a parameter, is also called a cycle function.
In the following, we show how to define a cycle function from any arbitrary acyclicity condition of finite skolem chase such as weak acyclicity (WA) [11], super-weak acyclicity (SWA) [12], etc. Definition 10. Let Π be an arbitrary condition of acyclicity of finite skolem chase. A cycle function Φ Π is defined as follows: For each rule set Σ and each cycle C based on Σ if the condition for checking whether Π holds for rules in Rules(C) 4 , then Φ Π maps (Σ, C) to F ; otherwise Φ Π maps (Σ, C) to T .
Example 5. Considering the rule set Σ 1 from Example 1, and assuming Π = WA in Def. 10, Φ Π maps all cycles C such that Rules(C) ∩ {σ 1 , σ 2 } = {σ 1 , σ 2 } to F and the rest of the cycles to T .
The following theorem is easy to show. Theorem 3. Let Π be a class of finite skolem chase that is defined by a condition of acyclicity and Φ Π be the corresponding cycle function as defined above. Then, for all
where Φ WA is the corresponding cycle function based on the condition of acyclicity for WA. Note that Φ WA maps 1-cycles of the form (σ i , σ i ), where i = 1, 2, to F and all other 1-cycles to T5 . Similarly, the rule set Σ 2 in the same example is 2-SAFE(Φ WA ).
In [9], a family of existential rule languages with finite (skolem) chase based on the notion of δ-boundedness has been introduced and the data and combined complexities of reasoning with those languages for specific bound functions (k-exponentially bounded functions). Our aim in this section is to provide an effective method to extend bounded languages to introduce all-instance terminating standard chase classes. Before we state our results, let us introduce some notions.
A bound function is a function from positive integers to positive integers. A rule set Σ is called δ-bounded under skolem chase for some bound function δ, if for all databases D, ht(chase sk (D, Σ)) ≤ δ(||Σ||), where ||Σ|| is the number of symbols occurring in Σ, and ht(A) is the maximum height (maximum nesting depth) of skolem terms that have at least one occurrence in A, and ∞ otherwise. Let us denote by δ-B sk the class of δ-bounded rule sets under skolem chase.
We consider the membership problem in δ-B std languages: given a rule set Σ and a bound function δ, whether Σ is δ-bounded under the standard chase variant. Proposition 6. Let δ be a bound function computable in DTIME(T (n)) 6 for some function T (n). Then, it is in
to check if a rule set Σ is δ-bounded under the standard chase variant, where
is the maximum number of body atoms for rules in Σ, and
Now consider what we call exponential tower functions:
Then, we have the following corollary from Prop. 6: Corollary 7. Checking if a rule ontology is exp κ -bounded under standard chase variant is in (κ + 2)-EXPTIME.
The corollary implies that, for any exponential tower function δ, the extra computation for checking δ-boundedness under standard chase stays within the same complexity upper bound for δ-boundedness under skolem chase, as reported in [9].
Remark 1. For membership checking, switching from skolem to standard chase variant does not increase the complexity for exp κ -bounded rule sets. However, it should be clear that for some syntactic classes of finite skolem chase which are known to belong to exp 0 -bounded rule sets (e.g. WA, JA, SWA, etc.), the penalty for going beyond finite skolem chase is the higher cost of membership checking.
Since the size of the tree generated by standard chase has the same upper bound as that generated by skolem chase, it is not difficult to show that the complexity upper bound for checking Σ ∪ D q for exp κ -bounded rule sets is the same for the standard and skolem chase variants. It then follows from [9] that we have Theorem 8. The problem of Boolean conjunctive answering for exp κ -bounded rule ontologies under standard chase variant is (κ + 2)-EXPTIME-complete for combined complexity and PTIME-complete for data complexity. Remark 2. Based on Theorem 8, it can be observed that the entire hierarchy of δbounded rule sets under skolem chase introduced in [9] can be extended with no increase in combined and data complexity of reasoning. This holds even for individual syntactic classes of finite skolem chase (such as WA, JA, SWA, etc.).
Many sufficient conditions have been discovered for termination of skolem and oblivious chase based on different notions of acyclicity based on graphs derived from the given rule set. Typically, such a graph is constructed based on some notion of dependencies in the rule set, e.g., position dependencies and rule dependencies. These classes include WA (weak acyclicity) [11], STR (stratification) [15], safety [16], SWA (superweak acyclicity) [4], aGRD (acyclicity of graph of rule dependencies) [17], and JA (joint acyclicity) [18].
To the best of our knowledge, [7] is the only work that have studied termination of the standard chase towards positive results. Their results are only in the context of Horn-SRIQ description logics and not applicable to existential rules. In [19] a notion called well of positivity has been devised which is an extension of the critical instance technique and has been applied in undecidability results. For their purpose, they only need one extra constant in addition to the well of positivity to show undecidability of the standard chase for all instances on all paths. However, in general, there is no bound for the number of constants needed to witness non-termination of the standard chase.
Under reasonable assumptions, one can find syntactic conditions that guarantee termination of the standard chase for all instances and all paths. As an example, consider the following rule Σ = {σ}, where:
σ : E(x, y) → ∃u 1 . . . u k E(y, u 1 ), E(u 1 , u 2 ), . . . , E(u k , y) for some k ≥ 1. It can be observed that starting from any database D, chase std (D, Σ) terminates in maximum |I E |+1 steps, where I E is the database D restricted to the tuple over predicate E. Intuitively, the reason that Σ ∈ CT std ∀∀ is the observation that predicate E (for which E[i], for some i, is the placeholder of (potentially) infinite terms), when seen as a graph in which it is interpreted as the edge relation, forms a cycle in head(σ), where σ belongs to the following cycle C = (σ, σ) that is mapped to T under any condition of (skolem) acyclicity.
In [20] it is shown that for (weakly-)guarded and (simple-)linear TGDs, the problem of deciding (non-)termination of oblivious/skolem chase is decidable. This characterization leads to finding upper bounds for the length of cycles that should be considered in order to decide (non-)termination w.r.t. the skolem chase. Theorem 1 provides tools to extend their results to all-instance, all-path standard chase variant. Note that they only consider single-head TGDs8 . So, their results cannot be trivially extended to the standard variant of chase for (arbitrary) multi-head TGDs. Further results in this direction are outside of the focus of this paper and is the subject of the future work.
In this work we introduced a technique to characterize finite standard chase, which can be applied to extend any class of finite skolem chase identified by a condition of acyclicity. Then, we showed how to apply our techniques to extend δ-bounded rule sets. Our complexity analyses showed that this extension does not increase the complexities of membership checking, nor the complexity of combined and data reasoning tasks for δ-bounded rule sets under standard chase compared to skolem chase. However, comparing with some subclasses of the exp 0 -bounded language, membership checking for finite standard chase incurs higher cost.
We will next investigate conditions for subclasses with a reduction of cost for membership testing. One idea is to find syntactic conditions under which triggers to a rule are necessarily active, and the other is on symmetric conditions under which triggers of certain kind cannot be active. We anticipate that position graphs could be useful in these analyses.