Database Reference
In-Depth Information
define
T
P
via an infinite coproduct (in
Set
it is the disjoint union
), commonly
written for a set of process variables in
X
(in
Set
the '
×
' denotes the Cartesian
product)
X
×{
i
}
n
X
ar(σ)
X
n
Σ
P
(X)
=
=
Act
∪{
nil
}
(7.1)
σ
∈
Σ
P
a
i
∈
Act
≥
2
}
n
≥
2
X
n
, where
and
X
Σ
P
(X)
=
X
∪
Act
∪{
nil
}∪{
X
×{
i
}|
a
i
∈
Act,i
=
1
,
2
,...
X
represents the set of variables,
X
×{
i
}
is the domain for the
i
th action-prefixing
unary operator
a
i
.
_in
Σ
P
, while the singleton
{
}
nil
is isomorphic to the terminal
n
X
object
1
in
Set
and the finite Cartesian products
X
n
=
×···×
X
is used as a
n
. More formally, for the signature
Σ
P
we
define the endofunctor (denoted by the same symbol)
Σ
P
:
domain for the finitary
n
-ary operator
Set
−→
Set
such that
σ
∈
Σ
P
B
ar(σ)
defined by (
7.1
), and any arrow in
for any object
B
in
Set
,
Σ
P
(B)
Set
(a function)
f
:
B
−→
C
,
Σ
P
(f )
σ
∈
Σ
P
f
ar(σ)
.
Moreover, for each set of variables
X
(an object in
Set
) we define the endo-
functor
(X
Σ
P
)
:
Set
−→
Set
such that for any object
B
in
Set
,
(X
Σ
P
)(B)
X
σ
∈
Σ
P
B
ar(σ)
, and any arrow in
Set
(a function)
f
:
B
−→
C
,
(X
Σ
P
)(f )
id
X
}
σ
∈
Σ
P
f
ar(σ)
, where
id
X
is the identity function for the set
X
.
For the signature endofunctor
Σ
P
and every set of process variables
X
, the initial
Σ
P
-algebra (Lambek's Lemma) is an isomorphism (for the carrier set
{
T
P
X
),
(X
Σ
P
)(
T
P
X)
I
T
P
X
with
I
=[
inl
X
, inr
X
]:
X
Σ
P
(
T
P
X)
−→
T
P
X
, where
inl
X
:
X
→
T
P
X
and
inr
X
:
Σ
P
(
T
P
X)
−→
T
P
X
are two injective arrows of the coproduct
X
Σ
P
(
T
P
X)
in
Set
. The free
Σ
P
-algebra
T
P
X
on a set of variables
X
may be computed as the
union of the chain obtained by iterating the functor
X
Σ
P
on the empty set
∅
Σ
P
X
)
∅⊆
X
Σ
P
(
∅
)
⊆
X
Σ
P
(
∅
Σ
P
X
Σ
P
X
)
⊆···
⊆
X
Σ
P
(
∅
∅
=
∪{
}
T
P
X,
I
)
is the
least
with
Σ
P
(
)
Act
nil
(so that the initial
X
Σ
P
-algebra
(
fixed point
of the functor
X
Σ
P
:
Set
→
Set
).
Consequently, the injection
inr
X
:
Σ
P
(
T
P
X)
−→
T
P
X
represents the composi-
tion of terms in the carrier set
T
P
X
(it is identity for the subset
Act
∪{
nil
}
), for
example:
1. For an element
(p
i
,
4
)
∈{
T
P
X
×{
4
}}⊆
Σ
P
(
T
P
X)
where
p
i
∈
X
⊆
T
P
X
is a
given variable,
inr
X
(p
i
,
4
)
=
a
4
.p
i
∈
T
P
X
is a term;
2. For
(t
1
,
3
)
∈{
T
P
X
×{
3
}}⊆
Σ
P
(
T
P
X)
where
t
1
is a term with variables in
T
P
X
,
a
3
.t
1
∈
T
P
X
is a term;
3. For
(t
1
,t
2
)
∈
T
P
X
2
,
inr
X
(t
1
,t
2
)
=
t
1
t
2
∈
T
P
X
is a term.
inr
X
(t
1
,
3
)
=
