[Prev][Next][Index][Thread]

Preprint available.

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 domain-theoretic 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 
 (one-dimensional) 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 formal-lub operator 
 satisfying three algebraic laws, which are exactly those needed of the lub 
 operator in order to prove the fixed-point theorem.  Computationally, the 
 passage from cuboidal sets to complete cuboidal sets corresponds to allowing 
 infinite processes.  In fact, the formal-lub 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 higher-dimensional analogue of the increasing 
 sequences of traditional domain theory.