Presheaf categories has been proposed as abstract models of
concurrency, with an inbuilt notion of bisimulation based on open
maps. The objects of the base category are to be thought of as
consisting of path objects, or computation-path shapes. The Yoneda
Lemma then justifies an intuition that a presheaf can be thought of as
specifying for a typical path object the set of computation paths of
shape that object. An open map between two presheaves is then defined
to be a natural transformation satisfying a particular path lifting
property.
With this intuition presheaf models encompassing more traditional ones
can be derived from natural definitions of path categories expressed
as dense and full subcategories of the traditional models.
But, suppose that we are not provided yet with a notion of a category
of models for a process language. Is there a general way to define
path categories and presheaf models for process languages?
Our attempts to answer this question will be the main subject of the
talk. We look for a suitable `space' of domains in which we have the
possibility of (recursively) describing the kind of observations we
wish to make. We will consider the bicategory of profunctors showing
how its structure has been used to derive presheaf model for the
pi-calculus for both early and late bisimulation as well as for other
variants and how, by considering `maps between models', this has cast
light on the formal relationships among such variants.
In doing so a theorem of limit/colimit coincidence is developed.
All this calls for a deeper study of presheaf categories as
generalised domains for non-deterministic computations. To this
purpose, we will describe the operation of taking presheaves (over a
basis of finitely presentable objects) as a monad construction on the
2-category of omega-accessible categories (the categorical analogue of
algebraic cpo's) for which the bicategory of profunctors will
constitute (in an appropriate sense) the Kleisli category. Thus they
can be regarded as playing the rôle of a powerdomain
construction, i.e., adding non-determinism to the computations
structure.
Time permitting we will address the issues in using these methods to
provide a semantics to Higher Order Process Calculi.
In the future we hope to be able to use this approach to more tightly
relate the theory of concurrency to a generalised theory of domains.
|