Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Logic and Semantics Seminar
10th October, 1997: Luca Cattani
Computer Laboratory > Research > TSG > Logic and Semantics Seminar > 10th October, 1997: Luca Cattani

Speaker: Luca Cattani
Title: Presheaf Models over Recursively Defined Path Categories
Time: 10th October, 1997, 14:00
Abstract:

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.