Person. John Longley [jlongley]

Lecturer
University of Edinburgh
https://homepages.inf.ed.ac.uk/jrl/

Backlinks

Lecture. Domain theory › Constructions on cpos and PCF [dt-001Z]

Liam O'Connor

This lecture is based on material from Graham Hutton, John Longley, Dana Scott, Joseph Stoy, Carl Gunter, and Glynn Winskel.

Products [dt-002K]

Liam O'Connor

Recall Construction [dt-000E], which showed that the product of two pointed posets is itself a pointed poset. In Exercise [dt-001X] you may also have shown that $A \times B$ is also a cpo if $A$ and $B$ are cpos, with this definition for lubs: $\bigsqcup X \; = \; \left (\bigsqcup \{ x \mid \exists y.\ (x,y) \in X \}, \bigsqcup \{ y \mid \exists x.\ (x,y) \in X \}\right )$ This definition can be made a little more comprehensible by defining it in terms of the two projection operators for pairs:

Definition. Projection operators for products [dt-0020]

Liam O'Connor

Destruction of pairs is captured by the two projection operators, defined as follows:

\begin {array}{lcl} \pi _0 : A \times B \rightarrow A & \qquad & \pi _1 : A \times B \rightarrow B \\ \pi _0(x, y) = x & & \pi _1(x, y) = y \\ \end {array}

Construction. Product of cpos [dt-0021]

Liam O'Connor

Given cpos $A$ and $B$ , the product $A \times B$ is itself a cpo, ordered by $(x,y) \sqsubseteq _{X \times Y} (x',y') \quad \text {iff} \quad x \sqsubseteq _X x' \land y \sqsubseteq _Y y'$ with bottom value $\bot _{X \times Y}$ being $(\bot _A, \bot _B)$ . Least upper bounds are found by taking the lubs of each component:

\bigsqcup X \; = \; \left (\bigsqcup \{ \pi _0(x) \mid x \in X \}, \bigsqcup \{ \pi _1(x) \mid x \in X \}\right )

Theorem. Continuity of projection operations [dt-0022]

Liam O'Connor

The projection functions $\pi _0$ and $\pi _1$ are continuous.

Definition. The split function [dt-0023]

Liam O'Connor

Construction of pairs is captured by the split function: If

f : A \rightarrow B

and

g : B \rightarrow C

, then split, written

\langle f , g \rangle

, is defined as:

\begin {array}{lr} \langle f , g \rangle : A \rightarrow B \times C\\ \langle f , g \rangle \ a = (f(a), g(a)) \end {array}

Theorem. Continuity of split [dt-0024]

Liam O'Connor

For continuous functions $f$ and $g$ , the split function $\langle f, g \rangle$ is continuous.

Proof.

Liam O'Connor

Using the alternative characterisation of continuity:

$\langle f, g \rangle$ is monotonic. Let $x \sqsubseteq y \in A$ . Then: $\begin {array}{lclr} \langle f , g \rangle \ x & = & (f(x), g(x)) & \text {(def)}\\ & \sqsubseteq & (f(y), g(y)) & \text {(monotonicity of $f$,$g$)}\\ & = & \langle f , g \rangle \ y & \text {(def)} \end {array}$
$\langle f , g \rangle$ preserves lubs of directed sets. Let $X \subseteq A$ be directed. Then:

\begin {array}{lclr} \langle f , g \rangle \ (\bigsqcup X) & = & (f(\bigsqcup X), g(\bigsqcup X)) & \text {(def)}\\ & = & (\bigsqcup \{ f(x) \mid x \in X \}, \bigsqcup \{ g(x) \mid x \in X \}) & \text {(continuity of $f$,$g$)}\\ & = & \bigsqcup \{ \langle f , g \rangle \ x \mid x \in X \} & \text {(def)} \end {array}

These building blocks can be used to make many functions on products (thereby ensuring continuity):

Definition. The $\mathit {swap}$ function [dt-0025]

Liam O'Connor

\begin {array}{l}\mathit {swap} : A \times B \rightarrow B \times A \\ \mathit {swap} = \langle \pi _1 , \pi _0 \rangle \end {array}

Definition. Product of functions [dt-0026]

Liam O'Connor

Given $f : A \rightarrow C$ and $g : B \rightarrow D$ , we overload the $\times$ operator for products to denote the combined function $f \times g : A \times B \rightarrow C \times D$ , given below:

$\begin {array}{l} f \times g : A \times B \rightarrow C \times D \\ f \times g = \langle f \circ \pi _0 , g \circ \pi _1 \rangle \end {array}$

Exercise. [dt-002G]

Liam O'Connor

Express the function $\mathit {juggle} (a, (b,c)) = ((a,b),c)$ using just our primitive combinators for projection and split.

Solution.

Liam O'Connor

$\mathit {juggle} \triangleq \langle \langle \pi _0 , \pi _0 \circ \pi _1 \rangle , \pi _1 \circ \pi _1 \rangle$

Pictorial Properties [dt-0027]

Liam O'Connor

The following properties of our projection and split functions follow from the pictorial reasoning we see on the right:

$\pi _0 \circ \langle f , g \rangle = f$
$\pi _1 \circ \langle f , g \rangle = g$
$\langle \pi _0 \circ h , \pi _1 \circ h \rangle = h$

Exercise. [dt-0028]

Liam O'Connor

Prove that the three properties in § [dt-0027] are equivalent to the universal property for products

(\pi _0 \circ h = f \land \pi _1 \circ h = g)\ \text {iff}\ h = \langle f , g \rangle

Solution.

Liam O'Connor

Showing in both directions:

The three properties follow from the universal property: The first two properties follow from the universal property where $h$ is set to $\langle f , g \rangle$ . The third property follows from the universal property where $f$ is set to $\pi _0\circ h$ and $g$ is set to $\pi _1\circ h$ .
The universal property follows from the universal property: In the $\Rightarrow$ direction of the universal property follows from the third property, and the $\Leftarrow$ direction follows from the first two.

Definition. Universal property for cpo products [dt-0029]

Liam O'Connor

(\pi _0 \circ h = f \land \pi _1 \circ h = g)\ \text {iff}\ h = \langle f , g \rangle

As commuting diagram on the category $\mathbf {Cpo}$ :

Aside. Category theory [dt-002A]

Liam O'Connor

Definition. Category [dm-000G]

Liam O'Connor

A category $C$ consists of a collection of things (objects) and a collection of arrows between these things (morphisms). If there is a morphism $A \xrightarrow {f} B$ and a morphism $B \xrightarrow {g} C$ , we also have the composed morphism $A \xrightarrow {g \circ f} C$ . This composition operator must be associative. Additionally each object $X$ has an identity morphism $X \xrightarrow {\mathsf {id}_X} X$ , such that for an arrow $X \xrightarrow {a} Y$ , $a \circ \mathsf {id}_X = \mathsf {id}_Y \circ a = a$ .

Example. The category $\mathbf {Set}$ [dm-000H]

Liam O'Connor

The category $\mathbf {Set}$ is the category where the objects are (small) sets, the morphisms are functions between these sets, composition is function composition ( $(g \circ f)(x) \triangleq g(f(x))$ ) and identity is just the identity function $\lambda x. x$ .

Example. The category $\mathbf {Rel}$ [dm-000I]

Liam O'Connor

The category $\mathbf {Rel}$ is the category where the objects are (small) sets, the morphisms are relations between these sets, composition is relational composition: $g \circ f \triangleq \{ (a,b) \mid \exists i.\ (a,i) \in f \land (i,b) \in g \}$ and identity is the diagonal relation (equality).

Example. The category $\mathbf {Cpo}$ [dt-002B]

Liam O'Connor

The category $\mathbf {Cpo}$ is the category where the objects are cpos, the morphisms are continuous functions between these cpos, composition is function composition ( $(g \circ f)(x) \triangleq g(f(x))$ ) and identity is just the identity function $\lambda x. x$ .

Definition. Functor [dm-000J]

Liam O'Connor

A functor $F$ from a category $\mathbf {C}$ to a category $\mathbf {D}$ consists of an object mapping that maps objects of $\mathbf {C}$ to objects of $\mathbf {D}$ , and a morphism mapping that maps morphisms of $\mathbf {C}$ to morphisms of $\mathbf {D}$ such that:

For each $A \xrightarrow {m} B$ in $\mathbf {C}$ , we have a morphism $F(A) \xrightarrow {F(m)} F(B)$ in $\mathbf {D}$ .
For each object $A$ in $\mathbf {C}$ , the equation $F(\mathsf {id}_A) = \mathsf {id}_{F(A)}$ holds in $\mathbf {D}$ .
For a pair of morphism $A \xrightarrow {f} B \xrightarrow {g} C$ in $\mathbf {C}$ , the equation $F (g \circ f) = F(g) \circ F(f)$ holds in $\mathbf {D}$ .

Example. The category $\mathbf {Cat}$ [dm-000K]

Liam O'Connor

The category $\mathbf {Cat}$ is the category where the objects are themselves (small) categories, the morphisms are structure-preserving maps between these categories, i.e., functors.

Commutative diagrams [dm-000L]

Liam O'Connor

When working in a category, we can state many theorems compactly using commutative diagrams, such as this diagram for products:

In these diagrams, the objects are vertices in the diagram, and the morphisms are the arrows in the diagram (we typically omit identity morphisms and morphisms that are just compositions of other morphisms). Looking at the above diagram, we can equate the two paths from

A

to

B

and the two paths from

A

to

C

, and produce the equations

\pi _0 \circ \langle f, g \rangle = f

and

\pi _1 \circ \langle f, g \rangle = g

. We adopt the convention that dotted lines indicate uniqueness, meaning that, from the diagram above, we can also infer the law:

\pi _0 \circ h = f \land \pi _1 \circ h = g \implies h = \langle f , g \rangle

Corollary. Derived properties of cpo products [dt-002C]

Liam O'Connor

The universal property is called such because all the familiar properties of products follow from it – thinking in pictures helps to see how (Indeed, the universal property characterises products up to isomorphism):

$\pi _0 \circ (f \times g) = f \circ \pi _0$
$\pi _1 \circ (f \times g) = g \circ \pi _1$
$(f \times g) \circ \langle h , i \rangle = \langle f \circ h, g \circ i \rangle$
$\langle f , g \rangle \circ h = \langle f \circ h, g \circ h \rangle$
$\mathsf {id}_A \times \mathsf {id}_B = \mathsf {id}_{A \times B} \quad (*)$
$(f \circ g) \times (h \circ i) = (f \times h) \circ (g \times i) \quad (**)$

These last two statements $(*)$ and $(**)$ show that $\times$ is a bifunctor on the category $\textbf {Cpo}$ , i.e., a functor $\textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo}$ .

Exercise. [dt-002I]

Liam O'Connor

Show using the universal property that $\langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle$

Solution.

Liam O'Connor

Instantiating the universal property where

h := \langle f, g \rangle \circ h

,

f := f \circ h

, and

g := g \circ h

:

\pi _0 \circ \langle f, g \rangle \circ h = f \circ h \land \pi _1 \circ \langle f, g \rangle \circ h = g \circ h\ \text {iff}\ \langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle

Simplifying using the pictorial properties in § [dt-0027] (shown equivalent to the universal property in Exercise [dt-0028]):

f \circ h = f \circ h \land g \circ h = g \circ h\ \text {iff}\ \langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle

By logical simplifications, we arrive at

\langle f, g \rangle \circ h = \langle f \circ h , g \circ h \rangle

as required.

Isomorphisms for cpo products [dt-002D]

Liam O'Connor

Definition. Cpo isomorphism [dt-002E]

Liam O'Connor

An isomorphism between two cpos $A$ and $B$ is a bijection $f$ between $A$ and $B$ such that $f$ preserves the cpo structure, i.e., that $f$ and $f^{-1}$ are continuous.

We say two cpos $A$ and $B$ are isomorphic, written $A \simeq B$ , iff an isomorphism exists between them.

Theorem. Commutative monoid structure for cpos [dt-002H]

Liam O'Connor

Cpos form a commutative monoid "up to isomorphism" under $\times$ and $\mathbf {1}$ (the cpo consisting of only one element $\bot$ ). That is, for all cpos $A, B$ and $C$ :

$A \times \mathbf {1} \simeq A$
$A \times (B \times C) \simeq (A \times B) \times C$
$A \times B \simeq B \times A$

Proof.

Liam O'Connor

The isomorphisms required are the projection $\pi _0$ , the $\mathit {juggle}$ function from Exercise [dt-002G], and the swap function.

Definition. The set of continuous functions [dt-002F]

Liam O'Connor

Let $A \twoheadrightarrow B$ denote just the continuous functions from cpo $A$ to cpo $B$ : $A \twoheadrightarrow B\; \triangleq \; \{ f : A \rightarrow B \mid f\ \text {is continuous} \}$

Theorem. [dt-002J]

Liam O'Connor

There is an isomorphism between pairs of continuous functions and continuous functions that output pairs: $(A \twoheadrightarrow B) \times (A \twoheadrightarrow C)\; \simeq \; (A \twoheadrightarrow (B \times C))$

Proof.

Liam O'Connor

Proof follows from the universal property after setting up the isomorphism with functions

f(g_0,g_1) = \langle g_0 , g_1 \rangle

and

f^{-1}(h) = (\pi _0 \circ h, \pi _1 \circ h)

.

Upshot.

Liam O'Connor

Because we have the functor $\times$ on $\textbf {Cpo}$ that satisfies the properties of products described above, the category $\textbf {Cpo}$ therefore has binary products.

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.

Sums [dt-0030]

Liam O'Connor

Construction. Sum of cpos [dt-0031]

Liam O'Connor

