关于LF类型论中的等价性和标准型
On Equivalence and Canonical Forms in the LF Type Theory
摘要：
定义相等的可判定性和项到规范形式的转换在类型论逻辑框架的元理论中起着核心作用。大多数定义平等的研究是基于一个融合的，强规范化的减少的概念。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 unit types or subtyping, and neither directly addresses the problem of conversion to canonical. In this paper 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
