## § 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 cardinalityof 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 cangive 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 considerationstell 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 canbe 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'.

#### § CPOs

• Given a partial order $(P, \leq)$. assume we have a subset $Q \subseteq P$. A least upper bound $u$ of $Q$ is an element that is the smallest element in $P$which is larger than every element in $Q$.
• A subset $Q$ of $P$ is called as a chain if its elements can be put into order.That is, there is a labelling of elements of $Q$ into $q1, q2, \dots, qn$ suchthat $q1 \leq q2 \leq \dots \leq qn$.

#### § CCPOs

• A partially ordered set is called as a chain complete partial order ifeach chain has a least upper bound.
• This is different from a lattice, where each subset has a least upper bound.
• Every ccpo has a minimal element given by $completion(\emptyset) = \bot$.
• TODO: example of ccpo that is not a lattice

#### § 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 isonly 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 continuousonly works for CCPOs.
• The composition of continuous functions of chain-complete partiallyordered 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.