Database Reference
In-Depth Information
Proof
Notice that the component of the commutative diagram (10) is the two com-
mutative diagrams bellow:
@
Thus,
f
=
T
◦
E
◦[
_
]
:
X
→T
∞
(
1
)
and, by Proposition
39
,
f
=
T
◦
s
E
, so that
(
T
∞
,
[
f,h
]
)
is an adequate denotational semantics for the
syntax
initial free algebra
(
T
P
X,
I
)
(in Proposition
38
), and the commutative diagram
follows from the following possible cases (note that the mapping
h
is defined in the
proof of Proposition
37
):
1. When
nil
Act
a
i
∈
Act
{{
}×
D
P
S
}
n
≥
2
(
)
n
,
∈
D
P
S
={
}∪
D
P
S
Σ
P
(
)
nil
i
=
T
◦
E
⊥
0
=
T
(nil)
0
,
T
◦
E
◦
D
ρ
(k)(nil)
=⊥
0
.
◦
T
◦
E
=
=⊥
and hence
h
Σ
P
(
)(nil)
h(nil)
2. When
(i,
L
B
)
∈
Σ
P
(
D
P
S
)
,
=
T
◦
E
A
L
B
a
i
T
◦
E
◦
D
ρ
(k)(i,
L
B
)
=
T
a
i
.
L
B
)
=
a
i
⊗
T
E
L
B
)
.
E
(
(
Thus,
h
◦
Σ
P
(
T
◦
E
)(i,
L
B
)
=
h(i,
T
(
E
(
L
B
)))
=
a
i
⊗
(
T
(
E
(
L
B
)))
.
L
B
1
,...,
L
B
n
)
∈
D
P
S
3. When
(
Σ
P
(
)
,
=
T
n
E
L
B
n
)
T
◦
E
◦
D
ρ
(k)(
L
B
1
,...,
L
B
n
)
(
L
B
1
),...,
E
(
n
T
E
L
B
1
)
,...,
T
E
L
B
n
)
.
=+
(
(
Hence,
h
◦
Σ
P
(
T
◦
E
)(
L
B
1
,...,
L
B
n
)
=
h
T
E
(
L
B
1
)
,...,
T
E
(
L
B
n
)
=+
n
T
E
(
L
B
1
)
,...,
T
E
(
L
B
n
)
.