The sum construct on cpo $A + B$ denotes a disjoint union of two cpos with a new, dedicated $\bot$ value: $A + B = \{ (0, a) \mid a \in A \} \cup \{ (1, b) \mid b \in B \} \cup \{ \bot _{A+B} \}$ This construct is a cpo under the ordering: $x \sqsubseteq y\;\;\text {iff}\;\;\begin {cases} \text {true} & \text {if}\ x=\bot _{A+B}\\ a \sqsubseteq a' & \text {if}\ x = (0,a)\ \text {and}\ y = (0, a') \\ b \sqsubseteq b' & \text {if}\ x = (1,b)\ \text {and}\ y = (1, b') \\ \text {false} & \text {otherwise} \end {cases}$ Intuitively, this says that the ordering on $A + B$ is the same as $A$ and $B$ separately, except that $\bot _{A+B}$ is less than anything.

The only directed sets are those that do not contain a mixture of elements from both $A$ and from $B$ , so the least upper bound operator is essentially the same as the least upper bounds for $A$ and for $B$ . Formally: $\bigsqcup X \;\; = \;\; \begin {cases} (0,\bigsqcup \{ a \mid (0,a) \in X \}) & \text {if}\ \{ a \mid (0,a) \in X \} \neq \emptyset \\ (1,\bigsqcup \{ b \mid (1,b) \in X \}) & \text {if}\ \{ b \mid (1,b) \in X \} \neq \emptyset \\ \bot _{A+B} & \text {otherwise}\\ \end {cases}$

Primitive functions for sums [dt-003D]

Liam O'Connor

Definition. Constructors for sums [dt-0032]

Liam O'Connor

For constructing sums, we use two primitive constructor functions, $\mathit {inl}$ and $\mathit {inr}$ : $\begin {array}{l} \mathit {inl} : A \twoheadrightarrow (A + B)\\ \mathit {inl}(x) = (0,x)\\[1em] \mathit {inr} : B \twoheadrightarrow (A + B)\\ \mathit {inr}(y) = (1,y) \end {array}$

Theorem. Continuity of sum constructors [dt-0033]

Liam O'Connor

The constructor functions $\mathit {inl}$ and $\mathit {inr}$ are continuous.

Definition. The case function [dt-0034]

Liam O'Connor

Elimination of sums is captured by the case function $[f,g] : (A + B) \twoheadrightarrow C$ , made from functions $f : A \twoheadrightarrow C$ and $g : B \twoheadrightarrow C$ . This function is defined by: $\begin {array}{l} [f,g] : (A + B) \twoheadrightarrow C\\ [f,g](x) = \begin {cases} f(a) & \text {if}\ x = (0,a) \\ g(b) & \text {if}\ x = (1,b) \\ \bot _C & \text {if}\ x = \bot _{A+B}\end {cases} \end {array}$

Exercise. [dt-0035]

Liam O'Connor

Prove that the case function $[f,g](x)$ is, given continuous functions $f : A \twoheadrightarrow C$ and $g : B \twoheadrightarrow C$ , continuous on its argument $x$ .

Solution.

Liam O'Connor

As mentioned in Construction [dt-0031], the only directed subsets of $A + B$ are those that contain entirely values of the format $(0,\_)$ and optionally $\bot _{A+B}$ , or those that contain entirely values of the format $(1,\_)$ and optionally $\bot _{A+B}$ . Call this directed subset $X$ .

When $\bigsqcup X = \bot _{A+B}$ : This means that $X = \{\bot _{A+B}\}$ as $\bot$ is always the least element. From Definition [dt-0034], we have: $\begin {array}{lcl} [f,g](\bigsqcup X) &=& [f,g](\bot _{A+B}) \\ &=& \bot _C \\ &=& \bigsqcup \{\bot _C\} \\ &=& \bigsqcup \{[f,g](\bot _{A+B})\} \\ &=& \bigsqcup \{[f,g](x) \mid x \in X\}\end {array}$ This discharges both requirements in Definition [dt-001J] for this case.
When $\bigsqcup X = (0,\_)$ : This means that $X$ consists of at least one $(0,\_)$ value plus possibly $\bot _{A+B}$ , that is $X \setminus \{\bot _{A+B}\} = \{ (0,a) \mid a \in Y\}$ for some nonempty $Y \subseteq A$ . We have the following, using the continuity of $f$ : $\begin {array}{lcl} [f,g](\bigsqcup X) &=& [f,g](\bigsqcup (X \setminus \{\bot _{A+B}\})) \\ &=& [f,g](\bigsqcup \{ (0,a) \mid a \in Y\} )\\ &=& [f,g](0,\bigsqcup Y) \\ &=& f(\bigsqcup Y) \\ &=& \bigsqcup \{ f(a) \mid a \in Y \} \\ &=& \bigsqcup \{ [f,g](0,a) \mid a \in Y\} \\ &=& \bigsqcup \{ [f,g](x) \mid x \in X \setminus \{\bot _{A+B}\} \} \\ &=& \bigsqcup (\{ [f,g](x) \mid x \in X \setminus \{\bot _{A+B}\} \} \cup \{\bot _C\}) \\ &=& \bigsqcup \{ [f,g](x) \mid x \in X \} \\ \end {array}$
When $\bigsqcup X = (1,\_)$ : Similar to the $(0,\_)$ case but using $g$ rather than $f$ .

Locality of sums [dt-0039]

Liam O'Connor

We can see by the definitions of case and our constructors that $[f,g] \circ \mathit {inl} = f$ and $[f,g] \circ \mathit {inr} = g$ , or, in a commutative diagram:

Note that this diagram is like the dual of the diagram seen in the universal property for products — the arrows are reversed. That is because, generally speaking, sums are dual to products. However, because of our additional $\bot$ value, our cpo sums are only weakly universal — the $h$ arrow is not unique.

Example. Weak universality of cpo sums [dt-003A]

Liam O'Connor

Consider this scenario with the cpos $\textbf {2} = \{ \top , \bot \}$ and $\textbf {1} = \{\bot \}$ :

In this case, setting the function

h = \lambda x.\ \top

makes the diagram commute, but

(\lambda x.\ \top ) \neq [\lambda x.\ \top , \lambda x.\ \top ]

due to the different handling of

\bot _{\textbf {1}+\textbf {1}}

.

Definition. Weak universal property for cpo sums [dt-003B]

Liam O'Connor

(h \circ \mathit {inl} = f \land h \circ \mathit {inr} = g)\;\; \text {iff}\;\; [f,g] \sqsubseteq h

This property is called weak because it uses only the information ordering rather than equality on the right hand side.

Warning. Failure of sum isomorphisms [dt-003C]

Liam O'Connor

The weakness of the universal property for sums means that many common isomorphisms for sums in other contexts do not hold:

$A + (B + C) \not \simeq (A + B) + C$
$(A \twoheadrightarrow C) \times (B \twoheadrightarrow C) \not \simeq (A+B) \twoheadrightarrow C$

Sums form a bifunctor [dt-0036]

Liam O'Connor

With these, we can define the morphism mapping for the sum bifunctor $(+) : \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo}$ . Just as with products and functions, we will overload the $+$ notation for morphisms as well as objects in the category $\mathbf {Cpo}$ .

Definition. Sum of functions [dt-0037]

Liam O'Connor

Given functions $f : A \twoheadrightarrow C$ and $g : B \twoheadrightarrow D$ , we have: $\begin {array}{l} f+g : (A + B)\twoheadrightarrow (C + D) \\ f+g = [\mathit {inl} \circ f, \mathit {inr} \circ g] \end {array}$

Theorem. [dt-0038]

Liam O'Connor

$+ : \mathbf {Cpo} \times \mathbf {Cpo} \rightarrow \mathbf {Cpo}$ is a lawful bifunctor, that is:

$(\lambda a. a) \times (\lambda b. b) = (\lambda x.x)$
$(f_1 \circ g_1) \times (f_2 \circ g_2) = (f_1 \times f_2) \circ (g_1 \times g_2)$

Upshot.

Liam O'Connor

Our category $\mathbf {Cpo}$ has only local sums.

Strict Constructions [dt-003E]

Liam O'Connor

When giving a semantics to a call-by-name (or "lazy") language, the constructions $\twoheadrightarrow$ for functions, $\times$ for products and $+$ for sums are exactly what we want. To properly capture call-by-value (or "strict") languages, however, we also need strict versions of these constructions.

Construction. The cpo of strict continuous functions [dt-003F]

Liam O'Connor

A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B = \{ f \in A \twoheadrightarrow B \mid f(\bot ) = \bot \}

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-002L].

Construction. Smash products of cpos [dt-003G]

Liam O'Connor

A \otimes B = \{ (a,b) \in A \times B \mid a \neq \bot \land b \neq \bot \} \cup \{ \bot _{A\otimes B}\}

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-0021]. This operator is called a smash product because the two $\bot$ values from $A$ and $B$ are "smashed" into one $\bot$ value.

Construction. Smash sums of cpos [dt-003H]

Liam O'Connor

A \oplus B = \{ (t,x) \in A + B \mid x \neq \bot \} \cup \{ \bot _{A\oplus B} \}

The ordering and lubs are, mutatis mutandis, as with the non-strict Construction [dt-0031]. This operator is called a smash sum because the two $\bot$ values from $A$ and $B$ are "smashed" into one $\bot$ value.

Theorem. Isomorphisms with strict constructions [dt-003J]

Liam O'Connor

The strict cpo constructions satisfy all the usual isomorphisms, including:

$(A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B) \times (A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)\;\; \simeq \;\; A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } (B\otimes C)$
$(A \otimes B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C) \;\; \simeq \;\; A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } (B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)$
$(A \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C) \times (B \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C)\;\; \simeq \;\; (A\oplus B) \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } C$

Definition. The category $\mathbf {Cpo_\bot }$ [dt-003I]

Liam O'Connor

The category $\mathbf {Cpo_\bot }$ is the category where the objects are cpos, the morphisms are strict continuous functions between these cpos, and composition and identity are as in $\mathbf {Cpo}$ .

Upshot.

Liam O'Connor

The category

\mathbf {Cpo_\bot }

has products, exponentials, and sums (as it doesn't suffer from the problem that

\textbf {Cpo}

does).

Definition. The lifting operator for cpos [dt-003K]

Liam O'Connor

The lifting operator $(\cdot )_\bot$ adds a new $\bot$ value to a cpo. That is, for a cpo $X$ : $X_\bot = X \cup \{\bot \} \quad \text {(where $\bot \notin X$)}$ For all $x \in X$ (including $\bot _X$ ), our new bottom value $\bot \sqsubseteq x$ .

Theorem. Isomorphisms with lifting [dt-003L]

Liam O'Connor

With the lifting operator, we can relate the lazy constructions like product and sum with strict constructions like smash product and sum via isomorphism:

$A\twoheadrightarrow B \simeq A_\bot \mathbin {\circ \hspace{-0.4em}\twoheadrightarrow } B$
$A + B \simeq A_\bot \oplus B_\bot$
$(A \times B)_\bot \simeq A_\bot \otimes B_\bot$

PCF [dt-003T]

Liam O'Connor

For most purposes in semantics, describing semantics in terms of (continuous functions on) cpos is enough. To demonstrate, we will give semantics to PCF: a Turing-complete, higher order functional programming language. We will then extend PCF to include more features, namely pairs (product types) and sum types.

Definition. The language PCF [dt-003M]

Liam O'Connor

The language for Programming Computable Functions (PCF) is a variant of typed $\lambda$ -calculus with minimal extensions to be Turing-complete. $\begin {array}{lcl} e & \Coloneqq & n \mid x \mid \lambda x : \tau .\ e \mid e_1\ e_2\mid \mathsf {succ} \mid \mathsf {pred} \mid \mathsf {ifz}\ e_1\ \mathsf {then}\ e_2\ \mathsf {else}\ e_3 \mid \mathsf {fix}\ x : \tau .\ e \\ \tau & \Coloneqq & \mathsf {nat} \mid \tau _1 \rightarrow \tau _2 \end {array}$

Definition. Typing rules for PCF [dt-003N]

Liam O'Connor

$\dfrac {n \in \mathbb {N}}{\Gamma \vdash n : \mathsf {nat}}\quad \dfrac {x : \tau \in \Gamma }{\Gamma \vdash x : \tau }\quad \dfrac {\Gamma , x : \tau _1 \vdash e : \tau _2 }{ \Gamma \vdash \lambda x : \tau _1.\ e : \tau _1 \rightarrow \tau _2}\quad \dfrac {\Gamma \vdash e_1 : \tau _1 \rightarrow \tau _2 \quad \Gamma \vdash e_2 : \tau _1}{\Gamma \vdash e_1\ e_2 : \tau _2}\\[2em] \dfrac { }{ \Gamma \vdash \mathsf {succ} : \mathsf {nat} \rightarrow \mathsf {nat}}\quad \dfrac { }{ \Gamma \vdash \mathsf {pred} : \mathsf {nat} \rightarrow \mathsf {nat}}\quad \dfrac { \Gamma \vdash e_1 : \mathsf {nat} \quad \Gamma \vdash e_2 : \tau \quad \Gamma \vdash e_3 : \tau }{ \Gamma \vdash \mathsf {ifz}\ e_1\ \mathsf {then}\ e_2\ \mathsf {else}\ e_3 : \tau }\quad \dfrac { \Gamma , x : \tau \vdash e : \tau }{\Gamma \vdash \mathsf {fix}\ x : \tau .\ e : \tau }$

Type-dependent denotations [dt-003O]

Liam O'Connor

