Database Reference
In-Depth Information
n
(t
1
,...,t
n
)
→
1
{
−
1
−
1
3.
+
Abs
(t
1
),...,
Abs
(t
n
)
}
, thus, in the particular case
→
L
=
1
−
1
t
n
)
,
n
(a
1
⊗
−
1
+
t
1
,...,a
n
⊗
t
n
)
Abs
(a
1
⊗
t
1
),...,
Abs
(a
n
⊗
0
so that
fst
S
(
L
)
=⊥
and
=
a
1
Abs
(t
n
)
.
a
n
−
1
−
1
L
snd
S
(
)
Abs
(t
1
),...,
Consequently, there exists the isomorphism
Abs
:
D
P
(
1
),
−
1
Abs
→
T
∞
,
]
−
1
Σ
P
−
1
Abs
◦
f,
Abs
◦
h
◦
[
f,h
between the
abstract
SOS-denotational semantics and the DB-denotational seman-
tics.
This corollary shows that the adequate DB-denotational semantics is equivalent
to the adequate
abstract
SOS-denotational semantics. Consequently, we can use
the DB-denotational semantics, based on
DB
category as a
canonical
denotational
semantics for the database-mapping programs.
Proposition 44
The following commutative diagram represents the adequateness
of the denotational semantics to the
abstract
operational semantics
(
when
S
=
1
=
0
{⊥
}
)
for the database-mapping programs with the final coalgebra isomorphism
DB
=
Abs
◦
B
◦
B
P
(
−
1
Abs
)
:
where
,
from Proposition
42
,
the mapping ℘
:
X
→
B
P
X represents the abstract
behavior
0
[
_
]=
ass,℘
:
X
→{⊥
}×
B
P
X of a program
,
the
general
behavior
