On equivalence and canonical forms in the LF type theory
On equivalence and canonical forms in the LF type theory
复制标题
DOI：
10.1145/1042038.1042041
复制
发表时间：
2001-10
期刊：
影响因子：
--
通讯作者：
R. Harper;F. Pfenning
中科院分区：
文献类型：
--
作者：
R. Harper;F. Pfenning
定义平等和术语转化为规范形式的可决定性在类型理论逻辑框架的元理论中起着核心作用。大多数定义平等的研究都是基于汇合的，强烈正常的减少概念。 Coquand考虑了一种不同的方法，直接证明了基于术语形状的实际等价算法的正确性。这两种方法似乎都可以很好地扩展到更丰富的语言，例如单位类型或子类型，也没有提供适合证明编码适当性的规范形式的概念。在本文中，我们提出了一种新的，类型定向的等价算法LF类型理论克服了先前方法的弱点。该算法是实用的，可以扩展到更丰富的语言，并产生一种新的概念的规范形式，足以足以对逻辑系统的足够编码。该算法由Kripke风格的逻辑关系参数与Coquand建议的参数相似。至关重要的是，算法本身和逻辑关系都仅依赖于类型的形状，而忽略了对术语的依赖性。
Decidability of definitional equality and conversion of terms into canonical form play a central role in the meta-theory of a type-theoretic logical framework. Most studies of definitional equality are based on a confluent, strongly normalizing notion of reduction. Coquand has considered a different approach, directly proving the correctness of a practical equivalance algorithm based on the shape of terms. Neither approach appears to scale well to richer languages with, for example, unit types or subtyping, and neither provides a notion of canonical form suitable for proving adequacy of encodings.In this article, we present a new, type-directed equivalence algorithm for the LF type theory that overcomes the weaknesses of previous approaches. The algorithm is practical, scales to richer languages, and yields a new notion of canonical form sufficient for adequate encodings of logical systems. The algorithm is proved complete by a Kripke-style logical relations argument similar to that suggested by Coquand. Crucially, both the algorithm itself and the logical relations rely only on the shapes of types, ignoring dependencies on terms.