Database Reference
In-Depth Information
u
,
v
, the notation
ξ
[
v
/
u
] is used for a variable substitution such that (
ξ
[
v
/
u
])(
w
)=
v
if
ξ
(
w
)=
u
,and(
ξ
[
v
/
u
])(
w
)=
ξ
(
w
) otherwise. Now compute a variable substitution
ρ
by
using the procedure below.
1:
D
:=
u
1
,
u
2
,...,
u
n
}
2:
V
:= set of variables mentioned in
{
ϕ
(
x
,
y
)
:= identity variable substitution with domain
V
4:
while there exist
i
ρ
3:
D
such that
u
i
=
v
i
do
∈{
1
,...,
}
and
u
,
v
∈
[
v
i
/
u
i
]
ρ
:=
ρ
5:
D
:=
{
ρ
(
w
)
|
w
∈
D
}
6:
7:
end while
It is straightforward to prove that
ρ
can be computed in polynomial time, that
ρ
unifies
{
u
1
,
u
2
,...,
u
n
}
in the sense that
ρ
(
u
1
)=
ρ
(
u
2
)=
···
=
ρ
(
u
n
),andthat
ρ
is the most
general unifier for
{
u
1
,
u
2
,...,
u
n
}
, in the sense that for every variable substitution
ξ
that
unifies
{
u
1
,
u
2
,...,
u
n
}
, there exists a variable substitution
λ
such that
λ
◦
ρ
=
ξ
. Finally,
Σ
st
the following LAV st-tgd:
include in
ϕ
(
ρ
(
x
)
,
ρ
(
y
))
→∃
z
ψ
(
ρ
(
x
)
,
z
)
.
Notice that the previous dependency is a LAV st-tgd as
ρ
unifies
{
u
1
,
u
2
,...,
u
n
}
and
ϕ
(
x
,
y
)
mentioned only the predicate symbol
U
.
We show next that
Σ
st
and
M
can be defined by a set of LAV st-tgds if and only if
Σ
st
Σ
st
and
define the same mapping from R
s
to R
t
.Clearly,if
Σ
st
define the same mapping
from R
s
to R
t
,then
M
can be defined by a finite set of LAV st-tgds. To prove the opposite
M
be the
M
direction, assume that
can be defined by a finite set of LAV st-tgds, and let
Σ
st
. Clearly, (
S
,
T
)
∈M
.Forthe
∈M
implies (
S
,
T
)
mapping from R
s
to R
t
defined by
∈M
, and for every fact
U
(
a
) mentioned in
S
,let
S
U
(
a
)
be an
instance of R
s
consisting only of the fact
U
(
a
). Then given that
converse, assume that (
S
,
T
)
M
is definable by a set of
LAV st-tgds, we have that
M
is closed under union by
Theorem 21.5
and, hence, to prove
that (
S
,
T
)
∈M
, it is enough to prove that (
S
U
(
a
)
,
T
)
∈M
for every fact
U
(
a
) mentioned
in
S
. In order to prove that (
S
U
(
a
)
,
T
)
∈M
, we have to show that (
S
U
(
a
)
,
T
)
|
=
Σ
st
. Thus,
assume that
ϕ
(
x
,
y
)
→∃
z
ψ
(
x
,
z
) is a st-tgd in
Σ
st
and that
σ
is a variable assignment such
that
S
U
(
a
)
|
=
ϕ
(
σ
(
x
)
,
σ
(
y
)).Thenwehavetoprovethat
T
|
=
∃
z
ψ
(
σ
(
x
)
,
z
). Given that
S
U
(
a
)
|
=
ϕ
(
σ
(
x
)
,
σ
(
y
)), we have by definition of
S
U
(
a
)
that:
(
x
,
y
)=
U
(
u
1
)
∧
∧···∧
U
(
u
n
)
,
ϕ
U
(
u
2
)
and that
σ
(
u
1
)=
σ
(
u
2
)=
···
=
σ
(
u
n
)=
a
.Let
ρ
be defined as shown previously for the
st-tgd
(
x
,
z
),and
f
be a one-to-one function that assigns a fresh variable to
each constant. Then we have that (
f
ϕ
(
x
,
y
)
→∃
z
ψ
◦
σ
) is a unifier for
{
u
1
,
u
2
,...,
u
n
}
and, hence, there
exists a variable substitution
λ
such that (
λ
◦
ρ
)=(
f
◦
σ
) (since
ρ
is a most general unifier