Axiomatic Domain Theory

My thesis (Axiomatic Domain Theory in Categories of Partial Maps) is 
available by anonymous ftp from ftp.dcs.ed.ac.uk directory pub/mf files
thesis.dvi.Z and thesis.ps.Z.

Marcelo Fiore

P.S. The abstract follows:


                  Axiomatic Domain Theory 
               in Categories of Partial Maps

                     Marcelo P. Fiore 
               Department of Computer Science   
         Laboratory for Foundations of Computer Science 
         University of Edinburgh, The King's Buildings 
                 Edinburgh EH9 3JZ, Scotland  

                 Phone: + 44 31 650 5145.
                   Fax: + 44 31 667 7209.

                       June 1994 


This thesis is an investigation into axiomatic categorical domain 
theory as needed for the denotational semantics of deterministic 
programming languages. 

To provide a direct semantic treatment of non-terminating computations,
we make partiality the core of our theory. Thus, we focus on categories
of partial maps. We study representability of partial maps and show its
equivalence with classifiability. We observe that, once partiality is 
taken as primitive, a notion of approximation may be derived. In fact, 
two notions of approximation, contextual approximation and 
specialisation, based on testing and observing partial maps are 
considered and shown to coincide. Further we characterise when the 
approximation relation between partial maps is domain-theoretic in the 
(technical) sense that the category of partial maps Cpo-enriches with 
respect to it.

Concerning the semantics of type constructors in categories of partial 
maps, we present a characterisation of colimits of diagrams of total 
maps; study order-enriched partial cartesian closure; and provide 
conditions to guarantee the existence of the limits needed to solve 
recursive type equations. Concerning the semantics of recursive types, 
we motivate the study of enriched algebraic compactness and make it the
central concept when interpreting recursive types. We establish the 
fundamental property of algebraically compact categories, namely that 
recursive types on them admit canonical interpretations, and show that
in algebraically compact categories recursive types reduce to inductive
types. Special attention is paid to Cpo-algebraic compactness, leading 
to the identification of a 2-category of kinds with very strong closure

As an application of the theory developed, enriched categorical models 
of the metalanguage FPC (a type theory with sums, products, 
exponentials and recursive types) are defined and two abstract examples
of models, including domain-theoretic models, are axiomatised. Further,
FPC is considered as a programming language with a call-by-value 
operational semantics and a denotational semantics defined on top of a 
categorical model. Operational and denotational semantics are related 
via a computational soundness result. The interpretation of FPC 
expressions in domain-theoretic Poset-models is observed to be 
representation-independent. And, to culminate, a computational adequacy
result for an axiomatisation of absolute non-trivial domain-theoretic 
models is proved.