Database Reference
In-Depth Information
3. Each
ψ
i
is a conjunction of atomic formulae
r
B
(t
1
,...,t
m
)
where
r
B
∈
S
B
is an
m
-ary relational symbol of schema
B
and
t
1
,...,t
m
are terms based on
x
i
,
f
and
constants.
4. Each variable in
x
i
appears in some atomic formula of
φ
i
.
Notice that each constant
a
in an atom on the left-hand side of implicat
io
ns must
be substituted by a new fresh variable
y
i
and by adding a conjunct
(y
i
=
a)
on the
left-hand side of this implication, so that such atoms will have only the variables
(condition 2 above). For the empty set of tgds, we will use the SOtgd tautology
r
. The forth condition is a “safety” condition, analogous to that made for
the (first-order) tgds. It is easy to see that every tgd is equivalent to one SOtgd
without equalities. For example, let
σ
be the tgd
∅
⇒
r
∅
⇒
∃
y
1
...
∃
y
n
ψ
B
(x
1
,...,x
m
,y
1
,...,y
n
))
. It is logically equivalent to the following
SOtgd without equalities, which is obtained by Skolemizing existential quantifiers
in
σ
:
∀
x
1
...
∀
x
m
(φ
A
(x
1
,...,x
m
)
f
n
∀
x
m
φ
A
(x
1
,...,x
m
)
∃
f
1
...
∃
x
1
...
∀
⇒
ψ
B
x
1
,...,x
m
,f
1
(x
1
,...,x
m
),...,f
n
(x
1
,...,x
m
)
.
Given a finite set
S
of tgds of an inter-schema mapping in Definition
3
, we can find a
single
SOtgd that is equivalent to
S
by taking, for each tgd
σ
in
S
, a conjunct of the
SOtgd to capture
σ
as described above (we use disjoint sets of function symbols in
each conjunct, as before). Based on these observations, we can define the algorithm
for transformation of a given set of tgds into an single SOtgd:
Transformation algorithm
TgdsToSOtgd(S)
Input.
Aset
S
of tgds from a schema
A
into a schema
B
,
=
∀
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
)
,
S
⇒∃
∀
⇒
where
y
i
⊆
x
i
and possibly
z
i
the empty set, for 1
≤
i
≤
n
.
Output.
ASOtgd
•
(
Create the set of implications from tgds
)
Initialize
S
AB
to be the empty set.
Put each of the
n
implications of tgds in
S
,
φ
A,i
(
x
i
)
⇒∃
z
i
ψ
B,i
(
y
i
,
z
i
)
in
S
AB
.
•
(
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
=
z
1
,...,z
k
≥
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
,
k
≤
j
≤
k
):
φ
A,i
(
x
)
∧
z
1
f
i,
1
(
x
)
∧···∧
z
k
f
i,k
(
x
)
⇒
.
=
.
=
ψ
B,i
(
y
,
z
).
•
(
Remove the variables originally quantified
)
For each implication
χ
i
in
S
AB
constructed in the previous step, perform an
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