Because PCF is typed, we shall assign denotations only to well-typed expressions. The range of our denotation function for expressions is determined by the type of its input expression. That is, the denotation of a type $\tau$ is the cpo whose elements will be the denotations of expressions of type $\tau$ . The denotation of the type $\mathsf {nat}$ , then, is merely the flat domain of the natural numbers $\mathbb {N}_\bot$ : $\llbracket \mathsf {nat} \rrbracket = \mathbb {N}_\bot$ And, the denotation of the function type is the domain of continuous functions on cpos: $\llbracket \tau _1 \rightarrow \tau _2 \rrbracket = \llbracket \tau _1 \rrbracket \twoheadrightarrow \llbracket \tau _2 \rrbracket$ A closed term $e : \tau$ with no free variables denotes an element of $\llbracket \tau \rrbracket$ , so we might be tempted to define our denotation function for expressions $e : \tau$ like so: $\llbracket e \rrbracket : \llbracket \tau \rrbracket$ However, if $e : \tau$ involves free variables from our context $\Gamma$ , the valuation of $e$ will depend on the values assigned to all the variables. Thus, the denotation of a typed expression $\Gamma \vdash e : \tau$ is defined instead as a continuous function: $\llbracket e \rrbracket _\Gamma : \llbracket \Gamma \rrbracket \twoheadrightarrow \llbracket \tau \rrbracket$ where the meaning of a context $\Gamma = (x_0 : \tau _0, x_1 : \tau _1,\dots , x_n : \tau _n)$ will be a a big $n$ -tuple of the values assigned to each variable: $\llbracket \Gamma \rrbracket = \llbracket \tau _0 \rrbracket \times \llbracket \tau _1 \rrbracket \times \cdots \times \llbracket \tau _n \rrbracket$

Definition. Notation for $n$ -tuples [dt-003Q]

Liam O'Connor

Given an $n$ -tuple, i.e. elements of the $n$ -ary product $X_0 \times X_1 \times X_2 \times \dots \times X_n$ , we typically denote the entire $n$ -tuple as in vector notation: $\vec {x} : X_0 \times X_1 \times X_2 \times \dots \times X_n$ And individual elements of the tuple are accessed with numeric subscripts: $x_0 : X_0 \quad x_2 : X_2 \quad \cdots$

Definition. Semantics of PCF [dt-003P]

Liam O'Connor

Types

Liam O'Connor

\begin {array}{lcl} \llbracket \mathsf {nat} \rrbracket &=& \mathbb {N}_\bot \\ \llbracket \tau _1 \rightarrow \tau _2 \rrbracket &=& \llbracket \tau _1 \rrbracket \twoheadrightarrow \llbracket \tau _2 \rrbracket \end {array}

Expressions

Liam O'Connor

For

\Gamma \vdash e : \tau

, we have

\llbracket e \rrbracket _\Gamma : \llbracket \tau \rrbracket

defined as follows:

\begin {array}{lcl} \llbracket n \rrbracket _\Gamma (\vec {z}) & =& n\\ \llbracket x \rrbracket _\Gamma (\vec {z}) & = & z_j\ \text {where}\ j\ \text {is largest}\ j\ \text {s.t.}\ x = x_j \\ \llbracket \lambda x : \tau _1.\ e \rrbracket _\Gamma (\vec {z}) & = & (\boldsymbol {\lambda } v \in \llbracket \tau _1 \rrbracket .\ \llbracket e\rrbracket _{\Gamma , x : \tau _1}(\vec {z}, v))\\ \llbracket e_1\ e_2 \rrbracket _\Gamma (\vec {z}) & = & \llbracket e_1 \rrbracket _\Gamma (\vec {z})(\llbracket e_2 \rrbracket _\Gamma (\vec {z}))\\ \llbracket \mathsf {succ} \rrbracket _\Gamma (\vec {z}) & = & (\boldsymbol {\lambda } v \in \mathbb {N}_\bot .\ v + 1)\\ \llbracket \mathsf {pred} \rrbracket _\Gamma (\vec {z}) & = & (\boldsymbol {\lambda } v \in \mathbb {N}_\bot .\ v - 1)\\ \llbracket \mathsf {ifz}\ e_1\ \mathsf {then}\ e_2\ \mathsf {else}\ e_3 \rrbracket _\Gamma (\vec {z}) & = & \begin {cases} \llbracket e_2 \rrbracket _\Gamma (\vec {z}) & \text {if}\ \llbracket e_1 \rrbracket _\Gamma (\vec {z}) > 0 \\ \llbracket e_3 \rrbracket _\Gamma (\vec {z}) & \text {if}\ \llbracket e_1 \rrbracket _\Gamma (\vec {z}) = 0 \\ \bot & \text {if}\ \llbracket e_1 \rrbracket _\Gamma (\vec {z}) = \bot \end {cases}\\ \llbracket \mathsf {fix}\ x : \tau .\ e \rrbracket _\Gamma (\vec {z}) &= & \mathbf {fix}(\boldsymbol {\lambda } v \in \llbracket \tau \rrbracket .\ \llbracket e\rrbracket _{\Gamma , x : \tau }(\vec {z}, v)) \end {array}

In the above definitions a boldface lambda

\boldsymbol {\lambda }

is used for an anonymous continuous function — boldface to distinguish it from the lambda in the syntax of PCF. Verifying that these functions are indeed continuous is straightforward, but is necessary to justify the use of the

\mathbf {fix}

operator.

Extending PCF with product types [dt-003R]

Liam O'Connor

We shall extend the syntax of PCF with a new type former, $\tau _1 \times \tau _2$ and three expression-level constructs for constructing and deconstructing pairs: $\begin {array}{lcl} e & \Coloneqq & \cdots \mid (e_1,e_2) \mid \mathsf {fst}\ e \mid \mathsf {snd}\ e \\ \tau & \Coloneqq & \cdots \mid \tau _1 \times \tau _2 \end {array}$ Adding to our typing rules similarly: $\dfrac {\Gamma \vdash e_1 : \tau _1 \quad e_2 : \tau _2}{(e_1,e_2) : \tau _1 \times \tau _2}\\[2em] \dfrac {\Gamma \vdash e : \tau _1 \times \tau _2}{\Gamma \vdash \mathsf {fst}\ e : \tau _1}\quad \dfrac {\Gamma \vdash e : \tau _1 \times \tau _2}{\Gamma \vdash \mathsf {snd}\ e : \tau _2}$ To extend our semantics, we make the product type $\tau _1 \times \tau _2$ denote the product cpo $\llbracket \tau _1 \rrbracket \times \llbracket \tau _2 \rrbracket$ , and our expression semantics are expressed straightforwardly using our projection and split operations for products: $\begin {array}{lcl} \llbracket (e_1, e_2) \rrbracket _\Gamma &=& \langle \llbracket e_1 \rrbracket _\Gamma , \llbracket e_2 \rrbracket _\Gamma \rangle \\ \llbracket \mathsf {fst}\ e \rrbracket _\Gamma & = & \pi _0 \circ \llbracket e \rrbracket _\Gamma \\ \llbracket \mathsf {snd}\ e \rrbracket _\Gamma & = & \pi _1 \circ \llbracket e \rrbracket _\Gamma \\ \end {array}$

Extending PCF with sum types [dt-003S]

Liam O'Connor

We shall extend the syntax of PCF with a new type former, $\tau _1 + \tau _2$ and three expression-level constructs for constructing and deconstructing sums: $\begin {array}{lcl} e & \Coloneqq & \cdots \mid \mathsf {inl}\ e \mid \mathsf {inr}\ e \mid \mathsf {case}\ e_0\ \mathsf {of}\ \mathsf {inl}\ x \rightarrow e_1 ; \mathsf {inr}\ y \rightarrow e_2 \\ \tau & \Coloneqq & \cdots \mid \tau _1 + \tau _2 \end {array}$ Adding to our typing rules similarly: $\dfrac {\Gamma \vdash e : \tau _1}{\Gamma \vdash \mathsf {inl}\ e : \tau _1 + \tau _2}\quad \dfrac {\Gamma \vdash e : \tau _2}{\Gamma \vdash \mathsf {inr}\ e : \tau _1 + \tau _2}\\[2em] \dfrac {\Gamma \vdash e_0 : \tau _1 + \tau _2 \quad \Gamma , x : \tau _1 \vdash e_1 : \tau \quad \Gamma , y : \tau _2 \vdash e_2 : \tau }{ \Gamma \vdash \mathsf {case}\ e_0\ \mathsf {of}\ \mathsf {inl}\ x \rightarrow e_1 ; \mathsf {inr}\ y \rightarrow e_2 : \tau }$ To extend our semantics, we make the sum type $\tau _1 + \tau _2$ denote the sum cpo $\llbracket \tau _1 \rrbracket + \llbracket \tau _2 \rrbracket$ , and our expression semantics are expressed using our primitive functions for sums. $\begin {array}{lcl} \llbracket \mathsf {inl}\ e \rrbracket _\Gamma & = & \mathit {inl} \circ \llbracket e \rrbracket _\Gamma \\ \llbracket \mathsf {inr}\ e \rrbracket _\Gamma & = & \mathit {inr} \circ \llbracket e \rrbracket _\Gamma \end {array}$ $\begin {array}{l}\llbracket \mathsf {case}\ e_0\ \mathsf {of}\ \mathsf {inl}\ x \rightarrow e_1 ; \mathsf {inr}\ y \rightarrow e_2 \rrbracket _\Gamma (\vec {z}) \\ \quad = [ \boldsymbol {\lambda }v. \llbracket e_1 \rrbracket _{\Gamma ,x:\tau _1}(\vec {z},v), \boldsymbol {\lambda }v. \llbracket e_2 \rrbracket _{\Gamma ,y:\tau _2}(\vec {z},v)] (\llbracket e_0 \rrbracket _\Gamma (\vec {z}))\end {array}$

Lecture. Domain theory › Monadic semantics, Scott domains and nondeterminism [dt-005V]

Liam O'Connor

This lecture is based on material from Carl Gunter, Glynn Winskel, Graham Hutton, Kai Engelhardt, Dexter Kozen, Andrew Myers, John Longley, Dana Scott, and Joseph Stoy.

Generalising our semantics [dt-005Z]

Liam O'Connor

We return to the $\mathcal {C}$ language we saw previously:

Definition. The $\mathcal {C}$ Language [dt-005R]

Liam O'Connor

Using notation similar to Backus-Naur Form (BNF): $\begin {array}{lcl} \mathcal {E} & \Coloneqq & n \mid x \mid \mathcal {E}_1 + \mathcal {E}_2 \mid \mathcal {E}_1 - \mathcal {E}_2\\ \mathcal {B} & \Coloneqq & \mathsf {false} \mid \mathsf {true} \mid \neg \mathcal {B} \mid \mathcal {E}_1 = \mathcal {E}_2\\ \mathcal {C} & \Coloneqq & \mathsf {skip} \mid x := \mathcal {E} \mid \mathcal {C}_1 ; \mathcal {C}_2 \mid \mathsf {if}\ \mathcal {B}\ \mathsf {then}\ \mathcal {C}_1\ \mathsf {else}\ \mathcal {C}_2 \mid \mathsf {while}\ \mathcal {B}\ \mathsf {do}\ \mathcal {C}\ \mathsf {od}\\ x & \in & \mathcal {V}\; \textit {(variables)}\\ n & \in & \mathbb {N} \end {array}$

If we wish to add other kinds of effects (beyond mutation of state) to our language, this will necessarily affect the semantic domain. Rather than rewrite the entire semantics for each possible setting, we will generalise the semantics to work over any instance of an algebraic structure, called a monad.

Definition. Monad [dm-000U]

Liam O'Connor

A monad on the category $\textbf {C}$ consists of an endofunctor $\mathcal {M} : \textbf {C} \rightarrow \textbf {C}$ and two operations (natural transformations) for all $\mathbf {C}$ -objects $X$ : $\mu _X : \mathcal {M}(\mathcal {M}(X)) \rightarrow \mathcal {M}(X)$ and $\eta _X : X \rightarrow \mathcal {M}(X)$ , such that the following diagrams commute:

In equational form, these laws are

$\mu _X \circ \mathcal {M}(\mu _X) = \mu _X \circ \mu _{\mathcal {M}(X)}$
$\mu _X \circ \mathcal {M}(\eta _X) = \mu _X \circ \eta _{\mathcal {M}(X)} = \mathsf {id}_{\mathcal {M}(X)}$

In computer science,

\eta _X

is sometimes called unit, pure, or return, and

\mu _X

is usually called join.

Example. Flat domains as monads [dt-005P]

Liam O'Connor

The flat domain lifting operation $(\cdot )_\bot$ forms a monad, where the endofunctor $\mathcal {M}(X) = X_\bot$ , the operation $\mu _X : (X_\bot )_\bot \rightarrow X_\bot$ collapses the two $\bot$ values, and $\eta _X : X \rightarrow X_\bot$ is simply $\eta _X(x) = x$ .

Sometimes it is more convenient to work with the Kleisli composition operator, rather than the operations $\mu$ and $\eta$ directly.

Definition. Kleisli category [dm-000T]

Liam O'Connor

For a monad $(\mathcal {M}, \mu , \eta )$ over the category $\mathbf {C}$ , the Kleisli category has the same objects as $\mathbf {C}$ , but the morphisms $A \xrightarrow {h} B$ are those morphisms $h$ of $\mathbf {C}$ that have the form $A \xrightarrow {h} \mathcal {M}(B)$ . Composition is defined as follows, for morphisms $A \xrightarrow {f} \mathcal {M}(B)$ and $B \xrightarrow {g} \mathcal {M}(C)$ : $g \circ _K f = \mu _C \circ \mathcal {M}(g) \circ f$ Identity morphisms for this category are just $\eta$ .

Definition. Monadic semantics for $\mathcal {C}$ [dt-005Q]

Liam O'Connor

