Database Reference
In-Depth Information
Let us show this property for our database-mapping programs (in [
39
], the au-
thors considered the language where
is a non-deterministic choice, while here it
is a parallel execution). The type
B
P
of the behavior of our database-mapping pro-
B
P
(X)
=
(
P
fin
(X))
Act
, the covariant functor mapping a set
of process variables
X
to the set of functions from
Act
to the finite subsets of
X
.
Let
p
k
and
p
i
+
1
,...,p
i
+
n
range over
X
,
β
range over
(
gramming language is
P
fin
(X))
Act
(a function
β
:
Act
→
P
fin
(X)
)), and let us write
a
{
p
i
+
1
,...,p
i
+
n
}
for the function
β
from
Act
to
P
fin
(X)
mapping
a
to
{
p
i
+
1
,...,p
i
+
n
}
.
For example, for
℘
:
X
→
P
fin
(Act
×
X)
,let
℘(p
k
)
={
(a
1
,p
i
+
1
),...,(a
n
,
p
i
+
n
)
n
, into the subset
of
π
2
(℘ (p
k
))
(where
π
1
and
π
2
denote the first and second Cartesian projec-
tions) such that
(a
m
,p
i
+
m
)
}
. Then
β
maps each action
a
m
∈
π
1
(℘ (p
k
))
,1
≤
m
≤
∈
℘(p
k
)
for each
p
i
+
m
∈
∈
π
2
(℘ (p
k
))
; for each
a
m
/
π
1
(℘ (p
k
))
,
β(a
m
)
=∅
(empty set), that is,
β(a)
={
p
i
|
(a,p
i
)
∈
℘(p
k
)
}
. Thus, the
set
℘(p
k
)
can be equivalently represented by this function
β
:
Act
→
P
fin
(X)
, i.e.,
β
∈
(
P
fin
(X))
Act
.
Consequently, in what follows, we will use for the behaviors the functor
B
P
=
P
fin
(
_
)
Act
P
fin
(Act
Set
used in [
39
]; this choice is justified specially when
Act
is infinite, an hence for the
finite
subsets in
×
_
)
:
Set
→
Set
, instead of its equivalent functor
:
Set
→
P
fin
(Act
×
X)
we have no need to use the functions
β
:
Act
→
X
with the infinite domains.
The difference of our language where '
' denotes the parallel executions, from
the syntactically equal language in [
39
] where '
' denotes the nondeterministic
choice instead, is that in our case the function
β
can have more than one argument
a
∈
(while in [
39
]
β
has exactly one such argument), so
that
β
means just the parallel execution of all actions in the set
Act
such that
β(a)
=∅
{
a
∈
Act
|
β(a)
=∅}
.
n
'for
n
Moreover, we are using the finitary parallel operators '
≥
2 as well.
Then, for example, for each operator
σ
of the signature
Σ
P
={
nil, Act,
{
a.
_
}
a
∈
Act
,
n
{
}
n
≥
2
}
, the corresponding rules can be modeled as a function
:
X
X)
arity(σ)
σ
×
P
fin
(Act
×
→
P
fin
(Act
×
T
P
X),
as follows:
1. For nullary operators,
σ
=
nil
or
σ
∈
Act
,
σ
=∅∈
P
fin
(Act
×
T
P
X)
a constant (nullary operator)
;
2. For unary operators,
p
i
,
(a
1
,p
k
1
),...,(a
n
,p
k
n
)
=
a,
a.
_
n
(a
1
.p
k
1
,...,a
n
.p
k
n
)
∈
P
fin
(Act
×
T
P
X)
;
3. For
m
-ary,
m
≥
2, operators,
p
i
1
,
(a
11
,p
k
1
1
),...,(a
n
1
1
,p
k
n
1
1
)
,...,
p
i
m
,
(a
1
m
,p
k
1
m
),...,(a
n
m
m
,p
k
n
m
m
)
m
