Database Reference
In-Depth Information
g
E
inr
X
(t
1
,...,t
k
,...,t
n
)
=
g
E
n
(t
1
,...,t
k
,...,t
n
)
(from
p
i
k
≡
t
k
)
g
E
n
(p
i
1
,...,p
0
,...,p
i
n
)
∈[
p
m
]
E
=
for
m
=
0 (because if
m
≥
1 then we would have the equation
(p
m
=
n
(p
i
1
,...,p
0
,...,p
i
n
))
in
E
, which is impossible). Thus, the commuta-
tivity is satisfied. From the fact that this is a (unique) homomorphism from
the initial
(X
Σ
P
)
-algebra into
(X
Σ
P
)
-algebra
(X,
[
id
X
,h
X
]
)
we con-
g
E
.
clude that
id
X
#
=
Note that this flattened system of equations with program variables can be given
by a function
g
E
:
X
→
T
P
(X)
which is a
coalgebra
of the endofunctor (and the
syntax monad)
T
P
(
_
)
:
Set
→
Set
of the signature
Σ
P
.
Proposition 36
Let
g
E
:
→
T
P
(X) be the guarded system of flattened equations
for a database mapping process-program P
.
There is a
unique
solution for such a
system of equations
,
given by the function
s
E
:
X
T
∞
denotes the Σ
P
algebra of all finite and infinite Σ
P
-labeled trees
(
of ground terms
).
That is
,
→
T
∞
X
,
where
T
∞
is the greatest fixed point of the endofunctor
T
P
:
→
Set
Set
,
denoted
T
P
)
(
i
.
e
.,
T
P
(gfp(
T
P
))
=
T
P
)
),
so that the set of finite ground terms
by gfp(
gfp(
T
P
(
∅
⊂
T
∞
is its strict subset
(
here
∅
)
denotes the empty set X of variables
).
Proof
We have seen that the algebra signature
Σ
P
of the database-mapping process
has only one nullary operator
nil
(the 'stop of execution' operation), the finitary
n
-
ary (
n
n
) and the set of unary operators (as
a
i
.(
_
)
for example, for
≥
2) operator
any
a
i
∈
Set
is polynomial.
It is known [
4
] that generalized polynomial endofunctors of
Set
are iteratable and
hence
Act
). Thus, the syntax monad (endofunctor)
T
P
:
Set
→
)
which is (by Lambek's theo-
rem) an isomorphism. Consequently, from the system of flattened equations given
by
g
E
:
T
P
has a final coalgebra
Σ
:
T
∞
→
T
P
(
T
∞
X
→
T
P
(X)
, which is a
T
P
(
_
)
-coalgebra, we obtain the unique homomor-
phism
s
E
:
into this final coalgebra: this homomorphism assigns to each
process variable in
X
a ground term which corresponds to the solution for this pro-
cess variable. The solutions for the set of variables in
X
satisfy the flattened set of
equations in Proposition
34
.
X
→
T
∞
Note that
T
∞
is computed by iterating the functor
T
P
on the empty set of vari-
ables
∅
up to the greatest fixed point (gfp), i.e., by the union of the chain
T
P
∅⊆
T
P
(
T
P
∅
)
⊆···
of the least fixed points
Σ
P
)
,etc.
The most interesting concrete syntax is an interpretation of the abstract
T
P
∅=
lfp(
∅
Σ
P
)
,
T
P
(
T
P
∅
)
=
lfp(
T
P
∅
T
P
syn-
0
, any unary operation
tax, given by Definition
53
, where '
nil
' is interpreted by
⊥
n
,
'
a
i
.
_' by the unary database operation
a
i
⊗
_ and the finitary
n
-ary operations
