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.
participants (1)
-
Marcelo Fiore