Database Reference
In-Depth Information
R such that
K
? In order to prove the proposition, we reduce this problem to the
complement of the problem of checking whether a Boolean FO formula admits an FO-
rewriting over the canonical universal solution or the core. That is, we show that for each
schema R and domain-independent Boolean FO formula
|
=
ϕ
ϕ
over R, one can compute a
relational mapping
M
=(R
s
,
R
t
,
Σ
st
) and a Boolean FO formula
θ
over R
t
such that the
following two facts are equivalent:
1. There is an instance
K
of R such that
K
|
=
ϕ
.
2.
θ
is
not
FO-rewritable over the canonical universal solution (respectively, the core)
under
M
.
Take an arbitrary schema R and a domain-independent Boolean FO formula
ϕ
over R.
We show how to construct
and R. First of all, we prove in the follow-
ing section (
Proposition 7.16
) that there is a relational mapping
M
and
θ
from
ϕ
M
=(R
s
,
R
t
,
Σ
st
) and a
domain-independent Boolean FO formula
ψ
nr
, such that
ψ
nr
is FO-rewritable neither over
M
. Without loss of generality we
assume that R
s
and R contain no relation symbols in common. With the help of
the canonical universal solution nor over the core under
M
and
ψ
nr
we can construct
M
=(R
s
,
R
t
,
Σ
st
) and
θ
as follows:
•
R
s
consists of all the relation symbols that are either in R or in R
s
(recall that R and R
s
are assumed to be disjoint).
•
R
t
consists of all the relation symbols that are either in R
or in R
t
,whereR
is a disjoint
copy of R;thatis,ifR =
and
R
i
and
R
i
have the
same arity. Further, we assume without loss of generality that R
has no relation symbols
in common with either R
t
or R
s
.
•
Σ
st
is defined as
then R
=
R
1
,...,
R
n
}
{
R
1
,...,
R
n
}
{
Σ
st
∪{
R
i
(
x
)
R
i
(
x
)
→
|
1
≤
i
≤
n
}
.
Σ
st
, that relate source relation symbols in R
s
with
target relation symbols in R
t
in a way that is consistent with
That is,
Σ
st
consists of the st-tgds in
M
,plusasetof
copying
st-
tgds that transfer the source content of each relation symbol in R into the corresponding
target relation symbol in R
.
ϕ
→
ψ
nr
,where
ϕ
is the Boolean FO formula over R
that is
•
Finally,
θ
is defined as
by replacing each occurrence of the relation symbol
R
i
with
R
i
,for
obtained from
ϕ
every 1
≤
i
≤
n
.
We prove next that there exists an instance
K
of R such that
K
|
=
ϕ
if and only if
θ
is
not rewritable over the canonical universal solution (respectively, over the core) under
M
.
Assume first that for every instance
K
of R it is the case that
K
|
=
ϕ
. Then for every
ϕ
. Assume otherwise.
Then the restriction
T
of
T
to the relation symbols in R
also satisfies
M
|
source instance
S
of R
s
, and solution
T
for
S
under
,wehave
T
=
ϕ
is
domain-independent), and, therefore, the instance
K
of R that is obtained from
T
by setting
R
j
to coincide with the interpretation of
R
j
in
T
, for each 1
ϕ
(since
≤
j
≤
n
, satisfies
ϕ
,whichis
