Mathematical Preliminaries - Semantics of Probabilistic Processes: An Operational Approach - page 11

(finite or infinite) strings with elements from A ∪{ nil } . The ground rules determined

by the two rules in ( 2.2 ) are

l

and, for each l ∈ X and a ∈ A , .

nil a · l

Let R be a set of ground rules on X . In general R is not necessarily continuous
or cocontinuous on the complete lattice (

P ( X ), ↆ ). For example, consider the rule

x 1 ... x n ...
x
whose premise is an infinite set. For any n ≥ 1, let X n ={ x 1 , ... , x n } . Then we

∈ n R ( X n ). Thus, R is not continuous.
Below we impose some conditions on R to recover continuity and cocontinuity.

∈ R ( n X n ), but x have x

Definition 2.5 A set of rules R is finite in the premises (FP), if in each rule ( S , x ) R

the premise set S is finite. A set of rules R is finite in the conclusions (FC), if for
each x , the set

∈

is finite; that is, there are finitely many rules whose
conclusion is x , though each premise set S may be infinite.

{ S | ( S , x ) ∈ R }

Proposition 2.2 Let R be a set of ground rules.
1. If R is FP, then R is continuous;
2. If R is FC, then R is cocontinuous.

Proof The two statements are dual, so we only prove the second one.
Let S 0 ↇ S 1 ↇ···ↇ S n ↇ··· be a decreasing chain. We need to show that

n ≥ 0 R ( S n )

= R (
n ≥ 0

S n ) .

One direction is easy. Since n ≥ 0 S n ↆ

S n and R is monotone, we have that

R (
n ≥ 0 R ( S n ) .

S n ) ↆ

0 n ≥

The converse inclusion follows from the condition that R is FC. Let x be any element
in n ≥ 0 R ( S n ). Then x ∈ R ( S n ) for each n , which means that for each n ≥ 0 there

is some S n ↆ S n with ( S n , x )

∈ R . Since R is FC, there exists some k ≥ 0 such

that S n = S k for all n ≥ k . Moreover, S k ↆ S k ↆ S n for all n ≤ k . Therefore,

S k ↆ n ≥ 0 S n and we have that x ∈ R ( n ≥ 0 S n ). Thus, we have proved that

n ≥ 0 R ( S n )

ↆ R (
n ≥ 0

S n ) .

Corollary 2.1 Let R be a set of ground rules on X.