Database Reference
In-Depth Information
respectively, a partial mapping and a sequence of instances over
R
s
,
R
t
that satisfy the
α
i
-chase sequence for
S
under
α
i
:
hypothesis. That is, (1)
C
i
is an
M
, for each
K
M
→
C
ONST
∪
V
AR
that extends
α
i
,and(2)
L
i
⊆
S
∪
T
.If
L
i
|
=
Σ
st
∪
Σ
t
, then the inductive
construction simply stops. Otherwise, we construct from
α
i
and
C
i
a partial mapping
α
i
+1
:
K
M
→
C
ONST
∪
V
AR
and a sequence
C
i
+1
=(
L
1
,...,
L
i
,
L
i
+1
) of instances of
R
s
,
R
t
as
follows.
Since
L
i
. Notice
that since
L
i
⊆
S
∪
T
, the dependency σ cannot be an egd (otherwise,
T
|
= σ,whichisa
contradiction since
T
is a solution for
S
). Thus,
|
=
Σ
∪
Σ
t
there must be a dependency
σ
∈
Σ
∪
Σ
t
such that
L
i
|
=
σ
st
st
σ
is an (st)-tgd.
Assume without loss of generality that
σ
=
ϕ
(
x
)
→∃
y
ψ
(
x
,
y
)
,
where
y
=(
y
1
,...,
y
k
). Thus, (1)
L
i
|
=
ϕ
(
a
) for some tuple
a
of elements in C
ONST
∪
V
AR
such that
|
a
|
=
|
x
|
,and(2)
L
i
|
=
ψ
(
a
,
v
) for every tuple
v
of elements in C
ONST
∪
V
AR
such
that
|
v
|
=
|
y
|
.Since
L
i
⊆
S
∪
T
it is the case that
T
|
=
ϕ
(
a
).But
T
is a solution for
S
,and
hence
T
|
=
ψ
(
a
,
w
) for some tuple
w
of elements in C
ONST
∪
V
AR
such that
|
w
|
=
|
y
|
.
Assuming
w
=(
w
1
,...,
w
k
), we define the partial mapping
α
i
+1
:
K
M
→
C
ONST
∪
V
AR
as follows. Let (
j
,
z
) beapairin
K
M
. Then:
⎧
⎨
w
,
if
j
=(
σ
,
a
) and
z
=
y
,for1
≤
≤
k
α
i
+1
(
j
,
z
)=
α
i
(
j
,
z
)
,
if
j
=(
σ
,
a
) and
α
i
(
j
,
z
) is defined
⎩
undefined
,
otherwise.
Now we let
C
i
+1
be (
L
1
,...,
L
i
,
L
i
+1
),where
L
i
+1
:=
L
i
∪B
α
i
+1
(
σ
,
a
).Thatis,
L
i
+1
extends
L
i
with every atom in
(
a
,
w
). Notice that by the induction hypothesis and the choice of
w
, we can immediately conclude
L
i
+1
is contained in
S
ψ
∪
T
. From the induction hypothesis
α
i
+1
-chase sequence for
S
under
α
i
+1
:
it also easily follows that
C
i
+1
is an
M
, for each
K
M
→
C
ONST
∪
V
AR
that extends
α
i
+1
.
α
i
-application of a tgd produces at least one new atom, we
conclude that the iterative construction of
Since
T
is finite and each
α
i
and
C
i
as described above stops after some
k
number
i
≥
0 of atoms (in fact
i
≤|
D
OM
(
T
)
|
for some
k
that only depends on the map-
ping). In particular, if
T
. In order to finish
the proof it will be sufficient to prove the following: (1)
L
i
is the result of a successful
α
C
i
=(
L
1
,...,
L
i
) then
L
i
|
=
Σ
st
∪
Σ
t
and
L
i
⊆
S
∪
V
AR
,and(2)if
T
is the restriction of
L
i
to the relation symbols in R
t
,then
T
=
T
. We prove this below.
First, we know that
L
i
is the result of a successful α-chase sequence, for each mapping
-chase sequence for
S
under
M
, for some mapping
α
:
K
M
→
C
ONST
∪
α
:
K
M
→
C
ONST
∪
V
AR
that extends
α
i
+1
. This proves (1). Second,
L
i
|
=
Σ
st
∪
Σ
t
,and
hence
T
is a solution for
S
under
. It follows that there exists a homomorphism from
T
into
T
,since
T
is a universal solution for
S
.Since
L
i
⊆
S
∪
T
,wehave
T
⊆
T
. It follows
that
T
=
T
; otherwise there would be a homomorphism from
T
into a proper subinstance
of itself, which contradicts the fact that
T
is a core. This proves (2).
M
Recall that in the absence of target dependencies the canonical universal solution was,
