Database Reference
In-Depth Information
Proposition 35
Given a
flattened
guarded system of equations E of a database-
mapping program represented by a graph G
,
there is a unique (X
Σ
P
)-
g
E
,
where
homomorphism id
X
#
:
T
P
X,
I
)
→
[
id
X
,h
X
]
) such that id
X
#
=
(
(X,
the mapping h
X
:
Σ
P
X
→
X is defined by
:
1.
nil
Act
,
A
→
p
k
if (p
k
=
A)
∈
E
;
p
0
otherwise
;
2.
(p
k
,i)
→
p
m
if (p
m
=
a
i
.p
k
)
∈
E
;
p
0
otherwise
;
3.
(p
i
1
,...,p
i
n
)
→
p
m
if (p
m
=
→
p
0
,
and for any A
∈
n
(p
i
1
,...,p
i
n
))
∈
E
;
p
0
otherwise
,
so that the following initial algebra semantics diagram commutes
:
Proof
It is easy to verify that the square diagram above commutes for
g
E
: for each
p
k
∈
p
k
, with
g
E
(p
k
)
X
,
inl
X
(p
k
)
=
=
p
k
, because
p
k
∈[
p
k
]
E
, so that the left
diagram commutes.
1. For
nil
T
P
X)
,
g
E
(inr
X
(nil))
g
E
(nil)
∈
Σ
P
(
=
=
p
0
because from
(p
0
=
nil)
∈
p
0
]
E
. At the same time,
h
X
(Σ
P
(
g
E
(nil)))
E
we have
nil
∈[
=
h
X
(nil)
=
p
0
.
Similarly, for each
A
∈
Act
(if
A/
∈[
p
i
]
E
for each
p
i
∈
X, i
≥
1, then
A
∈[
p
0
]
E
).
2. For
(t,i)
∈
Σ
P
(
T
P
X)
we have two cases:
2.1.
g
E
(t)
p
0
]
E
, so that
h
X
(Σ
P
(
g
E
(t,i)))
=
p
0
, i.e.,
t
∈[
=
h
X
(p
0
,i)
=
p
0
a
i
.p
0
)
in
E
). While
g
E
(inr
X
(t,i))
g
E
(a
i
.t)
(there is no equation
(p
0
=
=
=
∈[
p
0
]
E
then also
a
i
.t
∈[
p
0
]
E
.
p
0
because if
t
2.2.
g
E
(t)
1. This time
h
X
(Σ
P
(
g
E
(t,i)))
=
h
X
(p
k
,i)
=
p
m
if
(p
m
=
a
i
.p
k
)
∈
E
(or if
a
i
.p
k
∈[
p
m
]
E
, i.e., from
t
≡
p
k
,
a
i
.t
∈[
p
m
]
E
);
p
0
otherwise. While,
g
E
(inr
X
(t,i))
=
=
p
k
, i.e.,
t
∈[
p
k
]
E
or
t
≡
p
k
,
k
≥
g
E
(a
i
.t)
=
p
m
if
a
i
.t
∈[
p
m
]
E
);
p
0
otherwise. Thus, the commutativity is satisfied.
3. For
(t
1
,...,t
n
)
∈
Σ
P
(
T
P
X)
, we have two cases:
3.1. If
p
i
k
≡
t
k
with
i
k
>
0 for all
k
1
,...,n
then
h
X
Σ
P
g
E
(t
1
,...,t
n
)
=
=
h
X
(p
i
1
,...,p
i
n
)
=
p
m
n
(p
i
1
,...,p
i
n
))
n
(p
i
1
,...,p
i
n
)
if
(p
m
=
∈
E
, i.e., if
∈[
p
m
]
E
;
p
0
other-
wise. While,
g
E
(inr
X
(t
1
,...,t
n
))
g
E
(
n
(t
1
,...,t
n
))
n
(t
1
,...,
=
=
p
m
if
n
(p
i
1
,...,p
i
n
)
∈[
p
m
]
E
and, from
p
i
k
≡
∈[
p
m
]
E
;
p
0
otherwise.
t
n
)
t
k
,
Thus, the commutativity is satisfied.
3.2. If there exists 1
≤
k
≤
n
such that
t
k
≡
p
0
then
h
X
Σ
P
g
E
(t
1
,...,t
k
,...,t
n
)
=
h
X
(p
i
1
,...,p
0
,...,p
i
n
)
=
p
0
n
(p
i
1
,...,p
0
,...,p
i
n
))
because there does not exist the equation
(p
m
=
in
E
. At the same time,
