Database Reference
In-Depth Information
This inductive principle can be used to show that the operator
T
P
inductively ex-
tends to the
syntax
endofunctor
T
P
:
Set
→
Set
(a monad freely generated by sig-
nature
Σ
P
), so that its action
T
P
f
on an arrow (a function)
f
:
X
−→
Z
takes the
inductive extension of
inr
Z
:
Σ
P
(
T
P
Z)
−→
T
P
Z
along the composite
inl
Z
◦
f
, i.e.,
T
P
f
(inl
Z
◦
f)
#
, and hence the second diagram above commutes.
Let us consider the cases when
Σ
P
∈{
Σ
R
,Σ
R
,Σ
RE
}
Example 29
where, by Def-
Σ
R
⊆
inition
31
of classes of relational algebras,
Σ
R
⊆
Σ
RE
, with
X
×{
i
}
i
X
2
×{
i
}
X
ar(o
k
)
Σ
RE
(X)
=
={⊥}
o
k
∈
Σ
RE
o
i
∈
Σ
RE
,ar(o
i
)
=
1
,i
≥
1
=−
1
,
0
,
1
where
⊥∈
Σ
RE
(empty relation) is a constant (a unique nullary operator), unary op-
erators are the family of projections _
, selections _ WHERE
C
i
, and EXTEND
_ ADD
a,name
AS
e
operators, and the binary operators are Cartesian product _
TIMES _, _ UNION _ and _ MINUS _ operators.
Note that the nullary operator (a constant)
[
S
i
]
, together with the unary operators
'
EXTEND
...' and the binary operation '
UNION
', is able to define any relation.
Then
Z
in the initial algebra semantics diagram above is an instance database
(i.e., a simple object
Z
⊆
Υ
⊂
Υ
in
DB
, see Definition
26
in Sect.
3.2.5
) and hence
X
⊆R
⊥
and the mapping
f
:
X
→
Z
assigns the relations to variables (i.e., relational
symbols) in
X
(with the fixed assignment
f(r
)
=⊥∈
Z
for the empty relation
r
∅
∈
∅
R
). Thus, when
f
is a restriction of a general assignment
_
:
X
→
Υ
introduced
by Definition
31
for the class of relational algebras.
In all these cases, the unique
X
Σ
P
-algebra homomorphisms
f
#
:
T
P
X
→
Z
are the restrictions of the evaluation of terms mappings
_
#
:
T
P
R→
Υ
.
Z
, the mapping
h
:
Σ
P
(Z)
→
Z
has to satisfy
h(
⊥
)
=⊥∈
Z
(for a given type (i.e., a signature)
of algebras each carrier set
Z
must contain all constants, i.e., all nullary operators)
and the following conditions (in order to make the above initial algebra semantics
Consequently, in the
X
Σ
P
-algebra
[
f,h
]:
X
Σ
P
(Z)
→