Database Reference
In-Depth Information
o
i
t
R
,t
R
→
t
R
,t
R
,i
,
for the binary unary operators
,
1)
'UNION' (with
i
=
0), 'TIMES' (with
i
=−
Σ
R
(T
∞
(
with its inverse
p
O
r
:
0
))
0
)
defined by:
⊥
→
⊥
T
∞
(
⊥→⊥;
(t
R
,i)
→
o
i
(t
R
),
(for each unary operator with
i
≥
1)
t
R
,t
R
,i
→
o
i
t
R
,t
R
,
p
OP
and
p
O
r
◦
so that
p
r
◦
p
r
are the identity functions, thus
p
r
is an isomorphism
(bijection), such that
p
r
=◦
1
.
Consequently, the diagram
(
c
.
3
)
+
(
c
.
4
)
is equal to the diagram (c.5) and repre-
sents the final semantics of the
Σ
R
-coalgebras, where
f
s
=
f
#
is the unique homo-
morphism from the
Σ
R
-coalgebra
(X,f
T
)
into the final
Σ
R
-coalgebra
(T
∞
(
⊥
r
0
),
p
r
)
.
8.4
Kleisli Semantics for Database Mappings
The basic idea behind the semantic of programs [
21
] is that a program denotes a
morphism from
A
(the object of
values
of type
A
)to
TB
(the object of
computations
of type
B
), according to the view of “programs as functions from values to computa-
tions”, so that the natural category for interpreting programs (in our case, a particular
equivalent “computation” database mappings of the form
f
1
η
B
◦
f
:
A
−→
TB
,
derived from a database mapping
f
:
A
−→
B
, such that
f
1
≈
f
) is not the
DB
category, but the Kleisli category
DB
T
.
Definition 59
Given a monad
(T,η,μ)
over a category
C
,wehave[
14
]:
−
∗
)
, where for
f
TB
we have
f
∗
:
•
A
Kleisli triple
is a triple
(T,η,
:
A
−→
TB
such that the following equations hold:
η
∗
A
=
id
TA
,f
∗
◦
−→
η
A
=
TA
f
and
g
∗
◦
f
∗
=
(g
∗
◦
f)
∗
,for
f
TC
.
A Kleisli triple satisfies the
mono requirement
provided
η
A
is monic for each
object A.
:
A
−→
TB
and
g
:
B
−→
•
A
Kleisli category C
T
has the same objects as
C
category. For any two objects
A
and
B
there is the bijection between arrows
θ
C
(A,T B)
=
:
C
T
(A,B)
. For any
two arrows
f
:
A
−→
B
and
g
:
B
−→
C
in
C
T
, their composition is defined by
Tθ
−
1
(g)
θ
−
1
(f ))
.
g
◦
f
θ(μ
C
◦
◦
The mono requirement for the monad
(T, η,μ)
[
22
] is satisfied because, by
Proposition
9
in Sect.
3.2.1
, for each object
A
the arrow
η
A
:
A
−→
TA
is an
isomorphism
η
A
=
is
A
(we denote its inverse by
η
−
A
) and hence it is also monic.
Consequently, the category
DB
is a
computational model
for the view-mappings
(which are the programs) based on observations (i.e., views) with the typed operator
T
, so that:
