Database Reference
In-Depth Information
0
Remark
The empty database
Act
is an action as well: it is the '
nil
' action
which stops the execution of a path in the LTS of a given process graph
P
in Defi-
nition
48
.
⊥
∈
Definition 51
Based on Proposition
33
and on the correspondence between the
visible actions and atomic morphisms in
DB
, the process language for a database-
mapping program of a graph
G
(V
G
,E
G
)
is given by a general grammar (with
the terms
t
and the program variables
p
):
=
1
0
|
t
1
◦
f
a
|
t
1
,t
2
,
(
G
r) t
:=
p
|
f
a
|⊥
A
:
A
→⊥
where
•
f
a
:
A
→
B
is an atomic action such that
f
a
=
α
∗
(MakeOperads(
M
AB
))
where
α
∗
is a mapping-interpretation of
Sch
(G)
and
Δ
α, MakeOperads(
M
AB
)
,
a
=
and hence
f
a
=
Ta
.
0
in
DB
corresponding to '
nil
' operation, a basic inert program in GSOS
DB
(stop of
execution).
1
A
is a unique arrow from
A
=
α
∗
(
A
)
,
•⊥
A
∈
V
G
, into a terminal object
⊥
•
◦
'
' is a binary sequential composition of arrows (morphisms) in
DB
. That is,
the DB-denotational semantics of a sequential action-prefixing operator '
a.
_' in
GSOS
DB
here is given by '_
◦
f
a
'.
•
For any two morphisms
t
1
:
C
, their parallel composition
(execution) is given by the unique arrow of product diagram in
DB
,
A
→
B
and
t
2
:
A
→
t
1
,t
2
:
A
→
B
+
C
. That is, the coproduct pairing '
_
,
_
'in
DB
represents the DB-
denotational semantics of the syntax operator '
'inGSOS
DB
.
The weak point of this denotational grammar for abstract GSOS
DB
gram-
mar is that here we possibly have an infinite number of different 'nil' operators
⊥
0
that are terminal arrows in
DB
. What is common for all of them is
that their information flux is unique and equal to
1
A
:
A
→⊥
0
(i.e., zero object in
DB
), and
hence it will be more appropriate to pass to the
objects
in
DB
(thanks to its sym-
metry properties) as terms of the denotational semantics of the abstract GSOS
DB
grammar.
Hence, in order to pass from the atomic morphisms in
DB
into the
visible
ac-
tions, we have to use the categorial symmetry of
DB
with the 'conceptualizing' op-
erator
B
T
:
⊥
Ob
DB
(in Definition
4
and Theorem
4
). It is easy to see that
this category symmetry transformation corresponds to the algebraic homomorphism
B
T
:
Mor
DB
→
,
‡
)
(an extension of the homomorphism in
Sect.
5.4
with a dual composition of the objects
(Mor
DB
,
◦
,
_
,
_
)
→
(Ob
DB
,
⊗
Ob
2
DB
→
∗:
Ob
DB
equal to tenso-
rial product '
⊗
', i.e., to a matching operator such that for any two simple objects
A,B
TB
; it will be extended to a bifunctor in Sect.
8.1.1
),
such that the image of
B
T
is the subset of closed objects in
DB
and '‡' is the data-
separation operator (isomorphic to the disjoint union '
∈
Ob
DB
,
A
⊗
B
=
TA
∩
', i.e., coproduct '
+
') in
DB
(introduced in Sect.
3.3.2
). Consequently, we have:
