Database Reference
In-Depth Information
1. When
[
p
k
]=
(ass(p
k
),
{
(ass(p
k
+
1
),p
k
+
1
),...,(ass(p
k
+
n
),p
k
+
n
)
}
)
,
n
≥
2, we
n
(ass(p
k
+
1
).p
k
+
1
,...,ass(p
k
+
n
),p
k
+
n
)
which is equiv-
alent to the flattened term
obtain
ν(X)(
[
p
k
]
)
=
n
(p
k
+
1
,...,p
k
+
n
)
(see Example
36
) with equation
n
(p
k
+
1
,...,p
k
+
n
))
n
(p
k
+
1
,...,p
k
+
n
)
.
(p
k
=
∈
E
and hence
g
E
(p
k
)
=
2. When
[
p
k
]=
(ass(p
k
),
{
(ass(p
k
+
1
),p
k
+
1
)
}
)
, we obtain
ν(X)(
[
p
k
]
)
=
a.p
k
+
1
,
and from the fact that
(p
k
=
a.p
k
+
1
)
∈
E
, we obtain
g
E
(p
k
)
=
a.p
k
+
1
.
@
Consequently,
s
E
=
E
◦[
→
T
∞
, so that the final coalgebra semantics for the
guarded system of equations of a given database mapping system is the result of the
operational semantics based on the behavior endofunctor
_
]
:
X
B
P
and LTS of execution
of these database programs. In fact, the commutative diagrams (4) (the operational
semantics) and (5) (commutative diagram of the embedding of LTS trees into the
ground term trees and (5a) compose the final coalgebra (bijection
Σ
) semantics
diagram (1) for the flattened system of equations in Proposition
37
.
The commutative diagrams (4) (the operational semantics) and (5) (commutative
diagram of the embedding of LTS trees into ground term trees and (0) (commutative
diagram of isomorphisms in Proposition
37
) define the commutative diagram (3) in
Proposition
38
with arrows
g
E
and
s
E
.
Consequently, the commutative diagram of this proposition extends the com-
mutative diagram in Proposition
38
by the operational semantics and its final
coalgebra isomorphism
B
. Thus, the diagram above is composed of all funda-
mental (co)algebra isomorphisms: the initial
Σ
P
-algebra isomorphism
I
with
DB-denotational semantics
Σ
P
-algebra,
[
f,h
]:
X
Σ
P
(
T
∞
)
→T
∞
, where
f
=
T
◦
s
E
and both final coalgebra isomorphisms
B
and, derived from it,
F
.
In GSOS, only operations w.r.t. which bisimulation remains a congruence are
admitted since bisimilar trees are easily seen to be
trace equivalent,
and hence in
GSOS
DB
,
a.(b
c)
and
a.b
a.c
are bisimilar or observationally equivalent and de-
noted by
a.(b
(a.b,a.c)
.
One of the properties of Aczel's coinductive semantics is that it maps two pro-
grams to the same set if and only if they are observationally equivalent:
c)
=
@
@
[
p
k
]
=[
p
m
]
iff
p
k
∼
p
m
.
That is, the coinductive extension of the operational model
[
_
]:
S
−→
S
×
B
P
(X)
does preserve
B
P
-bisimulation and, conversely, it can be 'pulled back' to form the
largest
-bisimulation relation. The above is a property which holds in general for
every coinductive extension of coalgebras of endofunctors
B
B
P
preserving categorial
(weak) pullbacks.
Proposition 40
Let us define the set of the subcategories of the
DB
category
,
={
D
L
A
|
L
A
∈
D
P
S
}
Sub(
DB
)
,
where each tree
L
A
∈
D
P
S
is an oriented graph with the root node A
,
so that D
L
A
a
C in
is a small category defined by this graph as follows
:
Each transition B
