Ordered linear logic and applications
Ordered linear logic and applications
复制标题
有序线性逻辑及其应用
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
F. Pfenning
中科院分区：
文献类型：
--
作者：
Jeff Polakow;F. Pfenning
本文介绍了一种新的逻辑系统--有序线性逻辑，它将推理与非限制性、线性和有序假设相结合。该逻辑保守地扩展了（直觉主义）线性逻辑，其中包含无限制和线性假设，并有有序假设的概念。有序假设必须只使用一次，服从于假设它们的顺序（即，它们的顺序在推导过程中不能改变）。这种排序约束允许简单数据结构（如堆栈和队列）的逻辑表示。我们从假言判断的基本概念出发，构造马丁-洛夫风格的有序线性逻辑。然后，我们通过构建一个微积分表示和证明切消除的系统的系统的规范化。
在介绍了基本的逻辑系统之后，我们展示了如何从线性逻辑扩展技术来实现有序逻辑编程语言Olli和有序逻辑框架OLF。Olli和OLF允许对涉及简单数据结构的情况进行非常优雅的编码，这些情况在没有有序假设的情况下是不可能的。示例Olli程序包括到deBruijn符号和来自deBruijn符号的转换器，以及广度优先图遍历程序。本文主要介绍的OLF应用是CPS变换的一些语法性质的分析。
This thesis introduces a, new logical system, ordered linear logic, which combines reasoning with unrestricted, linear, and ordered hypotheses. The logic conservatively extends (intuitionistic) linear logic, which contains both unrestricted and linear hypotheses, with a notion of ordered hypotheses. Ordered hypotheses must be used exactly once, subject to the order in which they were assumed (i.e., their order cannot be changed during the course of a derivation). This ordering constraint allows for logical representations of simple data structures such as stacks and queues. We construct ordered linear logic in the style of Martin-Lof from the basic notion of a hypothetical judgement. We then show normalization for the system by constructing a sequent calculus presentation and proving cut-elimination of the sequent system.
After introducing the basic logical system, we show how to extend techniques from linear logic to achieve an ordered logic programming language, Olli, and an ordered logical framework, OLF. Olli and OLF allow quite elegant encodings of situations involving simple data structures which are not possible without ordered hypotheses. Example Olli programs include a translator to and from deBruijn notation, and a breadth-first graph traversal program. The major OLF application presented in this dissertation is an analysis of some syntactic properties of the CPS transform.