# 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
• Delivery-Date: Fri, 11 Apr 1997 08:36:31 -0500

```The following preprint is available at

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