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

• 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'.

• The presentation of a domain is quite messy. The nicest axiomatization of domains that I know of is in terms of information systems . One can find an introduction to these in the excellent book 'Introduction to Order Theory' by Davey and Priestly

§ Computation as fixpoints of continuous functions

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

This does not preserve least-upper-bounds. Consider the sequence of elements:

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:

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

§ $\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.
• Lecture notes on denotational semantics: Part 2 of the computer science Tripos
• Outline of a mathematical theory of computation
• Domain theory and measure theory: Video