Part 1: Domain Theory Basics

This section covers the fundamentals of domain theory. The reader is assumed to know basic definitions in order theory and topology (what is a poset, what is a topological space). I like to provide mathematical content for interested readers but if you just want to read about Lean this section is mostly optional, although I will refer to some things in here without explanation later on.

Table of Contents

1. Introduction
2. Least Fixed Points and Domains
3. Continuous Functions and Kleene’s Theorem
4. Reasoning About Fixed Points: Scott Induction
5. Connections to Topology
6. Conclusion

1. Introduction

Programming languages provide syntax to write programs which perform computations. To reason about our programs, the first step is to decide what programs mean. There are multiple approaches to programming language semantics, but here we will focus on the denotational approach. In denotational semantics, the meaning of a program is considered to be a mathematical object in some space.

If you come from logic, you can think of denotational semantics as the model theory of programming languages. An important property of denotational semantics is compositionality: a program’s meaning should be determined by the meanings of its components.

The most successful approach to denotational semantics is thanks to Scott and Strachey, via the subject of domain theory. The motivation is perhaps best seen through recursive programs.

Consider a simple while loop while b do c. We want to assign this some denotation $W$, and compositionality tells us $W$ should be built from the denotations of $b$ and $c$. Unfolding the loop once, we see that while b do c is equivalent to if b then (c; while b do c) else skip. So whatever $W$ is, it must satisfy:

\[W = \text{if } b \text{ then } (c\ ;\ W) \text{ else } \text{skip}\]

This is a fixed-point equation: $W$ is a fixed point of the function $F(X) = \text{if } b \text{ then } (c\ ;\ X) \text{ else } \text{skip}$. But what kind of object is $W$, and how do we know such a fixed point exists? A while loop can run forever, so we cannot treat $W$ as a total function.

Domain theory provides the structure to guarantee a least fixed point exists and is computable as a limit of finite approximations.

With that motivation, we can get into some of the technical definitions.

2. Least Fixed Points and Domains

Consider again our while loop. We said $W$ should be a fixed point of

\[F(X) = \text{if } b \text{ then } (c\ ;\ X) \text{ else } \text{skip}.\]

The intuition for finding $W$ is as follows. Start with the computation that does nothing and never terminates (call it $\bot$) and keep plugging it back into $F$. The approximation $F(\bot)$ describes the loop run for at most one iteration; $F(F(\bot))$ captures two iterations; and so on.

Each step tells us a little more about what $W$ does, and the “full” denotation should be some kind of limit of these ever-more-defined approximations.

This idea of computations carrying more or less information, arranged from less-defined to more-defined and converging to a limit is the intuition that domain theory formalizes. So our spaces of meanings need two things: an order capturing “is at least as defined as,” and a notion of limit for ascending sequences. The rest of this section makes these ideas formal. Throughout, let $(P, \leq)$ be a poset.

Basic vocabulary

Definition (Least element). A least element is an element $\bot \in P$ such that $\bot \leq p$ for all $p \in P$.

Definition (Chain). A chain is a sequence $(p_i)_{i \in \mathbb{N}}$ of elements in $P$ such that $p_0 \leq p_1 \leq p_2 \leq \cdots$.

Definition (Upper bound). An upper bound of a chain $(p_i)_{i \in \mathbb{N}}$ is an element $p \in P$ such that $p_i \leq p$ for all $i$. A least upper bound (lub) is an upper bound that sits below every other upper bound. We write the lub of $(p_i)$ as

\[\bigsqcup_{i \in \mathbb{N}} p_i.\]

Definition ($\omega$-cpo). An $\omega$-complete partial order ($\omega$-cpo) is a poset in which every chain has a least upper bound.

Definition (Domain). A domain is an $\omega$-cpo which has a least element. A domain is exactly the setting in which our “start from $\bot$ and iterate” construction makes sense, since we have a least element to start from, and we’re guaranteed the limit of our chain of approximations exists.

Examples of domains.

