Database Reference
In-Depth Information
where
t
is a tuple of terms with variables in
x
and
r
∈
S
A
,
is logically equivalent to
∀
∧¬
⇒
the FOL sentence
x
((φ
A
(
x
)
r(
t
))
r
(
0
,
1
))
.
Pr
oo
f
F
or
any assignment
g
, the formula
r
(
0
,
1
)
cannot be satisfied because
g(
0
),g(
1
)
=
0
,
1
∈
R
=
=
I
T
(r
)
, so that
φ
A
(
x
)
⇒
r(
t
)
is logically equival
en
t
t
o
the formula
φ
A
(
x
)
⇒
(r(
t
)
∨
r
(
0
,
1
))
, i.e., to the formul
a
¬
φ
A
(
x
)
∨
r(
t
)
∨
r
(
0
,
1
)
,
or equivalently, to the formu
la
¬
(φ
A
(
x
)
∧¬
r(
t
))
∨
r
(
0
,
1
)
, and hence to the for-
mula
(φ
A
(
x
)
∧¬
r(
t
))
⇒
r
(
0
,
1
)
.
Based on these considerations, we can define the following algorithm for trans-
formation of a given set of tgds into a single SOtgd:
Transformation algorithm
TgdsToConSOtgd(Σ
tgd
A
)
Input.
Aset
Σ
egd
A
of tgds of a given schema
A
,
A
=
∀
x
1
φ
A,
1
(
x
1
)
⇒∃
z
1
ψ
B,
1
(
y
1
,
z
1
)
,...,
∀
x
n
φ
A,n
(
x
n
)
⇒
z
n
ψ
B,n
(
y
n
,
z
n
)
,
Σ
tgd
where
y
i
⊆
x
i
and possibly
z
i
is the empty set, for 1
≤
i
≤
n
.
Output.
An SOtgd
1. (
Create the set of implications from tgds
)
Initialize
S
AB
to be the empty set.
Put each of the
n
implications of tgds in
Σ
tgd
A
,
φ
A,i
(
x
i
)
⇒∃
z
i
ψ
B,i
(
y
i
,
z
i
)
,in
S
AB
.
2. (
Eliminate the existential quantifiers by Skolemization
)
Repeat the following as far as possible:
For each implication
χ
in
S
AB
of the form
φ
A,i
(
x
)
⇒∃
z
ψ
B,i
(
y
,
z
)
with
z
=
1, eliminate this
χ
from
S
AB
and add the following implication
in
S
AB
(by introducing the set of new functional symbols
f
i,j
,for1
z
1
,...,z
k
,
k
≥
≤
j
≤
k
):
φ
A,i
(
x
)
∧
z
1
f
i,
1
(
x
)
∧···∧
z
k
f
i,k
(
x
)
⇒
.
=
.
=
ψ
B,i
(
y
,
z
).
3. (
Remove the variables originally quantified
)
For each implication
χ
i
in
S
AB
, constructed in the previous step, perform the
elimination of the variables
z
i
from this implication as far as possible: Select
an equality
z
j
.
=
f
i,j
(
x
)
that was generated in the previous step. Remove the
.
=
equality
z
j
f
i,j
(
x
)
from
χ
i
and replace every remaining occurrence of
z
j
in
χ
by
f
i,j
(
x
)
.
4. (
Normalize the tgds
)
Each implication
χ
in
S
AB
has the form
φ
A,i
(
x
i
)
k
⇒∧
1
r
j
(
t
j
)
where every mem-
ber of
x
i
is a universally quantified variable, and each
t
j
,for1
≤
≤
k
,isa
sequence (a tuple) of terms over
x
i
. We then replace each such implication
χ
in
S
AB
with
k
implications
φ
A,i
(
x
i
)
⇒
r
1
(
t
1
),...,φ
A,i
(
x
i
)
⇒
r
k
(
t
k
)
.
5. (
Convert the tgds
)
Remove each implication
χ
in
S
AB
of the form
φ
A
,i
(
x
i
)
j
r
j
(
t
j
)
from
S
AB
and
add the implication
(φ
A,i
(
x
i
)
∧¬
r
j
(
t
j
))
⇒
r
(
0
,
1
)
in
S
AB
.
⇒
