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
Search WWH ::




Custom Search