Database Reference
In-Depth Information
inr
X
◦
Σ
R
(inl
X
)
,
such that
F
=
2
◦◦
1
and
f
e
=
k
X
◦◦
f
T
, where
k
X
=
with the bijections (isomorphisms in
Set
)
(
p
l
and
p
r
are the left and
right projections, respectively, as in the diagram bellow), with the isomorphism
:
⊥
,(t
R
,i)
→
(t
R
,i)
;
1
=
p
l
,p
r
⊥
,
t
R
,t
R
,i
→
t
R
,t
R
,i
,
and the isomorphisms
t
R
,t
R
,i
→
o
i
t
R
,t
R
,
2
=
inr
T
∞
(
⊥
0
)
:
(t
R
,i)
→
o
i
(t
R
)
;
with its inverse
,
o
i
t
R
,t
R
→
t
R
,t
R
,i
.
−
2
:
o
i
(t
R
)
→
(t
R
,i)
;
Σ
R
)
-coalgebras,
0
Diagram (c.3) represents the final coalgebra semantics of the
(
⊥
×
Σ
R
)
-coalgebra
f
#
0
where
f
s
=
is the unique homomorphism from the
(
⊥
×
Σ
R
)
-coalgebra
(T
∞
(
0
0
),
(X,
f,f
T
)
into the final
(
⊥
×
⊥
1
)
, and can be rep-
resented by the following commutative diagram in
Set
:
Thus,
f
#
is the unique
coinductive extension of f
T
along the mapping f
, so that
the commutative triangle on the left represents the initialization for the relational
symbols (the variables) in
X
by initial extension equal to
(empty relation), while
the commutative square (c.5) on the right represents the final solution (extensions)
of these relational symbols in
X
, specified by
f
T
(the set of
flattened
guarded equa-
tions).
The first projection
p
l
assigns to each tree-term the unique value
⊥
0
,
while the second projection
p
r
is a mapping defined by (for any tree-term
t
R
,t
R
∈
T
∞
(
⊥∈⊥
0
)
):
⊥
⊥→⊥;
o
i
(t
R
)
→
(t
R
,i),
(for each unary operator with
i
≥
1)
