Definition. Upper bound [dm-000C]

An upper bound of a set $Y$ is some $x$ such that $\forall y \in Y.\ y \sqsubseteq x$ (where $\sqsubseteq$ is some partial order).

Backlinks

Exercise. [dt-001X]

Liam O'Connor

Show that if A and B are posets and X \subseteq A \times B is directed (by the ordering in Construction [dt-000E]), then the subsets \pi _0(X) \subseteq A and \pi _1(X) \subseteq B (defined below) are also directed. \begin {array}{lcl} \pi _0(X) & = & \{ a \in A \mid \exists b \in B.\ (a,b) \in X \}\\ \pi _1(X) & = & \{ b \in B \mid \exists a \in A.\ (a,b) \in X \}\\ \end {array}
Solution.
- Liam O'Connor
Given two elements $x,y \in \pi _0(X)$ , we know that there exists $b_x, b_y \in B$ such that $(x,b_x) \in X$ and $(y,b_y) \in X$ . Because $X$ is directed, we can conclude that there exists an upper bound $(z, b_z) \in X$ where $x \sqsubseteq z$ and $y \sqsubseteq z$ . As $z \in \pi _0(X)$ , $z$ is an upper bound in $\pi _0(X)$ for both $x$ and $y$ and thus $\pi _0(X)$ is directed. The proof for $\pi _1$ is analogous.
Give an example of a set X \subseteq \{\top ,\bot \}\times \{\top ,\bot \} such that \pi _0(X) and \pi _1(X) are directed, but X is not.
Solution.
- Liam O'Connor
$X = \{(\top ,\bot ), (\bot ,\top )\}$ is not directed as the two elements are not comparable, but $\pi _0(X) = \pi _1(X) = \{\top ,\bot \}$ which is directed as $\bot \sqsubseteq \top$ .
Show that if $A$ and $B$ are cpos and $X \subseteq A \times B$ is directed, then $\bigsqcup X = \left (\bigsqcup \pi _0(X), \bigsqcup \pi _1(X)\right )$ Note: Together with $\bot _{A\times B} = (\bot _A, \bot _B)$ this shows that the Cartesian product of two cpos is itself a cpo.

Solution.

Liam O'Connor

Let $(x,y) = \left (\bigsqcup \pi _0(X), \bigsqcup \pi _1(X)\right )$ . Because of the ordering in Construction [dt-000E], $(x,y)$ is certainly a upper bound of the directed set $X$ . To show it is the least upper bound, assume for the sake of contradiction that $(x,y)$ is not the least upper bound of $X$ . Then, there must be a $(v,w)\sqsubset (x,y)$ such that $\forall x \in X.\ x \sqsubseteq (v,w)$ . But then, $v$ would be a lesser upper bound for $\pi _0(X)$ than $x$ , which is supposed to be the lub. Thus there is a contradiction, and $(x,y)$ must be the lub of $X$ .

Exercise. [dt-001N]

Liam O'Connor

Show that if a function on cpos $f : A \rightarrow B$ is monotonic, then $\bigsqcup \{ f(x) \mid x \in X \}$ exists for any directed $X \subseteq A$ (i.e.the first condition for continuity in Definition [dt-001J]).

Hint: It suffices to show that $\{ f(x) \mid x \in X \} \subseteq B$ is directed.

Solution.

Liam O'Connor

Because $B$ is a cpo, it suffices to show that $\{ f(x) \mid x \in X \} \subseteq B$ is directed. Let $a,b \in \{ f(x) \mid x \in X \}$ . Let $x_a, x_b \in X$ be the values that $f$ maps to $a$ and $b$ respectively, i.e. $f(x_a) = a$ and $f(x_b) = b$ . Because $X$ is directed, an upper bound of $x_a$ and $x_b$ exists in $X$ . Call this upper bound $x_c$ . Because $x_a \sqsubseteq x_c$ and $x_b \sqsubseteq x_c$ , we know that $f(x_a) = a \sqsubseteq f(x_c)$ and $f(x_b) = b \sqsubseteq f(x_c)$ by monotonicity of $f$ . Also, $f(x_c) \in \{ f(x) \mid x \in X \}$ because $x_c \in X$ . Therefore, because two arbitrary elements in $\{ f(x) \mid x \in X \}$ have an upper bound within the set, the set $\{ f(x) \mid x \in X \}$ is directed.

Theorem. Alternative characterisation of directedness [dt-0014]

Liam O'Connor

A subset $Y \subseteq X$ of a poset $X$ is directed iff every finite subset of $Y' \subseteq Y$ has an upper bound in $Y$ .

Proof.

Liam O'Connor

