Database Reference
In-Depth Information
ω
TA
,is
It is easy to verify that
inl
A
=
η
A
:
A
→
EA
, where
EA
=
A
obtained from the natural transformation
η
:
I
DB
−→
E
. Another example is the
E
2
A
definition of the operation
μ
A
:
−→
EA
by inductively extending
inr
A
:
−→
Σ
D
EA
EA
along the identity
id
EA
of the object
EA
(consider the first dia-
gram, substituting
A
and
B
with the object
EA
ω
TA
,
f
with
id
EA
and
h
D
with
inr
A
). Inductively derived
η
A
(which is a monomorphism),
μ
A
(which is
an identity, i.e.,
μ
A
=
=
A
id
EA
, because
E
2
E
) and the endofunctor
E
, define the
monad
(E,η,μ)
, i.e., this monad is inductively extended in a
natural way
from the
signature endofunctor
Σ
D
=
T
:
=
DB
.
So the “DB-syntax” monad
(E,η,μ)
, where
E
=
I
DB
ω
◦
T
=
I
DB
T
◦
ω
is an inductive algebraic extension of the “coalgebraic”
observation based
power-
view monad
(T,η,μ)
.
With this result we internalized the initial
Set
-based SPRJU algebra semantics
used for database-mappings, into the initial
DB
-based semantics of the same
Σ
R
algebra.
DB
−→
8.3.2 DB Coinductive Principle and DB Morphisms
As we have seen in the chapter dedicated to operational semantics of database-
mappings, the coalgebras are suitable mathematical formalizations of reactive sys-
tems and their behavior, as in our case when we are considering database mappings
based on tgds, and their observable information fluxes which are parts of the tu-
ples generated from a source database by these mapping (tgds) and, successively,
transferred into the target database.
This subsection provides an application of the corecursion, that is, a construction
method which uses the final coalgebras [
1
]. In order to provide an intuitive under-
standing of the rest of this section, let us focus on the coalgebraic point of view of a
database mappings.
In fact, we know that each tgd used in the schema mappings, or as an integrity
constraint over a schema, produces the tuples. Hence, given a sketch's mapping
M
AB
={
q
1
,...,q
k
,
1
∅
}:
A
→
B
with
q
i
=
v
i
·
q
A,i
∈
O(r
i
1
,...,r
i
k
,r
B
i
)
, an op-
⇒
r
B
i
(
t
i
)
, where
v
i
∈
erad's expression
e
O(r
q
i
,r
B
i
)
(with a new introduced re-
of the same type as
r
B
i
) and
q
A,i
∈
lational symbol
r
q
i
O(r
i
1
,...,r
i
k
,r
q
i
)
,isan
operad's expression
e
r
q
i
(
t
i
)
with tuple of terms in
t
i
composed of variables in
e
and Skolem functions
f
m
obtained by Skolemization of the existential quantifiers in
a given tgd.
The functorial translation (Lawvere theories) by a mapping-interpretation
α
(i.e., an R-algebra in Definition
11
and Corollary
4
in Sect.
2.4.1
), from the
mapping sketch category into the
DB
, satisfies such a schema mapping
M
AB
if
α(v
i
)
:
α(r
q
i
)
→
α(r
B
i
)
is an injection. The computation of the relation
α(r
q
i
)
is done by the function
α(q
A,i
)
(in Definition
11
) obtained from the logical for-
mula
e
⇒
[
(
_
)m/r
im
]
1
≤
m
≤
k
, that can be equivalently represented by a composed term
t
e
=
(
_
)m/r
im
]
1
≤
m
≤
k
)
(where
E
is the algorithm of an equivalent translation
of the logical formulae into the relational algebra terms) of the relational algebra
E(e
[