We define our semantics generically in terms of a monad $(\mathcal {M},\mu ,\eta )$ , using the Kleisli composition operator for $\mathcal {M}$ : $\begin {array}{l} \mathsf {ite} : (\Sigma \rightarrow \mathbb {B}) \times (\Sigma \rightarrow \mathcal {M}(\Sigma )) \times (\Sigma \rightarrow \mathcal {M}(\Sigma )) \rightarrow (\Sigma \rightarrow \mathcal {M}(\Sigma ))\\ \mathsf {ite}(b,t,e)(\sigma ) = \begin {cases}t(\sigma ) & \text {if}\ b(\sigma ) = T \\ e(\sigma ) & \text {otherwise} \end {cases} \end {array}$ $\begin {array}{lcl} \llbracket \cdot \rrbracket _\mathcal {C} : \mathcal {C} \rightarrow \Sigma \rightarrow \mathcal {M}(\Sigma )\\[0.4em] \llbracket \mathsf {skip} \rrbracket _\mathcal {C} & = & \eta _\Sigma \\ \llbracket x := e \rrbracket _\mathcal {C} & = & \boldsymbol {\lambda } \sigma .\ \eta _\Sigma (\sigma \left (x \mapsto \llbracket e \rrbracket _\mathcal {E}\right )) \\ \llbracket c_1 ; c_2 \rrbracket _\mathcal {C} & = & \llbracket c_2 \rrbracket _\mathcal {C} \circ _K \llbracket c_1 \rrbracket _\mathcal {C} \\[0.3em] \llbracket \textsf {if}\ b\ \textsf {then}\ c_1\ \textsf {else}\ c_2 \rrbracket _\mathcal {C} & = & \mathsf {ite}(\llbracket b \rrbracket _\mathcal {B},\llbracket c_1 \rrbracket _\mathcal {C},\llbracket c_2 \rrbracket _\mathcal {C})\\ \llbracket \textsf {while}\ b\ \textsf {do}\ c\ \textsf {od} \rrbracket _\mathcal {C} & = & \mathbf {\mathbf {fix}}(\boldsymbol {\lambda } f.\ \mathsf {ite}(\llbracket b \rrbracket _\mathcal {B}, f \circ _K \llbracket c \rrbracket _\mathcal {C}, \eta _\Sigma ) ) \end {array}$

Example. Instantiating $\mathcal {C}$ with the lifting monad [dt-005S]

Liam O'Connor

Instantiating our monadic semantics where the monad $\mathcal {M}$ is flat domain lifting, we recover our original semantics of $\mathcal {C}$ .

Example. Instantiating $\mathcal {C}$ with exceptions [dt-005T]

Liam O'Connor

Let us instantiate our monadic semantics with the monad $\mathcal {M}(X) = X_\bot \oplus \mathbf {1}$ , where the added value (from $\mathbf {1}$ ) is called $\mathsf {fail}$ . The operation $\mu _X : (X_\bot \oplus \mathbf {1})_\bot \oplus \mathbf {1} \rightarrow X_\bot \oplus \mathbf {1}$ collapses the two possible $\bot$ values to $\bot$ and the two possible $\mathsf {fail}$ values to $\mathsf {fail}$ , and the operation $\eta _X : X \rightarrow X_\bot \oplus \mathbf {1}$ is the straightforward injection.

Then we may extend our language with lightweight exception constructs: $\mathcal {C} ::= \dots \mid \mathsf {throw} \mid \mathsf {try}\ \mathcal {C}_1\ \mathsf {catch}\ \mathcal {C}_2$ and define their semantics, leaving our existing semantics unchanged: $\begin {array}{lcl} \llbracket \mathsf {throw} \rrbracket \ \sigma &=& \mathsf {fail} \\ \llbracket \mathsf {try}\ c_1\ \mathsf {catch}\ c_2 \rrbracket \ \sigma &=& \begin {cases} \llbracket c_2 \rrbracket \ \sigma & \text {if}\ \llbracket c_1 \rrbracket \ \sigma = \mathsf {fail} \\ \llbracket c_1 \rrbracket \ \sigma & \text {otherwise}\end {cases} \end {array}$

Nondeterminism

Liam O'Connor

Introduction to nondeterminism [dt-005U]

Liam O'Connor

When modelling programming languages we sometimes require a way to be imprecise about some aspects of a program — usually, this takes the form of non-determinism. Non-determinism can be hard for beginners to grasp, but it typically has to be employed when modelling real programs. For example, suppose we had a greeting program that differed depending on the physical location of the computer: $\begin {array}{l} \textsf {\textbf {if}}\ \mathit {currentLocation}() = \text {Korea}\ \textsf {\textbf {then}} \\ \quad \textsf {\textbf {say}}\ \text {``안녕하세요''} \\ \textsf {\textbf {else}} \\ \quad \textsf {\textbf {say}}\ \text {``Hello!''}\\ \textsf {\textbf {fi}} \end {array}$ If we wanted to mathematically model the behaviour of this program, it would be frightfully inconvenient to include the geography of Earth and the computer's physical location in our model. That's where non-determinism comes in. If we abstract away from the geographical details, and instead regard the program as choosing between the two options based on some unspecified criteria, then we can get away with modelling less, at the cost of some detail: $\begin {array}{l} \textsf {\textbf {if}}\ \mathit {???}\ \textsf {\textbf {then}} \\ \quad \textsf {\textbf {say}}\ \text {``안녕하세요''} \\ \textsf {\textbf {else}} \\ \quad \textsf {\textbf {say}}\ \text {``Hello!''}\\ \textsf {\textbf {fi}} \end {array}$ Such underspecified conditionals are usually called non-deterministic choice, where our conditional $\textsf {\textbf {if}}\ \mathit {???}\ \textsf {\textbf {then}}\ P\ \textsf {\textbf {else}}\ Q\ \textsf {\textbf {fi}}$ is written simply as $P + Q$ .

While we tend to view our physical machines as deterministic automata, the state upon which each decision is deterministically made includes a number of external things which are tedious to model mathematically. We can also use non-determinism to ignore details that we don't care about for our particular domain — a common example is memory allocation, where it is very convenient (for some programs) to think of memory as infinite, and allocation as an operation that can potentially fail, without specifying exactly when and how this failure can occur. This is normally modelled as a choice between successful allocation and a failure state.

Instantiating our semantics for nondeterminism [dt-0060]

Liam O'Connor

Our initial semantics for $\mathcal {C}$ (without loops) was functions on states $\Sigma \rightarrow \Sigma$ . When adding loops, we used a cpo $\Sigma \twoheadrightarrow \Sigma _\bot$ for our semantic domain. Since non-deterministic programs can have more than one outcome, a natural choice of semantic domain would be $\Sigma \twoheadrightarrow \mathcal {P}(\Sigma _\bot ) \setminus \emptyset$ , i.e., functions from an initial state to a non-empty set of possible outcomes.

We can provide $\eta$ and $\mu$ operations for our proposed monad for non-determinism $\mathcal {M}(X) = \mathcal {P}(X_\bot ) \setminus \emptyset$ : $\begin {array}{l} \eta : X \rightarrow \mathcal {P}(X_\bot ) \setminus \emptyset \\ \eta (x) = \{ x \}\\ \mu : \mathcal {P}{((\mathcal {P}(X_\bot ) \setminus \emptyset )_\bot )}\rightarrow \mathcal {P}(X_\bot ) \setminus \emptyset \\ \mu (S) = (\bigcup _{X \neq \bot \in S} X) \cup (S \cap \{ \bot \}) \end {array}$ And, with this semantics, we can easily add a denotation for a non-deterministic choice operator, in terms of union: $\llbracket c_1 + c_2 \rrbracket _\mathcal {C} = \lambda \sigma . \llbracket c_1 \rrbracket _\mathcal {C} \sigma \cup \llbracket c_2 \rrbracket _\mathcal {C} \sigma$ Unfortunately this is only the beginning of our troubles. While we have given a valuation function above, its definition uses $\textbf {fix}$ , and therefore our domain $\Sigma \rightarrow \mathcal {M}(\Sigma )$ must be a cpo, and all our operations continuous. It is not clear how to order elements of $\mathcal {P}(X_\bot ) \setminus \emptyset$ . A natural choice of ordering would be subset inclusion $\subseteq$ . However, as we lack $\emptyset$ , there is no least element for this ordering. Furthermore, simply using $\subseteq$ as our ordering would mean that the deterministic, terminating program that always returns a single state $\{ \sigma \}$ would be considered less informative than the program that may diverge $\{ \bot , \sigma \}$ . This would make most of our operations non-continuous.

Instead, we shall examine three separate orderings on this set, each of which carries a different view of non-determinism. More generally, we wish to come up with a construction analogous to the powerset operator $\mathcal {P}$ , but for our semantic domains — a powerdomain. However, for these orderings to produce valid partial orders, we require a certain theorem that only applies to a certain class of cpos, called "algebraic" cpos. Thus, we will first introduce a richer class of cpos, called Scott domains, and then return to the problem of non-determinism.

Scott domains [dt-005W]

Liam O'Connor

Compactness and Finiteness [dt-0040]

Liam O'Connor

We begin by formalising the notion of an element in a cpo representing a finite amount of information.

Definition. Boring and interesting sets [dt-003W]

Liam O'Connor

There are two kinds of directed sets:

Boring sets contain their lub.

Example: Finite directed sets are boring (but boring sets aren't all finite!).
Interesting sets don't contain their lub.

Example: $\mathbb {N}$ in the chain $\mathbb {N} \cup \{ \infty \}$ is interesting.

Following the above intuition, we might be tempted to say that the "infinite" elements of a cpo are those which are the lub of an interesting set, but this notion is too weak. Consider this cpo $X$ :

By the above definition, the only infinite element would be

\infty

, but if we consider the following isomorphic cpo, ordered by subset inclusion:

Then the set

x

cannot be a finite set, as any finite set would be a subset of one of the finite sets in the chain

\emptyset \sqsubseteq \Set { 0 } \sqsubseteq \Set {0,1} \sqsubseteq \cdots

. Thus, it makes more sense for us to call

x

an "infinite" element as well.

Definition. Compactness [dt-003U]

Liam O'Connor

Let $A$ be a cpo. Then $x \in A$ is compact (a.k.a. finite) iff for all directed $X \subseteq A$ : $x \sqsubseteq \bigsqcup X \implies \exists y \in X.\ x \sqsubseteq y$ In English: A compact element will approximate some element of a directed set if it approximates the lub. We write $\mathsf {K}(A)$ for the set of compact elements of $A$ , i.e.: $\mathsf {K}(A) = \{x \in A \mid x\ \text {is compact} \}$

In the example cpo $X$ above, all the elements except $\infty$ and $x$ would be compact. Thus, compactness better captures our notion of an element representing a finite amount of information. This understanding of compact elements is a generalisation of the notion of a finite element from the theory of algebraic lattices.

Example. Compact elements [dt-003V]

Liam O'Connor

Every element in a finite cpo is compact. More generally, every element of a cpo of finite height (e.g. $\mathbb {Z}_\bot$ ) is compact. This is because finite directed sets are always boring.
Take the cpo $\mathcal {P}(X)$ of subsets of $X$ ordered by inclusion $\subseteq$ , as seen in Exercise [dt-001G]. The compact elements of $\mathcal {P}(X)$ are those of finite cardinality.
Take the cpo $\mathbb {N} \nrightarrow \mathbb {N}$ of partial functions on the natural numbers, ordered by inclusion of graphs. The compact elements of $\mathbb {N} \nrightarrow \mathbb {N}$ are the functions which are defined only for finite domains.

Example. Compact elements with infinitely many approximations [dt-003X]

Liam O'Connor

Compact elements may still have an infinite number of approximations. Consider the cpo $\mathbb {N} \cup \{ \infty , \infty + 1 \}$ , where we have tacked on an additional top element $\infty + 1$ to our normal cpo of natural numbers extended with infinity. Then, while $\infty$ is not compact, $\infty + 1$ is compact — it is not the lub of an interesting directed set. If $\infty + 1$ is the lub of a set $X$ then $\infty + 1$ must be in the set $X$ . Nonetheless, there are an infinite number of approximations to $\infty + 1$ , i.e., elements $x$ such that $x \sqsubseteq \infty + 1$ .

As an aside, requiring that our compact elements have a truly finite number of approximations is the basis for the theory of Berry domains and stable functions.

Theorem. Submonoids as a cpo [dt-003Y]

Liam O'Connor

The submonoids of a monoid $(X, \iota , \bullet )$ form a cpo under $\subseteq$ , where union gives the lub.

Exercise. Both infinite and compact [dt-003Z]

Liam O'Connor

Find a set in the cpo of submonoids of $(\mathbb {N},0,+)$ that is both infinite and compact.

Solution.

Liam O'Connor

Take $E \triangleq \{ n \in \mathbb {N} \mid n\ \text {is even}\}$ . Let $Y \subseteq \mathcal {P}(\mathbb {N})$ be directed and $E \subseteq \bigcup Y$ . Since $2 \in E$ there must exist $y \in Y$ such that $2 \in Y$ . Since $(y,0,+)$ is a monoid, every positive multiple of $2$ is also in $y$ , thus $E \subseteq y$ and therefore $E$ is compact.

Seeing as compact elements are also sometimes called finite, this is surprising as $E$ is an infinite set. The reason it is nonetheless compact is that $E$ is finitely generated — it is the smallest submonoid of $(\mathbb {N},0,+)$ such that the finite set $\{ 2 \} \subseteq E$ . In fact, the compact submonoids of $(\mathbb {N},0,+)$ are precisely the finitely generated ones.

Algebraicity and ideals [dt-005X]

Liam O'Connor

Definition. Algebraicity [dt-0041]

Liam O'Connor

A cpo is algebraic iff every element is the lub of its compact approximations. That is, a cpo $D$ is algebraic iff for all $x \in D$ ,

$\mathop {\downarrow }(x) = \{ y \in \mathsf {K}(D) \mid y \sqsubseteq x \}$ is directed;
$x = \bigsqcup \mathop {\downarrow }(x)$

Note: It's common in semantics to consider only algebraic cpos with a countable set of compact elements. Such cpos are called $\omega$ -algebraic.

Aside: Plotkin provides an equivalent definition of $\omega$ -algebraic cpos in which directed sets are replaced with $\omega$ -chains throughout. Hutton claims this is less appealing, as the definition speaks of an $\omega$ -chain of compact approximations, rather than the directed set of such.

Example. $\omega$ -algebraic cpos [dt-0042]

Liam O'Connor

Many standard examples of cpos are $\omega$ -algebraic cpos: finite cpos, subsets $\mathcal {P}(X)$ of a set $X$ , partial functions $\mathbb {N} \nrightarrow \mathbb {N}$ and submonoids of a monoid. In general, any cpo of subalgebras (e.g. subgroups of a group, subrings of a ring etc.) is $\omega$ -algebraic. This is the origin of the terminology.

Counterexample. Non-algebraic cpo [dt-0043]

Liam O'Connor

In the cpo on the right (seen also in § [dt-0040]), the element $x$ is not the lub of its compact approximations. The only compact element that approximates $x$ is $\bot$ , and the least upper bound of the set $\{\bot \}$ is just $\bot$ , not $x$ . That is: $\mathop {\downarrow }(x) = \{\bot \}$ but: $x \neq \bigsqcup \{\bot \}$

Theorem. Nothing suddenly invented at infinity [dt-0045]

Liam O'Connor

Let $D$ and $E$ be algebraic cpos. Then a function $f : D \rightarrow E$ is continuous iff, for all $x \in D$ : $f(x) = \bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \}$ In other words, in an algebraic cpo, continuous functions are completely defined by their behaviour for compact arguments.

