关于LF类型理论中的等价性和规范形式
摘要：决定性的定义相等和将术语转化为规范形式在类型理论逻辑框架的元理论中起着核心作用。绝大多数关于定义相等的研究都基于一种可决、强正则的减少观念。Coquand提出了一种不同的方法，直接验证基于术语形状的实际等价算法的正确性。这两种方法似乎都不适用于具有单元类型或子类型的更丰富的语言，而且都没有直接解决转化为规范性的问题。 在本文中，我们提出了一种新的面向类型的等价算法，用于克服之前方法的弱点，并且可以适用于更丰富的语言，并产生一个足以满足逻辑系统的充分编码的新规范形式的概念。该算法通过类似Coquand建议的基于Kripke风格的逻辑关系论证来证明其是完备的。关键是，算法本身和逻辑关系都仅依赖于类型的形状，而忽略对术语的依赖性。
作者：Robert Harper and Frank Pfenning
论文ID：cs/0110028
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23