Database Reference
In-Depth Information
Notice that this relationship, represented by the above commutative diagram, cor-
responds to the embedding of the SOS-denotational
(X
Σ
P
)
-algebra semantics
into the DB-denotational
(X
Σ
P
)
-algebra semantics, that is, the embedding ho-
momorphism
T
◦
E
:
D
P
S
,
[
D
ρ
(k)
→
T
∞
,
]
@
,
_
]
[
f,h
between these two adequate denotational semantics algebras for the
syntax
ini-
tial free algebra
(
T
P
X,
I
)
, in the commutative diagram in Corollary
23
between
(X
Σ
P
)
-algebras
Moreover, we obtain a more specific relationship between the SOS and DB denota-
tion semantics:
Corollary 24
The DB-denotational semantics is isomorphic to the
abstract
SOS-
denotational semantics
(
when
0
S
=
={⊥
}
1
is a terminal object in
Set
,
so that all
0
).
That is
,
the mapping
nodes of trees have the same name
⊥
T
◦
E
:
D
P
(
1
)
→T
∞
is an isomorphism
,
denoted by
Abs
.
Consequently
,
from the commutative diagram in Corollary
23
,
we obtain that
@
@
f
#
=
T
◦
E
◦[
_
]
#
=
Abs
◦[
_
]
#
.
Proof
The mapping
Abs
=
T
◦
E
:
D
P
(
1
)
→T
∞
is defined in Definition
56
of
the embedding
E
:
D
P
S
→
T
∞
, when
S
is the singleton (a terminal object in
Set
)
0
1
={⊥
}
and with the isomorphism
T
:
T
∞
→T
∞
in Definition
53
, so that:
0
;
2. For any tree
0
1.
⊥
→⊥
a
L
}
0
L
))
;
L
={⊥
,
L
→
a
⊗
(
Abs
(
3. For any tree
L
such that
L
is the union of the trees in
{
L
1
,...,
L
n
}
obtained by su-
L
=
1
{
L
1
,...,
perposition of their roots in the unique root of
L
, denoted by
L
n
}
,
n
(
L
→+
Abs
(
L
1
),...,
Abs
(
L
n
))
.
a
1
L
1
}
In the case when
snd(
L
i
)
={
for each 1
≤
i
≤
n
, we obtain a particular
n
(a
1
⊗
case
L
→+
(
Abs
(
L
1
)),...,a
n
⊗
(
Abs
(
L
n
)))
.
−
1
It is easy to verify that the inverse of '
Abs
', denoted by '
Abs
', is defined recur-
sively by:
1.
0
0
,
⊥
→⊥
a
(
0
−
1
2.
a
⊗
t
→
L
, such that
fst(
L
)
=⊥
and
snd(
L
)
={
Abs
(t))
}
,
