Proof as Computation

计算方面的证明系统一般可分为两种。在广义的函数式编程中，计算被看作是与证明约简相对应的项约简（即切消过程）。另一方面，在广义的逻辑规划中，计算在某些形式理论中是由目标导向的、无切割的证明搜索来表示的。逻辑编程范式的这种特征是基于Miller和Scedrov早期的联合工作。提出的研究旨在通过交互协议理解线性逻辑产生的证明系统，它们的计算和描述能力以及它们的语义。博弈论概念，如交互协议，应该有助于理解线性逻辑的语义和计算表达的“精细结构”。在逻辑编程设置中，这样的证明系统为处理上下文和资源之间的通信提供了原语。基于这种证明系统风格的规范语言可以用于声明性地、自然地指定计算的副作用、通信和延续等方面。＊＊＊

9400907 Miller Computational aspects of proofs systems may be generally divided into two kinds. In what may be broadly called functional programming, computation is seen as term reduction corresponding to proof reduction (i.e., to the process of cut elimination). On the other hand, in what may be broadly called logic programming, computation is expressed by goal directed, cut free proof search in certain formal theories. This characterization of the logic programming paradigm is based on Miller's and Scedrov's earlier joint work. The proposed research is aimed at understanding the proof systems arising from linear logic, their computational and descriptive powers, and their semantics by means of interactive protocols. Game-theoretic notions, such as interactive protocols, should contribute to the understanding of "fine structure" of both semantics and computational expressiveness of linear logic. In the logic programming setting, such proof systems provide primitives for handling contexts and communications among resources. A proposed specification language based on this style of proof system can be used to declaratively and naturally specify such aspects of computation as side-effects, communications, and continuations. ***