(Link)

Authors: Samson Abramsky (University of Oxford) and Achim Jung (University of Birmingham)

Reference: Abramsky, S., & Jung, A. (1994). Domain theory. In Handbook of Logic in Computer Science, Vol. III, Clarendon Press, 1994, pages 1-168

Why this paper? Cited by Tensorial structure of the lifting doctrine in constructive domain theory and Refinement Types for Liveness Properties in Denotational Semantics

Domains are certain forms of ordered sets used to address problems in the denotational semantics (mathematical interpretation) of programming languages. The area was invented by Dana Scott in a series of papers starting in 1969, building on earlier work by many others that used lattices. This book (which admittedly, I did not have time to read in full detail this week) does not examine the applications of domains, but rather is a handbook on their mathematics. Indeed, at a point where computing applications are discussed, the authors apologise for “deviat[ing] from our general philosophy [to] spend some time on examples”! This is therefore possibly not the best book to start with this topic – suggested references are included in the text – but rather should be considering a book for ‘working computer scientists’ to look up results in, or fill in gaps in their knowledge with.

The central motivation for domain theory is recursion: we have a program, type, or even programming language, say x, that is defined by an equation between x and a term that contains x. Denotationally, we naturally interpret the term as a function or functor F, and hence wish to find an interpretation X of x such that F(X) = X. Such an X is called a fixpoint. Moreover, if there are many choices of fixpoint, we would like there to be one that is ‘canonical’, which should line up with how the recursive program, type, etc behaves operationally in our application. Finally, we would like our mathematics to be able to handle the fact that some recursive definitions do not terminate.

This machinery can be provided by interpreting our programs and/or types in a mathematical universe of (pointed) directed-complete partial orders (dcpo’s), in which fixpoints are guaranteed to exist, and to be calculable in a uniform manner. The notion of (algebraic or continuous) domain extends dcpo’s with a basis, a certain subset that is well behaved with respect to an approximation order, which allows one to model non-termination and, indeed, other computational properties such as evaluation order.

I should note that I do not find the definitions of dcpo or domain particularly obvious; unlike a lot of useful mathematics that computer scientists use, this is not a beautiful concept that arises from pure mathematics that we then make use of, but rather something engineered for application. I find the fact that the central definitions all involve quantification over all possible directed subsets to be a little slippery to develop intuition for. Perhaps this is not just a personal failing, as a later chapter of this book remarks that “[the] elaboration of the resulting theory showed that these structures do indeed work; they meet the requirements with which we began. The question remains whether another class of structures might have served as well or better”. I do find the attempts to explore alternatives via axiomatic or synthetic approaches quite interesting; I am not completely sure what extent these attempts have succeeded in supplanting ‘classical domain theory’ in the two decades since this book appeared, but I know that they remain a focus of interesting work (e.g. here).