Database Reference
In-Depth Information
from
T
P
X
instead of
X
, which may increase the expressiveness of representation.
For the observations to be continued with these successors, the distributive law
λ
lifts the specification for
X
to
T
P
X
, so that we obtain the observables of the lan-
guage
T
P
X
.This
λ
-coiteration schema
n
eeds two additional assumptions in order
to uniquely define arrows into the final
B
)
.
A major application of the notion of a distributive law
λ
in computer science has
been given in [
39
].
The formal definition of the
λ
-coiteration schema [
6
] is based on the syntax
monad
(
T
P
,η,μ)
and behavior endofunctor
F
(here we will use the basic
Set
cat-
egory, with
B
P
-coalgebra
(
D
P
S
,
∅∈
F(X)
for any set
X
) with the distributive law, expressed by the
natural transformation
λ
:
T
P
F
→
F
T
P
such that the following diagrams (coher-
ence unit and multiplication axioms) for each set
X
commute:
A distributive law
λ
assigns
F
-behaviors to the set of the language terms (composed
programs) in
T
P
X
, given the behaviors of the elements from
X
. Intuitively, the pres-
ence of the distribution law tells us that the program terms and behaviors interact
appropriately.
In the case of the database-mapping operational semantics, we have the following
lemma:
Lemma 13
In the case when F
=
B
P
=
P
fin
(Act
×
_)
:
Set
→
Set
,
we have a
distributive law given by the natural transformation λ
:
T
P
B
P
→
B
P
T
P
,
defined re-
cursively for each set X by the mapping λ
X
:
T
P
(
B
P
(X))
→
B
P
(
T
P
X) as follows
:
1.
nil
;
2.
S
i
→
S
i
,
for any S
i
∈
B
P
(X)
⊆
T
P
(
B
P
(X))
;
3.
a.t
→{
(a,a
k
.t
k
)
|
(a
k
,t
k
)
∈
λ
X
(t)
}
→∅
,
and for any a
∈
Act
,
a
→∅
if n
=|
λ
X
(t)
|≥
1;
∅
otherwise
;
n
(t
1
,...,t
n
)
→
1
≤
i
≤
n
λ
X
(t
i
)
.
4.
Proof
For any renaming of the variables
f
:
X
→
Y
,
λ
Y
◦
T
P
B
P
(f )
=
B
P
)
T
P
(f )
◦
(
λ
X
,
