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

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:

  1. 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.
  2. \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.

      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.

      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.

      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.

      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.