Logic of Interaction and Information Flow

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

Our current understanding of computation has widened enormously beyond the original ``closed world'' picture of numerical calculation in isolation from the environment. In the age of the Internet and the Web, and now of pervasive and ubiquitous computing, it has become clear that interaction and information flow between multiple agents are essential features of computation. The standard unit of description or design, whether at a micro-scale of procedure call-return interfaces or hardware components, or a macro-scale of software agents on the Web, becomes a process or agent, the essence of whose behaviour ishow it interacts with its environment across some defined interface.These developments have required the introduction of novel mathematical models of interactive computation. The traditional view whereby a program is seen as computing a function or relation from inputs to outputs is no longer sufficient: what function does the Internet compute?One of the compelling ideas which has taken root is toconceptualize the interaction between the System and the Environment as a two-person game. A program specifying how the System should behave in the face of all possible actions by the Environment is then a strategy for the player corresponding to the System.These ideas have led to the development of Game semantics, which both provides powerful tools for analyzing many different forms of computation, and leads to new perspectives on logic itself.For example, consider the ``copy-cat strategy'', whereby we can beat a Grand-Master at chess, by the power of logic. The idea is that we play against two Grand-Masters on two boards, one as White and one as Black (corresponding to ``A or not A''). By simply copying moves back and forth, we end up playing one grand-master off against the other --- and hence do as well as our opponents! This is a kind of ``dynamic tautology'': we achieve a strong logical effect by a simple copying process. Note only do the considerations arising from this and related ideas lead to powerful applications in computation and logic, striking connections are also emerging to geometric ideas, related to knots and braids, and to information flow in entangled quantum systems.Thus one aim of the proposal is build a unified theory of interaction and information flow covering all these examples and more. Another to is to connect this ``dynamic'' or ``intrinsic'' approach to more traditional approaches to logics of interaction, and indeed to find useful ways of combining them.