Database Reference
In-Depth Information
in C
ONST
. Notice that a potential justification differs from a
justification, as defined in the previous section, since
∪
V
AR
such that
|
a
|
=
|
x
|
ϕ
(
a
) does not need to be satisfied.
Intuitively, (
σ
,
a
) is used to justify any tuple in
ψ
(
a
,
v
), provided the atoms in
ϕ
(
a
) are
already justified.
By slightly abusing notation, we denote by
J
M
the set of all potential justifications
under
M
, and by
K
M
the set of all pairs of the form (
j
,
z
),where:
•
j
=(
σ
,
a
) is a potential justification in
J
M
with
σ
=
ϕ
(
x
)
→∃
y
ψ
(
x
,
y
),and
•
z
is a variable in
y
.
As we did before, we assign values to the existentially quantified variables of (st-)tgds by
a mapping
α
:
K
M
→
C
ONST
∪
V
AR
. For each
j
=(
σ
,
a
) in
J
M
with
σ
of the form
ϕ
(
x
)
→∃
y
ψ
(
x
,
y
),let
B
α
(
j
) :=
ψ
(
a
,
α
(
y
)),where
α
(
y
) is obtained from
y
by replacing
each variable
z
in
y
with
α
(
j
,
z
).
V
AR
, corresponds to the following “controlled”
modification of the standard chase procedure (as defined in
Section 5.3
):
The
α
-chase
,for
α
:
K
M
→
C
ONST
∪
1. An
is a (finite or infinite) sequence
S
0
,
S
1
,...
of
instances such that: (i)
S
0
=
S
; and (ii) for each
i
α
-chase sequence for S under
M
≥
0 it is the case that
S
i
+1
is the result
of applying to
S
i
an
α
-chase step
given by a tgd
σ
in
Σ
st
∪
Σ
t
as follows:
Let
σ
be a tgd in
Σ
st
∪
Σ
t
of the form
ϕ
(
x
)
→∃
y
ψ
(
x
,
y
).Then
σ
can be applied to
instance
S
i
, if there is a tuple
a
of elements in D
OM
(
S
i
) with
|
a
|
=
|
x
|
such that
S
i
|
=
B
α
(
j
) that does not belong
to
S
i
.The
result
of this application is the instance
S
that extends
S
i
with every fact in
B
α
(
j
).
3. An
ϕ
(
a
),andif
j
=(
σ
,
a
) then there is at least one atom in
α
-chase sequence for
S
under
M
is
successful
, if it is finite and it cannot be extended
to a longer
α
-chase sequence for
S
under
M
.Thatis,if
S
m
is the last instance in the
sequence then no tgd in
Σ
st
∪
Σ
t
can be further applied to
S
m
. If this is the case, we
call
S
m
the
result
of the
-chase sequence. As usual, we identify this result with its
restriction to the relation symbols in R
t
.
α
It is easy to prove that, in the absence of egds, the usual chase for a source instance
S
under
M
always coincides with the
α
-chase, when
α
:
K
M
→
C
ONST
∪
V
AR
is the
mapping that assigns a distinct null value to each pair (
j
,
z
) in
K
M
. That is, we can see
the
-chase as a
refinement
of the chase previously defined in
Section 5.3
. Nevertheless,
there is a big difference in motivation between the two variations of chase. While the usual
chase is applied in data exchange to compute a universal solution, we use the
α
-chase to
show that all facts in a solution satisfy the requirements (A1) and (A2) formalized in the
previous section.
As in the case without target dependencies, in order to define CWA solutions it will be
convenient to introduce the notion of CWA presolutions. Notice that at this point we again
include the egds.
α
