[Prev][Next][Index][Thread]
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
<mf@dcs.ed.ac.uk>
Phone: + 44 31 650 5145.
Fax: + 44 31 667 7209.
June 1994
Synopsis
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
properties.
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.
------------------------------------------------------------------------