This makes precise our earlier slogan in Definition [dt-001J], that continuous functions don't suddenly behave differently for infinite (i.e. non-compact) elements.

Proof.

Liam O'Connor

First, assuming

f

is continuous, we show that

f(x) = \bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \}

:

\begin {array}{lclr} f(x) & = & f(\bigsqcup \mathop {\downarrow }(x)) & \text {($D$ is {algebraic})}\\ &=&\bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \} & \text {($f$ is continuous)}\\ \end {array}

It remains to show that if

f(x) = \bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \}

, then

f

is continuous. Using the alternative definition, we shall first show that

f

is monotone. Let

a \sqsubseteq b

for

a,b \in D

. Then

\mathop {\downarrow }(a) \subseteq \mathop {\downarrow }(b)

and thus

\{f(x) \mid x \in \mathop {\downarrow }(a)\} \subseteq \{f(x) \mid x \in \mathop {\downarrow }(b)\}

, therefore:

\begin {array}{lclr} f(a) &=&\bigsqcup \ \{ f(x) \mid x \in \mathop {\downarrow }(a) \} & \text {(assumption)}\\ & \sqsubseteq &\bigsqcup \ \{ f(x) \mid x \in \mathop {\downarrow }(b) \} & \text {(from above)}\\ & = & f(b) & \text {(assumption)}\\ \end {array}

Next, let

X \subseteq D

be directed.

\begin {array}{lclr} f(\bigsqcup X) &=&\bigsqcup \ \{ f(x) \mid x \in \mathop {\downarrow }(\bigsqcup X) \} & \text {(assumption)}\\ &=&\bigsqcup \ \{ f(x) \mid x \in \mathsf {K}(X) \land x \sqsubseteq \bigsqcup X \} & \text {(defn.~of $\downarrow $)}\\ &=&\bigsqcup \ \{ f(x) \mid \exists y \in X.\ x \in \mathsf {K}(X) \land x \sqsubseteq y \} & \text {(compactness)}\\ &=&\bigsqcup \ \{ f(x) \mid \exists y \in X.\ x \in \mathop {\downarrow }(y)\} & \text {(defn.~of $\downarrow $)}\\ &=&\bigsqcup \ \{ f(x) \mid x \in X\} & \text {(algebraicity)}\\ \end {array}

Exercise. [dt-0044]

Liam O'Connor

Let $f : D \twoheadrightarrow E$ be a continuous function between algebraic cpos. Define: $G_f = \{ (a,b) \in \mathsf {K}(D) \times \mathsf {K}(E) \mid b \sqsubseteq f(a) \}$ Then for all $x \in D$ , prove that: $f(x) = \bigsqcup \ \{ b \mid (a,b) \in G_f \land a \sqsubseteq x \}$

Solution.

Liam O'Connor

\begin {array}{lclr} f(x) & = & f(\bigsqcup \mathop {\downarrow }(x)) & \text {($D$ is {algebraic})}\\ &=&\bigsqcup \ \{ f(a) \mid a \in \mathop {\downarrow }(x) \} & \text {($f$ is continuous)}\\ &=&\bigsqcup \ \left \{ \bigsqcup \mathop {\downarrow }(f(a)) \mid a \in \mathop {\downarrow }(x) \right \} & \text {($E$ is {algebraic})}\\ &=&\bigsqcup \ \{ b \in \mathsf {K}(E) \mid b \sqsubseteq f(a) \land a \in \mathop {\downarrow }(x)\} & \text {(lubs and defn of $\downarrow $)}\\ &=&\bigsqcup \ \{ b \mid (a,b) \in G_f \land a \sqsubseteq x \}&\text {(defn of $G_f$)} \end {array}

This is powerful. For example, the continuous function $f : \mathcal {P}(\mathbb {N}) \twoheadrightarrow \mathcal {P}(\mathbb {N})$ on an uncountable cpo $\mathcal {P}(\mathbb {N})$ is completely determined by the countable relation $G_f$ .

Definition. Down-closure [dt-0047]

Liam O'Connor

Given a poset $Y$ , a set $X \subseteq Y$ is down-closed iff, for all $x \in X$ , any $y \sqsubseteq x$ is in $X$ .

Definition. Ideal [dt-0048]

Liam O'Connor

A set is ideal iff it is both down-closed and directed.

Definition. Ideal completion [dt-0046]

Liam O'Connor

The ideal completion of a set $A$ , written sometimes as $\mathsf {Id}(A)$ , is the set of all ideal subsets of $A$ , i.e.: $\mathsf {Id}(A) = \{ X \subseteq A \mid X\ \text {is ideal}\}$

Theorem. Representation theorem for algebraic cpos [dt-0049]

Liam O'Connor

Every algebraic cpo $D$ is isomorphic to the ideal completion of its compact elements, ordered by subset inclusion. That is, $\mathsf {Id}(K(D))$ is an algebraic cpo such that $D \simeq \mathsf {Id}(K(D))$ .

Getting closure [dt-005Y]

Liam O'Connor

Definition. Basis [dt-004A]

Liam O'Connor

A set of compact elements $X \subseteq \mathsf {K}(A)$ is a basis for a cpo $A$ iff for all $x\in A$ , $x= \bigsqcup \{a \in X \mid a \sqsubseteq x\}$ .

Theorem. Compact basis for algebraic cpos [dt-004B]

Liam O'Connor

If $X$ is a basis for $A$ , then $A$ is algebraic and $\mathsf {K}(A) = X$ .

Proof.

Liam O'Connor

If $a \in \mathsf {K}(A)$ , then $\bigsqcup M = a$ where $M = \{ x \in X \mid x \sqsubseteq a \}$ , as $X$ is a basis. Since $a$ is compact, $a \sqsubseteq b$ for some $b \in M$ . But since $a$ is the lub of $M$ , $b \sqsubseteq a$ as well. By antisymmetry $a = b$ , hence $a \in X$ . Thus $\mathsf {K}(A) \subseteq X$ , so $\mathsf {K}(A) = X$ and $A$ is algebraic.

Theorem. Closure of algebraic cpos under product [dt-004C]

Liam O'Connor

If $D$ and $E$ are algebraic cpos, then so is their product construction $D \times E$ .

Proof.

Liam O'Connor

In the following proof, we show that $\mathsf {K}(D) \times \mathsf {K}(E)$ is a basis for the product $D \times E$ and thereby show via Theorem [dt-004B] that $D \times E$ is algebraic if $D$ and $E$ are.

$\mathsf {K}(D) \times \mathsf {K}(E) \subseteq \mathsf {K}(D \times E)$ : Let $(x,y) \in \mathsf {K}(D) \times \mathsf {K}(E)$ . To show that $(x,y)$ is compact, let us assume that $(x,y) \in \bigsqcup X$ where $X \subseteq D \times E$ is directed. We must show that there exists some element $e$ of $X$ such that our $(x,y) \sqsubseteq e$ . As $(x,y) \in \bigsqcup X$ , by the definition of lub on products we can conclude that: $\begin {array}{lcl} x & \sqsubseteq & \bigsqcup \pi _0[ X] \\ y & \sqsubseteq & \bigsqcup \pi _1[X] \end {array}$ Here we use the notation $f[X]$ to indicate the image of a function on a set, i.e. $\{ f(v) \mid v \in X \}$ .

Since $x$ and $y$ are both compact, there must exist $x' \in \pi _0[ X]$ and $y' \in \pi _1[ X]$ such that $x \sqsubseteq x'$ and $y \sqsubseteq y'$ . While it does not follow that $(x', y') \in X$ , we know that there must exist a pair $(a,b) \in X$ such that $x' \sqsubseteq a$ and $y' \sqsubseteq b$ as $X$ is directed. Hence $(a,b)$ can be our element $e \in X$ that is approximated by $(x,y)$ , i.e. $(x,y) \sqsubseteq (a,b)$ .
$\mathop {\downarrow }(x,y)$ is directed for all $(x,y) \in D \times E$ : $\begin {array}{lcl} \mathop {\downarrow }(x,y) &= & \{ (a,b) \in \mathsf {K}(D) \times \mathsf {K}(E) \mid (a,b) \sqsubseteq (x,y) \} \\ & = & \{ a \in \mathsf {K}(D) \mid a \sqsubseteq x \} \times \{ b \in \mathsf {K}(E) \mid b \sqsubseteq y \}\\ & = & \mathop {\downarrow }(x) \times \mathop {\downarrow }(y) \end {array}$ Because $D$ and $E$ are algebraic, $\mathop {\downarrow }(x)$ and $\mathop {\downarrow }(y)$ are directed. As directedness is closed under product, $\mathop {\downarrow }(x,y)$ is directed too.
$(x,y) = \bigsqcup \mathop {\downarrow }(x,y)$ Starting from the right hand side: $\begin {array}{lclr} \bigsqcup \mathop {\downarrow }(x,y) & = & \bigsqcup (\mathop {\downarrow }(x) \times \mathop {\downarrow }(y)) & \text {(part 2)}\\ & = & (\bigsqcup (\mathop {\downarrow }(x), \bigsqcup \mathop {\downarrow }(y))) & \text {(lub on products)}\\ & = & (x,y) & \text {($D$, $E$ are {algebraic})} \end {array}$

Problem.

Liam O'Connor

\omega

-algebraic cpos are closed under all of our constructions (products and sums, including strict versions of these) except functions

\twoheadrightarrow

and strict functions

\mathbin {\circ \hspace{-0.4em}\twoheadrightarrow }

!

Aside. Scott's original solution: using complete lattices [dt-004D]

Liam O'Connor

The lack of closure of algebraicity under the (continuous) function arrow, strict or non-strict, is not satisfying as it means that our semantic domains are not guaranteed to be algebraic even if they are composed from algebraic cpos. Instead, we must replace algebraic cpos with something stronger still.

Scott's original solution to this lack of closure was to use a complete lattice instead of cpos, i.e. requiring lubs for all subsets, not just directed ones. This solves the problem with $\twoheadrightarrow$ but introduces new problems:

Complete lattices need a top element $\top$ , but adding a fictitious top (representing inconsistent information) to cpos like $\mathbb {B}_\bot$ is strange.
Extending the functions that capture our primitive semantic operations to complete lattices can spoil nice algebraic properties. Consider these two possible implementations of $\mathsf {ite}$ , the function for the semantics of an $\mathsf {if}$ expression: $\mathsf {ite}(\top ,x,y) = x \sqcup y\quad \quad \quad \quad \quad \mathsf {ite}(\top ,x,y) = \top$ Either of these solutions results in the failure of useful and expected laws for $\mathsf {if}$ expressions. For example, the left definition above results in the failure of the common equation to eliminate unreachable cases: $\mathsf {ite}(b, \mathsf {ite}(b,x,y),z) = \mathsf {ite}(b,x,z)$ And the second definition above results in the failure of this equation that removes redundant checks: $\mathsf {ite}(b,x,x) = x$
The powerdomain construction does not generalise to complete lattices, so semantics for non-deterministic programs are difficult in this setting.

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.

Example. Consistent completeness vs directed completeness [dt-004F]

Liam O'Connor


consistent complete	not consistent complete
not directed complete	directed complete

Definition. Scott domain [dt-004G]

Liam O'Connor

A cpo $D$ is a Scott domain iff:

$D$ is $\omega$ -algebraic,
$D$ is consistent complete,

In other words, Scott domains can be summed up by the acronym:

Remark. [dt-004H]

Liam O'Connor

The second requirement in Definition [dt-004G] can, in light of the first, be expressed equivalently as: $x \sqcup y$ exists for all consistent $x,y \in D$ . This is useful when needing to show that a given cpo is a Scott domain.

Theorem. Closure of Scott domains [dt-004I]

Liam O'Connor

