Database Reference
In-Depth Information
f
Over
65
∀
x
e
f
Emp
(x
e
)
.
∃
f
1
∃
f
Emp
∃
1
∧
Local
(x
e
)
⇒
Office
x
e
,f
1
(x
e
)
=
x
e
f
Emp
(x
e
)
.
1
∧
f
Over
65
(x
e
)
.
1
⇒
CanRetire
(x
e
)
.
∧∀
=
=
By application of the algorithm
VarTransform
to these two implications in
Φ
,we
obtain the following respective im
pl
icati
o
ns:
3.1.
(
Emp
(x
e
)
.
=
∧
Local
(y
1
)
∧
(
1
1
)
∧
(y
1
=
x
e
)
∧
(z
1
=
f
1
(x
e
)))
⇒
Office
(x
e
,z
1
)
.
3.2.
(
Emp
(x
e
)
.
=
∧
Over65
(y
1
)
∧
(
1
1
)
∧
(y
1
=
x
e
)
∧
r
(
1
,
1
))
⇒
CanRetire
(x
e
)
.
If we were to consider the case when an employee could retire when
he reached the age of 65 but with only 80 % of the full pension, and only
if he retired at the age of 70 or older he would receive the full pension, we
could introduce the function
f
%
:
N
→[
]
=
≤
0
,
1
such that
f
%
(x)
0if
x
64,
f
%
(x)
70.
Then we may replace the unary relation
Over65
by the binary relation
People
where the first attribute is equal to the attribute of
Over65
and the
second is for the age when he asked for the retirement. Analogously, we add
the second attribute to the relation
CanRetire
dedicated to the reduction
index for its pension. Consequently, the second implication above will be
substituted by the implication,
=
1if
x
≥
70, and
f
%
(x)
=
0
.
8
+
0
.
4
∗
(x
−
65
)
for 65
≤
x
≤
x
f
Emp
(x
e
)
.
1
∧
f
Person
(x
e
,x)
.
1
⇒
CanRetire
x
e
,f
%
(x)
.
∀
x
e
∀
=
=
By application of the algorithm
VarTransform
to this new implication, we
obtain the following implication:
3.3.
(
Emp
(x
e
)
∧
Person
(y
1
,x)
∧
(x
≥
65
)
∧
(y
1
=
x
e
)
∧
(z
1
=
f
%
(x)))
⇒
CanRetire
(x
e
,z
1
)
,
and hence
C(x)
is a condition
(x
≥
65
)
,
S
j
={
(y
1
=
x
e
)
}
and
S
F
=
{
(z
1
=
f
%
(x))
}
.
Based on this algorithm, we can demonstrate the following theorem:
Theorem 9
The signature of the R-algebra used to define the database mappings
in the
DB
category is composed of the following family of operations
:
1.
The identity functions id
R
:
R
→
R
,
for any relation R
∈
Υ
;
2.
The injections
(
inclusion functions
)
in
:
R
→
R
1
(
with R
⊆
R
1
)
and the inverse-
inclusions in
−
1
:
R
1
R
(
i
.
e
.,
the surjective one-to-one functions
);
3.
The projections π
S
:
R
2
such that the list S is a subset of the set of at-
tributes of R
1
and the set attributes of R
2
is equal to this list S
;
4.
The n-ary
(
n
≥
R
1
→
2)
Cartesian functions f
(n)
⊗
:
R
1
×···×
R
n
→
R such that
=
1
≤
i
≤
n
ar(R
i
)
,
and for any
d
i
∈
ar(R)
R
i
,
1
≤
i
≤
n
,
f
(n)
⊗
(
d
1
,...,
d
n
)
=
d
1
&
···
&
d
n
;
