Database Reference
In-Depth Information
3. We introduce the bijection
[
_
]
E
:
X
→
T
P
X/
≡
, where
T
P
X/
≡
is the quotient
Σ
P
algebra of terms with the congruence
≡
defined for any two terms
t
1
,t
2
∈
T
P
X
by
t
1
≡
t
2
iff
[
t
1
]
E
=[
t
2
]
E
. Furthermore, for each
n
-ary operator
σ
∈
Σ
,inthis
quotient algebra of terms
T
P
X/
we have the corresponding
n
-ary operator
σ
≡
≡
such that
σ
≡
(
[
t
1
]
E
,...,
[
t
n
]
E
)
=[
σ(t
1
,...,t
n
)
]
E
.
From this definition, for any two terms
t
1
,t
2
∈
T
P
X
,
t
1
≡
t
2
iff
t
1
,t
2
∈[
p
k
]
E
for
some
p
k
∈
X
.
The following properties for a flattened system of equations obtained by the al-
gorithm
DBprog
are valid:
Proposition 34
For any flattened system of
(
also infinite
)
equations E with the as-
signment ass
,
obtained by the algorithm DBprog from a database-mapping
program specified by a graph G
,
there exist the following mappings
:
•
:
X
→
S
A
T
P
-coalgebra
g
E
=
inr
X
◦
Σ
P
(inl
X
)
◦
f
T
:
X
→
T
P
X
,
where f
T
:
X
→
Σ
P
(X) is a flattening mapping such that for any variable p
i
∈
X
,
⎧
⎨
⎩
a
if (p
i
=
a)
∈
E, a
∈
Act
∪{
nil
};
f
T
(p
i
)
=
(p
k
,m)
if (p
i
=
a
m
.p
k
)
∈
E
;
n
(p
k
1
,...,p
k
n
))
(p
k
1
,...,p
k
n
) if (p
i
=
∈
E.
Thus
,
g
E
(p
i
)
=
t
∈
T
P
X if (p
i
=
t)
∈
E
.
T
P
-algebra
g
E
∈
T
P
X
,
g
E
(t)
•
:
T
P
X
→
=
A
X such that for any term t
p
i
if
t
∈[
p
i
]
E
,
where
[
_
]
E
:
X
→
T
P
X/
≡
is a bijection in Definition
55
.
Hence
,
g
E
◦
g
E
=
id
X
:
X
→
X
.
•
A mapping
[
_
]=
ass,℘
:
X
→
S
×
P
fin
(Act
×
X)
,
where ass
:
X
→
S
is the
assignment for variables in the equations in E
,
and ℘
:
X
→
P
fin
(Act
×
X) is
defined by
:
for any p
k
∈
X
,
⎧
⎨
1
≤
i
≤
n
{
n
(p
k
+
1
,...,p
k
+
n
)
(ass(p
k
+
i
),p
k
+
i
)
}
if
g
E
(p
k
)
=
;
℘(p
k
)
=
{
(a,p
k
+
1
)
}
if
g
E
(p
k
)
=
a.p
k
+
1
;
⎩
∅
otherwise,
where
P
fin
is the powerset operator for all
finite
subsets
(
∅∈
P
fin
(Z) for any
,
including the empty
,
set Z
).
Proof
From the algorithm
DBprog
, we have no two different equations with the
same program variable on the left side, so that
g
E
is a function, and also
g
E
◦
g
E
=
p
i
]
E
, and
g
E
(t)
id
X
: for any
p
i
∈
X
,
g
E
(p
i
)
=
t
if
(p
i
=
t)
∈
E
⊆≡
, so that
t
∈[
=
p
i
.
Notice that from the algorithm
DBprog
, we always have a variable
p
0
∈
X
such
nil
and
g
E
(nil)
that
g
E
(p
0
)
=
=
p
0
because
(p
0
=
nil)
∈
E
always.
