Database Reference
In-Depth Information
n
. This concrete DB-syntax in Def-
inition
53
is provided by a bijection between the set of abstract and these concrete
terms,
≥
2 by the corresponding
DB
n
-ary coproducts
+
T
:
T
P
(X)
→
T
P
(X)
, such that
0
,
T
(nil)
=⊥
T
(a
i
.t)
=
a
i
⊗
(
T
(t))
,
n
(t
1
,...,t
n
))
n
((
and
T
(
=+
T
(t
1
)),...,(
T
(t
2
)))
.
Consequently, for the set of abstract trees
T
∞
we define its corresponding set of
T
:
T
P
(X)
→
T
P
(X)
and (for the ground
concrete trees
T
∞
, with the bijection
terms only)
T
:
T
∞
→T
∞
. Now we are able to define the semantics of process-
programs based on the coalgebras, both for the abstract
T
P
and concrete DB-syntax
T
P
:
Proposition 37
→
T
P
(X) be a guarded system of equations for a
database mapping process-program P
(
in Proposition
34
).
Thus
,
the coalgebraic
semantics for the database mapping process-programs can be given by the follow-
ing commutative diagram in
Set
:
Let
g
E
:
X
where
T
is the isomorphism between the abstract and DB-terms in Definition
53
,
so that the terms in
T
∞
are the objects in
DB
,
that is
,
the instance-databases
.
The
isomorphism
F
is the concrete interpretation of the Lambek's final coalgebra iso-
morphism
Σ
.
Consequently
,
we are able to use
T
∞
⊆
Ob
DB
as a DB-denotational
semantics for the abstract Σ
P
-algebras
.
Proof
From [
4
], the inner commutative diagram (1) represents the final coalgebra
semantics for
Σ
P
, while the diagram (0) is composed of only isomorphisms, so
that
T
∞
⊆
Ob
DB
can be used as an adequate DB-denotational semantics algebra
h
:
Σ
P
(
→T
∞
, represented by the (syntax) initial algebra commutative diagram
in Sect.
7.3.1
, where
Z
T
∞
)
=T
∞
, such that
Σ
P
(
T
∞
)
=
Act
∪{
nil
}∪{T
∞
×{
i
}|
a
i
∈
}
n
≥
2
T
n
∞
0
, and for
t
1
,t
2
∈T
∞
Act
, with
h
being the identity for
Act
,
h(nil)
=⊥
,
n
(t
1
,...,t
n
)
.
So we obtain the following initial algebra semantics commutative diagram:
h(t
1
,i)
=
a
i
⊗
t
1
,
h(t
1
,...,t
n
)
=+
