Database Reference
In-Depth Information
directly from Universal algebra because the closure operator
T
is
algebraic
and
(
C
,
⊆
)
, where
is a set of all closed simple objects in
DB
, is an algebraic (com-
plete+compact) lattice.
C
The notion of T-algebra subsumes the notion of a
Σ
R
-algebra (
Σ
R
-algebras can
be understood as algebras in which the operators (of the signature) are not subject
to any law, i.e., with empty set of equations). In particular, the monad
T
P
freely
generated by a signature
Σ
R
is such that
T
alg
is isomorphic to the category of
Σ
R
-
algebras. Therefore, the
syntax
of a programming language can be identified with
monad, the
syntactical monad
T
P
freely generated by the program constructors
Σ
R
.
More formally, as it was presented in Sect.
5.1.1
, for the signature
Σ
R
there
is an endofunctor
Σ
R
:
Set
−→
Set
such that for any object
B
,
Σ
R
(B)
o
i
∈
Σ
R
B
ar(o
i
)
, and for any arrow in
Set
(a function)
f
:
B
−→
C
,
Σ
R
(f )
o
i
∈
Σ
R
f
ar(o
i
)
.
Thus, also for any object
A
in
Set
we have an endofunctor
Σ
R
A
=
A
Σ
R
:
Set
−→
Set
such that for any object
B
in
Set
,
Σ
R
A
(B)
=
(Σ
R
A)(B)
=
A
Σ
R
B
A
σ
B
ar(σ)
,
∈
Σ
R
id
A
σ
∈
Σ
R
f
ar(σ)
.
We define an
iteratable
endofunctor
H
of a category
D
if for every object
X
of
D
the endofunctor
X
H(
_
)
has an initial algebra. It is well known that the signature
endofunctor
Σ
R
in
Set
category is
ω
-cocontinuous and iteratable.
The problem which will be analyzed in details in what follows is: What are the
concepts in the
DB
category (and relative commutative diagrams) corresponding to
the initial
Σ
R
-algebra concepts and syntax monad
and for any arrow
f
:
B
−→
C
,
Σ
R
A
(f )
T
P
X
for the SPRJU relational
algebra terms expressed by the commutative diagrams in the
Set
category? For ex-
ample, the set of terms
T
P
X
in the initial algebra semantics diagram is not an object
in the
DB
category, but
α
#
image which is a set
TA
of the relations (views) ob-
tained by evaluation of terms in
T
P
X
is a power-view object in
DB
. Hence, the
power-view monad
T
:
DB
→
DB
is a natural correspondence to the syntax monad
T
P
:
Set
.
This process of translation of (co)inductive principles from standard
Set
into
DB
category will be elaborated in the next sections.
We have to take in mind the difference between
Set
,
as an elementary topos used
for ordinary Lawvere theories, that is, to study equational theories (varieties in Uni-
versal algebra), and finitary monads on
Set
(for example, Moggi's leading examples
of monads in the setting of call-by-value
λ
-calculus, with examples drawn primar-
ily from the programming language ML and adopted in functional programming, in
particular in the development of the language Haskell), from our monoidal closed
V-category
DB
in the setting of enriched Lawvere theories.
More specifically, the idea of a monad as a model of computations, where the
programs take values in
A
, say, to computations in
TB
, Kleisli categories provide
the right setting to describe this approach and hence will be presented in a dedicated
Sect.
8.4
.
Set
→
