Database Reference
In-Depth Information
Note that the set of infinite ground terms
T
∞
cannot be obtained in the inductive
way we defined the set
).
The external commutative diagram of this proposition represents the final coal-
gebra semantics diagram analog to (1), but for its concrete DB-interpretation.
The isomorphism
T
P
(X)
(when
X
=∅
T
:
T
∞
→T
∞
satisfies the homomorphic properties. Indeed,
for any two terms
t,t
∈
T
∞
,
0
,
T
(a.t)
=
T
(a.
_
)
T
(t)
=
a
⊗
T
(t)
,
T
(nil)
=⊥
T
n
(t
1
,...,t
n
)
=
T
n
T
(t
1
),...,
T
(t
n
)
=+
n
T
(t
1
),...,
T
(t
n
)
.
Thus, the commutative diagram (0) is composed of the isomorphic arrows (i.e., the
bijections) in
Set
.
T
∞
are obtained from the trees in
T
∞
by replacing
Consequently, the trees in
n
0
,a
n
, respectively.
∈
∈
⊥
⊗
+
the nodes
a
Act, nil,a.
_ and
with
a
Act,
_ and
F
:T
∞
→
T
P
(
T
∞
)
is a 'final' isomorphism as well, between the set of
infinite trees that are possible solutions of the database-mapping process-programs.
For any given assignment
f
Therefore,
:
X
→T
∞
,the
(X
Σ
P
)
-algebra,
[
]:
T
∞
)
→T
∞
f,h
X
Σ
P
(
of the diagram in the proof of Proposition
37
will be called as
DB
-
denotational
semantics
for the initial
T
P
X
algebra of the database-mapping process language
with the set
X
of process variables.
Only for a particular assignment
f
this DB-denotational algebra is
adequate
for
the operational semantics, as it will be explained in what follows. Notice that two
terms in
T
∞
T
∞
(or, equivalently, in
) are equal iff they are congruent (w.r.t. the set
of equations of the operator
, that is, its commutativity and associativity equations).
The final coalgebra semantics presented above is not observational, as is charac-
teristic property of the behavior-based operational semantics. Such a behavior-based
observational semantics will be presented in the next Sect.
7.4
. Two precesses in the
operational semantics (i.e., LTS trees) are equal if they are
bisimilar
, consequently,
from the result above, if the terms (corresponding to these LTS trees) are congruent.
Example 37
Let us consider the continuation of Strong Data Integration seman-
tics in Example
36
, of the graph
G
with three edges,
M
AB
1
:
A
→
B
1
,
M
AB
2
:
M
AB
3
:
A
→
B
3
, with a model (functor)
α
∗
∈
DB
Sch
(G)
A
→
B
2
and
Mod(G)
⊆
