Database Reference
In-Depth Information
Next, suppose the constraint is of the form
ϕ
1
∧···∧
ϕ
k
−→
η
,
where
ϕ
1
−→
ψ
1
,
ϕ
2
−→
ψ
2
, ...,
ϕ
k
−→
ψ
k
∈
Σ
12
and
ρ
∧
η
= cpl
D
2
(
ψ
1
∧···∧
ψ
k
).Pick
ϕ
1
∧···∧
ϕ
k
[
f
,
a
].Then
T
2
|
ψ
1
∧···∧
ψ
k
[
f
,
a
], and by
Lemma 13.14
(1),
a
such that
T
1
|
=
=
[
f
,
a
] holds.
Finally, assume the constraint is of the form
η
ϕ
1
∧···∧
ϕ
k
∧
h
(
α
)
−→
h
(
ψ
)
,
where
ϕ
i
−→
ψ
i
and
ρ
∧
η
are like above,
π
∧
α
−→
ψ
∈
Σ
23
,and
h
is a homomorphism
)[
f
,
a
].Then
T
2
|
ψ
1
∧···∧
ψ
k
[
f
,
a
]
from
π
into
ρ
.Pick
a
such that
T
1
|
=
ϕ
1
∧···∧
ϕ
k
∧
h
(
α
=
[
f
,
a
]. Hence
T
2
|
)[
f
,
a
].As
h
(
)[
f
,
a
] holds,
and by
Lemma 13.14
(1) we get
T
2
|
=
ρ
=
h
(
π
α
)[
f
,
a
] and hence
T
3
|
)[
f
,
a
].
we have
T
2
|
=
h
(
π
)
∧
h
(
α
=
h
(
ψ
f , there exists an inter-
Lemma 19.23
If
(
T
1
,
T
3
)
∈
M
13
with a witnessing valuation
mediate tree T
2
such that
(
T
1
,
T
2
)
∈
M
12
and
(
T
2
,
T
3
)
∈
M
23
with the same witnessing
f.
valuation
Proof
Let
(
a
)
ϕ
(
a
,
b
)[
f
] for some
b
}
Δ
=
{
ψ
(
x
,
y
)
−→
ψ
(
x
)
∈
Σ
12
and
T
1
|
=
ϕ
.
(
a
,
b
) we mean formulae where variables
x
,
y
are substituted by
a
,
b
,butthe
functions are not evaluated. In other words, these formulae contain ground terms. By
ϕ
By
ψ
(
a
),
ϕ
(
a
,
b
)[
f
] we denote the formula where functions are evaluated according to
f
. Recall
that a tree
T
2
|
=
D
2
is a solution for
T
1
with witnessing valuation
f
if and only if
=(
δ
∈
Δ
δ
)[
f
] (
Lemma 12.1
). We shall construct
T
2
from mrg
D
2
(
δ
∈
Δ
δ
T
2
|
) and check
that it has the desired properties. The proof essentially relies on the simple observation that
for each pattern
ξ
(
z
) and each tuple
c
(
z
)
(
c
)
.
(19.5)
First, we need to see that mrg
D
2
(
δ
∈
Δ
δ ) is not
⊥
. This can only happen if the pure
(
c
)=
mrg
D
2
ξ
mrg
D
2
ξ
pattern underlying
δ
∈
Δ
δ
is not satisfiable wrt to
D
2
even when attributes are ignored.
But then, using the fact that
D
2
is nested-relational, we conclude easily that there exists a
pattern
which is not satisfiable wrt
D
2
even when attributes are ignored. Thanks to
the preprocessing phase, we then have
δ
∈
Δ
δ
=
⊥
. In this case there is a dependency
ϕ
(
x
,
y
)
−→
(
a
,
b
)[
f
].As
⊥
in
Σ
12
such that
T
1
|
=
ϕ
Σ
13
also contains
ϕ
(
x
,
y
)
−→ ⊥
,weget
T
3
|
=
⊥
,
which is a contradiction. Hence, the pure pattern underlying
δ
∈
Δ
δ
is satisfiable (up to the
values of attributes).
Next, we check that
f
satisfies all the equalities in mrg
D
2
(
δ
∈
Δ
δ
). Pick an equality
t
=
t
. If it was already present in some (
π
∧
α
)(
a
)
∈
Δ
, then there exists
ϕ
−→
π
,
α
∈
Σ
12
(
a
,
b
)[
f
] for some
b
, and some iteration of the outer loop adds constraint
such that
T
1
|
=
ϕ
(
a
)[
f
], which means
ϕ
−→
α
to
Σ
13
. Since the pair (
T
1
,
T
3
) satisfies
Σ
13
,wehave
T
3
|
=
α
that
t
=
t
holds.
