Computer Laboratory

Motivation and High-level Background

For a technical introduction to ecsym and its goals, see the project synopsis. Below, we give a high-level outline of the project and its goals.

The reader is also urged to consult the materials available at http://www.cl.cam.ac.uk/~gw104/erc2010.html for a more full picture of the background to the project.

Understanding Programs

Increasingly, the world around us is filled with computing agents --- computers, or computer like processes, that are processing information and interacting with their environment according to a program. Not only are we building ever more complex systems ourselves, we are increasingly learning to model the natural world in terms of networks of interacting systems, for example in chemical signalling networks inside biological cells and inter-cellular co-ordination.

In order to understand this world, we need to be able to reason about the programs that drive it: we need mathematical representations and analytical techniques that allow us to describe processes in terms of what they are rather than how they are implemented.

This project of assigning meanings to programs is not a new one, and is known as program semantics.

Program semantics

The question of how to model programs is not a new one. There are three current techniques, each with their own advantages and disadvantages:

  • Denotational semantics and domain theory. This has provided a global mathematical setting for sequential computation, and thereby placed programming languages in connection with each other and with the mathematical worlds of algebra, topology and logic.
  • Structural operational semantics. This method is based on syntax-directed rule-based inductive definitions to specify the evalua- tion and execution of programs. It is easy to use and flexible, but low-level and syntax-oriented.
  • Causal models. These include Petri nets and event structures which represent systems in terms of the events associated with their behaviour together with relations expressing the local dependencies and conflicts between events.

Each of these approaches, however, presents difficulty when we consider the full range of problems which we currently wish to address:

  • Denotational semantics:It has become clear that many aspects of computation do not fit within the traditional framework of denotational semantics and domain theory. It has abstracted away from operational concerns too early, and does not adequately deal with the interactivity of computer programs.
  • Operational semantics: Operational semantics is often too low-level to support the reasoning we wish to perform. It has an underdeveloped mathematical theory, which does not support many algebraic operations for program manipulation. It generally represents parallelism through a global nondeterministic interleaving of actions, which obscures the crucial local causal dependencies of the underlying events.
  • Causal models lack a comprehensive theory or even a methodology with which systematically to provide semantics to a broad range of programming languages and systems. The difficulties in establishing a comprehensive theory for present causal models are partly due to their overly-concrete nature, and to the conceptual puzzle that, historically, they are used both to represent data types as well as the process of computation—a mismatch with traditional denotational semantics.

There is therefore a crying need for a new approach to program semantics that:

  • Extends the methodology of denotational semantics and domain theory to the challenges in analyzing computation today
  • Maintains clean algebraic structure and abstraction alongside the operational nature of computation
  • Provides a comprehensive theory of causal models

ecsym's approach

By bringing to bear new developments in the algebraic treatment of the semantics of concurrency, the project aims to meet the crying need for a new unified approach to semantics that combines the advantages of the three techniques described above.

Broadly, ecsym may be understood to be bringing operational meaning to the denotation of processes, by enriching that denotation --- which, traditionally, described what was computed --- with information about how those values were computed.

The name ecsym comes from the crucial role that symmetry seems to play in allowing us to transcend the sometimes too-concrete representations of event-based program operational semantics. Applying this technique allows us to recover the good algebraic properties of denotational semantics, while keeping touch with the causality and events involved in the computation of a function.