## § Crash course on DCPO: formalizing lambda calculus

In lambda calculus, we often see functions of the form $\lambda x \rightarrow x(x)$. We would like a way to associate a "natural" mathematical object to such a function. The most obvious choice for lambda calculus is to try to create a set $V$ of values which contains its own function space: $(V \rightarrow V) \subseteq V$. This seems to ask for a set whose cardinality is such that $|V|^|V| = |V|$, which is only possible if $|V| = 1$, ie $V$ is the trivial set $\{ * \}$. However, we know that lambda calculus has at least two types of functions: functions that terminate and those that don't terminate. Hence the trivial set is not a valid solution. However, there is a way out. The crucial insight is one that I shall explain by analogy:
• We can see that the cardinality of $\mathbb R$ is different from the cardinality of the space of functions over it, $\mathbb R \rightarrow \mathbb R$.
• However, "the set of all functions" isn't really something mathematicians consider. One would most likely consider "the set of all continuous functions" $\mathbb R \rightarrow \mathbb R$.
• Now note that a function that is continuous over the reals is determined by its values at the rationals . So, rather than giving me a continus function $f: \mathbb R \rightarrow \mathbb R$, you can give me a continuous function $f': \mathbb Q \rightarrow \mathbb R$ which I can Cauchy-complete, to get a function $\texttt{completion}(f') : \mathbb R \rightarrow \mathbb R = f$.
• Now, cardinality considerations tell us that:
$|\mathbb R^\mathbb Q| = (2^{\aleph_0})^{\aleph_0} = 2^{\aleph_0 \cdot \aleph_0} = 2^\aleph_0 = |R|$
• We've won! We have a space $\mathbb R$ whose space of continuous functions $\mathbb R \rightarrow \mathbb R$ is isomorphic to $\mathbb R$.
• We bravely posit: all functions computed by lambda-calculus are continuous! Very well. This leaves us two questions to answer to answer: (1) over what space? (2) with what topology? The answers are (1) a space of partial orders (2) with the Scott topology

#### § Difference between DCPO theory and Domain theory

• A DCPO (directed-complete partial order) is an algebraic structure that can be satisfied by some partial orders. This definition ports 'continuity' to partial orders.
• A domain is an algebraic structure of even greater generality than a DCPO. This attempts to capture the fundamental notion of 'finitely approximable'.

#### § Posets, (least) upper bounds

• A partial order $(P, \leq)$ is a set equipped with a reflexive, transitive, relation $\leq$ such that $x \leq y$ and $y \leq x$ implies $x = y$.
• A subset $D \subseteq P$ is said to have an upper bound $u_D \in P$ iff for all $d \in D$, it is true that $d \leq u_D$.
• An upper bound is essentially a cone over the subset $D$ in the category $P$.
• A subset $D \subseteq P$ has a least upper bound $l_D$ iff (1) $l_D$ is an upper bound of $D$, and (2) for every upper bound $u_D$, it is true that $l_D \leq u_D$
• Least upper bounds are unique, since they are essentially limits of the set $D$ when $D$ is taken as a thin category

#### § Directed Sets

• A subset $D \subseteq P$ is said to be directed iff for every finite subset $S \subseteq D$, $S$ has a upper bound $d_S$ in $D$. That is, the set $D$ is closed under the upper bound of all of its subsets.
• Topologically, we can think of it as being closure , since the upper bound is sort of a "limit point" of the subset, and we are saying that $D$ has all of its limit points.
• Categorically, this means that $D \subseteq P$ taken as a subcategory of $P$ has cones over all finite subsets. (See that we do not ask for limits/least upper bounds over all finite subsets, only cones/upper bounds).
• We can think of the condition as saying that the information in $D$ is internally consistent: for any two facts, there is a third fact that "covers" them both.
• slogan: internal consistency begets an external infinite approximation.
• QUESTION: why not ask for countable limits as well?
• QUESTION: why upper bounds in $D$? why not external upper bounds in $P$?
• QUESTION: why only upper bounds in $D$? why not least upper bounds in $D$?
• ANSWER: I think the point is that as long as we ask for upper bounds, we can pushforward via a function $f$, since the image of a directed set will be directed.

#### § Directed Complete Partial Order ( DCPO)

• A poset is said to be directed complete iff every directed set $D \subseteq P$ has a least upper bound in $P$.
• Compare to chain complete, CCPO, where every chain has a LUB.
• QUESTION: why not postulate that the least upper bound must be in $D$?
• In a DCPO, for a directed set $D$, denote the upper bound by $\cup D$.

#### § Monotonicity and Continuity

• A function $f: P \to Q$ between posets is said to be monotone iff $p \leq p'$ implies that $f(p) \leq f(p')$.
• A function $f: P \to Q$ is continuous, iff for every directed set $D \subseteq P$, it is true that $f(\cup D) = \cup f(D)$.
• This has the subtle claim that the image of a directed set is directed.

#### § Monotone map

• A function from $P$ to $Q$ is said to be monotone if $p \leq p' \implies f(p) \leq f(p')$.
• Composition of monotone functions is monotone.
• The image of a chain wrt a monotone function is a chain.
• A monotone function need not preserve least upper bounds . Consider:
$f: 2^{\mathbb N} \rightarrow 2^{\mathbb N} f(S) \equiv \begin{cases} S & \text{S} is finite \\ S U \{ 0 \} &\text{S is infinite} \end{cases}$
This does not preserve least-upper-bounds. Consider the sequence of elements:
$A_1 = \{ 1\}, A_2 = \{1, 2\}, A_3 = \{1, 2, 3\}, \dots, A_n = \{1, 2, 3, \dots, n \}$
The union of all $A_i$ is $\mathbb N$. Each of these sets is finite. Hence $f(\{1 \}) = \{1 \}$, $f(\{1, 2 \}) = \{1, 2\}$ and so on. Therefore:
$f(\sqcup A_i) = f(\mathbb N) = \mathbb N \cup \{ 0 \}\\ \sqcup f(A_i) = \sqcup A_i = \mathbb N$

#### § Continuous function

• A function is continous if it is monotone and preserves all LUBs. This is only sensible as a definition on ccpos, because the equation defining it is: lub . f = f . lub, where lub: chain(P) \rightarrow P. However, for lubto always exist, we need P to be a CCPO. So, the definition of continuous only works for CCPOs.
• The composition of continuous functions of chain-complete partially ordered sets is continuous.

#### § Fixpoints of continuous functions

The least fixed point of a continous function $f: D \rightarrow D$ is:
$\texttt{FIX}(f) \equiv \texttt{lub}(\{ f^n(\bot) : n \geq 0 \})$

#### § $\leq$ as implication

We can think of $b \leq a$ as $b \implies a$. That is, $b$ has more information than $a$, and hence implies $a$.

#### § References

• Semantics with Applications: Hanne Riis Nielson, Flemming Nielson.