Database Reference
In-Depth Information
added to st-tgds to obtain a language capable of expressing the composition of such depen-
dencies. We know that C
OMPOSITION
(
M
23
) is in NP. By Fagin's theorem in finite
model theory, the class NP has a logical characterization as the class of problems defined
in existential second-order logic, i.e., by formulae of the form
M
12
,
∃
R
1
...
∃
R
n
ϕ
,wherethe
R
i
's
range over sets or relations, and
is an FO formula.
So it appears that some sort of second-order quantification is necessary to capture rela-
tional composition. In the following section we confirm this by presenting an extension of
st-tgds with existential second-order quantification that gives rise to the
right
mapping
language for dealing with the composition operator. As hinted in an earlier example in this
section, the existential quantification is not over arbitrary relations but rather functions,
such as, for instance, the function from student names to student ids in
Example 19.2
.
ϕ
19.3 Extending st-tgds with second-order quantification
In the previous section, we showed that first-order logic is not expressive enough to rep-
resent the composition of mappings given by st-tgds. The bounds on the complexity of
composition suggested that the existential fragment of second-order logic can be used to
express the composition of this type of mappings. In this section, we go deeper into this,
and show that the extension of st-tgds with existential second-order quantification is the
right language for composition.
Our quantification will be over functions, like the function that associates a student id
with a student name in
Example 19.2
. These functions will be used to build
terms
which
will then be used in formulae. Recall that terms are built as follows:
•
every variable is a term; and
•
if
f
is an
n
-ary function symbol, and
t
1
,...,
t
n
are terms, then
f
(
t
1
,...,
t
n
) is a term.
For instance, if
f
is a unary function and
g
is a binary function, then
f
(
x
),
f
(
f
(
x
)),
g
(
f
(
x
)
,
x
) are all terms.
Now we are ready to define the extended class of dependencies used in mappings that
are closed under composition.
Definition 19.4 Given schemas R
s
and R
t
with no relation symbols in common, a
second-
order tuple-generating dependency from
R
s
to
R
t
(SO tgd) is a formula of the form:
f
m
ϕ
n
→
ψ
n
)
,
∃
f
1
···∃
∀
x
1
(
ϕ
1
→
ψ
1
)
∧···∧∀
x
n
(
where
1. each
f
i
(1
≤
i
≤
m
) is a function symbol,
2. each formula
n
) is a conjunction of relational atoms of the form
P
(
y
1
,...,
y
k
)
and equality atoms of the form
t
=
t
,where
P
is a
k
-ary relation symbol of R
s
,
y
1
,
...
,
y
k
are (not necessarily distinct) variables in
x
i
,and
t
,
t
are terms built from
x
i
and
f
1
,
...
,
f
m
,
ϕ
i
(1
≤
i
≤
