Database Reference
In-Depth Information
for a given Tarski's interpretation
I
T
, where
I
T
is the extension of
I
T
to all FOL
formulae, as defined in Sect.
1.3
.
If
M
AB
is satisfied by the mapping-interpretation
α
, this value of
f(
d
1
,
d
2
,
d
3
)
corresponds to the truth of the normalized implication in the SOtgd of
M
AB
,
φ
Ai
(
x
)
, when
φ
Ai
(
x
)/g
is true. Hence,
r
B
(
t
)/g
is equal to
r
B
(
a
1
,a
3
,b
3
,I
T
(f
2
)(b
1
,a
3
)
)
, i.e., to
r
B
(f (
⇒
r
B
(
t
)
for the assignment
g
derived by substitution
[
x
/
d
]
d
1
,
))
and has to be true as well (i.e.,
I
T
(r
B
(f (
d
2
,
d
3
d
1
,
d
2
,
d
3
)))
=
1 or, equiva-
lently,
f(
d
1
,
d
2
,
d
3
)
∈
α(r
B
)
=
I
T
(r
B
)
).
M
AB
is satisfied by a mapping-interpretation
α
(and hence
α(v
i
)
is an injection function with
α(r
q
)
⊆
α(r
B
)
) then
f(
Consequently, if
d
1
,
d
2
,
d
3
)
∈
r
B
α
∗
(
B
)
,
so that the function
f
α(q
A,i
)
represents the transferring of the tuples in relations
of the source instance databases into the target instance database
B
=
α
∗
(
=
B
)
, ac-
cording to the SOtgd
Φ
of the mapping
.
In this way, for a given R-algebra
α
which satisfies the conditions for the
mapping-interpretations in Definition
11
, we translate a logical representation of
database mappings, based on SOtgds, into an algebraic representation based on re-
lations of the instance databases and the functions obtained from mapping-operads.
M
AB
={
Φ
}:
A
→
B
It is easy to verify that for a
query mapping φ
Ai
(
x
)
⇒
r
B
(
t
)
, a mapping-
interpretation
α
is an R-algebra such that the relation
α(r
q
)
is just equal to the
image of the function
α(q
A,i
)
. The mapping-interpretation of
v
i
is the transfer of
information of this computed query into the relation
α(r
B
)
of the database
B
.
When
α
satisfies this query mapping
φ
Ai
(
x
)
⇒
r
B
(
t
)
, then
α(r
q
)
⊆
α(r
B
)
(with
proof in Proposition
4
) and, consequently, the function
α(v
i
)
is an injection, i.e., the
inclusion
of
α(r
q
)
into
α(r
B
)
.
Proposition 2
Let φ
Ai
(
x
)
⇒
r
B
(
t
) be an implication in the normalized SOtgd
∃
f
Ψ of a mapping
M
AB
:
A
→
B
,
where
t
is a tuple of terms with variables
in
x
M
AB
) be the operad's operation
of this implication obtained by MakeOperads algorithm
,
equal to the expression
(e
=
x
1
,...,x
m
.
Let q
i
∈
MakeOperads(
O(r
1
,...,r
k
,r
B
)
,
and let S be the set of sets that contain the pairs
of mutually equal
(
joined
)
free variables in q
i
as specified in Definition
11
.
Then
,
for a given Tarski's interpretation of all FOL formulae in Ψ and
,
extended
from it
,
a mapping-interpretation α in Definition
11
(
such that for each
1
⇒
(_ )(
t
))
∈
≤
i
≤
k
,
ar(r
i
)
R
i
=
U
\
I
T
(r
i
) if the place symbol (_ )
i
∈
q
i
is preceded by negation operator
¬
;
I
T
(r
i
) otherwise
),
the following is true
:
If for every tuple
R
k
such that
{
d
1
,...,
d
k
∈
R
1
×···×
π
j
h
(
d
j
)
=
π
n
h
(
d
n
)
|
{
(j
h
,j),(n
h
,n)
}∈
S
}
is true
,
we have that α(q
i
)(
d
1
,...,
d
k
)
∈
I
T
(r
B
)
,
then
I
T
(
∀
x
(φ
Ai
(
x
)
⇒
r
B
(
t
)))
=
1,
and vice versa
.
Proof
We have to show that for every
d
1
,...,
d
k
∈
R
1
×···×
R
k
such that
{
π
j
h
(
d
j
)
=
π
n
h
(
d
n
)
|{
(j
h
,j),(n
h
,n)
}∈
S
}
is true, with
d
=
Cmp(S,
d
1
,...,
,
I
T
(φ
Ai
(
x
)/g
d
k
)
and the assignment
g
derived from the substitution
[
x
/
d
]
⇒
r
B
(
t
)/g)
1.
If
I
T
(φ
Ai
(
x
)/g)
=
=
0 then it is satisfied. Thus, we have to consider only the fol-
lowing cases:
