Definition. Universal property for functions [dt-002T]

Liam O'Connor

\mathit {apply} \circ h = f\; \text {iff}\; h = \mathit {curry}(f)\times \mathsf {id}_B

Context

Functions [dt-002Z]

Liam O'Connor

Previously, such as in Example [dt-001U], we already implicitly assumed that the set of continuous functions on cpos $A \twoheadrightarrow B$ is itself a cpo. In this section, we will formalise this construction.

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$ .

Example. The space $\mathbb {B}_\bot \twoheadrightarrow \mathbb {B}_\bot$ [dt-002M]

Liam O'Connor

At each step "upwards" on this cpo, one arrow that ends in $\bot$ now points to a non- $\bot$ value (moving up the cpo $\mathbb {B}_\bot$ ).

Primitive functions for functions [dt-002P]

Liam O'Connor

Definition. The $\mathit {apply}$ function [dt-002N]

Liam O'Connor

The $\mathit {apply}$ function simply applies a given function to a given argument: $\begin {array}{l} \mathit {apply} : ((A \twoheadrightarrow B) \times A) \twoheadrightarrow B\\ \mathit {apply} (f, a) = f(a) \end {array}$

Exercise. [dt-002Q]

Liam O'Connor

Show that $\mathit {apply}$ is continuous.

Hint: A function $f : A \times B \rightarrow C$ is continuous iff it is continuous in each argument separately, i.e., iff $\forall a \in A.\ f(a,\cdot ) : B \rightarrow C$ is continuous, and $\forall b \in B.\ f(\cdot ,b) : A \rightarrow C$ is continuous.

Solution.

Liam O'Connor

First showing $\mathit {apply}(f,\cdot )$ is continuous for some continuous $f : A \twoheadrightarrow B$ , using the alternative characterisation

$\mathit {apply}(f,\cdot )$ is monotonic: Given $a, b \in A$ where $a \sqsubseteq b$ , we can see that $\mathit {apply}(f,a) = f(a) \sqsubseteq f(b) = \mathit {apply}(f,b)$ by the monotonicity of $f$ .
$\mathit {apply}(f,\cdot )$ preserves lubs: Given a directed $X \subseteq A$ , we can see that $\mathit {apply}(f,\bigsqcup X) = f(\bigsqcup X) = \bigsqcup \{f(x) \mid x \in X\} = \bigsqcup \{\mathit {apply}(f,x) \mid x \in X\}$ follows from the continuity of $f$ .

Next, showing

\mathit {apply}(\cdot ,a)

is continuous for some fixed

a \in A

:

$\mathit {apply}(\cdot ,a)$ is monotonic: Given $f, g \in A \twoheadrightarrow B$ where $f \sqsubseteq g$ , we can see that $\mathit {apply}(f,a) = f(a) \sqsubseteq g(a) = \mathit {apply}(g,a)$ by the pointwise ordering of functions.
$\mathit {apply}(\cdot ,a)$ preserves lubs: Given a directed $X \subseteq A \twoheadrightarrow B$ , we can see that $\mathit {apply}(\bigsqcup X, a) = \left (\bigsqcup X\right )(a) = \bigsqcup \{f(a) \mid f \in X\} = \bigsqcup \{\mathit {apply}(f,a) \mid f \in X\}$ follows from the lub definition for functions.

Definition. The $\mathit {curry}$ function [dt-002O]

Liam O'Connor

The function $\mathit {curry}$ transforms a function that takes two arguments all at once (as a product) into a function that takes the arguments one at a time. That is, if $f : A \times B \twoheadrightarrow C$ then: $\begin {array}{l} \mathit {curry}(f) : A \twoheadrightarrow (B \twoheadrightarrow C)\\ \mathit {curry}(f)(a)(b) = f(a, b) \end {array}$

Theorem. Continuity of $\mathit {curry}$ [dt-002S]

Liam O'Connor

$\mathit {curry}$ is continuous on $A \times B \twoheadrightarrow C$ .
$\mathit {curry}(f)$ , given continuous $f : A \times B \twoheadrightarrow C$ , is continuous on $A$ .
$\mathit {curry}(f)(a)$ , given continuous $f : A \times B \twoheadrightarrow C$ and $a \in A$ , is continuous on $B$ .

Exercise. [dt-002R]

Liam O'Connor

What is the common (functional programming) name for $\mathit {apply} \circ (f \times \mathsf {id})$ ?

Solution.

Liam O'Connor

$\mathit {uncurry}$

Definition. Universal property for functions [dt-002T]

Liam O'Connor

\mathit {apply} \circ h = f\; \text {iff}\; h = \mathit {curry}(f)\times \mathsf {id}_B

Theorem. The currying isomorphism [dt-002U]

Liam O'Connor

(A \times B)\twoheadrightarrow C \;\;\simeq \;\; A\twoheadrightarrow (B\twoheadrightarrow C)

Proof.

Liam O'Connor

Follows from the universal property for functions when set up with the isomorphism from curry and its inverse, the function in Exercise [dt-002R].

Remark. Why the function arrow is not a covariant bifunctor [dt-002V]

Liam O'Connor

For the $\twoheadrightarrow$ operator on cpos (Definition [dt-002F]) to be the object mapping for a bifunctor $\textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo}$ like $\times$ is (see Corollary [dt-002C]), we would need to define a morphism mapping $f \twoheadrightarrow g$ that, given two functions $f : A \twoheadrightarrow B$ and $g : C \twoheadrightarrow D$ , gives a function $(A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D)$ . But such a function is not implementable: $\begin {array}{l} f \twoheadrightarrow g : (A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D) \\ (f \twoheadrightarrow g)(h)(b) =\ \textcolor {red}{???}\\ \end {array}$ In the above hole $\textcolor {red}{???}$ , $h : A \twoheadrightarrow C$ and $b \in B$ . Given the value $b \in B$ , none of our functions $f, g$ or $h$ take elements of $B$ , so there would be no way to produce the $D$ value required. This is because our function $f : A \twoheadrightarrow B$ goes the wrong way. If $f$ were a function $B \twoheadrightarrow A$ , things would be a lot easier.

Definition. Dual category [dm-000Q]

Liam O'Connor

The dual of a category $\mathbf {C}$ , written $\mathbf {C}^\mathsf {op}$ , is a category with the same objects as $\mathbf {C}$ but the arrows are reversed, that is, for each morphism $A \xrightarrow {m} B$ in $\mathbf {C}$ , there is a morphism $B \xrightarrow {m} A$ in $\mathbf {C}^\mathsf {op}$ .

The function arrow is a bifunctor [dt-002W]

Liam O'Connor

The operator $\twoheadrightarrow$ introduced in Definition [dt-002F] is is the object mapping for a binary functor: $(\twoheadrightarrow ) : \mathbf {Cpo}^\mathsf {op} \times \mathbf {Cpo} \rightarrow \mathbf {Cpo}$ The category $\mathbf {Cpo}^\mathsf {op}$ is the dual category to $\mathbf {Cpo}$ .

Thus, a morphism $A \xrightarrow {m} B$ in the category $\mathbf {Cpo}^\mathsf {op}$ is a continuous function $m : B \twoheadrightarrow A$ . Thus, the morphism mapping for our functor must take two functions $f : B \twoheadrightarrow A$ (the morphism from $\mathbf {Cpo}^\mathsf {op}$ ) and $g : C \twoheadrightarrow D$ (the morphism from $\mathbf {Cpo}$ ), and produce $(A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D)$ . As with products, we will overload the $\twoheadrightarrow$ notation for this mapping as well.

Definition. Morphism mapping for $\twoheadrightarrow$ [dt-002X]

Liam O'Connor

Given $f : B \twoheadrightarrow A$ and $g : C \twoheadrightarrow D$ , we have: $\begin {array}{l} f \twoheadrightarrow g : (A \twoheadrightarrow C) \twoheadrightarrow (B \twoheadrightarrow D)\\ f \twoheadrightarrow g = \mathit {curry}\ (g \circ \mathit {apply} \circ (\mathsf {id} \times f))\\[2em] \text {(or, operationally:)}\\ (f \twoheadrightarrow g)(h) = g \circ h \circ f\\ \end {array}$

Theorem. [dt-002Y]

Liam O'Connor

The two functor laws follow as a consequence of the universal property for functions:

$\mathsf {id}_A \twoheadrightarrow \mathsf {id}_B = \mathsf {id}_{A \twoheadrightarrow B}$
$(f \circ g) \twoheadrightarrow (h \circ i) = (g \twoheadrightarrow h) \circ (f \twoheadrightarrow i)$

Upshot.

Liam O'Connor

Our category $\textbf {Cpo}$ has exponentials.

Backlinks

Theorem. [dt-002Y]

Liam O'Connor

The two functor laws follow as a consequence of the universal property for functions:

$\mathsf {id}_A \twoheadrightarrow \mathsf {id}_B = \mathsf {id}_{A \twoheadrightarrow B}$
$(f \circ g) \twoheadrightarrow (h \circ i) = (g \twoheadrightarrow h) \circ (f \twoheadrightarrow i)$

Theorem. The currying isomorphism [dt-002U]

Liam O'Connor

(A \times B)\twoheadrightarrow C \;\;\simeq \;\; A\twoheadrightarrow (B\twoheadrightarrow C)

Proof.

Liam O'Connor

Follows from the universal property for functions when set up with the isomorphism from curry and its inverse, the function in Exercise [dt-002R].