Scott domains are closed under all our cpo constructions, including sums $+$ , products $\times$ , continuous functions $\twoheadrightarrow$ , smash sums $\oplus$ , smash products $\otimes$ and strict functions $\mathbin {\circ \hspace{-0.4em}\twoheadrightarrow }$ .

Thesis.

Liam O'Connor

Our semantic domains are Scott domains.

The Hoare powerdomain [dt-0061]

Liam O'Connor

We write $\mathcal {P}_f^\ast (S)$ to denote finite non-empty subsets of $S$ . Let $X, Y \in \mathcal {P}_f^\ast (\mathsf {K}(A))$ be finite, non-empty sets of compact elements of a Scott domain $A$ . The Hoare powerdomain construction is based on the following ordering: $X \preceq _H Y\quad \text {iff}\quad (\forall x \in X.\ \exists y \in Y.\ x \sqsubseteq _A y)$ The intuition behind this is that "Anything $X$ can do, $Y$ can do better". This ordering has some desirable properties: The least element is $\{\bot \}$ , as we might expect. It also satisfies the equation $X \preceq _H X \cup Y$ , which intuitively means that a non-deterministic choice is considered to have more information than any of its components. When specialised to the case where $A$ is a flat domain like $\Sigma _\bot$ , it simplifies to: $X \preceq _H Y\quad \text {iff}\quad X \setminus \{\bot \} \subseteq Y$ This is, however, not a proper order, but a preorder, as it fails antisymmetry. Even in the flat domain case, $\{ x, \bot \} \preceq _H \{x \}$ and $\{ x \} \preceq _H \{x, \bot \}$ but they are not equal. However, any preorder does induce an equivalence relation, where $X \approx _H Y$ iff $X \preceq _H Y$ and $Y \preceq _H X$ . Furthermore, if we take the ideal completion of $\mathcal {P}_f^\ast (K(A))$ with respect to the preorder $\preceq _H$ (i.e., the set of all $\preceq _H$ -downwards-closed directed subsets of $\mathcal {P}_f^\ast (\mathsf {K}(A))$ ), we can order them by inclusion to obtain an algebraic domain with compact elements which correspond to equivalence classes of elements under $\approx _H$ . We have a lub operation for these ideals: $A \sqcup _H B = \{ X \cup Y \mid X \in A \land Y \in B \}$

Example. Hoare powerdomain of $\mathbb {N}_\bot$ [dt-0062]

Liam O'Connor

Let us find the Hoare powerdomain of $\mathbb {N}_\bot$ . Note that $\mathbb {N}_\bot$ is a flat domain so all elements are compact, i.e. $\mathsf {K}(\mathbb {N}_\bot ) = \mathbb {N}_\bot$ . Let us find examine the $\preceq _H$ -ideal subsets of $\mathcal {P}_f^\ast (\mathbb {N}_\bot )$ . If $v$ and $u$ both contain $\bot$ , then $v \preceq _H u$ iff $v \subseteq u$ . As ideal subsets are downwards closed, we can identify an ideal $I \in \mathsf {Id}({\mathcal {P}_f^\ast (\mathbb {N}_\bot )})$ with its union $\bigcup I$ . The ideals of $\mathcal {P}^\ast _f(\mathbb {N}_\bot )$ are then isomorphic to domain $\mathcal {P}(\mathbb {N})$ of all subsets of $\mathbb {N}$ under subset inclusion.

Remark. Angelic nondeterminism [dt-0063]

Liam O'Connor

Consider the following three programs:

$x := 1$
$\textsf {while}\ \textsf {true}\ \textsf {do}\ \textsf {skip}$
$\textsf {while}\ \textsf {true}\ \textsf {do}\ \textsf {skip}\ \textsf {od} + x := 1$

Given a state

\sigma

, let

\sigma ' = \sigma (x \mapsto 1)

. Then, the possible results of these programs are

\{ \sigma ' \}

,

\{ \bot \}

, and

\{\sigma ', \bot \}

respectively. Because the Hoare construction identifies

\approx _H

-equivalent sets, the Hoare powerdomain semantics will consider programs 1 and 3 to be the same. That is, the non-determinism is angelic. The bad outcome (

\bot

) is only said to happen if it is inevitable.

The Smyth powerdomain [dt-0064]

Liam O'Connor

As before, let $X, Y \in \mathcal {P}_f^\ast (\mathsf {K}(A))$ be finite, non-empty sets of compact elements of a Scott domain $A$ . The Smyth powerdomain construction is based on the following preorder: $X \preceq _S Y\quad \text {iff}\quad (\forall y \in Y.\ \exists x \in X.\ x \sqsubseteq _A y)$ The intuition here is "Everything $Y$ can do, $X$ can do worse". It satisfies the equation $X \cup Y \preceq _S X$ , which intuitively means that a non-deterministic choice is considered to have less information than any of its components. When applied to a flat domain, it simplifies to: $X \preceq _S Y\quad \text {iff}\quad \bot \in X \lor Y \subseteq X$ As with the Hoare powerdomain, this fails to be a partial order, but we can use the same ideal completion trick to induce an algebraic domain where compact elements correspond to equivalence classes of elements under $\approx _S$ (where $X \approx _S Y$ is, as with $\approx _H$ , just defined as $X \preceq _S Y \land Y \preceq _S X$ ).

Example. Smyth powerdomain of $\mathbb {N}_\bot$ [dt-0065]

Liam O'Connor

Firstly note that, as ideals are downwards-closed, any $\preceq _S$ -ideal subsets of $\mathcal {P}^\ast _f(\mathbb {N}_\bot )$ will contain all finite subsets of $\mathbb {N}_\bot$ that contain $\bot$ . Let us call those sets trivial. So, a set in $\mathcal {P}^\ast _f(\mathbb {N}_\bot )$ is non-trivial if it does not contain $\bot$ and an ideal subset of $\mathcal {P}^\ast _f(\mathbb {N}_\bot )$ is non-trivial if it contains a non-trivial set. Observe that for non-trivial sets $X$ and $Y$ , $X \preceq _S Y$ iff $X \supseteq Y$ . Thus, we can identify an ideal $I \in \mathsf {Id}({\mathcal {P}_f^\ast (\mathbb {N}_\bot )})$ with the down-closure of the intersection of its non-trivial elements. The smaller this set is, the larger the ideal $I$ . Hence, and confusingly, the non-trivial ideals in the powerdomain (ordered by subset inclusion) correspond to finite subsets of $\mathbb {N}$ ordered by superset inclusion. As all trivial sets are identified, we just need to throw in the unique trivial ideal, and we can see that the Smyth powerdomain of $\mathbb {N}$ is isomorphic to the domain of sets $\{ \mathbb {N} \} \cup \mathcal {P}_f^\ast (\mathbb {N})$ ordered by subset inclusion.

Remark. Demonic nondeterminism [dt-0066]

Liam O'Connor

Note that all sets that contain $\bot$ are considered equivalent by the Smyth construction $\approx _S$ . Thus, this models demonic non-determinism: Of the three programs in Remark [dt-0063], the Smyth semantics considers 2 and 3 to be the same. Thus, the possibility of divergence $\bot$ is no different from inevitable divergence.

The Plotkin powerdomain [dt-0067]

Liam O'Connor

As before, let $X, Y \in \mathcal {P}_f^\ast (\mathsf {K}(A))$ be finite, non-empty sets of compact elements of a Scott domain $A$ . The Plotkin powerdomain construction is based on the following preorder, simply combining the orderings from the Hoare and Smyth constructions: $X \preceq _P Y\quad \text {iff}\quad X \preceq _H Y \land X \preceq _S Y$ This ordering is also called the Egli-Milner ordering. On a flat domain, it simplifies to: $A\sqsubseteq B\quad \text {iff}\quad A = B \lor (\bot \in A \land (A \setminus \{\bot \})\subseteq B)$ Note that this is antisymmetric in the case of a flat domain, and the lub of a chain of sets can be found by taking the union of all elements of the chain if all elements contain $\bot$ If not, then the element without $\bot$ will be the least upper bound.

The failures of antisymmetry can only be observed in domains of height higher than one. Consider a set $\{x,y\}$ containing two elements. According to the induced equivalence from this preorder $\approx _P$ , this set would be considered equal to the set that contains those two elements plus any elements that lie between them on the information ordering: $\{x,y\} \approx _P \{ z \mid x \sqsubseteq z \sqsubseteq y \}$ The Plotkin powerdomain is sometimes called the convex powerdomain, due to the similarity of this to the geometric definition of convexity. Thus, we use the ideal completion trick (as with the Hoare and Smyth constructions) here to arrive at a definition of powerdomain that distinguishes between all three programs outlined in Remark [dt-0063].

Aside.

Liam O'Connor

There is a beautiful algebraic characterisation of Plotkin powerdomains in Matthew Hennessy Gordon Plotkin's paper, Full abstraction for a simple parallel programming language.

Lecture. Domain theory › Recursively defined domains and $\lambda$ -calculus [dt-004Z]

Liam O'Connor

This lecture is based on material from Graham Hutton, John Longley, Dana Scott, Joseph Stoy, Carl Gunter, and Glynn Winskel.

Why we need recursively defined domains [dt-004J]

Liam O'Connor

We saw recursive domain equations with higher-order procedures in § [dt-0007], but there are numerous other examples where they come up.

Recursive algebraic data types [dt-004L]

Liam O'Connor

Suppose we have a language with recursive data types, such as this $\mathit {List}$ type in Haskell-style syntax: $\textbf {data}\ \mathit {List} = \mathsf {Nil} \mid \mathsf {Cons}\ (\mathit {Int} \times \mathit {List})$ As in PCF, the denotation of a type $\tau$ is the domain which contains all the denotations of all closed expressions of type $\tau$ . What, then, is the domain that corresponds to $\mathit {List}\ a$ ? We need a cpo $L$ that satisfies the below equation (where $\mathbf {1}$ is the cpo containing just one element $\bot$ ): $L \simeq \mathbf {1} + (\mathbb {Z}_\bot \times L)$

Untyped higher-order languages [dt-004M]

Liam O'Connor

If we take PCF, discard the type system, $\textbf {fix}$ , natural number primitives and any other superfluous features, and just boil our language down to a minimal, Turing-complete subset, we end up with the untyped $\lambda$ -calculus — a language consisting only of untyped functions.

Definition. Untyped $\lambda$ -calculus [dt-004K]

Liam O'Connor

Untyped $\lambda$ -calculus consists only of untyped (higher-order) functions: $e \; \Coloneqq \; x \mid \lambda x. e \mid e_1\ e_2$

Trying to give a semantics to the untyped $\lambda$ calculus poses an issue: we can no longer rely on the type of an expression to select an appropriate semantic domain. Instead, we we must pick a single domain $D$ which, since functions can be applied to themselves, must apparently include the set of functions $D \twoheadrightarrow D$ : $D \simeq D\twoheadrightarrow D$

How can we find solutions to such recursive equations? How can we guarantee the existence of a (least) solution?

We can start by generalising the fixed point approach we used for values (i.e. elements of cpos) to domains (i.e. cpos themselves).

Example. Recursive domain equations as endofunctors [dt-004N]

Liam O'Connor

This recursive equation for lists: $L \simeq \mathbf {1} + (\mathbb {Z}_\bot \times L)$ Can be expressed as the least fixed point of this mapping (specifically an endofunctor) $\mathcal {F}$ on cpos: $\mathcal {F}(A) \triangleq \mathbf {1} + (\mathbb {Z}_\bot \times A)$

To ensure that least fixed points exist, and to give us a means of finding them, we must now generalise all of the concepts we used for least fixed points on values (information ordering, least upper bounds, continuity etc.) to domains themselves.

From a cpo to the category $\mathbf {Cpo}$ [dt-004O]

Liam O'Connor

Problem.

Liam O'Connor

The following definitions are insufficient when using function constructions in our domain equations ( $\twoheadrightarrow$ and $\mathbin {\circ \hspace{-0.4em}\twoheadrightarrow }$ ), but it will suffice for our purposes for now.

Let us say (for now) that a cpo $A$ approximates a cpo $B$ (i.e. $A \sqsubseteq B$ ) iff there is a continuous function $f : A\twoheadrightarrow B$ . Then, there is a least element for this ordering: the one-element cpo $\mathbf {1} = \{ \bot \}$ , as the continuous function $(\lambda x. \bot ) : \mathbf {1} \twoheadrightarrow A$ exists for any cpo $A$ .

Categorical Aside. Initiality

Liam O'Connor

The category $\mathbf {Cpo}$ has no initial object. The cpo $\mathbf {1}$ is terminal; but also serves as a "pseudo" initial object due to the above.

Colimits in the category $\mathbf {Cpo}$ [dt-004P]

Liam O'Connor

Definition. $\omega$ -chains of cpos in the category $\mathbf {Cpo}$ [dt-004Q]

Liam O'Connor

An $\omega$ -chain of cpos in the category $\mathbf {Cpo}$ consists of a family of cpos $\{A_i \mid i \in \mathbb {N} \}$ , together with a family of continuous functions $\{ f_i : A_i\twoheadrightarrow A_{i+1} \mid i \in \mathbb {N}\}$ , shown below:

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. Least upper bounds in the category $\mathbf {Cpo}$ [dt-004S]

Liam O'Connor

A cpo $A$ is the least upper bound of an $\omega$ -chain of cpos if is both an upper bound and if there exists a unique $k$ for any other upper bound $B$ such that the following diagram commutes (i.e. $h_i = k \circ g_i$ for all $i \in \mathbb {N}$ ):

The least upper bound of such an $\omega$ -chain is also called its colimit.

Note: Uniqueness of lubs is up to isomorphism. That is, if $A$ and $B$ are both colimits of our $\omega$ -chain, then $A \simeq B$ .

Definition. Endofunctors on $\textbf {Cpo}$ [dt-004T]

Liam O'Connor

An endofunctor on the category $\textbf {Cpo}$ is a functor $\textbf {Cpo} \rightarrow \textbf {Cpo}$ , i.e. a mapping $\mathcal {F}$ on cpos together with a mapping $\mathcal {F}$ on continuous functions, such that:

If $f : A \twoheadrightarrow B$ then $\mathcal {F}(f) : \mathcal {F}(A)\twoheadrightarrow \mathcal {F}(B)$
$\mathcal {F}(\mathsf {id}_A : A\twoheadrightarrow A) = \mathsf {id}_{\mathcal {F}(A)} : \mathcal {F}(A)\twoheadrightarrow \mathcal {F}(A)$
$\mathcal {F}(f \circ g) = \mathcal {F}(f) \circ \mathcal {F}(g)$

Remark. [dt-004U]

Liam O'Connor

Observe that, given the information ordering for cpos where $A \sqsubseteq B$ if there exists a continuous function $A \twoheadrightarrow B$ , the functor laws necessarily imply monotonicity for all endofunctors $\mathcal {F}$ .

Definition. Cocontinuous endofunctors [dt-004V]

An endofunctor $\mathcal {F}$ is cocontinuous iff it preserves colimits of $\omega$ -chains of cpos. That is, given a chain where $A$ is a colimit:

Then

\mathcal {F}(A)

is a colimit for the following chain:

Definition. Fixed points of endofunctors on $\mathbf {Cpo}$ [dt-004W]

Liam O'Connor

A fixed point of an endofunctor on cpos $\mathcal {F}$ is a cpo $\mathcal {F}$ such that $\mathcal {F}(A) \simeq A$ .

Note.

Liam O'Connor

In Scott's approach, which we follow here, our fixed points are up to isomorphism (suitable for languages with isorecursive types), but there are other approaches where they are equalities (suitable for languages with equirecursive types).

Theorem. Fixed point theorem for endofunctors on $\mathbf {Cpo}$ [dt-004X]

Liam O'Connor

Every cocontinuous endofunctor $\mathcal {F}$ on cpos has a least fixed point, given by the colimit of the $\omega$ -chain:

Example. Binary Numbers [dt-004Y]

Liam O'Connor

Consider the Haskell-style data type: $\textbf {data}\ \mathit {Bin} = \mathsf {Zero}\ \mathit {Bin} \mid \mathsf {Empty} \mid \mathsf {One}\ \mathit {Bin}$ So, e.g. $\mathsf {One}\ (\mathsf {Zero}\ (\mathsf {One}\ \mathsf {Empty})) : \mathit {Bin}$ .

The recursive domain equation is, expressed as a fixed point: $B \simeq \mathcal {F}(B)\quad \text {where}\ \mathcal {F}(X) = X + \mathbf {1} + X$ We wish to show that $\mathcal {F}$ is a cocontinuous endofunctor.

We have a mapping $\mathcal {F}$ on cpos (objects of the category $\textbf {Cpo}$ ), but for it to be a functor we additionally need a mapping $\mathcal {F}$ on continuous functions (morphisms of the category $\textbf {Cpo}$ ).

Recalling our sum construction, we may remember that sums are already a bifunctor $\textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo}$ (Theorem [dt-0038]). Thus, our mapping on continuous functions $\mathcal {F}$ can be derived from our mapping on cpos $\mathcal {F}$ by using the morphism mapping from the sum construction (Definition [dt-0037]). Given a continuous function $f : A \twoheadrightarrow B$ , our morphism mapping is:

\begin {array}{l} \mathcal {F}(f) : \mathcal {F}(A)\twoheadrightarrow \mathcal {F}(B)\\ \mathcal {F}(f) \triangleq f + \mathsf {id}_\textbf {1} + f \end {array}

Proof that this endofunctor is cocontinuous is left for the reader. Hence the semantics of the type $\mathit {Bin}$ , i.e. $\llbracket \mathit {Bin} \rrbracket : \textbf {Cpo}$ is the least fixed point of $\mathcal {F}$ , i.e. the colimit of the $\omega$ -chain:

Let us visualise this chain. Here the sum injections have been written as $\textsf {Z, E, O}$ rather than (combinations of) $\textsf {inl}$ and $\textsf {inr}$ to keep the connection with the Haskell data type clear.

Thus, the $n$ th cpo in the chain contains binary numbers with at most $n$ defined digits. The colimit of the chain contains all binary numbers (finite, partial, and infinite!).

Exercise. [dt-005M]

Liam O'Connor

Show that $\mathcal {F}(X) \triangleq \mathbf {1} + X$ and $\mathcal {F}(f) \triangleq \mathsf {id}_\mathbf {1} + f$ (using our $+$ operator for functions) define an endofunctor $\mathbf {Cpo} \rightarrow \mathbf {Cpo}$ , i.e. that they satisfy the functor laws.

Solution.

Liam O'Connor

We must show $\mathcal {F}(\mathsf {id}_A : A \twoheadrightarrow A) = \mathsf {id}_{\mathcal {F}(A)} : \mathcal {F}(A) \twoheadrightarrow \mathcal {F}(A)$ . $\begin {array}{lcl} \mathcal {F}(\mathsf {id}_A)& =& \mathsf {id}_\mathbf {1} + \mathsf {id}_A\\ &=& \mathsf {id}_{\mathbf {1} + A}\\ &=& \mathsf {id}_{\mathcal {F}(A)} \end {array}$
We must show $\mathcal {F}(f \circ g) = \mathcal {F}(f) \circ \mathcal {F}(g)$ . $\begin {array}{lcl} \mathcal {F}(f \circ g) &=& \mathsf {id}_\mathbf {1} + (f \circ g) \\ &=& (\mathsf {id}_\mathbf {1} + f) \circ (\mathsf {id}_\mathbf {1} + g) \\ & = & \mathcal {F}(f) \circ \mathcal {F}(g) \end {array}$

Constructing endofunctors [dt-0050]

Liam O'Connor

If we have a mapping on cpos $\mathcal {F} : \textbf {Cpo} \rightarrow \textbf {Cpo}$ that is made up of the primitives $\times$ , $+$ , $\otimes$ , $\oplus$ , $\mathbf {1}$ and $(\cdot )_\bot$ , we can generate a corresponding morphism mapping on continuous functions $\mathcal {F} : (A\twoheadrightarrow B) \rightarrow (\mathcal {F}(A)\twoheadrightarrow \mathcal {F}(B))$ by using the corresponding morphism mappings of each of these operators. Thus any such mapping can be turned into an endofunctor.

Example. Making endofunctors for algebraic data types [dt-0051]

Liam O'Connor

$\begin {array}{llr} \textsf {Object mapping} & \textsf {Morphism mapping}\\[0.2em] \mathcal {F}(X) = X + \mathbf {1} & \mathcal {F}(f) = f + \mathsf {id}_\mathbf {1} & \quad \quad \text {((co)-natural numbers)} \\ \mathcal {F}(X) = \mathbf {1} + (\mathbb {Z}_\bot \times X) & \mathcal {F}(f) = \mathsf {id}_\mathbf {1} + (\mathsf {id}_{\mathbb {Z}_\bot } \times f) & \text {((co)-lists of integers)}\\ \end {array}$

Exercise. [dt-005N]

Liam O'Connor

The lazy natural numbers, also called conats, are defined as the least solution to the equation $X \simeq \mathbf {1} + X$ .

Sketch the first four approximations to the least fixed point. Call the two sum injections \mathsf {zero} and \mathsf {succ}.
Solution.
- Liam O'Connor
$\begin {array}{lcl} A_0 & = & \{\bot \} \\ A_1 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ \bot , \bot \} \\ A_2 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ \bot ), \bot \} \\ A_3 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {zero}\ \bot )), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {succ}\ \bot )), \bot \} \\ \end {array}$
Repeat this exercise assuming:
1. \mathsf {zero} is strict (i.e. \mathsf {zero}\ \bot = \bot )
  Solution.
  Liam O'Connor
  $\begin {array}{lcl} A_0 & = & \{\bot \} \\ A_1 & = & \{\mathsf {succ}\ \bot , \bot \} \\ A_2 & = & \{\mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {succ}\ \bot ), \bot \} \\ A_3 & = & \{\mathsf {succ}\ \bot , \mathsf {succ}\ (\mathsf {succ}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {succ}\ \bot )), \bot \} \\ \end {array}$
