Domain theory and denotational semantics, explained

The problem: what does a recursive definition mean?

Denotational semantics assigns to every program a mathematical object, its denotation, in such a way that the meaning of a compound program is built from the meanings of its parts. Christopher Strachey and Dana Scott began the project at Oxford around 1970. It runs into trouble immediately with recursion. Consider

This is not a definition in the ordinary sense: $\mathit{fact}$ appears on both sides. It is an equation, $\mathit{fact} = F(\mathit{fact})$, where $F$ is the operator that takes any function $g$ to the function “$n \mapsto$ if $n = 0$ then 1 else $n \times g(n-1)$”. A solution is a fixed point of $F$. But equations can have no solutions or many: $g(n) = g(n) + 1$ has none among total functions, and $g(n) = g(n)$ has every function as a solution. And programs that loop forever need a meaning too.

Domain theory resolves all three issues at once. It adds an element $\bot$ (“bottom”) meaning “no information yet” or “does not terminate”, orders values by information, and shows that the recursive equations arising from programs always have a least solution, which is the one the program computes.

Ordering by information

A partial order $\sqsubseteq$ is reflexive, antisymmetric and transitive (see sets, relations and functions). In domain theory, $x \sqsubseteq y$ is read “$y$ is at least as defined as $x$”, or “$y$ refines $x$”.

• Flat domains. The natural numbers with a bottom added, $\mathbb{N}_\bot$, are ordered so that $\bot \sqsubseteq n$ for every $n$ and distinct numbers are incomparable. A computation of a number either hasn’t produced one ($\bot$) or has produced a definite answer, which is then never revised.
• Partial functions. Functions $\mathbb{N} \rightharpoonup \mathbb{N}$ are ordered by $f \sqsubseteq g$ when $g$ agrees with $f$ wherever $f$ is defined and may be defined in more places. The everywhere-undefined function is the least element.
• Streams. Finite and infinite sequences, ordered by “is a prefix of”. A program printing an infinite stream produces ever longer prefixes.

Limits: directed-complete partial orders

A computation that runs forever, such as one printing an infinite stream or approximating a real number, produces an increasing chain of partial results $x_0 \sqsubseteq x_1 \sqsubseteq x_2 \sqsubseteq \cdots$. We want such chains to have a limit. More generally, a set $D$ is directed if it is non-empty and any two of its elements have an upper bound in it.

All three examples above are dcpos. The least upper bound of a chain of partial functions is their union; of a chain of stream prefixes, the stream they converge to.

Continuous functions

A computable function cannot look at a whole infinite object at once: any finite amount of output depends on only a finite amount of input. Domain theory captures this as continuity.

Monotonicity says more input never retracts output. Preservation of limits says the output on a limit is the limit of the outputs on its approximations: nothing new appears “only at infinity”. Every function you can write in a programming language denotes a continuous function. A function that, say, returns 1 exactly when its input stream is infinite would not be continuous, and indeed no program computes it.

The fixed-point theorem

Why it works. Since $\bot \sqsubseteq f(\bot)$ and $f$ is monotone, applying $f$ repeatedly gives a chain $\bot \sqsubseteq f(\bot) \sqsubseteq f^2(\bot) \sqsubseteq \cdots$, which has a least upper bound $x$ because $D$ is a dcpo. By continuity, $f(x) = \bigsqcup_n f^{n+1}(\bot) = x$, so $x$ is a fixed point. If $y$ is any fixed point, then $\bot \sqsubseteq y$, so $f^n(\bot) \sqsubseteq f^n(y) = y$ for every $n$, and hence $x \sqsubseteq y$.

The chain is literally the computation unfolding. For the factorial operator $F$, $F^k(\bot)$ is the function that answers correctly on $0, \dots, k-1$ and is undefined elsewhere, exactly what you would get by allowing the recursion to unfold at most $k$ times. Step through it:

The least fixed point is also the right one for nontermination. For the equation $g(n) = g(n)$, every function is a fixed point, but the least is the everywhere-undefined one, which is exactly what a program defined that way does: it loops.

Building new domains

To give semantics to a whole language we need domains for every type, built from smaller ones. The key constructions all preserve “being a dcpo”:

• Products $D \times E$, ordered componentwise, for pairs and records.
• Lifting $D_\bot$, a new bottom below $D$, to model computations that may not terminate.
• Sums for variants and tagged unions.
• Function spaces $[D \to E]$, the continuous functions ordered pointwise. That this is again a dcpo makes the category of dcpos and continuous functions cartesian closed, which is what is needed to interpret the typed λ-calculus.

Recursive domain equations

Recursive types lead to equations between domains. A type of lists of integers should satisfy $L \cong 1 + (\mathbb{Z} \times L)$. The untyped λ-calculus, where every term can be applied to any other, needs a domain with

For sets this is impossible when $D$ has more than one element, by Cantor’s argument. Scott’s breakthrough in 1969 was to construct a non-trivial solution among domains, as the limit of a sequence of approximations $D_0, D_1 = [D_0 \to D_0], \dots$ (the inverse limit construction). It was the first mathematical model of the untyped λ-calculus, and the same technique solves the domain equations for recursive types in general.

The Scott topology: observable properties

Domain theory has a topological reading. A set $U$ of elements is Scott-open if it is upward closed (if $x \in U$ and $x \sqsubseteq y$ then $y \in U$) and inaccessible by directed limits (if $\bigsqcup D \in U$ then already some $d \in D$ is in $U$). Think of an open set as a property you can observe after a finite amount of computation, such as “the stream starts with 0, 1”. Once observed, more information cannot falsify it, and if a limit has it, some finite stage already showed it.

