Logics of Types and Computation

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 in our view is a simple connection between domains and the common 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 suddenly saw 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 also allowing a suitable general logic. The primary category is called Equ, the category of equilogical spaces. There are several possible versions of this idea leading to a number of different categories.

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. This also lead us to a more general study of realizability theory and in particular relative realizability. The future project now is to pursue these ideas further as a unifying platform for semantics and reasoning.