## A New Category for Semantics

June 2001
#### Abstract:

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 T_{0}-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 T_{0}-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.