Semantics of Nondeterminism: Functions, Strategies and Bisimulation

点击翻译按钮获取中文摘要

A key question in the theory of programming is: when are two programs equivalent? The answer will depend on what we think a program means. For example, we can think of a program as a function: the user gives all the required input, and then the computer behaves accordingly. Or we can think of it as a strategy for a game between the computer and the user: the computer gives some information, the user responds, the computer gives some more information, the user responds, and so on. These viewpoints have been extremely fruitful in recent years.To reason about a computer system, it is often necessary to idealize it as nondeterministic, i.e.\ possessing a range of possible behaviours. The factors that determine its actual behaviour are too low-level and complex to consider explicitly. But this apparently simple idea has ramifications for the theory of programming language semantics that are not well understood. They centre on the same questions: when are two programs equivalent, and what do programs mean? Previous research has used mathematical structures known from the theory of deterministic programs. But these have limited applicability to nondeterministic programs, and lead to somewhat awkward notions of equivalence. This research will proceed in the opposite direction: begin with certain computationally natural notions of equivalence, and investigate what structures they lead to. In some cases (thinking of programs as strategies), these are likely to be structures that we already know, but, by proceeding in this way, we aim to relate them more closely to the way programs actually behave.In other cases (thinking of programs as functions), completely new structures will be required. Some mysterious theorems have been proved that show that, in a sense, all programs (of a certain kind) share some behaviour---yet they do not tell us what this behaviour is. We will therefore undertake a careful examination of programs' behaviour to solve this mystery, and thereby obtain the required structures.