On Conditional Chase Termination Gösta Grahne and Adrian Onet Concordia University,Montreal, Canada, H3G 1M8 {grahne,a onet}@cs.concordia.ca Keywords: chase, closed world assumption, incomplete information, data ex- change 1 Introduction The chase procedure was initially developed for testing logical implication be- tween 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 intro- duced 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 so- lution 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 in- troduced 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 con- straints 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 non- terminating, 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. 2 Preliminaries For required background knowledge the reader should consult [1]. Throughout the paper, the symbol ω will denote the set {0, 1, 2, . . .}. Relational instances. 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 expres- sions of the form R(a1 , a2 , . . . , ak ), where R is a “k-ary” relation name from R, and the ai ’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. {R1 (a1 , a3 ), R2 (a2 , a3 , a4 )}. 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 ∀x ∶ α(x, y) → ∃z β(x, z) 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 ξ,h′ variables in β. The standard chase step is denoted T ÐÐ→ U . We also say that 1 Note that there is no loss of generality in assuming that the head consists of a single atom, cf. [4] the trigger (ξ, h) was fired on T . The standard chase [6, 5] on a tableau T is defined as a sequence T0 , T1 , T2 , . . . , Tn , . . . where T = T0 , and for each i we have that Ti ÐÐ→ Ti+1 , for some (ξ, h) ∈ trigg Σ (Ti ). If there are no active triggers in ξ,h′ trigg Σ (Ti ) we let Ti+1 = Ti . We say that the sequence terminates (in the finite) if Ti = Ti+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∈ω Ti . 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 hasestand Σ (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. 3 The conditional chase 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 in- completely 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 as- sumption is required, as the set of models represented by a universal one is closed under homomorphic images, and thus amounts to an open world as- sumption. 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 pos- sible worlds, denoted Rep(T ). Formally, Rep(T ) = {v(T ) ∶ v is a valuation}. Then a tableau T is said to satisfy a set Σ of dependencies, if I ⊧ Σ, for all I ∈ Rep(T ). A tableau U = C hasestand Σ (T ) is indeed a universal model for T ∪ Σ, but there can be ground instances in Rep(U ) that do not satisfy Σ. For in- stance, let T = {R(a, b), R(X, c)}, and Σ = {R(x, y), R(y, z) → S(x, z)}. Then C hasestand Σ (T ) = T , I = {R(a, b), R(b, c)} ∈ Rep(T ), but I ⊧/ Σ. Consider now the nonmonotonic Boolean query R(a, b) ∧ ¬S(a, c). Evaluated on T the certain answer will be true, which clearly should not be the case, as the query evaluates to false on the instance I ∪ {S(a, c)}, and I ∪ {S(a, c)} is a model of T ∪ Σ. 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. Con- sider 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 vari- ables, 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, in- stead 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). Conditional tables. A conditional table (c-table) [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 Rep(T, ϕ) = {v(T, ϕ) ∶ v is a valuation }. 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 T = {R(X, Y ), R(Y, Z)} and U = {R(a, V ), R(b, W )}. Then (θ1 , θ2 ), with θ1 = {X/a, Y /b, Z/W } and θ2 = {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 rep- resentation: t ϕ(t) R(X, b) true R(b, c) true R(Y, d) true Let Σ = {ξ1 , ξ2 }, where tgd ξ1 is R(x, y), R(y, z) → S(x, z) and tgd ξ2 is S(x, x) → R(x, x). Then trigg Σ (T, ϕ) = {τ1 , τ2 , τ3 , , τ4 , τ5 }, with τ1 = (ξ1 , ({x/X, y/b, z/c}, {}), {R(X, b), R(b, c)}), τ2 = (ξ1 , ({x/X, y/b, z/d}, {Y /b}), {R(X, b), R(Y, d)}), τ3 = (ξ1 , ({x/b, y/c, z/d}, {Y /c}), {R(b, c), R(Y, d)}), τ4 = (ξ1 , ({x/Y, y/d, z/b}, {X/d}), {R(Y, d), R(X, b)}), τ5 = (ξ1 , ({x/c, y/c, z/b}, {X/c}), {R(b, c), R(X, b)}). 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 ⩕(T, ϕ) =def ⋀ ϕ(t). t∈T Also, when θ is finite partial mapping from Vars to the set Vars ∪ Const we shall use the abbreviation ⩕(θ) =def ⋀ Xi = θ(Xi ), i where the Xi ’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 φ(t) =def ϕ(t) ∨ ⩕(τ ), where ⩕(τ ) denotes 2 the formula ⩕(T ′ , ϕ) ∧ ⩕(θ2 ), else add the c-tuple θ1′ (β) with local condition φ(θ1′ (β)) =def ⩕(τ ). 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 (T, ϕ) →τ1 (U1 , ϕ1 ) →τ2 ⋯ →τn (Un , ϕn ), 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, ϕ). Example 2. Let us continue with the c-table from Example 1. The c-table (U1 , ψ1 ) in Figure 1 is obtained from (T, ϕ) in one chase micro-step by applying the trig- ger τ1 . That is (T, ϕ) →τ1 (U1 , ψ1 ). Next, by applying trigger τ2 to (U1 , ψ1 ), we obtain (U2 , ψ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 (U2 , ψ2 ), ob- taining (U3 , ψ3 ). Then by applying τ4 , c-table (U4 , ψ4 ) is obtained, to which we apply τ5 , obtaining c-table (U5 , ψ5 ). This gives the following sequence of chase micro-steps: (T, ϕ) →τ1 (U1 , ψ1 ) →τ2 (U2 , ψ2 ) →τ3 (U3 , ψ3 ) →τ4 (U4 , ψ4 ) →τ5 (U5 , ψ5 ), 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 Σ. 2 Note that the formula ⩕(τ ) is uniquely determined by τ . Intuitively it represents the (“abducted”) conditions induced by τ and necessary for the body α to apply in the standard sense. Fig. 1. Conditional tables from Example 2 (U1 , ψ1 ) (U2 , ψ2 ) (U3 , ψ3 ) (U4 , ψ4 ) (U5 , ψ5 ) t ψ1 (t) t ψ2 (t) t ψ3 (t) t ψ4 (t) t ψ5 (t) R(X, b) true R(X, b) true R(X, b) true R(X, b) true R(X, b) true R(b, c) true R(b, c) true R(b, c) true R(b, c) true R(b, c) true R(Y, d) true R(Y, d) true R(Y, d) true R(Y, d) true R(Y, d) true S(X, c) true S(X, c) true S(X, c) true S(X, c) true S(X, c) true S(X, d) Y = b S(X, d) Y = b S(X, d) Y = b S(X, d) Y = b S(b, d) Y = c S(b, d) Y = c S(b, d) Y = c S(Y, b) X = d S(Y, b) X = d S(b, b) X = c 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 (T0 , ϕ0 ), (T1 , ϕ1 ), . . . , (Tn , ϕn ), . . . of c-tables, inductively constructed as (T0 , ϕ0 ) = (T, ϕ), (Ti+1 , ϕi+1 ) = (U, φ), where (Ti , ϕi ) ⇒Σ (U, φ), (Tω , ϕω ) = ⋃ (Ti , ϕi ), i∈ω is called a conditional chase sequence associated with (T, ϕ) and Σ. If there is an i ∈ ω, such that Rep(Ti , ϕi ) = Rep(Ti+1 , ϕi+1 ), we say that the conditional chase sequence terminates (in the finite). Example 3. Continuing example 2, let (T0 , ϕ0 ) = (T, ϕ) and (T1 , ϕ1 ) = (U5 , ψ5 ). Then (T0 , ϕ0 ) ⇒Σ (T1 , ϕ1 ). Next, trigg Σ (T1 , ϕ1 ) = {τ1 , τ2 , τ3 , τ4 , τ5 , τ6 , τ7 , τ8 }, where τ1 , . . . , τ5 are as before, and τ6 = (ξ2 , ({x/d, y/d}, {X/d}), {S(X, d)}), τ7 = (ξ2 , ({x/b, y/b}, {Y /b}), {S(Y, b)}), τ8 = (ξ2 , ({x/b, y/b}, {}), {S(b, b)}), By applying the triggers in the order τ1 , τ2 , . . . , τ8 we obtain another micro- sequence ending in (T2 , ϕ2 ), shown in Figure 2. In other words, (T1 , ϕ1 ) ⇒Σ (T2 , ϕ2 ). Note that the conditional chase process is not finished yet, as for ta- ble (T2 , ϕ2 ), beside the previous triggers the following new triggers need to be considered as well: τ9 = (ξ1 , ({x/X, y/b, z/b}, {}), {R(X, b), R(b, b)}), τ10 = (ξ1 , ({x/b, y/b, z/b}, {X/b}), {R(b, b), R(X, b)}), τ11 = (ξ1 , ({x/Y, y/d, z/d}, {}), {R(Y, d), R(d, d)}), τ12 = (ξ1 , ({x/d, y/d, z/d}, {Y /d}), {R(d, d), R(Y, d)}). Fig. 2. Conditional tables (T2 , ϕ2 ) and (T3 , ϕ3 ) from Example 3 (T2 , ϕ2 ) (T3 , ϕ3 ) t ϕ2 (t) t ϕ3 (t) R(X, b) true R(X, b) true R(b, c) true R(b, c) true R(Y, d) true R(Y, d) true S(X, c) true S(X, c) true S(X, d) Y = b ∨ Y = b S(X, d) Y = b S(b, d) Y = c ∨ Y = c S(b, d) Y = c S(Y, b) X = d ∨ X = d S(Y, b) X = d R(d, d) (Y = b ∨ Y = b) ∧ (X = d) R(d, d) Y = b ∧ X = d R(b, b) ((X = d ∨ X = d) ∧ (Y = b)) ∨ (X = c) R(b, b) (X = d ∧ Y = b) ∨ (X = c) S(X, b) (X = d ∧ Y = b) ∨ (X = c) S(Y, d) Y = b ∧ X = d By applying τ1 , . . . , τ12 the micro-sequence will end up in the c-table (T3 , ϕ3 ), in Figure 2. Thus (T0 , ϕ0 ), (T1 , ϕ1 ), (T2 , ϕ2 ), (T3 , ϕ3 ) is (the finite part of) a conditional chase sequence associated with (T, ϕ) and Σ. For readability, (T3 , ϕ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 (T0 , ϕ0 ), (T1 , ϕ1 ), . . . , (Tn , ϕn ), . . . and (T0′ , ϕ′0 ), (T1′ , ϕ′1 ), . . . , (Tn′ , ϕ′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. Σ (T, ϕ) for one representative of (Tω , ϕω ) We shall use the notation C hasecond 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. Σ (T, ϕ)) = Σ(Rep(T, ϕ)). Theorem 2. Rep(C hasecond 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, ex- cept 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 haseoblΣ (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 obliv- ious 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 Σ (T ) terminates if and only if C haseΣ Theorem 3. C haseobl (T ) terminates. stand ̂ 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 ξ̂0 , h′0 ξ̂1 , h′1 ξ̂n−1 , h′n−1 ξ̂n , h′n T = T0 ÐÐÐ→ T1 ÐÐÐ→ . . . . . . ÐÐÐÐÐ→ Tn ÐÐÐ→ . . . . Let αi denote the antecedent of ξˆi Then hi (αi ) ⊆ Ti , for all i ∈ ω. Since αi also is the antecedent of ξi , we have that ξ0 , h′0 ξ1 , h′1 ξn−1 , h′n−1 ξn , h′n T = U0 ÐÐÐ→ U1 ÐÐÐ→ . . . . . . ÐÐÐÐÐ→ Un ÐÐÐ→ . . . , where Ui is Ti 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 ξ0 , h′0 ξ1 , h′1 ξn−1 , h′n−1 ξn , h′n T = T0 ÐÐÐ→ T1 ÐÐÐ→ . . . . . . ÐÐÐÐÐ→ Tn ÐÐÐ→ . . . . Let U0 = T0 , and for all i ∈ ω, let Ui+1 = Ti+1 ∪ {β(h′i (x), h′i (z)), H(h′i (x), h′i ( y))}. We claim that ξ̂0 , h′0 ξ̂1 , h′1 ξ̂n−1 , h′n−1 ξ̂n , h′n T = U0 ÐÐÐ→ U1 ÐÐÐ→ . . . . . . ÐÐÐÐÐ→ Un ÐÐÐ→ . . . 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 hi and ξˆi on Ui . Let ξi = α(x, y) → β(x, z). Then ξˆi = α(x, y) → β(x, z), H(x, y). If ξˆi cannot be applied with hi on Ui , there exists an extension hei of hi such that β(hei (x), hei ( z))) and H(hei (x), hei ( y))) are in Ui . Since hei is an exten- sion of hi , it follows that hei (x) = hi (x) and hei (y) = hi (y), meaning that H(hi (x), hi ( y))) ∈ Ui . Because atoms over H are only introduced by the chase, it means that the homomorphism hi has already been applied with ξˆi earlier in the standard chase sequence. But then hi 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 hi 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 hasestand Σ (T ) ter- minates 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. ̂ is weakly acyclic. Lemma 2. Let Σ be a richly acyclic set of tgd’s. Then Σ From Theorem 3, and Lemmas 1 and 2, we can conclude Σ (T ) termi- Corollary 1. Let Σ be a richly acyclic set of tgd’s. Then C haseobl nates 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 condi- tional 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 Σ termi- nates 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.∎ t ϕ(t) R(a, b, b) true R(a, X1 , X2 ) true R(a, X3 , X4 ) X1 = X2 R(a, X5 , X6 ) (X1 = X2 ) ∧ (X3 = X4 ) ... ... In order to obtain the sufficient condition for the conditional chase termi- nation we introduce our second rewriting of a set of tgd’s Σ, called disjoin- ing, 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 occur- rences, except the first, of x in the body with a fresh new universally quanti- fied variable. For instance, if ξ = R(x, y, x), R(y, z, x) → ∃v, w R(x, v, w), then ξ¨ = R(x, y, x1 ), R(y1 , z, x2 ) → ∃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 obliv- ious 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. Σ (T, ϕ) terminates if C haseΣ̈ (T ) terminates. Lemma 3. C hasecond obl 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. Σ (T, ϕ) terminates. Then C hasecond Proof. By Lemma 4, the set Σ̈ is also richly acyclic, and by Lemma 2, the set ̂ is weakly acyclic. By [6], C hasestand (T, true) terminates. By Corollary 1, Σ̈ ̂ Σ̈ C haseobl Σ̈ (T, true) also terminates, and then by Theorem 3, C hasecond Σ (T, ϕ) terminates.∎ 5 Conclusions 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, C- stratified) 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. References 1. Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases. Addison-Wesley (1995) 2. Aho, A.V., Beeri, C., Ullman, J.D.: The theory of joins in relational databases. ACM Trans. Database Syst. 4(3), 297–314 (1979) 3. Beeri, C., Vardi, M.Y.: A proof procedure for data dependencies. J. ACM 31(4), 718–741 (1984) 4. Calı̀, A., Gottlob, G., Kifer, M.: Taming the infinite chase: Query answering under expressive relational constraints. In: KR. pp. 70–80 (2008) 5. Deutsch, A., Nash, A., Remmel, J.B.: The chase revisited. In: PODS. pp. 149–158 (2008) 6. Fagin, R., Kolaitis, P.G., Miller, R.J., Popa, L.: Data exchange: Semantics and query answering. In: ICDT. pp. 207–224 (2003) 7. Grahne, G., Onet, A.: Closed world chasing. In: LID. pp. 7–14 (2011) 8. Hernich, A.: Answering non-monotonic queries in relational data exchange. In: ICDT. pp. 143–154 (2010) 9. Hernich, A., Schweikardt, N.: Cwa-solutions for data exchange settings with target dependencies. In: PODS. pp. 113–122 (2007) 10. Imielinski, T., Jr., W.L.: Incomplete information in relational databases. J. ACM 31(4), 761–791 (1984) 11. Libkin, L.: Data exchange and incomplete information. In: PODS. pp. 60–69 (2006) 12. Marnette, B.: Generalized schema-mappings: from termination to tractability. In: PODS. pp. 13–22 (2009) 13. Meier, M., Schmidt, M., Lausen, G.: On chase termination beyond stratification. PVLDB 2(1), 970–981 (2009) 14. Mendelzon, A.O.: Database states and their tableaux. In: XP2 Workshop on Re- lational Database Theory (1981) 15. Spezzano, F., Greco, S.: Chase termination: A constraints rewriting approach. PVLDB 3(1), 93–104 (2010)