纯类型系统

证明或反驳Barendregt-Geuvers-Klop猜想。(计算机科学中更多未解决的问题)在被称为证明理论和类型理论的数理逻辑分支中，纯类型系统（PTS），以前被称为广义类型系统（GTS），是一种类型化的lambda计算形式，它允许任意数量的排序和其中任何一个排序之间的依赖关系。这个框架可以被看作是Barendregt的lambdacube的泛化，在这个意义上，cube的所有角落都可以被表示为只有两种类型的PTS的实例。事实上，Barendregt(1991)在这个背景下构建了他的立方体。纯类型系统可能掩盖了类型和术语之间的区别，并折叠了类型层次，正如构造微积分的情况一样，但通常不是这样的，例如简单类型的lambda微积分只允许术语依赖于术语。纯类型系统是由StefanoBerardi（1988）和JanTerlouw（1989）独立提出的。Barendregt在他后来的论文中详细地讨论了它们。在他的博士论文中，Berardi定义了一个类似于lambdacube的构造逻辑的立方体（这些规范是不依赖的）。这个立方体的一个修改后来被Geuvers称为L立方体，他在他的博士论文中把Curry-Howard对应关系扩展到这个环境中。基于这些想法，Barthe和其他人通过增加一个双重否定算子定义了经典纯类型系统（CPTS）。同样，在1998年，TijnBorghuis引入了模态纯类型系统（MPTS）。Roorda讨论了纯类型系统在函数式编程中的应用；而Roorda和Jeuring提出了一种基于纯类型系统的编程语言。来自lambdacube的系统都是已知的强规范化的。

一般来说，纯类型系统不需要是这样的，例如吉拉德悖论中的系统U就不是。(粗略地说，Girard发现了纯类型系统，在这个系统中，人们可以表达类型构成类型的句子)。此外，所有已知的不是强规范化的纯类型系统的例子甚至不是（弱）规范化的：它们包含不具有规范形式的表达式，就像无类型的λ微积分。这是否总是如此，即一个（弱）规范化的PTS是否总是具有强规范化属性，这是这个领域的一个主要的开放问题。这被称为Barendregt-Geuvers-Klop猜想（以HenkBarendregt,HermanGeuvers和JanWillemKlop命名）。

一个纯类型系统是由一个三联体定义的{displaystyle{frac{GammavdashA:BquadB=_{beta}B'quadGammavdashB':s}{GammavdashA:B'}quad{text{（转换）}}。

以下编程语言有纯类型系统。SAGEYarrowHenk2000