Proof as Computation

证明作为计算

• 批准号: 9400907
• 负责人: Dale Miller
• 金额: --
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1994
• 资助国家: 美国
• 起止时间: 1994-09-15 至 1997-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9400907&HistoricalAwards=false
• 关键词: Proof; Computation

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. ***

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