Database Reference
In-Depth Information
algebra for the particular meaning of
k
. Thus,
D
ρ
(k)
is a
conservative extension
of
k
:
Σ
P
S
→
S
from the states (that are single-node trees) to all trees in
D
P
S
, by:
•
D
ρ
(k)(y)
=
k(y)
,for
y
∈{
nil
}∪
Act
;
•
D
ρ
(k)(i,
L
B
)
(where
L
B
is a tree with a root state
B
in
D
P
S
) is the resulting tree
L
A
∈
D
P
S
, equal to
a
i
,
L
B
, i.e., with the branch
a
i
from the root
A
=
k(i,B)
into the tree
L
B
;
•
D
ρ
(k)(
L
B
1
,...,
L
B
n
)
is the resulting tree
L
A
∈
D
P
S
, equal to the union of the
trees
L
B
i
,i
=
1
,...,n
, with the superposition of all roots
B
i
of these trees
i
=
1
,...,n
into the unique new root state equal to
A
=
k(B
1
,...,B
n
)
.
Proposition 43
Let us consider the commutative diagram
(9)
in the case when k
=
g
E
ass
represents the behavior of a program as in Proposition
42
.
Then
,
the commutative diagram in Proposition
42
can be extended to the following
commutative diagram
:
◦
◦
κ
:
Σ
P
S
→
S
g
E
)
@
#
where
=
(ass
◦
=[
_
]
is both a unique (
S
×
B
P
)-coalgebra and (X
Σ
P
)-
algebra homomorphism
,
and κ
:
Σ
P
(
S
)
→
T
P
∅⊂
T
P
(X) is defined by
:
→
→
∈
1.
nil
nil
,
a
a
,
for each a
Act
,
2.
(A,i)
→
a
i
.A
∈
T
P
∅
,
because A
∈
S
⊂
Act
,
n
(A
1
,...,A
n
)
∈
T
P
∅
3.
(A
1
,...,A
n
)
→
,
because for
1
≤
i
≤
n
,
A
i
∈
S
⊂
Act
.
Proof
It is enough to show that the diagram (1a) on the left commutes for
=
g
E
)
(defined in Proposition
42
).
However, from the fact that
(ass
◦
is the unique homomorphism from the initial
X
@
,
#
Σ
P
algebra into
(
D
P
S
,
[[
_
]
D
ρ
(k)
]
)
-algebra, also
=[
_
]
must be satisfied,
g
E
)
#
:
T
P
X
and hence
=
(ass
◦
=[
_
]
→
D
P
S
.
