Domain theory is the study of domains, which are ordered sets of a particular kind, whch can be used to give general descriptions of approximation and continuity. An important application of domain theory is in the denotational semantics of computer programs, which may be represented as functions between domains (representing the data on which the program operates).

Denotations are typically ordered extensionally (the Scott order) --- one program approximates another if the first diverges, or applying them to approximating inputs yields approximating outputs. I am interested in domain-based semantics which give a richer characterization of program behaviour than this. Historically, this has been associated with the quest for domain-theoretic characterizations of sequentiality: there is a mismatch between sequential programs, which must evaluate their arguments step-by-step, and so must diverge if they try to evaluate a non-terminating argument, and Scott-continuous functions, which may return a result if any of their arguments terminate, but diverge if none do (for example "parallel_or". "Sequential domain theory" adds extra structure to domains (such as additional orders or coherence relations on their elements) and requires functions to preserve it. This enables complete descriptions of hierarchies of computable functionals, with properties such as full abstraction to be given.

Much of my work on this subject was the subject of a project: "Extensional Semantics of Program Behaviour" supported by the UK Engineering and Physical Sciences Research Council ( EPSRC).

Bidomains

Bidomains were introduced by Gerard Berry. They combine the extensional (Scott) order with the stable order, which is sparser, and captures, to some degree, the information required to compute a function (very loosely speaking, a function is stable if for any piece of output information, there is a smallest piece of input information which will produce that output). Bidomains can also be decomposed into event structures, which give a model of classical linear logic.

In general, stable and continuous functions on bidomains are not sequential, but for bidomains bounded above (by what we might think of as an error element), then sequentiality is straightforward to establish. Using these domains, we may give simple, fully abstract and universal models for functional languages in which we can only test for convergence, such as Unary PCF, and the typed and untyped call-by-value and lazy lambda-calculi.

Stable and continuous functions on bounded bidomains are (Kahn-Plotkin) sequential (at any argument and result we can always identify an extension to the argument which is required in order to extend the result), but not strongly sequential (this extension is not unique). Thus they are more suitable for representing non-deterministic computation. Interestingly, they may also give a rather precise representation of "fair" non-determinism (via countable choice), despite the fact that this is inherently non-continuous, and thus yields a rather strange domain theory: the information supplied by the stable order somewhat compensates for the loss of continuity.

One way to obtain strong sequentiality is by also requiring sequentiality with respect to the error, or top element). This is achieved in bistable bidomains by replacing the stable order with a "bistable" order, or (equivalently) a bistable equivalence relation which is symmetric with respect to the two types of failure. Loosely speaking, elements are bistably coherent if they have the same computational behaviour except at points of failure, where one may diverge and the other may enter an error state. Bistable bidomains may be used to give models of languages with control operators (such as SPCF) as well as CPS languages which are universal (at finite types) and fully abstract.

In fact, we can strengthen these results, in the case of SPCF, to show that every bistable function in our model is the denotation of an affinely typable term (one in which functions cannot "share" variables with their arguments, and can only use iteration rather than arbitrary fixpoints). This is significant because it establishes that each term in this language is contextually equivalent to one with no nested or recursive function calls.

These universality results tell us that the bistable functionals are a purely extensional characterization of the "observably sequential functionals", which are the functionals computed by sequential algorithms (established by Cartwright, Curien and Felleisen). Can we then also give an abstract characterization of the domains which correspond to the sequential data structures (or games) on which sequential algorithms are defined? Locally Boolean domains in which the duality between error and divergence is formally captured by an involutive "negation" operator provide an (affirmative) answer.

A further question suggested by these results: is there an intensional representation of stable monotone or continuous functions on (stable) bidomains? By adding an ordering to concrete data structures, and defining non-deterministic sequential algorithms to be up-closed sets with respect to this ordering, we can give such a characterization --- there is a full and faithful functor from the category of ordered and non-deterministic sequential algorithms into the category of bidomains and stable and monotone functions.

Another possible application of bistability is in the semantics of fresh names (an important step in describing locally declared features such as references and exceptions). As shown by Pitts and others, we can describe fresh names in a higher-order setting by adding an action of the natural number permutations to an appropriate category of domains, and this can be done in the case of bistable biorders, (to get a kind of FM (Fraenkel-Mostowski) biorder. CPS interpretation in FM-cpos and FM-bicpos admits a simple interpretation of new-name declaration: bistability cuts out a lot of the "junk" in the FM-cpo model.

Taking a more abstract view, we may represent bidomains as algebras with a coherence relation, and stable functions as homomorphisms on their coherent cliques.

Links

Other researchers with work on bidomains: Domains IX a workshop in Domain theory to be held in Brighton, UK 22-24 September 2008.