A New Category for Semantics

Andrej Bauer and Dana S. Scott

June 2001


Domain theory for denotational semantics is over thirty years old. There are many variations on the idea and many interesting constructs that have been proposed by many people for realizing a wide variety of types as domains. Generally, the effort has been to create categories of domains that are cartesian closed (that is, have products and function spaces interpreting typed lambda calculus) and permit solutions to domain equations (that is, interpret recursive domain definitions and perhaps untyped lambda calculus).

What has been missing is a simple connection between domains and the usual set-theoretical structures of mathematics as well as a comprehensive logic to reason about domains and the functions to be defined upon them. In December of 1996, Scott realized that the very old idea of partial equivalence relations on types could be applied to produce a large and rich category containing many specific categories of domains and allowing a suitable general logic. The category is called Equ, the category of equilogical spaces.

The simplest definition is the category of T0-spaces and total equivalence relations with continuous maps that are equivariant (meaning, preserving the equivalence relations). An equivalent definition uses algebraic (or continuous) lattices and partial equivalence relations, together with continuous equivariant maps. This category is not only cartesian closed, but it is locally cartesian closed (that is, it has dependent sums and products). Moreover, it contains as a full subcategory all T0-spaces (and therefore the category of sets and the category of domains).

The logic for this category is intuitionistic and can be explained by a form of the realizability interpretation. The project now is to use this idea as a unifying platform for semantics and reasoning. Our small group of faculty and students at Carnegie Mellon, namely Steven Awodey, Andrej Bauer, Lars Birkedal, and Jesse Hughes, has begun work on this program. A selection of our theses and papers is listed in the bibliography.

Back to Logics of Types and Computation page.