Database Reference
In-Depth Information
r
X,
5
nr(
1
),nr(
3
)
;
r
X,
7
≈
R
;
r
X,
8
≈
r
X,
6
≈
S.
Thus, the flattened system of
recursive
guarded equations above may be ex-
pressed by the function
f
e
:
T
P
(X)
(for example,
f
e
(r
X,
1
)
→
=
X
A
r
X,
4
UNION
r
X,
7
,
f
e
(r
X,
4
)
=
r
X,
3
[
nr(
2
),nr(
3
)
]
,
f
e
(r
X,
8
)
=
S
∈
A
), where the “param-
eters” are the relations of the database
A
={
R,S
}∈
Ob
DB
. This system is just a
T
P
(
_
)
coalgebra of the polynomial endofunctor
A
Set
with the signature
Σ
R
. The right-hand sides of equations (except for two last equations) belong to
T
P
(X)
. The right-hand sides of the last two equations belong to “parameters” in
the database
A
:
Set
→
Ob
DB
.
Hence, the flattened guarded system of equations defined by a mapping
f
e
has
the
unique
solution
f
s
:
={
R,S
}∈
T
P
(
_
)
-coalgebra homomor-
phism from the coalgebra
(X,f
e
)
into the final coalgebra
(T
∞
(A),
X
→
T
(A)
, which is the
A
∞
)
. In our case,
when the mapping
f
e
defines the flattened guarded system of equations presented
above, the unique solution of this system, provided by the mapping
f
s
, defines the
R-algebra
α
which satisfies the constraint mapping
T
GA
:
G
→
A
, by:
α(r)
f
s
(r
X,
1
),
α(s)
f
s
(r
X,
2
),
so that
α
∗
(
G
)
=
. In this case of the
recursive system of equations with the Skolem functions
f
1
and
f
2
that introduce
the new Skolem constants, both
f
s
(r
X,
1
)
and
f
s
(r
X,
2
)
are infinite trees (i.e., infinite
ground terms with constants in
A
={
R,S
}
can(
I
,D)
is a model of the global schema
G
).
and
S
is an empty relation. Then we
obtain the following infinite set of tuples for the relations
α(r)
and
α(s)
:
Let us consider the case when
R
={
(a,b)
}
α(r)
α(s)
a,b
b,ω
1
b,ω
2
ω
2
,ω
3
ω
2
,ω
4
ω
4
,ω
5
...
...
where
ω
1
=
f
1
(a,b)
,
ω
2
=
f
2
(b,ω
1
)
,
ω
3
=
f
1
(b,ω
2
)
,
ω
4
=
f
2
(ω
2
,ω
3
)
,
ω
5
=
f
1
(ω
2
,ω
4
)
,etc.
Diagram (c.2) in Corollary
33
is valid for a general guarded system of equations,
and we need to specify the flattening of such a system. It may be provided by spec-
ifying the equations with a mapping
f
T
:
X
→
Σ
R
(X)
, so that diagram (c.2) above
can be substituted by (notice that
0
⊥
={⊥}
is a singleton set, thus a terminal object
in
Set
) the following diagram:
