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)
Search WWH ::




Custom Search