The chase procedure was initially developed for testing logical implication between sets of dependencies [3], for determining equivalence of database instances known to satisfy a given set of dependencies [14,10], and for determining query equivalence under database constrains [2]. More recently the chase has been used to compute representative target solutions in data exchange. Intuitively, the data exchange problem consists of transforming a source database into a target database, according to a set of source to target dependencies describing the mapping between the source and the target. The set of dependencies may also include target dependencies, that is, constraints over for the target database. The source and the target schemas are considered to be distinct. Given a source instance I and a set Σ of dependencies, an instance J over the target schema is said to be a solution if I ∪ J satisfies all dependencies in Σ. One of the most important representations for this (usually infinite) set of solutions was introduced by Fagin et al. [6]. They considered the finite tableau obtained by chasing the initial instance with the dependencies. Such a tableau, if exists, was called a universal solution. In their paper, Fagin et al. showed that the universal solution is a good candidate for materializing the target. In particular, the universal solution can be used to compute certain answers to (unions of) conjunctive queries over the target instance. The universal solution is however not a good candidate for materialization in case we are dealing with nonmonotonic queries, or even conjunctive queries with inequalities. It was soon realized that a closed world semantics is needed. The first closed world approach in data exchange was introduced by Libkin [11] and extended by Hernich and Schweikardt in [9], and by Hernich in [8]. The paper by Deutsch et al. [5] also contained a proposal for dealing with nonmonotonic queries. In a previous paper [7], we analyzed these proposals and found that they can give unintuitive answers. To remedy this, we introduced the constructible solutions (constructible models) semantics, and showed that the space of constructible solutions can be represented by a conditional table, and obtained by a conditional chase, also given in [7].
Since the chase procedure was first adopted for data exchange one of the main problems was whether it terminates in a finite number of steps. Clearly, when considering only source to target dependencies the chase procedure terminates, as there is no recursion involved. Unfortunately, adding even simple target constraints may lead to non-termination. For example, consider the data exchange setting given by one source to target dependency ∀x, y ∶ S(x, y) → R(x, y), the target dependency ∀x, y ∶ R(x, y) → ∃z R(y, z), and the source instance I = {S(a, b)}. It is easy to see that chasing I with the given dependencies is nonterminating, as at each step the target dependency will generate a new tuple, containing a fresh new labeled null, and that this new tuple will cause the target dependency to fire again.
This leads to a fundamental question: "When does the chase terminate?" This question was shown to be undecidable Deutsch et al. in [5]. Motivated by this negative result there has been several efforts to find sufficient conditions for the chase termination. The first of these was already given by Fagin et al. [6] who introduced the weakly acyclic sets of dependencies, and showed that the chase with such a set terminates. This was soon followed by several generalizations for which the chase is guaranteed to terminate [5,13,12,15]. All of these previous results are for termination of the standard chase. The termination for variations of the chase did not receive much attention.
In this paper we show that our conditional chase is guaranteed to terminate for the richly acyclic dependencies introduced by Hernich and Schweikardt [9]. This class is slightly more restrictive than the weakly acyclic one. We also show that the termination of oblivious chase, introduced by Calì et al. [4], is strongly related to the termination of the standard chase, and that the oblivious chase always terminates with richly acyclic dependencies.
The rest of this paper is organized as follows. In Section 2 we introduce basic notions used throughout the paper. In Section 3 we describe the constructible solutions semantics and the conditional chase procedure. Then, in Section 4 we show that the conditional chase with richly acyclic sets of dependencies is guaranteed to terminate. Conclusions are drawn in the last section.
For required background knowledge the reader should consult [1]. Throughout the paper, the symbol ω will denote the set {0, 1, 2, . . .}.
Let Cons be a countably infinite set of constants, usually denoted a, b, c, . . ., possibly subscripted. From the domain Cons and a finite set R of relation names, we build up a Herbrand structure consisting of all expressions of the form R(a 1 , a 2 , . . . , a k ), where R is a "k-ary" relation name from R, and the a i 's are values in Cons. Such expressions are called ground atoms, or ground tuples. A database instance I is then simply a finite set of ground tuples, e.g. {R 1 (a 1 , a 3 ), R 2 (a 2 , a 3 , a 4 )}. We denote the set of constants occurring in an instance I with d om(I).
Relational tableaux. Let Vars be a countably infinite set, disjoint from the set of constants. Elements in Vars are called variables, and are denoted X, Y, Z, . . ., possibly subscripted. We can then also allow non-ground atoms, i.e. expressions of the form R(a, X, b, . . . , X, Y ). A tableau T is a finite set of atoms (ground, or non-ground). A non-ground atom represents a sentence where the variables are existentially quantified. The set of variables and constants in a tableau is denoted d om(T ).
Let T and U be tableaux. A mapping h from d om(T ) to d om(U ), that is the identity on Cons, extended component-wise, is called a homomorphism from T to U if h(T ) ⊆ U . If there is an injective homomorphism h such that h(T ) = U , and the inverse of h is a homomorphism from U to T , we say that T and U are isomorphic. An endomorphism on a tableau T is a mapping on d om(T ) such that h(T ) ⊆ T . Finally, a valuation is a homomorphism whose image is contained in Cons.
Tuple generating dependencies. A tuple generating dependency (tgd) is a first order formula of the form
where α is a conjunction of atoms, β is a single atom1 , and x,y and z are sequences of variables. We assume that the variables occurring in dependencies are disjoint from all variables occurring in any tableaux under consideration. To emphasize this, we use lowercase letters for variables in dependencies. When α is the antecedent of a tgd, we shall sometimes conveniently regard it as a tableau, and refer to it as the body of the tgd. Similarly we refer to β as the head of the tgd. If there are no existentially quantified variables the dependency is said to be full, otherwise it is embedded. Frequently, we omit the universal quantifiers in tgd formulae. Also, when the variables are not relevant in the context, we denote a tgd α(x, y) → ∃z β(x, z) simply as α →β.
Let ξ = α → β be a tuple generating dependency, and I an instance. Then we say that I satisfies ξ, if I ⊧ ξ in the standard model theoretic sense, or equivalently, if for every homomorphism h, such that h(α) ⊆ I, there is an extension h ′ of h, such that h ′ (β) ∈ I.
The standard chase. The standard chase works on tableaux. Let Σ be a set of tgd's and T a tableau. A trigger for Σ on T is a pair (ξ, h), where ξ = α →β ∈ Σ, and h is a homomorphism such that h(α) ⊆ T . The set of all triggers for Σ on T is denoted trigg Σ (T ). It is easy to see that trigg Σ (T ) is finite.
A trigger (ξ, h) ∈ trigg Σ (T ), with ξ = α →β, is said to be active if there is no extension h ′ of for which h ′ (β) ∈ T . The standard chase step [6,5] on a tableau T with such an active trigger results in a tableau U = T ∪ {h ′ (β)}, where h ′ is an extension of h that assigns new fresh (uppercase) variables to the existential variables in β. The standard chase step is denoted T ξ,h ′ → U . We also say that the trigger (ξ, h) was fired on T . The standard chase [6,5] on a tableau T is defined as a sequence T 0 , T 1 , T 2 , . . . , T n , . . . where T = T 0 , and for each i we have
If there are no active triggers in trigg Σ (T i ) we let T i+1 = T i . We say that the sequence terminates (in the finite) if T i = T i+1 , for some i ∈ ω. In the rest of this paper we consider all sequences to be fair, meaning that all active triggers either become inactivated or are eventually fired. The standard chase result for the sequence is ⋃ i∈ω T i . Note that a chase sequence is not necessarily unique, since there is nondeterminism involved when choosing a trigger at each step. It is however known [6,5] that all standard chase results are homomorphically equivalent. Let therefore C hase stand Σ (T ) denote one representative of this homomorphic equivalence class; in particular it denotes a finite representative, if one exists. Note that Deutsch et al. [5] have show that it is undecidable both whether some or whether all chase sequences terminate in the finite. There are however several classes of dependencies that guarantee termination of the standard chase, the most notable of them being the weakly acyclic dependencies for which all standard chase sequences terminate on all input instances. We shall return to this class of dependencies in Section 4.
Deutsch et al. [5], building on the work on data exchange by Fagin et al. [6], regard the chase as a tool for computing a universal model for a tableau T and a set Σ of dependencies. A universal model for a theory is a model that has a homomorphism into every model of the theory. Such universal models have the desirable property that they are a sufficiently strong representative for computing certain answers to monotone queries on a database instance incompletely specified by T ∪ Σ. A ground tuple t is in the certain answer to a query if t is in the answer to the query on every model of T ∪ Σ. Recently it has been noted that for first order queries some sort of closed world assumption is required, as the set of models represented by a universal one is closed under homomorphic images, and thus amounts to an open world assumption. Several closed world assumptions have recently been proposed [11,9,5,8]. These assumptions are scrutinized in [7], where a new closed world assumption, called constructible models, is put forward. This new semantics is based on the theory of incomplete information [10], where a tableau T is seen as a representative of a (possibly infinite) set of ground instances, or possible worlds, denoted Rep(T ). Formally, In [7] we show that the conditional tables [10] are sufficiently strong to exactly represent the aforementioned constructible models of T ∪ Σ, and that such a conditional table can be obtained by a novel conditional chase. Next we briefly describe the constructible models, the conditional tables, and the conditional chase. More details can be found in [7].
Constructible models. Let I be a ground instance and Σ a set of tgd's. Consider a chase step on I with a tgd ξ = α(x, y) → ∃z β(x, z), and trigger (ξ, h). Instead of adding the tuple β(h(x), Z ′ ), where Z ′ is a sequence of new fresh variables, we create a branch for each sequence c of constants and add the ground tuple β(h(x), c) to I. Continuing in this fashion we will have a chase tree, instead of a chase sequence. Notably, all nodes in the tree will be ground instances. The leaves of the chase tree form the set of constructible models of I and Σ, denoted Σ(I). If the initial input to the chase is a tableau T , the constructible models of T ∪ Σ will be Σ(Rep(T )) = ⋃ I∈Rep(T ) Σ(I).
[10] is a pair (T, ϕ), where T is a tableau, and ϕ is a mapping that associates a local condition ϕ(t) with each tuple t ∈ T . A (local) condition is a Boolean formula built up from atoms of the form x = y, x = a, and a = b for x, y ∈ Vars, and a, b ∈ Cons. An atomic equality of the form a = a, for a ∈ Cons represents the logical constant true, and for two distinct constants a and b, the equality a = b represents false. If ϕ(t) = true, for all t ∈ T , the conditional table (T, ϕ) is denoted (T, true), or sometimes simply with T . A conditional table (T, ϕ) represents a set of possible worlds (ground instances, complete databases). For this, let v be a valuation. Then v(T, ϕ) = {v(t) ∶ t ∈ T, and v ϕ(t) = true}.
The set of possible worlds represented by (T, ϕ) is
Unifiers. Let T and U be tableaux. A unifier for T and U , if it exists, is a pair (θ 1 , θ 2 ), where θ 1 is a homomorphism from d om(T ) to d om(U ), and θ 2 is an endomorphism on d om(U ), such that θ 1 (T ) = θ 2 (U ). Note the asymmetrical role of T and U : a unifier for (T, U ) is not necessarily a unifier for (U, T ). The notion of a most general unifier (mgu) is defined in the obvious way, see [7]. For example, let
{V b} is an mgu for T and U . Another mgu for T and U is (γ 1 , γ 2 ), with γ 1 = {X b, Y a, Z V } and γ 2 = {W a}. We denote by mgu(T, U ) the set of all mgu's of T and U .
Triggers. Recall that for the classical chase a trigger for a tableau T is a pair (ξ, h), where ξ = α →β, and h(α) ⊆ T . Let us now return to example given in the beginning of this section. We had T = {R(a, b), R(X, c)}, and Σ = {ξ}, where ξ = {R(x, y), R(y, z) → S(x, z)}. We want to fire ξ on T resulting in conditional table ({R(a, b), R(X, c), S(a, c)}, ϕ), where ϕ(S(a, c)) is (X = b), and ϕ(t) remains true for the two other tuples t. We can fire ξ on T provided that we unify X with b. Formally, this is achieved by the trigger (ξ, ({x a, y b}, {X b}, T ), where ({x a, y b}, {X b}), is an mgu for the body of ξ, that is {R(x, y), R(y, z)}, and T . In general, the part of T that will be unified with the body of ξ is some subset of T . Let Σ be a set of tgd's, and (T, ϕ) a conditional table. A trigger for Σ on (T, ϕ) is a tuple τ = (ξ, θ, T ′ ), where ξ ∈ Σ, and θ = (θ 1 , θ 2 ) is an mgu that unifies the body of dependency ξ with T ′ , where T ′ ⊆ T . The set trigg Σ (T, ϕ) contains the set of all triggers for Σ on (T, ϕ).
Example 1. Consider the conditional table (T, ϕ) with the following tabular representation:
Note that ξ 2 , does not generate any triggers, as there are no tuples over relation name S. ◂ As applying a trigger on a c-table will generate new variables (unless the tgd is total), we need a mechanism for controlling this generation in such a way that the new variables are true representatives of the implicit Skolemization taking place. Let τ = (ξ, (θ 1 , θ 2 ), T ′ ) be a trigger, where ξ = α(x, y) → ∃z β(x, z). For each z in z, consider a function z ↦ Z τ , such that if ρ = (ξ, (θ 1 , θ 3 ), T ′′ ), then Z τ = Z ρ . Clearly such a function exists (assuming Vars can be well ordered).
The following abbreviation will be useful. Let (T, ϕ) be a conditional table. Then we define
Also, when θ is finite partial mapping from Vars to the set Vars ∪ Const we shall use the abbreviation
where the X i 's are all the variables in the domain of θ. We are now ready to define the conditional chase step. Let τ = (α → β, (θ 1 , θ 2 ), T ′ ) ∈ trigg Σ (T, ϕ). We denote with θ ′ 1 the extension of θ 1 that maps each existentially quantified variable z from the tgd to the variable Z τ . We say that the conditional table (U, φ) is obtained from (T, ϕ) by applying the trigger τ if (U, φ) contains all the c-tuples from T together with their possibly modified local conditions, and possibly a new c-tuple, as follows:
If T contains a tuple t that is syntactically equal to θ ′ 1 (β), then for (U, φ) the local condition of t is changed to
where ⩕(τ ) denotes2 the formula ⩕(T ′ , ϕ) ∧ ⩕(θ 2 ), else add the c-tuple θ ′ 1 (β) with local condition
If (U, φ) is obtained from (T, ϕ) in this way we write (T, ϕ) → τ (U, φ), and call the transformation a conditional chase micro-step.
Having a table (T, ϕ) and a finite set Σ of tgd's, the set of triggers trigg Σ (T, ϕ) is obviously finite. Consider a sequence
where τ 1 , τ 2 , . . . , τ n is an ordering of all the triggers from the set trigg Σ (T, ϕ). We call it a conditional chase micro-sequence for (T, ϕ) using trigg Σ (T, ϕ).
in Figure 1 is obtained from (T, ϕ) in one chase micro-step by applying the trigger τ 1 . That is (T, ϕ) → τ1 (U 1 , ψ 1 ). Next, by applying trigger τ 2 to (U 1 , ψ 1 ), we obtain (U 2 , ψ 2 ). Note that the last tuple has a local condition generated by the substitution {Y b} from τ 2 . In the same way we apply τ 3 to (U 2 , ψ 2 ), obtaining (U 3 , ψ 3 ). Then by applying τ 4 , c-table (U 4 , ψ 4 ) is obtained, to which we apply τ 5 , obtaining c-table (U 5 , ψ 5 ). This gives the following sequence of chase micro-steps:
where the c-tables in question are displayed in Figure 1.◂ We note that the order in which the triggers are applied in a conditional micro-sequence does affect the outcome, but we shall see that in the end the order will not matter.
After a micro-sequence, it is not guaranteed that the result will satisfy the dependencies. Then additional triggers will be generated. We therefore abstract a micro-sequence into a macro-step, as follows.
Let (T, ϕ) and (U, φ) be conditional tables, and Σ be a set of tgd's. We write (T, ϕ) ⇒ Σ (U, φ), if (U, φ) is obtained from (T, ϕ) by applying all micro-steps generated from trigg Σ (T, ϕ). The transformation from (T, ϕ) to (U, φ) is called a conditional chase macro-step using Σ.
The macro-step is monotone, that is, if (T, ϕ) ⇒ Σ (U, φ), then T ⊆ U and ϕ logically implies φ, which we by a slight abuse of notation denote ϕ ⊆ φ. We next introduce the concept of a conditional chase-sequence.
Let (T, ϕ) be a c-table and Σ a set of tgd's. A sequence (T 0 , ϕ 0 ), (T 1 , ϕ 1 ), . . . , (T n , ϕ n ), . . . of c-tables, inductively constructed as
is called a conditional chase sequence associated with (T, ϕ) and Σ. If there is an i ∈ ω, such that Rep(T i , ϕ i ) = Rep(T i+1 , ϕ i+1 ), we say that the conditional chase sequence terminates (in the finite). Example 3. Continuing example 2, let (T 0 , ϕ 0 ) = (T, ϕ) and (T 1 , ϕ 1 ) = (U 5 , ψ 5 ). Then (T 0 , ϕ 0 ) ⇒ Σ (T 1 , ϕ 1 ). Next, trigg Σ (T 1 , ϕ 1 ) = {τ 1 , τ 2 , τ 3 , τ 4 , τ 5 , τ 6 , τ 7 , τ 8 }, where τ 1 , . . . , τ 5 are as before, and
By applying the triggers in the order τ 1 , τ 2 , . . . , τ 8 we obtain another microsequence ending in (T 2 , ϕ 2 ), shown in Figure 2. In other words, (T 1 , ϕ 1 ) ⇒ Σ (T 2 , ϕ 2 ). Note that the conditional chase process is not finished yet, as for table (T 2 , ϕ 2 ), beside the previous triggers the following new triggers need to be considered as well:
By applying τ 1 , . . . , τ 12 the micro-sequence will end up in the c-table (T 3 , ϕ 3 ), in Figure 2. Thus (T 0 , ϕ 0 ), (T 1 , ϕ 1 ), (T 2 , ϕ 2 ), (T 3 , ϕ 3 ) is (the finite part of) a conditional chase sequence associated with (T, ϕ) and Σ. For readability, (T 3 , ϕ 3 ) is shown in a "cleaner" isomorphically equivalent form.◂
The following result shows that no matter what order we choose to apply the triggers in the micro-sequences, the results of the corresponding conditional chase sequences are equivalent. Theorem 1. Let (T, ϕ) be a conditional table and Σ a set of tgd's. Then, let (T 0 , ϕ 0 ), (T 1 , ϕ 1 ), . . . , (T n , ϕ n ), . . . and (T ′ 0 , ϕ ′ 0 ), (T ′ 1 , ϕ ′ 1 ), . . . , (T ′ n , ϕ ′ n ), . . . be two distinct conditional chase sequences with different orders of triggers in their micro-sequences. Then Rep(T ω , ϕ ω ) = Rep(T ′ ω , ϕ ′ ω ). Even more, T ω = T ′ ω .
The theorem means that distinct orders in the micro-sequences only affect the syntactic form of the local conditions. The atoms in the table will be syntactically equal, and the corresponding local conditions equivalent.
We shall use the notation C hase cond Σ (T, ϕ) for one representative of (T ω , ϕ ω ) in the conditional chase sequence, starting with (T, ϕ) and Σ. We conclude this section by stating the main property of the conditional chase. The theorem means that the conditional chase computes exactly the set of constructible models. 4 When does the conditional chase terminate?
We will show that the conditional chase with richly acyclic set of tgd's always terminates. The class of richly acyclic [9] sets of tgd's is slightly smaller than the well known class of weakly acyclic sets of tgd's. To prove our result we need the oblivious chase, introduced by Calì et al. [4].
The oblivious chase. The oblivious chase proceeds as the standard chase, except that each dependency is fired once for each trigger, irrespectively of whether the trigger is active or not. As in the standard chase, we assume that all the dependencies are applied fairly in the oblivious chase process. Fairness of the oblivious chase means that each trigger, active or not, is eventually applied. The details of how to construct a fair oblivious chase sequence are described in [4].
In case we use a fair oblivious chase, the result is unique up to isomorphism. We denote with C hase obl Σ (T ) one representative instance of the result. Clearly there are cases where the standard chase terminates, but the oblivious does not. However, Calì et al. [4] show that the results of the standard and the oblivious chases are homomorphically equivalent, even if one (or both) of them is nonterminating.
Enrichment of dependencies. In order to relate termination of the standard and the oblivious chase, we introduce a transformation, called enrichment, that takes a tuple generating dependency ξ = α(x, y) → ∃z β(x, z) and converts it into the tgd ξ = α(x, y) → ∃z β(x, z), H(x, y), where H is a new relational symbol that does not appear in R. For a set Σ of tgd's, the transformed set is Σ = { ξ ∶ ξ ∈ Σ}. We now have Proof. Let Σ be a set of tgd's, and suppose that there is a tableau T for which the standard chase with Σ does not terminate. This means that there is an infinite standard chase sequence
Let α i denote the antecedent of ξi Then h i (α i ) ⊆ T i , for all i ∈ ω. Since α i also is the antecedent of ξ i , we have that
where U i is T i with all atoms over H deleted, is an infinite oblivious chase sequence with Σ on T . Suppose then that there is a tableau T for which the oblivious chase with Σ does not terminate. Then there is an infinite oblivious chase sequence
We claim that
is an infinite standard chase sequence with Σ on T . Suppose it is not. Then there must be an i ∈ ω, such that the standard chase step cannot be applied with h i and ξi on U i . Let ξ i = α(x, y) → β(x, z). Then ξi = α(x, y) → β(x, z), H(x, y).
If ξi cannot be applied with h i on U i , there exists an extension h e i of h i such that β(h e i (x), h e i ( z))) and H(h e i (x), h e i ( y))) are in U i . Since h e i is an extension of h i , it follows that h e i (x) = h i (x) and h e i (y) = h i (y), meaning that H(h i (x), h i ( y))) ∈ U i . Because atoms over H are only introduced by the chase, it means that the homomorphism h i has already been applied with ξi earlier in the standard chase sequence. But then h i must also have been applied with ξ i at the same earlier stage in the oblivious chase sequence. This is a contradiction, since it entails that ξ i would have been fired twice with h i in the oblivious chase sequence. ∎ Weakly and richly acyclic sets of tgd's. For a set Σ of tgd's over a database schema R the dependency graph of Σ is the directed graph that has as vertices (R, i), where R ∈ R, and i ∈ {1, . . . , arity(R)}. The graph has two types of edges:
1. Regular edges. There is a regular edge between vertices (R, i) and (S, j) if there a tgd in Σ that has a variable y that appears both in position (R, i) in the body, and in position (S, j) in the head. 2. Existential edges. There is an existential edge between vertices (R, i) and
(S, j) if there is a tgd in Σ that has a variable y that appears in position (R, i) of the body and in some position in the head, and an existentially quantified variable z that appears in position (S, j) in the head.
A set of Σ of tgd's is said to be weakly acyclic if the dependency graph of Σ does not have any cycles containing an existential edge [6]. In particular, Fagin et al. have shown Lemma 1. [6] Let Σ be a weakly acyclic set of tgd's. Then C hase stand Σ (T ) terminates for all tableaux T . Hernich and Schweikardt [9] defined a slight restriction on the weakly acyclic sets of dependencies as follows: If the previous dependency graph is extended by also adding an existential edge from position (R, i) and (S, j) whenever there is a dependency in ξ ∈ Σ that has a variable x that appears in position (R, i) of the body and an existentially quantified variable z appears in position (S, j) in the head of ξ. The newly created graph is called extended dependency graph. A set of Σ of tgd's is said to be richly acyclic if the extended dependency graph of Σ does not have any cycles containing an existential edge. The following lemma is immediate. Lemma 2. Let Σ be a richly acyclic set of tgd's. Then Σ is weakly acyclic.
From Theorem 3, and Lemmas 1 and 2, we can conclude Corollary 1. Let Σ be a richly acyclic set of tgd's. Then C hase obl Σ (T ) terminates on all tableaux T .
It is easy to see that whenever the conditional chase terminates, the oblivious chase also terminates. The reverse is however not true. Proposition 1. There exists a set Σ of tgd's and a tableau T , such that the oblivious chase with Σ terminates on all instances (including T ), but the conditional chase with Σ does not terminate on (T, true).
Proof: Let Σ = {R(x, y, y) → ∃z, v R(x, z, v)}. Using the technique in [12] it can easily be shown that the standard chase with Σ terminates on all instances. From this, and Theorem 3 it follows that the oblivious chase with Σ terminates on all instances. Consider then the conditional chase starting with c-table {R(a, b, b)} (the local condition of R(a, b, b) is true). The result of this chase can be represented by the infinite conditional table below.
In order to obtain the sufficient condition for the conditional chase termination we introduce our second rewriting of a set of tgd's Σ, called disjoining, and denoted Σ. Given a tgd ξ, we denote with ξ the same dependency where for each variable x, that is repeated in the body, we replace all occurrences, except the first, of x in the body with a fresh new universally quantified variable. For instance, if ξ = R(x, y, x), R(y, z, x) → ∃v, w R(x, v, w), then ξ = R(x, y, x 1 ), R(y 1 , z, x 2 ) → ∃v, w R(x, v, w), where the subscripted variables are fresh. The set Σ is then { ξ ∶ ξ ∈ Σ}.
From the observation that a difference between the conditional and the oblivious chase is that the former may fire based on unifiers (θ 1 , θ 2 ), and the latter based only on homomorphisms θ 1 , we obtain the following lemma.
From the observation that the extended dependency graph for Σ can be obtained from the extended dependency graph of Σ by deleting edges we get Lemma 4. If Σ is a richly acyclic set of tgd's, then Σ is also richly acyclic.
We now have the main result of this section Theorem 4. Let Σ be a set of richly acyclic set of tgd's and (T, ϕ) a c-table. Then C hase cond Σ (T, ϕ) terminates.
Proof. By Lemma 4, the set Σ is also richly acyclic, and by Lemma 2, the set Σ is weakly acyclic. By [6], C hase stand Σ (T, true) terminates. By Corollary 1, C hase obl Σ (T, true) also terminates, and then by Theorem 3, C hase cond Σ (T, ϕ) terminates. ∎
In this paper we have shown that the conditional chase with a richly acyclic set of dependencies terminates on all instances. This class is based on the well known weakly acyclic class of dependencies that ensures the standard chase termination on all instances. One may extend the class of dependencies for which the conditional chase terminates, by considering classes of dependencies for which the standard chase terminates (such as super weakly acyclic, safe constraints, Cstratified) and then using our characterization of the oblivious chase termination (Theorem 3) and by suitable extensions of Lemma 3.
Due to the space restrictions complexity results are not included. In the full version of this paper we show that for richly acyclic sets of dependencies the problem of checking if a tuple is the certain answer to a given first order query is coNP-complete and remains polynomial for unions of conjunctive queries.