2. \mathsf {succ} is strict (i.e. \mathsf {succ}\ \bot = \bot )
  Solution.
  Liam O'Connor
  $\begin {array}{lcl} A_0 & = & \{\bot \} \\ A_1 & = & \{\mathsf {zero}\ \bot , \bot \} \\ A_2 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \bot \} \\ A_3 & = & \{\mathsf {zero}\ \bot , \mathsf {succ}\ (\mathsf {zero}\ \bot ), \mathsf {succ}\ (\mathsf {succ}\ (\mathsf {zero}\ \bot )), \bot \} \\ \end {array}$

From $\textbf {Cpo}$ to $\textbf {Cpo}^{\textbf {R}}$ [dt-0052]

Liam O'Connor

Problem. Contravariance in the function arrow [dt-0053]

Liam O'Connor

We cannot get morphism mappings in the category $\textbf {Cpo}$ as easily as § [dt-0050] when our object mapping makes use of the function operators $\mathbin {\circ \hspace{-0.4em}\twoheadrightarrow }$ and $\twoheadrightarrow$ , as they are contravariant in their first argument. This means the functor that they extend to is not $\textbf {Cpo} \rightarrow \textbf {Cpo}$ but $\textbf {Cpo}^\textsf {op} \rightarrow \textbf {Cpo}$ , where $\textbf {Cpo}^\textsf {op}$ is the dual category of $\textbf {Cpo}$ . The morphisms end up the wrong way around.

As an example, consider $\mathcal {F}(X) = X\twoheadrightarrow \mathbb {Z}_\bot$ . Then, recalling the morphism mapping of the $\twoheadrightarrow$ functor: $\dfrac {f : A \twoheadrightarrow B \quad g : C\twoheadrightarrow D}{f\twoheadrightarrow g : (B\twoheadrightarrow C)\twoheadrightarrow (A\twoheadrightarrow D)}$ We can generate a morphism mapping for $\mathcal {F}$ : $\mathcal {F}(f)\; =\; f\twoheadrightarrow \mathsf {id}_{\mathbb {Z}_\bot }\; =\; (\lambda h.\ \mathsf {id}_{\mathbb {Z}_\bot }\circ h \circ f)\; = \;(\lambda h.\ h \circ f)$ However, this mapping has the wrong type. For $f : A\twoheadrightarrow B$ , then $\mathcal {F}(f) : (B\twoheadrightarrow \mathbb {Z}_\bot ) \rightarrow (A\twoheadrightarrow \mathbb {Z}_\bot )$ , which is $\mathcal {F}(B)\twoheadrightarrow \mathcal {F}(A)$ , not the required $\mathcal {F}(A)\twoheadrightarrow \mathcal {F}(B)$ . This is because the generated functor is contravariant, not covariant.

Exercise. [dt-005O]

Liam O'Connor

Show that, in contrast to $\mathcal {F}(X) = X\twoheadrightarrow \mathbb {Z}_\bot$ from Problem [dt-0053], the mapping $\mathcal {G}(X) = \mathbb {Z}_\bot \twoheadrightarrow X$ can be extended to continuous functions giving a covariant endofunctor on $\textbf {Cpo}$ .

Solution.

Liam O'Connor

Given a continuous function $f : A \twoheadrightarrow B$ , we must produce a continuous function $\mathcal {F}(f) : (\mathbb {Z}_\bot \twoheadrightarrow A) \twoheadrightarrow (\mathbb {Z}_\bot \twoheadrightarrow B)$ , defined as follows: $\mathcal {F}(f)(g)(x) = f \circ g(x)$ Composition of continuous functions preserves continuity. The functor laws can be shown straightforwardly.

Definition. Retraction pair [dt-0054]

Liam O'Connor

A retraction pair $(f,g)$ on cpos $A$ to $B$ consists of two continuous functions $A \xtofrom [g]{f} B$ such that:

$g \circ f = \mathsf {id}_A\quad$ (i.e. $\forall x \in A.\ g(f(x)) = x$ )
$f \circ g \sqsubseteq \mathsf {id}_B\quad$ (i.e. $\forall y \in B.\ f(g(y)) \sqsubseteq y$ )

In this retraction pair,

f

is called a embedding and

g

is called a projection.

Retraction pairs are weakenings of isomorphisms. Intuitively, going $A \twoheadrightarrow B\twoheadrightarrow A$ , all information is preserved due to requirement 1, but going $B\twoheadrightarrow A\twoheadrightarrow B$ , we may lose some information (hence the use of $\sqsubseteq$ in requirement 2).

Example. Examples and counterexamples of retraction pairs [dt-0055]

Liam O'Connor

Here are two examples of retraction pairs:

(this demonstrates that there can be many retraction pairs

A \xtofrom [g]{f} B

)

The following, however, are not retraction pairs $A \xtofrom [g]{f} B$ :


( $y \mapsto b \mapsto z$ but $z \not \sqsubseteq y$ )	( $b \mapsto x \mapsto a$ but $a \neq b$ )

Definition. Composition of retraction pairs [dt-0056]

Liam O'Connor

We can compose retraction pairs by composing their embedding and projection:

Corollary. Derived products of retraction pairs [dt-0057]

It follows from the definition of retraction pairs that, for a pair $\xtofrom [g]{f}$ :

