Information Technology Reference
In-Depth Information
is a finite set. In previous works, for example in [CHS92], these properties are
guaranteed by using results from [BBK87] that every BPA process is bisimulation
equivalent to a process which is a solution to an equation system in Greibach
Normal Form. Here we take a more direct approach to prove the properties
directly for the labelled transition system.
For
E
, the closure set of
E
, written
cl
(
E
), is inductively defined on the
structure of
E
as follows:
∈E
cl
(
a
)=
cl
(
X
)=
,
cl
(
Σ
i∈I
E
i
)=
i∈I
cl
(
E
i
)
,
cl
(
E
;
F
)=
cl
(
E
)
∅
∪
cl
(
F
)
∪{
F
}
,
E
{
E
∈
cl
(
μX.E
)=
{
μX.E/X
}|
cl
(
E
)
}
.
The following two lemmas are easily proved by direct structural induction.
Lemma 1.
Let
E
∈E
,then
cl
(
E
)
is a finite set.
Lemma 2.
Let
E, F
∈E
.If
E
∈
cl
(
F
)
then
fv
(
E
)
⊆
fv
(
F
)
.
∈E
∗
, its closure, also written
cl
(
α
) (a harmless misuse of notation), is
defined such that
cl
(
)=
For
α
cl
(
α
). Now the finiteness
property which we need to show is that if
E
occurs in the sequence
β
which is
reachable from
α
, then either
E
occurs in
α
or
E
∅
and
cl
(
Eα
)=
cl
(
E
)
∪
cl
(
α
). Thus such
E
must
be from a finite set, since obviously by Lemma 1
cl
(
α
) is a finite set, and the
number of processes that occur in
α
is also finite.
∈
Lemma 3.
cl
(
E
{
μX.E/X
}
)
⊆
cl
(
μX.E
)
.
Proof:
We prove by induction on the structure of
F
the following inclusion:
F
{
F
∈
cl
(
F
{
μX.E/X
}
)
⊆{
μX.E/X
}|
cl
(
F
)
}∪
cl
(
μX.E
)
.
Then take
F
to be
E
we obtain the inclusion relation we want.
When
F
≡
F
1
;
F
2
we have the following sequence of inclusions:
cl
(
F
{
μX.E/X
}
)
=
cl
(
F
1
{
μX.E/X
}
;
F
2
{
μX.E/X
}
)
=
cl
(
F
1
{
μX.E/X
}
)
∪
cl
(
F
2
{
μX.E/X
}
)
∪{
F
2
{
μX.E/X
}}
def. of
cl
F
{
F
∈
F
{
F
∈
⊆{
μX.E/X
}|
cl
(
F
1
)
}∪{
μX.E/X
}|
cl
(
F
2
)
}
∪
cl
(
μX.E
)
∪{
F
2
{
μX.E/X
}}
ind. hyp.
F
{
F
∈
cl
(
μX.E
)
.
def. of
cl
When
F ≡ Σ
i∈I
E
i
the calculation is similar to the case for
F
1
;
F
2
.
The key case is when
F ≡ μY.F
1
, and without loss of generality we can assume
that
Y
does not occur free in
μX.E
. We calculate as follows:
=
{
μX.E/X
}|
cl
(
F
1
;
F
2
)
}∪
Search WWH ::
Custom Search