Database Reference
In-Depth Information
If
t
=
t
was introduced as a result of merging some nodes of
ψ
(
a
)
ψ
(
a
)
,
∈
Δ
,then
ψ
(
a
) has a subformula
(
t
),
•
ψ
(
a
) has a subformula
σ
(
t
) and
σ
ψ
(
a
) is the same,
•
the path from
r
to this subformula in
ψ
(
a
) and in
σ
1
σ
2
...
σ
n
, with
σ
n
=
σ
,
•
for all
j
either
σ
j
→
...
σ
j
+1
...
or
σ
j
→
...
σ
j
+1
?
...
in DTD
D
2
.
ϕ
−→
ψ
∈
Σ
In one of the iterations of the outer loop the algorithm processes
ϕ
−→
ψ
,
12
such that
T
1
|
= ϕ(
a
,
b
)[
f
] and
T
1
|
= ϕ
(
a
,
b
)[
f
] for some
b
,
b
. By merging ψ and ψ
with
respect to
D
2
, the algorithm introduces an equality
t
=
t
such that by substituting variables
of
t
according to
a
we get
t
, by substituting variables of
t
according to
a
we get
t
,anda
constraint of the form
ϕ
∧
ϕ
−→
t
=
t
∧
...
is added to
Σ
13
. Like before, we conclude that
t
=
t
holds.
Thus
f
satisfies all the equalities in mrg
D
2
(
δ
∈
Δ
δ
) and we can construct a tree
T
2
from
mrg
D
2
(
δ
∈
Δ
δ
) in the usual way by evaluating the terms according to
f
. Since each
δ
∈
Δ
is complete, so is
δ
∈
Δ
δ
=(
δ
∈
Δ
δ
)[
f
].This
. Hence, by
Lemma 13.15
,
T
2
|
=
D
2
and
T
2
|
implies that (
T
1
,
T
2
)
.
It remains to verify that (
T
2
,
T
3
)
∈
M
12
∈
M
23
. Pick a dependency (
π
∧
α
)(
x
,
y
)
−→
ψ
(
x
)
)(
a
,
b
)[
f
] and let
g
:
from
Σ
23
. Suppose that
T
2
|
=(
π
∧
α
π
→
T
2
be a witnessing ho-
momorphism. Recall that
uses each variable exactly once, and it does not use func-
tion symbols. In consequence,
g
can be interpreted as a homomorphism from
π
π
to the
pure pattern underlying mrg
D
2
(
δ
∈
Δ
δ
,thevalue
g
(
z
) under
f
is equal to the value of
z
according to
a
,
b
. Examining the definition of
mrg
D
2
, it is easy to see that
g
can also be seen as a homomorphism into
), such that for each variable
z
in
π
ρ
,where
ρ
∧
η
= mrg
D
2
(
ψ
1
(
a
1
)
∧···∧
ψ
k
(
a
k
)) for some
ψ
1
(
a
1
)
,...,
ψ
k
(
a
k
)
∈
Δ
,
k
≤
π
.Bythe
definition of
Δ
,thereexist
ϕ
1
−→
ψ
1
,
ϕ
2
−→
ψ
2
, ...,
ϕ
k
−→
ψ
k
∈
Σ
12
such that for some
b
1
,...,
b
k
,
T
1
|
ϕ
i
(
a
i
,
b
i
)[
f
] for all
i
.By
(19.5)
,wehave
ρ
∧
η
=(
ˆ
ρ
∧
ˆ
)(
a
1
,...,
a
k
) for
=
η
ρ
∧
ˆ
ˆ
ψ
1
∧···∧
ψ
k
). Using again the fact that
η
= mrg
D
2
(
π
uses each variable exactly once
and does not use function symbols, we lift
g
:
π
→
ρ
to a homomorphism
g
:
π
→
ρ
ˆ
such
that
g
(
z
) evaluated according to
f
,
a
1
,...,
a
k
equals
z
evaluated according to
a
,
b
.
(19.6)
Consequently,
Σ
13
contains the dependency
ϕ
1
∧···∧
ϕ
k
∧
g
(
α
)
→
g
(
ψ
). Recall that
T
1
|
=
ϕ
i
(
a
i
,
b
i
)[
f
] for
i
= 1
,
2
,...,
k
and
g
(
)[
f
,
a
1
,...,
a
k
] holds by
(19.6)
and by the assumption
α
(
a
,
b
) holds under
f
. Hence,
T
3
|
)[
f
,
a
1
,...,
a
k
], which implies
T
3
|
(
a
)[
f
].
that
α
=
g
(
ψ
=
ψ
