Database Reference
In-Depth Information
to define an algebraic database lattice, its enrichments and then investigate induc-
tive/coinductive and computational properties.
8.1.1 Matching Tensor Product
Since the data residing in different databases may have inter-dependencies (they are
based on the partial overlapping between databases, which is information about a
common part of the world), we can define such an (partial) overlapping by mor-
phisms of the category
DB
: information flux of each mapping between two objects
A
and
B
in
DB
is just a subset of this overlapping between these two databases,
denoted by
A
B
. It is “bidirectional”, i.e., (by duality) for any mapping
f
from
A
into
B
there exists an
equivalent
mapping
f
OP
from
B
into
A
.
This overlapping represents the common matching between these two databases,
and is equal to the maximal information flux which can be defined between these
two databases. Consequently, we can formally introduce a denotational semantics
for the database matching operation
⊗
⊗
as follows:
Theorem 12
DB
is a strictly symmetric idempotent monoidal category
(
DB
,
⊗
,Υ,α,β,γ),
where Υ is the total object for a given universe of databases
,
with the “matching”
tensor product
⊗:
DB
×
DB
−→
DB
defined as follows
:
1.
Υ
⊗
A
=
A
⊗
Υ
TA
;
Otherwise
,
for any two database instances
(
objects
)
A
=
1
≤
j
≤
m
A
j
and
=
1
≤
i
≤
k
B
i
,
where all A
j
and B
i
are simple objects
,
with k,m
B
≥
1,
the
object A
(A,B) is the overlapping
(
matching
)
between A and B
,
intro-
duced by Definition
19
:
⊗
B
≡⊗
TA
∩
TB
if m
=
k
=
1
,A
=
A
1
,B
=
B
1
;
A
⊗
B
1
≤
i
≤
k
&1
≤
j
≤
m
(A
j
⊗
B
i
) otherwise.
2.
id
Υ
⊗
f
=
f
⊗
id
Υ
Tf
;
Otherwise
,
for any two arrows f
:
A
→
C and g
:
B
→
D
,
the f
⊗
g
≡
⊗
(f,g)
:
A
⊗
B
→
C
⊗
D is defined by canonical representation
(
Lemma
8
)
of the set of ptp arrows
{{
if
f
g
={
(f
0
id
R
:
R
→
R
|
R
∈
∩
g)
=⊥
}}
={
f
}
,
g
};
f
⊗
g
id
R
|
R
∈
f
i
∩
g
j
}=⊥
f
g
1
{
h
ij
={
|
f
i
∈
,g
j
∈
}
otherwise
such that for each point-to-point arrow
T
dom(f
i
)
∩
T
dom(g
j
)
→
T
cod(f
i
)
∩
T
cod(g
j
)
in
f
⊗
g
h
ij
:
,
one has h
ij
=
f
i
∩
g
j
=⊥
0
.
