PLS Lab

\omega-complete partial order

A partial order (D, \sqsubseteq) is \omega complete (or an \omega-cpo) just if it has least upper bounds for all \omega-chains.

What is an \omega-chain?

An \omega-chain (x_i){i \in \omega} is just an increasing sequence

x_0 \sqsubseteq x_1 \sqsubseteq x_2 \sqsubseteq \ldots

of elements of D. The x_i's can be thought of as a sequence of increasingly informative elements of D, and the least upper bound \bigsqcup_{i \in \omega} x_i \in D can be thought of as the "limit" of this sequence, i.e. the least informative object that contains all the information carried by the approximations x_i.

What is it used for?

The useful thing about \omega cpos if that every \omega-continuous map f : D \to D has a least fixed point. This is known as Kleene's fixed point theorem.