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

≤