[Prev][Next][Index][Thread]
Preprint available.

To: types@cs.indiana.edu

Subject: Preprint available.

From: Marcelo Fiore <mf@dcs.ed.ac.uk>

Date: Fri, 11 Apr 1997 14:31:29 +0100

DeliveryDate: Fri, 11 Apr 1997 08:36:31 0500
The following preprint is available at
http://www.dcs.ed.ac.uk/home/mf/ADT/
as cub.dvi and cub.ps. Best, Marcelo.
Complete Cuboidal Sets in Axiomatic Domain Theory
Marcelo Fiore Gordon Plotkin John Power
<mf@dcs.ed.ac.uk> <gdp@dcs.ed.ac.uk> <ajp@dcs.ed.ac.uk>
Department of Computer Science
Laboratory for Foundations of Computer Science
University of Edinburgh, The King's Buildings
Edinburgh EH9 3JZ, Scotland
Synopsis
We study the enrichment of models of axiomatic domain theory. To this end, we
introduce a new and broader notion of domain, viz. that of complete cuboidal
set, that complies with the axiomatic requirements. We show that the category
of complete cuboidal sets provides a general notion of enrichment for a wide
class of axiomatic domaintheoretic structures.
Cuboidal sets play a role similar to that played by posets in the traditional
setting. They are the analogue of simplicial sets but with the simplicial
category enlarged to the cuboidal category of cuboids, i.e. of finite
products O_n1 x ... x O_ni of finite ordinals. These cuboids are the
possible shapes of paths. A cuboidal set P has a set P(C) of paths of
every shape C = n1 x ... x ni; indeed, it is a (rooted) presheaf over the
cuboidal category. The set of points of P is P(O_1). The set of
(onedimensional) paths of length n is P(O_n+1); they can be thought of
as (linear) computations conditional on the occurrence of n linearly
ordered events e_1 < ... < e_n. Evidently, O_n is the partial order
associated to this simple linear event structure, and can be considered as a
sequential process of length n. At higher dimensions, P(O_n1 x ... x O_ni)
can be thought of as the set of computations conditional on the occurrence of
n_1 + ... + n_i events ordered by e_1,1 < ... < e_1,n1 ; ... ;
e_i,1 < ... < e_i,ni. This is the event structure which can be considered
as i sequential processes, of respective lengths O_n1, ..., O_ni, running
concurrently.
Complete cuboidal sets are cuboidal sets equipped with a formallub operator
satisfying three algebraic laws, which are exactly those needed of the lub
operator in order to prove the fixedpoint theorem. Computationally, the
passage from cuboidal sets to complete cuboidal sets corresponds to allowing
infinite processes. In fact, the formallub operator assigns paths of shape
C to `paths of shape C x omega', for every C. Here the set of paths of
shape C x omega is the colimit of the paths of shape C x O_n; such paths
can be thought of as the higherdimensional analogue of the increasing
sequences of traditional domain theory.