⇐: Every pair of elements $x,y \in Y$ has an upper bound simply by taking the upper bound of the set $\{x,y\}.$
⇒: Given a finite set $X = \{x_1,x_2,\dots , x_n\}$ , we can show it has an upper bound by an inductive process, first taking the upper bound of $x_1$ and $x_2$ , and then taking the upper bound of that an $x_3$ and so on until we have an upper bound for the whole set. This induction works because the set $X$ is finite.

Theorem. Chain → Directed [dt-0012]

Liam O'Connor

All non-empty chains are directed.

Proof.

Liam O'Connor

Let $C$ be a chain. Then, given two elements $x,y \in C$ we know from totality that either $x \sqsubseteq y$ or $y \sqsubseteq x$ . If $x \sqsubseteq y$ , then $y$ is the upper bound, otherwise $x$ is the upper bound.

Definition. Consistent completeness [dt-004E]

Liam O'Connor

A poset $A$ is consistent complete (or bounded complete) iff $\bigsqcup X$ exists for all consistent $X \subseteq A$ . That is, any set with an upper bound (a consistent set) has a least upper bound.

Definition. Consistent subset [dt-0013]

A subset $Y \subseteq X$ of a poset $X$ is consistent iff $\exists x \in X.\ \forall y \in Y.\ y \sqsubseteq x$ Such an $x$ is called an upper bound of $Y$ .

Definition. Directed set [dt-0010]

Liam O'Connor

Formally, a non-empty subset $Y \subseteq X$ of a poset $(X,\sqsubseteq )$ is directed iff: $\forall x, y \in Y.\ \exists z \in Y.\ x \sqsubseteq z \land y \sqsubseteq z$

The

z

above is an upper bound of

x

and

y

. Hence, a non-empty set is directed iff every pair of values has an upper bound in the set.

Intuitively, directed sets are "going somewhere" — given two elements we can always find a "greater" one in the set.

Definition. Least upper bound [dt-0017]

Liam O'Connor

Let $X \subseteq Y$ be a subset of a poset $Y$ . An element $y \in Y$ is a least upper bound (or lub) for $X$ iff:

It is an upper bound: $\forall x \in X.\ x \sqsubseteq y$
It is less than any other upper bound: $\forall y' \in Y.\ (\forall x \in X. x \sqsubseteq y') \Rightarrow y \sqsubseteq y'$

It follows that lubs are unique if they exist. We write the lub of a set

X

as

\bigsqcup X

, and usually write

x \sqcup y

as a shorthand for

\bigsqcup \{x,y\}

.

Theorem. The Kleene fixed point theorem [dt-001P]

Let $(S, \sqsubseteq )$ be a cpo and $f : S \rightarrow S$ be a continuous function. Then the lub of the Kleene chain $\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )$ is the least fixed point of $f$ .

Proof.

We apply continuity to show that it is a fixed point: $\begin {array}{lclr} f(\bigsqcup _{n \in \mathbb {N}} f^n(\bot ) ) & = & \bigsqcup _{n \in \mathbb {N}} f(f^n(\bot )) & \text {(continuity)} \\[0.5em] &=& \bigsqcup _{n \in \mathbb {N}} f^{n+1}(\bot )\\[0.5em] &=& \bigsqcup _{n=1,2\dots }f^{n}(\bot ) &\qquad \text {(reindexing)}\\[0.5em] &=& \bot \sqcup \bigsqcup _{n=1,2\dots }f^{n}(\bot )\\[0.5em] &=&\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )\\[0.5em] \end {array}$ To see that it is the least fixed point: Let $y$ be a fixed point of $f$ . We know that $\bot \sqsubseteq y$ by definition of $\bot$ . Taking $f$ of both sides, we get $f(\bot ) \sqsubseteq y$ . We can continue this inductively and thus we know that, for all $n \in \mathbb {N}$ , $f^n(\bot ) \sqsubseteq y$ . Because $y$ is, therefore, an upper bound of the ascending Kleene chain, it must also be at least as large as the lub of that chain.

Construction. The cpo of functions [dt-002L]

Liam O'Connor

If $A$ and $B$ are cpos, the set of continuous functions $A \twoheadrightarrow B$ is a cpo under the pointwise ordering: $f \sqsubseteq g\;\; \text {iff}\;\; \forall a \in A.\ f(a) \sqsubseteq g(a)$ The intuition of this ordering in terms of information is that we increase the information content of a function overall by increasing the information content of any (or many) argument values. To prove this, we must show:

