Classical domain theory and denotational semantics, started by
Strachey and Scott, has been quite inspirational in suggesting
programming languages, their types and ways to understand them. They
have played a much lesser role in research in
interactive/concurrent/distributed computation. One reason perhaps is
that classical domain theory has not scaled up to the more intricate
models we find used in concurrency.
The course will move towards a path-based domain theory for
interacting processes, one aim being a general theory of bisimulation,
also for higher-order process languages. This mini-course, structured
as a series of lectures, will explain the origins of this work and the
ideas and mathematics on which it rests.
The first lecture should be very accessible and give a gentle
introduction to the advantages of viewing models for concurrency as
categories, in which the arrows are forms of simulation. It will show
how many operations of process algebra arise as universal
constructions in a category and introduce a general definition of
bisimulation based on ``open maps''. The lecture will be mainly based
on the familiar model of labelled transition systems, but will
indicate how the ideas are equally applicable to other models such as
event structures and Petri nets, and how relations between different
models are often expressed as adjunctions.
The following lectures will introduce and motivate a broader space of
models of concurrent computation, leading to a form of domain theory
for concurrency, in which nondeterministic processes are represented
by presheaves; the role of domain will be replaced by that of presheaf
category. There are several ways to introduce presheaves, but this
course will emphasise the guiding intuition that presheaves are a form
of transition system which allow computation paths to have a variety
of forms. Bisimulation between presheaves is again obtained from open
maps. Here a useful theorem is that colimit-preserving functors
between presheaf categories preserve open maps, and so
bisimulation. Its proof will be presented, helped some of the way by
the view of presheaves as transition systems.
Finally, I hope to give an idea of the languages for concurrency and
the concepts of linearity and nonlinearity the mathematics suggests.
The prior PPS seminar on April 11 should help in giving a general
overview.
References:
The relevant mathematics can be found in: Mario Ca'ccamo and Glynn
Winskel. Lecture Notes on Category Theory. Inspired by a Mathematics
Part III course of Martin Hyland. See http://www.brics.dk/~mcaccamo.
An introduction to open maps in: Andre' Joyal, Mogens Nielsen, and
Glynn Winskel. Bisimulation from Open Maps. May 1994. 42 pp. Appears
in LICS '93 special issue of Information and Computation,
127(2):164-185, June 1986. An early version is obtainable from:
http://www.brics.dk/RS/94/Ref/BRICS-RS-94-Ref/BRICS-RS-94-Ref.html.
A discussion of different models for concurrency in: Glynn Winskel and
Mogens Nielsen. Models for Concurrency. May 1994. 144 pp. Appears as a
chapter in the Handbook of Logic and the Foundations of Computer
Science, vol. 4, pages 1-148, Oxford University Press, 1995.
First ideas on the suggested languages in: Glynn Winskel. A linear
metalanguage for concurrency. Invited lecture in proc. AMAST'98,
Brazil, Springer Lecture Notes in CS, vol. 1548, 1999. Obtainable
from:
http://www.brics.dk/RS/98/Ref/BRICS-RS-98-Ref/BRICS-RS-98-Ref.html.