• Partial functions. For sets $X$ and $Y$, the domain of partial functions from $X$ to $Y$ is the set of all functions $f$ with $\mathrm{dom}(f) \subseteq X$ taking values in $Y$, with the ordering $f \leq g$ iff $\mathrm{dom}(f) \subseteq \mathrm{dom}(g)$ and $f(x) = g(x)$ for all $x \in \mathrm{dom}(f)$. In this case the “more defined” interpretation is literal, since $g$ is defined at least wherever $f$ is, and $\bot$ is the nowhere-defined function.

• The flat natural numbers. Consider the set $\mathbb{N}_\bot = \mathbb{N} \cup {\bot}$ where $\bot$ is a special least element, with the ordering $\bot \leq n$ for all $n \in \mathbb{N}$ and all other elements pairwise incomparable. This is visualized by the following Hasse diagram:

In general, given a set $X$ we can construct the flat domain $X_\bot$ in the same way. Keep this in mind for part 2, as this will be an important construction.

Fixed points

Definition (Fixed point). A fixed point of a function $f : D \to D$ is an element $d \in D$ such that $f(d) = d$.

When $D$ is a poset, we can consider the weaker notion of a pre-fixed point:

Definition (Pre-fixed point). An element $d \in D$ is a pre-fixed point of $f$ when $f(d) \leq d$. We write the least pre-fixed point of $f$, when it exists, as $\mathrm{fix}(f)$. It is thus uniquely specified by the two properties:

• $f(\mathrm{fix}(f)) \leq \mathrm{fix}(f)$
• $\forall d \in D,\ f(d) \leq d \implies \mathrm{fix}(f) \leq d$

3. Continuous Functions and Kleene’s Theorem

We’ve now seen a new structure which we call a domain. Given a new structure one should usually ask, what are its structure-preserving maps? In the case of domains/$\omega$-cpos, these are called continuous functions.

Definition (Monotone). A function $f : D_1 \to D_2$ between posets is monotone if it preserves order, i.e. $\forall x, y \in D_1,\ x \leq y \implies f(x) \leq f(y)$.

Theorem. If $f : D \to D$ is monotone and has a least pre-fixed point $\mathrm{fix}(f)$, then $\mathrm{fix}(f)$ is a fixed point, and is the least of these.

Proof. Exercise. $\blacksquare$

Definition (Continuous). A function $f : D_1 \to D_2$ between $\omega$-cpos/domains is continuous if it preserves least upper bounds of chains, i.e.

\[f\!\left(\bigsqcup_{i \in \mathbb{N}} p_i\right) = \bigsqcup_{i \in \mathbb{N}} f(p_i).\]

Exercise: Prove monotonicity follows from continuity

The following theorem says that our iterative construction (start from $\bot$, keep applying $f$, take the lub) does in fact land at the least fixed point, provided $f$ is continuous. This is the result that makes denotational semantics of recursive programs go through.

Theorem (Kleene’s fixed point theorem). Let $D$ be a domain and $f : D \to D$ continuous. Then $f$ has a least fixed point, given by

\[\mathrm{fix}(f) = \bigsqcup_{n \geq 0} f^n(\bot).\]

Proof sketch. First, the iterates $f^n(\bot)$ form a chain: $\bot \leq f(\bot)$ holds trivially since $\bot$ is least, and monotonicity (which we got from continuity) propagates this up. The lub exists because $D$ is a domain, and continuity lets us push $f$ through it:

\[f\!\left(\bigsqcup_n f^n(\bot)\right) = \bigsqcup_n f(f^n(\bot)) = \bigsqcup_n f^{n+1}(\bot) = \bigsqcup_n f^n(\bot).\]

So $\mathrm{fix}(f)$ is a fixed point. For least-ness: if $d$ is any pre-fixed point, i.e. $f(d) \leq d$, then $\bot \leq d$ forces $f^n(\bot) \leq d$ for every $n$ by induction, and taking lubs gives $\mathrm{fix}(f) \leq d$. By the earlier theorem this is in fact the least fixed point. $\blacksquare$

Exercise: Prove the category of $\omega$-cpos (objects are $\omega$-cpos, morphisms are continuous functions) is cartesian closed, i.e. has a terminal object, binary products, and exponentials.

4. Reasoning About Fixed Points: Scott Induction