$A \twoheadrightarrow B$ has a least element. $\bot _{A \twoheadrightarrow B}$ is the constant function that returns $\bot _B$ , i.e. $\lambda a.\ \bot _B$ .
$\bigsqcup X$ exists for all directed $X \subseteq A \twoheadrightarrow B$ . Our lub of a set of continuous functions \bigsqcup X is the function \Phi where: \Phi (a) = \bigsqcup \{ f(a) \mid f \in X\} We must show a number of properties of this lub \Phi . Specifically:
1. $\bigsqcup \{ f(a) \mid f \in X\}$ exists in $B$ .
  Proof.
  Liam O'Connor
  We want to show that the set $\{ f(a) \mid f \in X\}$ is directed. Take two values $g(a), h(a) \in \{ f(a) \mid f \in X\}$ . Since $X$ is directed, there exists a function $k \in X$ such that $g \sqsubseteq k$ and $h \sqsubseteq k$ . By applying the definition of $\sqsubseteq$ for functions above, we have $g(a) \sqsubseteq k(a)$ and $h(a) \sqsubseteq k(a)$ . Thus $k(a)$ is an upper bound of these two values $g(a), h(a)$ , and thus $\{ f(a) \mid f \in X\}$ is directed, and thus its lub exists since $B$ is a cpo.
2. $\Phi (a) = \bigsqcup \{ f(a) \mid f \in X \}$ is continuous.
  Proof.
  Liam O'Connor
  Using the alternative characterisation of continuity
  $\begin {array}{lclr} \Phi (\bigsqcup Y) &=& \bigsqcup \{ f(\bigsqcup Y) \mid f \in X \} & \text {(defn. $\Phi $)}\\ & = & \bigsqcup \{\bigsqcup \{ f(y) \mid y \in Y \} \mid f \in X \} & \text {($f$ is continuous)}\\ & = & \bigsqcup \{\bigsqcup \{ f(y) \mid f \in X \} \mid y \in Y \} & \text {(swap lubs)}\\ & = & \bigsqcup \{ \Phi (y) \mid y \in Y \} & \text {(defn. $\Phi $)}\\ \end {array}$ Monotonicity is similar to prove.
3. $\Phi$ is an upper bound for $X \subseteq A \twoheadrightarrow B$ .
  Proof.
  Liam O'Connor
  Let $g \in X$ . Then for any $a \in A$ we have $g(a) \in \{ f(a) \mid f \in X\}$ . Now, by 2a and lubs, we have $g(a) \sqsubseteq \bigsqcup \{ f(a) \mid f \in X \}$ , which by the definition of $\Phi$ gives $g(a) \sqsubseteq \Phi (a)$ . Hence, by the definition of $\sqsubseteq$ on functions, we can conclude $g \sqsubseteq \Phi$ .
4. $\Phi$ is the least upper bound for $X$ .
  Proof.
  Liam O'Connor
  Let $g \in A \twoheadrightarrow B$ be an upper bound for $X \subseteq A \twoheadrightarrow B$ . Then (using $\sqsubseteq$ on functions) $g(a)$ is an upper bound for $\{f(a) \mid f \in X\}$ for all $a \in A$ . Now, by 2a and lubs, we have $\bigsqcup \{f(a) \mid f \in X\} \sqsubseteq g(a)$ , i.e. $\Phi (a) \sqsubseteq g(a)$ , which, by the definition of $\sqsubseteq$ on functions, allows us to conclude $\Phi \sqsubseteq g$ .

Definition. Upper bounds in the category $\mathbf {Cpo}$ [dt-004R]

A cpo $A$ is an upper bound of an $\omega$ -chain of cpos in the category $\mathbf {Cpo}$ if there is a family of continuous functions $\{g_i : A_i \twoheadrightarrow A \mid i \in \mathbb {N}\}$ such that the following diagram commutes (i.e. $g_i = g_{i+1} \circ f_i$ for all $i \in \mathbb {N}$ ):

Definition. Upper bounds in the category $\mathbf {Cpo}^\mathbf {R}$ [dt-005G]

A cpo $A$ is an upper bound of an $\omega$ -chain of cpos $A_i$ in the category $\mathbf {Cpo}^\textbf {R}$ if there is a family of retraction pairs $A_i \xtofrom [g_i]{f_i} A$ such that the following diagram commutes (i.e. for all $i \in \mathbb {N}$ , $(f_i, g_i) = (f_{i+1},g_{i+1}) \circ (s_i,t_i)$ , where $\circ$ is composition of retraction pairs):

Related

Definition. Partial order [dm-0000]

Liam O'Connor

A binary relation $(\sqsubseteq ) \subseteq X \times X$ is a partial order if it is, for all $x, y, z \in X$ :

reflexive: $x \sqsubseteq x$ ,
transitive: $x \sqsubseteq y$ and $y \sqsubseteq z$ implies $x \sqsubseteq z$ ,
antisymmetric: $x \sqsubseteq y$ and $y \sqsubseteq x$ implies $x = y$ .