类型理论

在数学、逻辑学和计算机科学中，类型理论是对特定类型系统的正式表述，一般来说，类型理论是对类型系统的学术研究。一些类型理论作为集合理论的替代品，作为数学的基础。

两个被提议作为基础的有影响力的类型理论是AlonzoChurch的类型化λ-微积分和PerMartin-Löf的直觉类型理论。大多数计算机化的证明书写系统都使用类型理论作为其基础。一个常见的是ThierryCoquand的归纳构造微积分（CalculusofInductiveConstructions）。

类型理论是为了避免在基于天真的集合论和形式逻辑的数学基础上出现悖论而创建的。罗素悖论是由伯特兰-罗素发现的，它的存在是因为一个集合可以用所有可能的集合来定义，其中包括它自己。1902年至1908年期间，伯特兰-罗素提出了各种类型的理论来解决这个问题。到了1908年，罗素得出了一个夯实的类型理论，以及一个可还原性公理，这两者在怀特海和罗素的《数学原理》中都有突出的表现，在1910年至1913年期间出版。这个系统避免了罗素的悖论，它建立了一个类型的层次结构，然后把每个具体的数学实体分配给一个类型。

一个给定类型的实体完全由该类型的子类型建立，从而防止一个实体被定义为使用其本身。罗素的类型理论排除了一个集合是自身成员的可能性。

类型并不总是在逻辑中使用。还有其他技术来避免罗素的悖论。当与一个特定的逻辑，即AlonzoChurch的lambdacalculus一起使用时，类型确实得到了支持。

最著名的早期例子是丘奇的简单类型的λ微积分。Church的类型理论帮助形式化系统避免了困扰最初的无类型λ微积分的Kleene-Rosser悖论。Church证明了它可以作为数学的基础，它被称为高阶逻辑。现在，类型理论这个短语一般指的是围绕λ微积分的类型系统。

一个有影响力的系统是PerMartin-Löf的直觉类型理论，它被提议作为构造数学的基础。另一个是ThierryCoquand的构造微积分，它被Coq、Lean和其他证明助手（计算机化的证明书写程序）作为基础。

类型理论是一个活跃的研究领域，正如同构类型理论所证明的那样。

有很多类型理论，这使得我们很难产生一个全面的分类法；本文并不是一个详尽的分类法。

下面是对那些不熟悉类型理论的人的介绍，包括一些主要的方法。

在类型理论中，每个术语都有一个类型。一个术语和它的类型通常被写成术语：类型。

在类型理论中，一个常见的类型是自然数，通常写成或nat。另一个是布尔逻辑值。

因此，一些非常简单的术语及其类型是。0+0:nat2+3:nat1+(1+(1+0)):nat术语也可以包含变量。

变量总是有一个类型。因此，假设x和y是nat类型的变量，以下也是有效的术语。x:natx+2:natx+(x+y):nat除了nat和bool，还有更多类型。我们已经看到了术语add，它不是一个nat，而是一个函数，当应用于两个nat时，计算出一个nat。

add的类型将在后面介绍。首先，我们需要描述计算到。计算类型理论有一个内置的计算符号。下面的术语都是不同的。1+4:nat3+2:nat0+5:nat，但它们都计算到了5:nat这个术语。

在类型理论中，我们用reduction和reduce来指代计算。