A Logical Study of Interactive Computational Problems Understood as Games

本研究的目标是为交互式计算问题阐述一种优雅而全面的规范语言和语义，并探索相应的逻辑，即用该语言表达的交互式可计算性的有效原则。这样的逻辑为我们提供了一个强大的工具，系统地研究计算任务，并自动生成解决方案，从已知的老问题的新问题。其他应用包括基于这种逻辑知识和面向资源的自动推理系统的可能性。交互式计算问题的直观概念被形式化为两个玩家之间的游戏：机器和环境（用户）。游戏的移动代表这些代理的动作/选择，位置代表交互过程中出现的状态/情况。一个游戏被认为是可赢的（因此相应的问题是可解的），如果有一个计算机程序在任何可能的环境中赢得了它。 语言的逻辑交互式计算问题的研究者建议的是一个非不相交的联盟的语言的经典，直觉和线性逻辑，与逻辑运算符解释为某些，-最基本和自然的，-操作的游戏。公式的有效性被理解为它的原子的每个游戏/问题解释的可赢性。对语言的经典片段的可赢性的限制结果等同于经典的真概念，这使得经典逻辑成为交互计算问题逻辑的自然句法片段。直觉主义逻辑和线性逻辑（的一个版本）的情况也是如此。这样，交互式计算问题的逻辑就可以在一个通用语义的框架内，将经典逻辑、直觉逻辑和线性逻辑与它们看似无关甚至对立的哲学统一起来。验证这一猜想，沿着找到一个公理化的逻辑交互计算问题，是本研究的主要技术目标。

The goal of this research is to elaborate an elegant and comprehensive specification language and semantics for interactive computational problems and explore the corresponding logic, --- the set of valid principles of interactive computability expressible in that language. Such a logic provides us with a powerful tool for systematically studying computational tasks and automatically generating solutions to new problems from known solutions to old problems. Other applications include the possibility to base on this logic knowledge- and resource-oriented automatic reasoning systems. The intuitive notion of interactive computational problem is formalized as a game between two players: the machine and the environment (user). Moves of the game represent actions/choices by these agents, and positions represent states/situations that emerge in the course of interaction. A game is considered winnable (and hence the corresponding problem solvable), if there is a computer program that wins it against any possible environment. The language of the logic of interactive computational problems suggested by the investigator is a non-disjoint union of the languages of classical, intuitionistic and linear logics, with logical operators interpreted as certain, --- most basic and natural, --- operations on games. Validity of a formula is understood as winnability for every game/problem interpretation of its atoms. The restriction of winnability to the classical fragment of the language turns out to be equivalent to the classical concept of truth, which makes classical logic a natural syntactic fragment of the logic of interactive computational problems. The same is conjectured to be the case for the intuitionistic logic and (a version of) linear logic. This way, the logic of interactive computational problems can unify, within the framework of one general semantics, the classical, intuitionistic and linear logics, with their seemingly unrelated or even antagonistic philosophies. Verifying this conjecture, along with finding an axiomatization for the logic of interactive computational problems, is among the main technical objectives of this research.