Logic of Interaction and Information Flow

交互逻辑与信息流

• 批准号: EP/F067607/1
• 负责人: Samson Abramsky
• 金额: $ 38.98万
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2008
• 资助国家: 英国
• 起止时间: 2008 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FF067607%2F1
• 关键词: Logic; Interaction; 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.

我们目前对计算的理解已经大大超出了原始的“封闭世界”，即与环境隔离的数值计算。在互联网和Web的时代，以及现在的普适和无处不在的计算，它已经变得很清楚，多个代理之间的交互和信息流是计算的基本特征。描述或设计的标准单元，无论是在过程调用返回接口或硬件组件的微观尺度上，还是在Web上的软件代理的宏观尺度上，都成为一个过程或代理，其行为的本质表明它通过一些定义的接口与环境进行交互。传统的观点认为，程序被看作是计算一个函数或从输入到输出的关系，这已经不足够了：互联网计算什么函数？其中一个引人注目的想法已经扎根是将系统和环境之间的相互作用概念化为两个人的游戏。指定系统在面对环境的所有可能行为时应该如何表现的程序是与系统相对应的玩家的策略。这些想法导致了游戏语义的发展，它既为分析许多不同形式的计算提供了强大的工具，也为逻辑本身带来了新的视角。例如，考虑“复制猫策略”，凭借逻辑的力量，我们可以在国际象棋上击败大师。我们的想法是，我们对两个大师在两个板，一个作为白色和一个作为黑色（对应于"A或不A“）。通过简单地来回复制动作，我们最终让一位大师与另一位大师竞争-因此我们做得和对手一样好！这是一种“动态重言式”：我们通过一个简单的复制过程来达到一种强有力的逻辑效果。值得注意的是，由此产生的考虑和相关的想法导致了计算和逻辑中的强大应用，与几何思想的惊人联系也正在出现，与结和辫子有关，以及与纠缠量子系统中的信息流有关。因此，该提案的目的之一是建立一个统一的相互作用和信息流理论，涵盖所有这些例子和更多。另一个目标是将这种"动态“或"内在”方法与更传统的交互逻辑方法联系起来，并找到将它们结合起来的有用方法。

项目成果

Full abstraction for Reduced ML

• DOI: 10.1016/j.apal.2013.05.007
• 发表时间: 2009-03
• 作者: A. Murawski;N. Tzevelekos

Block structure vs scope extrusion: between innocence and omniscience

块结构与范围挤压：天真与全知之间

• DOI: 10.2168/lmcs-12(3:3)2016
• 发表时间: 2017
• 期刊: Logical Methods in Computer Science
• 影响因子: 0.6
• 作者: Murawski A

Foundations of Software Science and Computational Structures

软件科学和计算结构基础

• DOI: 10.1007/978-3-642-19805-2_3
• 发表时间: 2011
• 作者: Levy P

From Lawvere to Brandenburger-Keisler: interactive forms of diagonalization and self-reference

从劳维尔到勃兰登堡-凯斯勒：对角化和自我参照的互动形式

• DOI: 10.48550/arxiv.1006.0992
• 发表时间: 2010
• 作者: Abramsky S

Fresh-register automata

• DOI: 10.1145/1926385.1926420
• 发表时间: 2011-01
• 作者: N. Tzevelekos