Database Reference
In-Depth Information
1
f
2
)(t
RA,
1
⊗
t
RA,
2
)
Proof
It is enough to demonstrate that
(f
1
⊗
#
=
f
1
(t
RA,
1
)
⊗
f
2
(t
RA,
2
)
t
RA,
2
→
t
RA,
2
))
is
1
f
2
:
1
f
2
)((t
RA,
1
⊗
#
and hence
f
1
⊗
t
RA,
1
⊗
(f
1
⊗
just an arrow in
RA
.
In fact, the first arrow
f
1
t
RA,
1
#
as the
executes all operations over the relation
original arrow
f
1
, while all projection operations _
[
S
]
with a tuple of attributes in
S
[
S
&
nr(R
2
)
]
in
f
1
are transformed into _
(concatenation of the tuple
S
and the tuple
of names
nr(R
2
)
, in the way that also all columns of the relation
R
2
are propagated
to the final result. Analogously, the second arrow
f
2
executes all operations over
the relation
R
ρ
2
as the original arrow
f
2
, while all projection operations _
[
S
]
in
f
2
are transformed into _
, in the way that all columns of the relation
R
1
are propagated to the final result. Consequently,
[
nr(R
1
)
&
S
]
t
ρ
1
f
2
)(t
RA,
1
⊗
(f
1
⊗
RA,
2
)
#
=
t
ρ
f
2
(t
ρ
(f
2
(f
1
(t
RA,
1
⊗
RA,
2
)))
#
=
f
1
(t
RA,
1
)
⊗
RA,
2
)
#
.
f
2
◦
f
1
1
f
2
=
From the fact that
f
1
⊗
, for the cases when
f
1
or
f
2
(or both) are
the identity arrows, we obtain that
f
2
=
1
(id
1
,f
2
)
,
f
1
=
1
f
2
=⊗
1
id
2
=
id
1
⊗
f
1
⊗
f
2
◦
f
1
=
1
(f
1
, id
2
)
and hence
1
(id
1
, id
2
)
1
f
2
=
1
f
2
)
⊗
⊗
=
id
. Thus,
f
1
⊗
(id
1
⊗
◦
1
id
2
)
1
(f
2
◦
(f
1
⊗
id
2
)
(it is easy to show that this is a special case
of the more general property
(g
2
⊗
=
(id
1
◦
f
1
)
⊗
1
h
2
)
1
h
1
)
1
(h
2
◦
◦
(g
1
⊗
=
(g
2
◦
g
1
)
⊗
h
1
)
), and
1
hence
⊗
satisfies the functorial properties.
Hence
(A
⊗
B)
⊗
C
#
=
A
⊗
(B
⊗
C)
#
,
⊥⊗
A
#
=
A
#
, and
A
⊗⊥
#
=
#
, so that the isomorphisms
α
A,B,C
,
λ
A
and
A
are the identity arrows in
RA
,
and hence
RA
is a strict monoidal category.
A
Based on the definition, we can reduce each term
f
1
(t
RA,
1
)
⊗
f
2
(t
RA,
2
)
to a
unique arrow in
RA
by an unfolding of
⊗
, as follows:
Definition 33
The unfolding of a simple binary tree-term in
T
RA
X
, with the node
_TIMES_(or_
dom(f
2
)
in
T
RA
X
where the paths
f
1
and
f
2
are the compositions of the unary operations
in
Σ
RA
\
⊗
_) and the leafs
t
RA,
1
=
dom(f
1
)
and
t
RA,
2
=
t
ρ
Σ
RA
, into a simple path tree with a unique leaf
t
RA,
1
⊗
RA,
2
∈
T
RA
X
,is
presented by:
