Database Reference
In-Depth Information
3.
[
t
is a variable then
K
l
is
the position of this variable in the Cartesian product
t
R
; otherwise, if
t
l
=
S
]=[
K
1
,...,K
n
]
, where, for each 1
≤
l
≤
n
,if
t
l
∈
t
i
j
∈
t
1
then
K
l
=
N
+
j
;
4.
C
is the condition
α((q
A,i
)(
x
1
,...,
x
k
))
=
, where for 1
≤
i
≤
k
we have the
tuples of variables
x
i
=
(x
i,
1
,...,x
i,ar(r
i
)
)
for each conjunct
(
_
)
i
(
x
i
)
∈
e
.
Based on this proposition, which demonstrated that each arrow in
DB
(a set of
functions) is computationally equivalent to the corresponding set of terms of the
Σ
RE
-algebra, and on the fact that each object (a database instance) can be obtained
by terms of
Σ
R
⊂
Σ
RE
algebra, we obtain the following corollary:
Corollary 18
The denotational database-mapping category
DB
is computationally
equivalent to the relational Σ
RE
algebra
.
Based on the fact that the extension
Σ
RE
of the Codd's relational algebra
Σ
R
is
computationally strictly less expressive than the typed
λ
-calculus, it holds that
DB
cannot be a topos: in fact, in the last chapter, we will demonstrate that
DB
is less
expressive and a kind of weak monoidal topos.
This corollary demonstrates that the evaluation functor
Eval
DB
in
Proposition
24
is a mapping between two computationally equivalent categories,
and hence the database algebra
Alg
DB
=
:
RA
→
((Ob
DB
, Mor
DB
),Σ
DB
)
is the strict gen-
eralization of the relational algebra
Σ
RE
, from the relations to the databases and
their mappings.
Let us define the
inverse-inclusion
function
in
−
1
:
R
2
R
1
for an injective func-
tion
in
:
R
1
→
R
2
, for two relations
R
1
⊆
R
2
, such that for each tuple
d
∈
R
2
:
in
−
1
(
d
)
=
d
if
d
∈
R
1
;
(
empty tuple
)
otherwise
.
We can see by Proposition
24
that the unary operators (i.e., atomic arrows in
RA
)
are mapped by the functor
Eval
into the following family of elementary R-algebra
functions: identities, projections, and inverse-inclusions.
The question is what the full family of the elementary R-algebra functions used
in the
DB
category is, which compose the algebra signature the database-mappings
R-algebra.
We recall that for a given set of formulae
S
={
φ
1
,...,φ
n
}
by
S
we denote the
conjunction
φ
1
∧···∧
φ
n
.
Let us define an algorithm that transforms a mapping implication
φ
Ai
(
x
)
⇒
r
B
(
t
)
inanSOtgd
f
(Ψ )
(where
Ψ
is an FOL formula, i.e., a conjunction of a number
of such implications of a mapping
∃
(t
1
,...,t
n
)
is a tuple
of terms with variables in
x
and functional symbols in
f
), into the logically equiva-
lent implication, where all variables in each relational symbol on the left-hand side
are unique (i.e., different from all other variables in all relational symbols) and the
relation in the right-hand side has a tuple of the variables only:
M
AB
:
A
→
B
, and
t
=
