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.