Complete partial orders and fixpoint theorems

The pair is called a partial order, when is a partial order on D, that is, a reflexive, antisymmetric and transitive relation. Let . We say that d is a lower bound of X if, for all , . d is the greatest lower bound (glb) of X, if d is a lower bound, and, for every e such that e is a lower bound of X, we have . An analogue definition holds for upper bounds and the least upper bound (lub). We say that is a minimal (or bottom) element of D, if is a lower bound for D.

Definition 136. is a complete partial order (cpo) if is a partial order, and, for every increasing, countable sequence (so-called chain) , , of elements of D its least upper bound exists.

Definition 137. Let D, E be partial orders. A function is monotonic, if for every , , implies .

Definition 138. Let D, E be complete partial orders. A function is continuous, if it is monotonic, and, for every chain of elements of D,

The set of continuous functions from the cpo D to the cpo E will be denoted by .

Example 139. ([11])

  1. Every set ordered by the identity function is a discrete cpo. Any function from discrete cpo’s to discrete cpo’s are continuous.

  2. Let be the cpo consisting of elements and such that .

  3. Let X be a set. Let . Then is a complete lattice.

  4. Let . Then F is a cpo.

  5. Let be the partial order . Then is a cpo. Let be such that

    Then is continuous for every , but is not continuous.

Lemma 140. Let and . Then , where is the function composition of f and g.

Definition 141. Let be a partial order, let . Then

  1. d is a prefixpoint of f if ,

  2. d is a postpoint of f if .

A fixpoint of f is both a prefixpoint and a postfixpoint. d is called the least fixpoint (lfp) of f , if d is a fixpoint, and, for every , .

Without proof we state the following theorem.

Theorem 142. (Knaster and Tarski) Let be a cpo with bottom, assume . Then

is the least fixpoint of f , where , , and . Moreover, is the least prefixpoint of f , that is, if , then .

Below, we consider a straightforward application of the Knaster-Tarski theorem. Let X be a set, and be a relation over X. As before, let

and let . We assert the following lemma.

Lemma 143. Let , where and is the identity relation over X and . Then

Proof. First of all, observe that is continuous. For, let be a chain in . Then

This means, Theorem 142 is applicable. Let , and for . Thus,

By this, the lemma is proved.

As a consequence, we prove that indeed defines the reflexive, transitive closure of R.

Corollary 144. Let , and let be defined as above, and let . Furthermore, assume is such that Q is reflexive, transitive and . Then

Proof. By the Knaster–Tarski theorem it is enough to verify that Q is a prefixpoint of . By the reflexivity of Q, we have , moreover, by assumption, , which, together with transitivity, yields .