=Paper=
{{Paper
|id=None
|storemode=property
|title=On Conditional Chase Termination
|pdfUrl=https://ceur-ws.org/Vol-749/paper12.pdf
|volume=Vol-749
|dblpUrl=https://dblp.org/rec/conf/amw/GrahneO11
}}
==On Conditional Chase Termination==
https://ceur-ws.org/Vol-749/paper12.pdf
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)