$f$ and $g$ are strict, i.e. $f(\bot ) = \bot$ and $g(\bot ) = \bot$ .
$g$ is uniquely determined by $f$ and vice-versa, so if another retraction pair $\xtofrom [g']{f}$ exists, then $g = g'$ . To see why, remember that $f$ and $g$ must be continuous and therefore monotonic.
$A$ is isomorphic to the range of $f$ , i.e. $A \simeq \{ f(x) \mid x \in A\} \subseteq B$ .

Definition. The category $\textbf {Cpo}^\textbf {R}$ [dt-0058]

Liam O'Connor

The category $\textbf {Cpo}^\textbf {R}$ is the category where the objects are cpos, the morphisms are retraction pairs, composition is as in Definition [dt-0056] and identity is just the retraction pair $A \xtofrom [\lambda x. x]{\lambda x. x} A$ .

Definition. Information ordering in $\textbf {Cpo}^\textbf {R}$ [dt-0059]

Liam O'Connor

The third point in Corollary [dt-0057] suggests a notion of approximation, or information ordering, for cpos. Rather than say, as we did in § [dt-004O], that for cpos $A$ and $B$ , $A \sqsubseteq B$ iff there exists a continuous function $A\twoheadrightarrow B$ , we now say:

A \sqsubseteq B

iff there exists a retraction pair

A \xtofrom [g]{f} B

Generalising to $\textbf {Cpo}^\textbf {R}$ [dt-005A]

Liam O'Connor

All of our other notions for $\textbf {Cpo}$ naturally generalise to a setting with retraction pairs $\textbf {Cpo}^\textbf {R}$ : least elements, $\omega$ -chains, upper bounds, colimits, cocontinuous endofunctors and so on.

Definition. $\omega$ -chains of cpos in the category $\mathbf {Cpo}^\textbf {R}$ [dt-005C]

Liam O'Connor

An $\omega$ -chain of cpos in the category $\mathbf {Cpo}^\textbf {R}$ consists of a family of cpos $\{D_i \mid i \in \mathbb {N} \}$ , together with a family of retraction pairs $D_i \xtofrom [g_i]{f_i} D_{i+1}$ , shown below:

Definition. Endofunctors on $\textbf {Cpo}^\textbf {R}$ [dt-005D]

Liam O'Connor

An endofunctor on the category $\textbf {Cpo}^\textbf {R}$ is a functor $\textbf {Cpo}^\textbf {R} \rightarrow \textbf {Cpo}^\textbf {R}$ , i.e. a mapping $\mathcal {F}$ on cpos together with a mapping $\mathcal {F}$ on retraction pairs, such that:

If $(f,g)$ is a retraction pair $A \xtofrom [g]{f} B$ then $\mathcal {F}(f,g)$ is a retraction pair $\mathcal {F}(A)\xtofrom []{} \mathcal {F}(B)$
$\mathcal {F}(\mathsf {id}_A : A\xtofrom []{} A) = \mathsf {id}_{\mathcal {F}(A)} : \mathcal {F}(A)\xtofrom []{} \mathcal {F}(A)$
$\mathcal {F}(f \circ g) = \mathcal {F}(f) \circ \mathcal {F}(g)$

\circ

composition of retraction pairs

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):

Definition. Colimits in the category $\mathbf {Cpo}^\mathbf {R}$ [dt-005F]

Liam O'Connor

A cpo $A$ is the colimit of an $\omega$ -chain of cpos $A_i$ if is both an upper bound, i.e. there exists retraction pairs $(f_i,g_i) : A_i \xtofrom []{} A$ , and for any other upper bound $B$ , for which there will exist retraction pairs $(m_i,n_i) : A_i \xtofrom []{} B$ , there exists a unique retraction pair $A \xtofrom [k']{k} B$ such that $(m_i,n_i) = (k,k') \circ (f_i,g_i)$ for all $i \in \mathbb {N}$ , where $\circ$ is composition of retraction pairs. Viewed diagramatically, it is the same as Definition [dt-004S] where continuous functions are replaced by retraction pairs.

Definition. Cocontinuous endofunctors on $\textbf {Cpo}^\textbf {R}$ [dt-005E]

An endofunctor $\mathcal {F}$ is cocontinuous iff it preserves colimits of $\omega$ -chains of cpos. That is, given a chain where $A$ is a colimit:

Then

\mathcal {F}(A)

is a colimit for the following chain:

Extending cpo Mappings to endofunctors on $\textbf {Cpo}^\mathbf {R}$ [dt-005I]

Liam O'Connor

If $\mathcal {F}$ is a mapping on cpos built up from basic cpos using the constructions $\times$ , $\otimes$ , $+$ , $\oplus$ , $(\cdot )_\bot$ , as well as $\twoheadrightarrow$ and $\mathbin {\circ \hspace{-0.4em}\twoheadrightarrow }$ , then $\mathcal {F}$ extends to a (covariant!) cocontinuous functor on $\textbf {Cpo}^\mathbf {R}$ . We shall detail the construction for products and functions here, but the other constructions are all similar.

Definition. $\times$ operation for retraction pairs [dt-005J]

Liam O'Connor

Given two retraction pairs $(f,g)$ and $(h,i)$ , our retraction pair for their product is just the product of their embedding and projection, i.e. $(f \times h, g \times i)$ , using our product operation on continuous functions: $\dfrac {A \xtofrom [g]{f} B\quad C \xtofrom [i]{h} D}{A\times C \xtofrom [g \times i]{f \times h} B \times D}$

Definition. $\twoheadrightarrow$ operation for retraction pairs [dt-005K]

Liam O'Connor

We are given two retraction pairs $A \xtofrom [g]{f} B$ and $C \xtofrom [i]{h} D$ . To define a suitable covariant functor, we define our morphism mapping in terms of our $\twoheadrightarrow$ operation on continuous functions: $(f,g) \twoheadrightarrow (h,i) \; \triangleq \; (g\twoheadrightarrow h, f \twoheadrightarrow i)$ Note that the positions of $f$ and $g$ are swapped in the above definition. $\dfrac {A \xtofrom [g]{f} B \quad C \xtofrom [i]{h} D}{A \twoheadrightarrow C \xtofrom [f \twoheadrightarrow i]{g \twoheadrightarrow h} B \twoheadrightarrow D}$ Unlike with the category $\textbf {Cpo}$ , this functor is not contravariant but covariant: Note the positions of $A$ and $B$ are not swapped!

Theorem. Fixed point theorem for endofunctors on $\textbf {Cpo}^\textbf {R}$ [dt-005B]

Every cocontinuous endofunctor $\mathcal {F}$ on $\mathbf {Cpo}^\textbf {R}$ has a least fixed point, given by the colimit of the ascending $\omega$ -chain:

Where the retraction pairs

(f_i, g_i)

are defined by:

\begin {array}{lcl} (f_0,g_0) & \triangleq & (\lambda x. \bot , \lambda x. \bot )\\ (f_{i+1},g_{i+1}) & \triangleq & \mathcal {F}(f_i,g_i) \\ \end {array}

Construction. The colimit $D^\infty$ [dt-005H]

Liam O'Connor

Given an $\omega$ -chain:

The colimit (or inverse limit) is the cpo of $\omega$ -tuples: $D_\infty \; \triangleq \; \left \{ (x_0, x_1, \dots ) \mid x_i \in D_i \land x_i = g_i(x_{i+1}) \right \}$ That is, it is countable sequence of elements, one for each domain $D_i$ , where each element is consistent with earlier elements.

Ordering: The ordering is the pointwise ordering of products, naturally generalised to $\omega$ -tuples. Under this ordering, $D_\infty$ is a cpo. In fact if each $D_i$ is a Scott domain, so is $D_\infty$ .

Proof.

Liam O'Connor

We shall prove that $D_\infty$ is an upper bound of the $\omega$ -chain. Proof that it is the least upper bound is straightforward but tedious, and is omitted.

We must construct a family of retraction pairs: $\left \{ D_i \xtofrom [\theta _{\infty ,i}]{\theta _{i,\infty }} D_\infty \middle |\;\; i \in \mathbb {N}\;\; \right \}$ such that the following diagram commutes:

Defining the projection of the retraction pair

D_i \xtofrom [\theta _{\infty ,i}]{\theta _{i,\infty }} D_\infty

is straightforward:

\theta _{\infty ,i}(x_0,x_1,\dots ) \; \triangleq \; x_i

However, to define the embedding

\theta _{i,\infty }

requires us to, for a given value

x \in D_i

, produce an

\omega

-tuple of values consistent with

x

in every domain

D_k

. We do this by defining

\theta _{i,\infty }

in terms of helper functions

\theta _{i,j}

:

\theta _{i,\infty }(x) \; \triangleq \; (\theta _{i,0}(x),\theta _{i,1}(x),\theta _{i,2}(x),\dots )

The helper functions

\theta _{i,j}

are defined by composing sequences of embeddings (

f

s) or projections (

g

s), depending on whether

i < j

or

j < i

. For example, when

i = 2

:

\begin {array}{lcl} \theta _{2,\infty }(x) &=& (\theta _{i,0}(x),\theta _{i,1}(x),\theta _{i,2}(x),\theta _{i,3}(x),\theta _{i,4}(x),\dots ) \\[1em] &=& (\underbrace {g_0(g_1(x))), g_1(x)}_{\text {\emph {approximations} to}\ x}, x, \underbrace {f_2(x), f_3(f_2(x)),\dots }_{\text {\emph {equivalent} to}\ x}) \end {array}

Semantics of untyped $\lambda$ -calculus [dt-005L]

Liam O'Connor

Recall the untyped $\lambda$ calculus:

Definition. Untyped $\lambda$ -calculus [dt-004K]

Liam O'Connor

Untyped $\lambda$ -calculus consists only of untyped (higher-order) functions: $e \; \Coloneqq \; x \mid \lambda x. e \mid e_1\ e_2$

We mentioned before that the semantic domain of this language must be a cpo

D

such that

D \simeq D\twoheadrightarrow D

In other words, solutions to this equation are fixed points of

\mathcal {F}(X) = X\twoheadrightarrow X

. The least such fixed point can expressed, by Theorem [dt-005B], as the colimit of the

\omega

-chain:

But, the least solution to this equation is trivial:

D_\infty \simeq \mathbf {1}

, because

\mathbf {1} \simeq \mathbf {1}\twoheadrightarrow \mathbf {1}

. A non-trivial solution is obtained by starting the chain at

\mathbf {2}

, the cpo containing just

\{\top ,\bot \}

, rather than

\mathbf {1}

.

We will now sketch a proof of the retraction pair between $D_\infty$ and $D_\infty \twoheadrightarrow D_\infty$ , by providing two functions, $\textbf {\textsf {up}} : D_\infty \rightarrow (D_\infty \twoheadrightarrow D_\infty )$ and its inverse $\textbf {\textsf {down}} : (D_\infty \twoheadrightarrow D_\infty ) \rightarrow D_\infty$ .

Observe that each element of $D_i$ (for $i > 0$ ) is a function $D_{i-1} \twoheadrightarrow D_{i-1}$ . Therefore, an element of the colimit $D_\infty$ is an $\omega$ -tuple of such functions. To define $\textbf {\textsf {up}}(d)(x)$ , we must essentially "apply" each function in the element $d \in D_\infty$ (viewed as an $\omega$ -tuple of functions) to the element $x \in D_\infty$ (viewed as an $\omega$ -tuple of values). More specifically, we say that $\textbf {\textsf {up}}(d)(x)$ is an $\omega$ -tuple $(y_m \mid y \in \mathbb {N})$ , as follows: $y_m = \bigsqcup _{k \in \mathbb {N}} \theta _{m+k,m}(d_{m+k+1}(x_{m+k}))$ To define $\textbf {\textsf {down}}(f)$ , we are given a (continuous) function $f : D_\infty \twoheadrightarrow D_\infty$ and must construct the $\omega$ -tuple of approximations at every $D_n$ . We do this by projecting the action of $f$ down to $D_n$ . We say that $\textbf {\textsf {down}}(f)$ is an $\omega$ -tuple $(v_n \mid n \in \mathbb {N})$ where: $\begin {array}{lcl} v_0 & \triangleq & \theta _{\infty ,0}(f(\theta _{0,\infty }(\bot _{D_0})))\\ v_{n+1} & \triangleq & \theta _{\infty ,n} \circ f \circ \theta _{n,\infty } \end {array}$

Definition. Denotations for untyped $\lambda$ -calculus

Liam O'Connor

Using the new functions $\textbf {\textsf {up}}$ and $\textbf {\textsf {down}}$ , it is now straightforward to define a semantics for untyped $\lambda$ -calculus, where $\sigma$ is an environment $\mathsf {Var} \rightarrow D_\infty$ : $\llbracket \cdot \rrbracket : (\mathsf {Var} \rightarrow D_\infty )\twoheadrightarrow D_\infty$ $\begin {array}{lcl} \llbracket x \rrbracket \sigma & = & \sigma (x) \\ \llbracket e_0\ e_1 \rrbracket \sigma & = & \textbf {\textsf {up}}(\llbracket e_0 \rrbracket \sigma ) (\llbracket e_1 \rrbracket \sigma )\\ \llbracket \lambda x.\ e \rrbracket \sigma & = & \textbf {\textsf {down}}(\boldsymbol {\lambda } v \in D_{\infty }.\ \llbracket e \rrbracket \ \sigma (x \mapsto v) ) \end {array}$ This semantics does not distinguish non-terminating computations from terminating ones. To model call-by-value more faithfully, we could use the equation $D \simeq D\twoheadrightarrow D_\bot$ instead, and for call-by-name we could use $D \simeq D_\bot \twoheadrightarrow D_\bot$ . The constructions are very similar.

Institution. University of Edinburgh [uoe]

Scotland, United Kingdom
https://ed.ac.uk