Last year, the BCS-FACS annual Christmas meeting covered the topic of Domain Theory. The two day format included introductory and intermediate level tutorials, and more advanced lectures; there was something for everybody. Below, I attempt to give a flavour of the presentations, from my own point of view as an attendee. This summary is necessarily incomplete: it is impossible to compress two days of dense mathematics into a few pages. So at the end there is a list of 'further reading', where more on the various topics can be found.
This introductory tutorial motivated giving formal mathematical meanings to programs, introduced denotational semantics as one such approach, and gave an justification for why domains are a necessary component of the process.
A meaning can be given to a program by interpreting it as a mathematical object. With denotational semantics, the mathematical structure used is an algebra, and each language construct is given an interpretation as an operator in the algebra. The programming language construct 'denotes' the mathematical object.
For a simple imperative language, the algebra can be one of sets and functions. For example, expressions can be interpreted as denoting numbers (the appropriate value of the expression) and commands as denoting state transitions functions. The first problem with this simple approach occurs with the 'while' command, which has a recursive definition with the possibility of non-termination. A partial function approach can be used to solve this problem: 'before states' corresponding to non-terminating loops are not in the domain of the partial state transition function. But eventually, as the language being defined gets more complicated (for example, procedures as parameters to procedures) a richer mathematical model is needed to represent it: domain theory.
Consideration of the desirable properties of a denotational specification language (such as existence of fixed points, and handling of non-termination) leads to an axiomatic definition of the properties required of domains. For example, non-termination is denoted by partial objects, with 'more defined' being formalized by partial ordering, and 'fully defined' by the limit. So, domains are complete partial orders (partial orders that have a least upper bound). Using set theory allows 'too many' functions to be represented: we want only the computable functions between domains, those that preserve the structure of the domains. 'Monotonic' functions preserve the order (which implies the Halting Problem cannot be solved), and 'continuous' functions preserve limits (which implies only a finite amount of information about the input data can be used in the computation).
This tutorial presented Scott Information Systems as one approach to solving domain equations (another approach uses category theory).
A Scott Information System (SIS) is a domain presented from an informational point of view. It comprises a set of 'tokens' (units of information), a consistency predicate (to say whether tokens have been combined consistently) and an entailment rule (that says whether one piece of information automatically entails another). These components must satisfy various properties.
The set of all 'ideals' of a SIS form a domain. Although not all domains can be constructed this way, enough 'useful' ones can; the advantage is that when sets of simultaneous equations involving domains are translated into SIS terms, they can be solved more easily.
This tutorial presented a number of domain equations for natural numbers, lists, and functions, and discussed their solutions.
Similar data structures can come with a variety of evaluation strategies. For example, lists can be 'strict cons' (eager, finite lists), 'lazy cons' (finite and infinite lists), and 'head-strict tail-lazy cons' (infinite lists). These different computational models are captured by different domain equations.
More complex domains occur when considering 'self-application' in the \(\lambda\)-calculus: terms of the form \(x\,x\). Considering the types, \(x\) must have a type \(D\) and also type \(D \rightarrow D\). The structure of non-trivial domains that satisfy this requirement is rather complex.
This lecture presented recent approaches for formalizing the language used to define the denotational semantics of another language (the metalanguage) and for improving the structuring of the definition.
Given a domain, a new domain modelling a new kind of computation can be constructed from it. For example, domains supporting side-effects, exceptions and non-determinism can be constructed from a simpler domain in a systematic manner. It has been noted that all these constructions have the same form, that of a strong monad on the category of semantic domains.
This research is continuing, with the aim of providing a structured way of adding new language features.
This tutorial presented the denotational semantics of the parallel language CSP (Communicating Sequential Processes).
The denotation of programs in CSP is the set of all possible observations. In the simplest model, the 'traces' model, the observations are the communications between processes. However, this model is not rich enough to distinguish some undesirable programs from desirable ones: it does not handle deadlock properly. A more sophisticated model, the 'failures-divergences' model has to be used, where the communications processes refuse to engage in are also considered.
This lecture presented the problem with an infinite traces model of CSP (as opposed to the standard, finite, traces model), and its resolution.
The failures-divergences model of CSP cannot model 'fairness' properties. An infinite traces model, dealing with infinitely non-deterministic processes, in needed. Unfortunately, this model does not have a complete partial order: it does not have upper bounds required by the domain axioms. A more sophisticated treatment is needed.
This tutorial presented powerdomains, used in the denotation of concurrent languages (except for CSP, which has its own, hand-crafted domains).
Powerdomains model (finite) non-determinism. Informally, a non deterministic command can be considered as a mapping from the before state to a set of after states: \( S \rightarrow \mathbb{P} S\). Powerdomains are the domain theoretic analogues of the sets of finite subsets of a set.
When reasoning about liveness, non-determinism is 'good': a larger set of possible outcomes means more good things might happen. When reasoning about safety, non-determinism is 'bad': a larger set of possible outcomes means less control over the process. Hence there are various different order relations necessary on powerdomains.
Recent work on powerdomains has been in the area of databases. A database can be considered as a set of records. When different records with identical fields are allowed, 'bag domains' can be used, but these are outside conventional domain theory.
This lecture presented the connection between denotational semantics using power domains, and axiomatic semantics using Dijkstra's weakest preconditions, when viewed from a topological perspective.
The numbers before the references refer to the presentations where they were mentioned.
(2) S. Abramsky. The lazy \(\lambda\)-calculus. In D. Turner, editor, Research Topics in Functional Programming. Addison Wesley, 1990.
(8) M. Hennesy and G. D. Plotkin. Full abstraction for a simple parallel programming language. In J. Becvár, editor, Proc. Mathematical Foundations of Computer Science, volume 74 of Lecture Notes in Computer Science, pages 108-120. Springer-Verlag, 1979.
(5) E. Moggi. A Modular Approach to Denotational Semantics. preprint. 1990.
(5) E. Moggi. Inf & Comp. 93:55-92, 1991.
(4) L. C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF, volume 2 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1987.
(9) M. B. Smyth. Power domains and predicate transformers: a topological view. In P. Diaz, editor, Proc. 10th International Colloquium on Automata, Languages and Programming, volume 154 of Lecture Notes in Computer Science, pages 662-675. Springer-Verlag, 1983.
(-) R. D. Tennent. Semantics of Programming Languages. Prentice Hall, 1991.
(8) S. Vickers. Topology via Logic. Cambridge University Press.