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

Chapter 2
Mathematical Preliminaries

Abstract We briefly introduce some mathematical concepts and associated important
theorems that will be used in the subsequent chapters to study the semantics of
probabilistic processes. The main topics covered in this chapter include the Knaster-
Tarski fixed-point theorem, continuous functions over complete lattices, induction
and coinduction proof principles, compact sets in topological spaces, the separation
theorem, the Banach fixed-point theorem, the ˀ - ʻ theorem and the duality theorem
in linear programming. Most of the theorems are stated without proofs because they
can be found in many textbooks.

· · · · · ·

Keywords Lattice Induction Coinduction Topology Metric Probability Linear

programming

2.1 Lattice Theory

A very useful tool to study the semantics of formal languages is the Knaster-Tarski
fixed-point theorem, which will be used many times in subsequent chapters. We
begin with some basic notions from lattice theory.

Definition 2.1 A set X with a binary relation is called a partially ordered set ,if

the following holds for all x , y , z ∈ X :

1. x x (reflexivity);

2. If x y and y x , then x = y (antisymmetry);

3. If x y and y z , then x z (transitivity).

An element x ∈ X is called an upper bound for a subset Y ↆ X ,if y x for all

y ∈ Y . Dually, x is a lower bound for Y if x y for all y ∈ Y . Note that a subset

might not have any upper bound or lower bound.

Example 2.1 Consider the set X ={ 0, 1, 2 } with the binary relation defined by

= Id X ∪{ (0, 1), (0, 2) } , where Id X is the identity relation { (0, 0), (1, 1), (2, 2) } .It

{ }

constitutes a partially ordered set. The subset 1, 2 has no upper bound, as Fig. 2.1 a

shows.
Often we can use Hasse diagrams to describe finite partially ordered sets. For a
partially ordered set ( X , ), we represent each element of X as a vertex and draw