With this topology, the Scott-continuous functions are exactly the topologically continuous ones. Abramsky’s domain theory in logical form pushes the idea further, using Stone duality to turn domains into logics of observable properties, so that program logics and denotational models are two sides of the same structure.

Approximation: algebraic and continuous domains

An element $c$ is compact (or finite) if whenever $c \sqsubseteq \bigsqcup D$ for a directed $D$, already $c \sqsubseteq d$ for some $d \in D$. In the domain of partial functions the compact elements are the functions defined on finitely many inputs. A domain is algebraic if every element is the least upper bound of the compact elements below it: everything is a limit of finite pieces of information, which is what makes it possible to compute with infinite objects at all. Continuous domains relax this using the “way-below” relation $\ll$, and include important examples such as the interval domain used to compute with real numbers exactly.

Powerdomains: nondeterminism and probability

A nondeterministic program can produce one of several results, so its meaning should be a set of outcomes. Powerdomains are the domain-theoretic analogue of the power set, and there are three classic ones, differing in how they treat the possibility of nontermination:

Plotkin introduced the first powerdomain in 1976 and Smyth the upper one in 1978. For randomised programs, the meaning is a probability distribution over outcomes; Jones and Plotkin’s probabilistic powerdomain of valuations does this domain-theoretically, and combining it with nondeterminism has been a long-running research problem. Today these ideas underpin the semantics of probabilistic programming languages.

Full abstraction and PCF

A denotational model is adequate if programs with equal denotations behave the same, and fully abstract if the converse also holds: two program fragments get the same denotation exactly when no program can tell them apart. In 1977 Plotkin studied PCF, a typed λ-calculus with recursion and arithmetic, and showed that Scott’s model is adequate but not fully abstract. The culprit is “parallel or”, a function that exists in the model but cannot be written in the sequential language; adding it to the language makes the model fully abstract. Milner showed the same year that a fully abstract model of PCF itself exists, but built it out of the syntax. Constructing one by genuinely semantic means became known as the full abstraction problem. Game semantics, developed in the early 1990s and published in full in 2000, gave the first such models: types are games and programs are strategies for playing them.

Where domain theory is used

• Language semantics and design. Denotational models justify program equivalences, compiler optimisations and type-system soundness, and Moggi’s monads, now standard in functional programming, came from structuring such models.
• Static analysis. Abstract interpretation computes properties of programs as fixed points over lattices of abstract values, the same least-fixed-point idea applied to approximation.
• Exact real arithmetic and computable analysis, using continuous domains such as the interval domain.
• Probabilistic and quantum programming, where valuations and related powerdomains give meaning to random and quantum choice.

The field’s results appear mostly at the Mathematical Foundations of Programming Semantics (MFPS) conference, held since 1985, and at LICS and ICALP.

Reading list

Where to start

1. S. Abramsky and A. Jung, “Domain theory”, in Handbook of Logic in Computer Science, vol. 3, Oxford University Press, 1994. The standard long survey; the authors have made a copy freely available.
2. G. Winskel, The Formal Semantics of Programming Languages: An Introduction, MIT Press, 1993. Chapters 5 and 8 introduce denotational semantics and domains gently.
3. R. M. Amadio and P.-L. Curien, Domains and Lambda-Calculi, Cambridge University Press, 1998. doi:10.1017/CBO9780511983504
4. G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson et al., Continuous Lattices and Domains, Cambridge University Press, 2003. The comprehensive reference. doi:10.1017/CBO9780511542725

Foundations

1. D. S. Scott, “Continuous lattices”, in Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, Springer, 1972. doi:10.1007/BFb0073967
2. D. S. Scott, “Data types as lattices”, SIAM Journal on Computing 5(3), 1976. doi:10.1137/0205037
3. C. Strachey and C. P. Wadsworth, “Continuations: a mathematical semantics for handling full jumps”, Higher-Order and Symbolic Computation 13, 2000 (reprint of a 1974 Oxford technical monograph). doi:10.1023/A:1010026413531
4. G. D. Plotkin, “LCF considered as a programming language”, Theoretical Computer Science 5(3), 1977. doi:10.1016/0304-3975(77)90044-5

Powerdomains and probability

1. G. D. Plotkin, “A powerdomain construction”, SIAM Journal on Computing 5(3), 1976. doi:10.1137/0205035
2. M. B. Smyth, “Power domains”, Journal of Computer and System Sciences 16(1), 1978. doi:10.1016/0022-0000(78)90048-X
3. C. Jones and G. D. Plotkin, “A probabilistic powerdomain of evaluations”, Proceedings of the 4th IEEE Symposium on Logic in Computer Science, 1989. doi:10.1109/LICS.1989.39173

Logic, effects and full abstraction

1. S. Abramsky, “Domain theory in logical form”, Annals of Pure and Applied Logic 51, 1991. doi:10.1016/0168-0072(91)90065-T
2. E. Moggi, “Notions of computation and monads”, Information and Computation 93(1), 1991. doi:10.1016/0890-5401(91)90052-4
3. S. Abramsky, R. Jagadeesan and P. Malacaria, “Full abstraction for PCF”, Information and Computation 163(2), 2000. doi:10.1006/inco.2000.2930
4. J. M. E. Hyland and C.-H. L. Ong, “On full abstraction for PCF: I, II, and III”, Information and Computation 163(2), 2000. doi:10.1006/inco.2000.2917
5. P. Cousot and R. Cousot, “Abstract interpretation: a unified lattice model for static analysis of programs”, POPL 1977. doi:10.1145/512950.512973

For an overview and further links, see also domain theory on Wikipedia.