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.