Database Reference
In-Depth Information
the initial-semantics diagram. Consequently, the unique extension to all terms with
variables,
f
#
:
T
P
X
→T
∞
(of
h
, which is defined in the proof of Proposition
37
,
along
f
) is defined recursively by (for
t,t
1
,..,t
n
∈
T
P
X
):
1. For each variable
p
A
∈
:
X
→T
∞
X
,
f
#
(p
A
)
=
f(p
A
)
=
T
(
s
E
(p
A
))
;
0
, and
A
→
A
;
2.
nil
→⊥
3.
a.t
→
a
⊗
f
#
(t)
;
n
(t
1
,...,t
n
)
n
(f
#
(t
1
),...,f
#
(t
n
))
.
4.
→+
In order to represent the adequateness of the DB-denotational semantics of the
initial
T
P
(X)
algebra, for the behavioral operational semantics expressed in the
diagram (4) (in Sect.
7.4
for the behavior functor
B
P
), we need the embedding
E
:
D
P
S
→
T
∞
D
P
S
=
S
×
B
P
)
into the ground
of (also infinite) LTS trees in
gfp(
terms (trees) in
T
∞
and the embedding
E
X
:
B
P
(
S
)
→
T
P
(X)
:
Definition 56
We define inductively the following embedding between (also infi-
nite) trees,
E
:
D
P
S
→
T
∞
, such that:
•
For a single-state LTS (without the outgoing transitions)
A
∈
D
P
S
,
A
→
A
;
•
For an LTS (tree)
L
A
∈
D
P
S
with the root state
A
=
fst
S
(
L
A
)
and
snd
S
(
L
A
)
=
a
L
B
}
{
where
L
B
∈
D
P
(
S
)
,
L
A
→
a.
E
(
L
B
)
;
•
For an LTS (tree)
L
A
∈
D
P
S
with the root state
A
=
fst
S
(
L
A
)
and
snd
S
(
L
A
)
=
a
i
L
B
i
|
{
1
≤
i
≤
n
}
where
L
B
i
∈
D
P
S
,
n
a
i
.
n
.
L
A
→
E
(
L
B
i
)
|
1
≤
i
≤
Moreover, we define the embedding of the behavior into the syntax, for each set
X
,
ν
X
:
S
×
B
P
(X)
→
T
P
(X)
, natural in
X
, as follows:
•
For the empty set
∅∈
B
P
(X)
=
P
fin
(Act
×
X), (A,
∅
)
→
A
;
•
For the singleton
{
(a,p
B
)
}∈
B
P
(X)
,
(A,
{
(a,p
B
)
}
)
→
a.p
B
;
•
For
{
(a
i
,p
B(i)
)
|
1
≤
i
≤
n
}∈
B
P
(X)
,
n
≥
2,
A,
(a
i
,p
B(i)
)
|
≤
i
≤
n
→
n
1
{
a
i
.p
B(i)
|
1
≤
i
≤
n
}
.
T
P
is a natural transformation, with a component
ν
X
=
Thus,
ν
:
S
×
B
P
ν(X)
.
X
of variables in
X
(possibly involving equating some of the variables, first renaming and then applying
the embedding is the same as first applying the embedding and then renaming. Thus,
ν
It is easy to show that for each renaming function
f
:
X
→
:
S
×
B
P
T
P
is a natural transformation between the behavior and syntax
endofunctors on
Set
.
Proposition 39
Based on the embedding in Definition
56
,
the following is valid
:
@
g
E
=
ν(X)
◦[
_
]:
X
→
T
P
(X) and
s
E
=
E
◦[
_
]
◦:
X
→
T
∞
.
T
∞
is adequate for the operational semantics when the following diagram commutes
:
Consequently
,
the denotational semantics (X
Σ
P
)-algebra with the carrier set
