直觉类型论

直觉类型论（Intuitionistic type theory）、或构造类型论、或Martin-Löf 类型论、或就叫类型论是基于数学构造主义的函数式编程语言、逻辑和集合论。直觉类型论由瑞典数学家和哲学家 Per Martin-Löf 在1972年介入。 Martin-Löf 已经多次修改了它的提议；先是非直谓性的而后是直谓性的，先是外延的而后是内涵的类型论变体。直觉类型论基于的是命题和类型的同一: 一个命题同一于它的证明的类型。这种同一通常叫做Curry-Howard同构，它最初公式化了命题逻辑和简单类型 lambda 演算。类型论通过介入包含着值的依赖类型把这种同一扩展到谓词逻辑。类型论内在化了 Brouwer、Heyting 和 Kolmogorov 提议的叫做 BHK释义的直觉逻辑释义。类型论的类型扮演了类似于集合在集合论的角色，但是在类型论中的函数总是可计算的。在类型论的上下文中，连结词是可能使用已给定的类型而构造类型的一种方式。类型论的基本连结词有:Π {displaystyle Pi } -类型，也叫做依赖函数类型，一般化了普通的函数空间，建模其结果的类型可以随它们的输入而变化的函数，比如，对实数的 n {displaystyle n} -元组写为 Vec ( R , n ) {displaystyle {mbox{Vec}}({mathbb {R} },n)} ，则 Π n : N . Vec ( R , n ) {displaystyle Pi n:{mathbb {N} }.{mbox{Vec}}({mathbb {R} },n)} 表示对给定的自然数返回这个大小的实数元组的函数的类型。在值域类型实际上不依赖于输入的时候，普通函数空间作为特殊情况出现，比如 Π n : N . R {displaystyle Pi n:{mathbb {N} }.{mathbb {R} }} 是从自然数到实数的函数的类型，它也写为 N → R {displaystyle {mathbb {N} }to {mathbb {R} }} 。使用 Curry-Howard同构， Π {displaystyle Pi } -类型还充当建模蕴涵和全称量化: 比如，居留于 Π m , n : N . m + n = n + m {displaystyle Pi m,n:{mathbb {N} }.m+n=n+m} 的一个项，它对任何一对自然数的函数指派加法对这个数对是交换性的证明，并因此可以被当作加法对于所有自然数是交换性的一个证明。Σ {displaystyle Sigma } -类型，也叫做依赖乘积类型，一般化了普通的笛卡尔积，建模第二个构件的类型依赖于第一个构件的有序对，比如类型 Σ n : N . Vec ( R , n ) {displaystyle Sigma n:{mathbb {N} }.{mbox{Vec}}({mathbb {R} },n)} 表示自然数和这个大小的实数的元组的有序对的类型，就是说，这个类型可以用来建模任意长度的序列(通常叫做列表)。在第二个构件的类型实际上不依赖于第一个构件的时候，常规的笛卡尔积类型作为特殊情况出现，比如 Σ n : N . R {displaystyle Sigma n:{mathbb {N} }.{mathbb {R} }} 是自然数和实数的有序对的类型，它也写为 N × R {displaystyle {mathbb {N} }times {mathbb {R} }} 。再次使用 Curry-Howard同构， Σ {displaystyle Sigma } -类型也充当建模合取和存在量化。特别重要的是 0 {displaystyle 0} (空类型)、 1 {displaystyle 1} (单位类型)和 2 {displaystyle 2} (布尔值或真值)。再次用到 Curry-Howard同构， 0 {displaystyle 0} 表示假而 1 {displaystyle 1} 表示真。使用有限类型，我们可以定义否定为 ¬ A = A → 0 {displaystyle neg A=Ato 0} ，服从Curry-Howard同构，不相交并集也表示析取，它可以定义为 A + B = Σ b : 2. if b then A else B {displaystyle A+B=Sigma b:2.{mbox{if}},b,{mbox{then}},A,{mbox{else}},B} 。给定 a , b : A {displaystyle a,b:A} ，则 a = b {displaystyle a=b} 是 a {displaystyle a} 等于 b {displaystyle b} 的等式证明。只有一个(规范的) a = b {displaystyle a=b} 的居留，并且这是自反性 refl : Π a : A . a = a {displaystyle {mbox{refl}}:Pi a:A.a=a} 的证明。归纳类型的基本例子是自然数 N {displaystyle mathbb {N} } 的类型，它是通过 0 : N {displaystyle 0:{mathbb {N} }} 和 succ : N → N {displaystyle {mbox{succ}}:{mathbb {N} }to {mathbb {N} }} 生成的。命题为类型原理的一个重要应用是通过对用 n : N {displaystyle n:{mathbb {N} }} 索引的给定类型 P ( n ) {displaystyle P(n)} 的一个消除常量: N − elim : P ( 0 ) → ( Π n : N . P ( n ) → P ( succ ( n ) ) ) → Π n : N . P ( n ) {displaystyle {mathbb {N} }-{mbox{elim}}:P(0)to (Pi n:{mathbb {N} }.P(n)to P({mbox{succ}}(n)))to Pi n:{mathbb {N} }.P(n)} 来把(依赖的)原始递归和归纳同一起来的。在一般的归纳类型中可以被定义为 W-类型，它是良基的树的类型。一类重要的归纳类型是像上面提及的向量 Vec ( A , n ) {displaystyle {mbox{Vec}}(A,n)} 的归纳类型家族，它们是归纳生成自构造子 vnil : Vec ( A , 0 ) {displaystyle {mbox{vnil}}:{mbox{Vec}}(A,0)} 和 vcons : A → Π n : N . Vec ( A , n ) → Vec ( A , succ ( n ) ) {displaystyle {mbox{vcons}}:Ato Pi n:{mathbb {N} }.{mbox{Vec}}(A,n)to {mbox{Vec}}(A,{mbox{succ}}(n))} 。再次用到Curry-Howard同构，归纳类型家族对应于归纳定义的关系。全集的一个例子是 U 0 {displaystyle U_{0}} ，它是所有小类型的全集，它包含前面介绍的所有类型的名字。对于每个名字 a : U 0 {displaystyle a:U_{0}} 我们关联上一个类型 E l ( a ) {displaystyle El(a)} ，这是它的外延或意义。标准上是假定全集的一个直谓性等级: 对于每个自然数 n : N {displaystyle n:{mathbb {N} }} 的 U n {displaystyle U_{n}} ，这里的全集 U n + 1 {displaystyle U_{n+1}} 包含以前的全集的一个代码，就是说，我们通过 E l ( u n ) = U n {displaystyle El(u_{n})=U_{n}} 而有 u n : U n + 1 {displaystyle u_{n}:U_{n+1}} 。这个等级经常被假定为是累积性的，就是说来自 U n {displaystyle U_{n}} 的代码被嵌入了 U n + 1 {displaystyle U_{n+1}} 。已经研究了更强的全集原理，比如超全集和 Mahlo 全集。在 1992 年 Huet 和 Coquand 介入了构造演算，它是带有非直谓性全集的类型论，从而把类型论同 Girard 的系统F 合并起来了。这个扩展不被直觉主义者所普遍接受，因为它允许非直谓性的，就是循环的构造，这经常用经典推理来识别。类型论通常表示为依赖的有类型 lambda 演算，使用判断:特别重要的是转换规则，它声称给定 Γ ⊢ t : σ {displaystyle Gamma vdash t:sigma } 和 Γ ⊢ σ ≡ τ {displaystyle Gamma vdash sigma equiv tau } 则 Γ ⊢ t : τ {displaystyle Gamma vdash t:tau } 。一个基本区别是外延和内涵的类型论。在外延类型论中定义性(就是计算性)等式不区别于需要证明的命题性等式。作为结论类型检查成为不可判定性的。相反的，在内涵类型论中，类型检查是可判定性的，但是很多数学概念的表达是不标准的，因为缺乏外延推理。这是目前对这种折中是否是不可避免的和在内涵类型论中缺乏外延原理是一个特色还是一个缺陷的讨论的一个主题。类型论已经被用做很多证明助理的基础，比如 NuPRL、LEGO、Coq 和 Agda。最近，依赖类型也作为编程语言设计的特征，比如Dependent ML 和 Epigram。