We have defined least fixed point $\mathrm{fix}(f)$ and shown that it always exists. What’s missing though is how we can reason and prove things about $\mathrm{fix}(f)$. This flavor of iterating $n$ times feels like there is some induction principle at play here, which is exactly the case. Scott induction is a way of reasoning about fixed points and is defined as follows:

Theorem (Scott Induction). Let $D$ be a domain, $f : D \to D$ a continuous function, and $P \subseteq D$ be any subset of $D$. If $P$:

• Contains $\bot$
• Is stable under $f$: ie. $f(P) \subseteq P$
• Is chain closed, ie. for any chain $(p_i) \subseteq P$, the lub $\bigsqcup p_i$ is in $P$

Then $\mathrm{fix}(f) \in P$

That is, to prove that $fix(f)$ has some property $P$, we must show that $\bot$ has property $P$, $f$ preserves $P$, and that $P$ is closed under least upper bounds.

Example. Let $f : D \times (D \times D) \to D$ be continuous and define $g : D \times D \to D \times D$ by

\[g(d_1, d_2) = \bigl(f(d_1, (d_1, d_2)),\ f(d_1, (d_2, d_2))\bigr).\]

Then $g$ is continuous (built from $f$, projections, and pairing), so $\mathrm{fix}(g) = (u_1, u_2)$ exists; we claim $u_1 = u_2$.

Proof. Apply Scott induction with $P = {(d_1, d_2) \in D \times D \mid d_1 = d_2}$. It contains $(\bot, \bot)$, and is chain closed since lubs in $D \times D$ are taken componentwise. It is stable under $g$: if $d_1 = d_2$ then both components of $g(d_1, d_2)$ collapse to $f(d_1, (d_1, d_1))$. $\blacksquare$

5. Connections to Topology

These order-theoretic concepts have a nice connection to topology: any $\omega$-cpo carries a natural topological structure called the Scott topology. Intuitively, the opens are “observable properties”, properties of a computation that can already be detected at some finite stage of a converging computation.

Definition (Scott topology). Let $(D, \leq)$ be an $\omega$-cpo. A subset $O \subseteq D$ is Scott open if

• it is upward closed: $\forall x \in O,\ y \in D,\ x \leq y \implies y \in O$, and
• it is inaccessible by lubs: for any chain $(x_i)_{i \in \mathbb{N}}$ in $D$, if $\bigsqcup_i x_i \in O$ then $x_i \in O$ for some $i$.

The Scott topology on $D$ has the Scott opens as its open sets. We denote the resulting topological space $\Omega D$.

The convenient correspondence is that the two notions of “continuous” we now have, order-theoretic (preserves lubs of chains) and topological (preimages of opens are open), coincide. Formally,

\[\mathrm{Hom}_{\omega\text{-}\mathrm{CPO}}(D, E) = \mathrm{Hom}_{\mathrm{Top}}(\Omega D, \Omega E)\]

for any $\omega$-cpos $D$ and $E$. So $\omega$-CPO sits inside Top as a full subcategory via $D \mapsto \Omega D$.

This picture connects two styles of denotational semantics via Stone duality. In general, Stone duality says a space $X$ is determined (under suitable hypotheses) by its frame of opens $\Omega X$, with continuous maps $f : X \to Y$ corresponding contravariantly to frame homomorphisms $f^{-1} : \Omega Y \to \Omega X$.

Applied to domains, this gives a natural correspondence between state transformers $f : D \to E$ (programs as functions on states) and predicate transformers $f^{-1} : \Omega E \to \Omega D$, which program logics like Hoare logic and separation logic use to map programs to their weakest preconditions. A proper treatment of Stone duality is out of scope here, but for more I recommend Abramsky’s Domain Theory in Logical Form.

6. Conclusion

We’ve given the basic core vocabulary of domain theory: $\omega$-cpos and domains, continuous functions, Kleene’s theorem, Scott induction, and the topological view that links everything to program logics through Stone duality. This is a very small piece of domain theory. For a full exposition see Zhang’s Logic of Domains or Abramsky.

In Part 2 we will look at Lean, in particular Part α, Mathlib’s type of partial values. We’ll unpack its definition, and work through its definition and API, pointing out the underlying domain theory we’ve just covered. In Part 3 we combine Part with Kleene’s theorem to give denotational semantics to a small imperative language with loops.