查看“︁直觉类型论”︁的源代码

'''直觉类型论'''（{{lang-en|Intuitionistic type theory}}），也可简称'''类型论'''，此外也有'''构造类型论'''或'''马汀-洛夫类型论'''称呼。是基于[[数学构造主义]]的[[函数式编程语言]]、[[逻辑]]和[[集合论]]。

直觉类型论由[[瑞典]][[数学家]]和[[哲学家]] [[佩尔·马丁-洛夫]]于1972年引入。此前马丁已经多次修改了他的提议，先是[[非直谓性]]的而后是直谓性的，先是[[外延]]的而后是[[内涵]]的类型论变体。直觉类型论基于的是[[命题]]和[[等价类]]的同一一个命题同一于它的证明的类型。这种同一通常叫做[[柯里-霍华德同构]]，它最初公式化了[[命题逻辑]]和[[简单类型λ演算]]。

类型论通过介入包含着值的[[依赖类型]]把这种同一扩展到[[谓词逻辑]]。[[类型论]]内在化了 [[鲁伊兹·布劳威尔]]、[[阿兰德·海廷]] 和 [[安德雷·柯爾莫哥洛夫]]提议的[[BHK释义|布劳威尔-海廷-柯尔莫哥洛夫释义]]的[[直觉逻辑]]释义。类型论的类型扮演了类似于集合在[[集合论]]的角色，但是在类型论中的函数总是可计算的。

==类型论的连结词==

在类型论的语境中，[[连结词]]是使用已给定的类型而构造类型的一种方式。类型论的基本连结词有:

===<math>\Pi</math>-类型=== 

<math>\Pi</math>-类型，也叫做依赖函数类型，一般化了普通的[[函数空间]]，建模其结果的类型可以随它们的输入而变化的函数，比如，对[[实数]]的 <math>n</math>-元组写为 <math>\mbox{Vec}({\mathbb R},n)</math>，则<math>\Pi n:{\mathbb N}.\mbox{Vec}({\mathbb R},n)</math> 表示对给定的[[自然数]]返回这个大小的实数元组的函数的类型。在值域类型实际上不依赖于输入的时候，普通函数空间作为特殊情况出现，比如 <math>\Pi n:{\mathbb N}.{\mathbb R}</math> 是从自然数到实数的函数的类型，它也写为 <math>{\mathbb N}\to{\mathbb R}</math>。使用 [[Curry-Howard同构]]，<math>\Pi</math>-类型还充当建模[[蕴涵]]和[[全称量化]]: 比如，具有类型 <math>\Pi m,n:{\mathbb N}.m+n = n+m</math> 的一个项，是对任何一对自然数的函数指派加法对这个数对是[[交换律|交换性]]的证明，并因此可以被当作加法对于所有自然数是交换性的一个证明。

===<math>\Sigma</math>-类型=== 

<math>\Sigma</math>-类型，也叫做依赖乘积类型，一般化了普通的[[笛卡尔积]]，建模第二个构件的类型依赖于第一个构件的有序对，比如类型 <math>\Sigma n:{\mathbb N}.\mbox{Vec}({\mathbb R},n)</math> 表示[[自然数]]和这个大小的[[实数]]的[[元组]]的有序对的类型，就是说，这个类型可以用来建模任意长度的序列(通常叫做列表)。在第二个构件的类型实际上不依赖于第一个构件的时候，常规的[[笛卡尔积]]类型作为特殊情况出现，比如 <math>\Sigma n:{\mathbb N}.{\mathbb R}</math> 是[[自然数]]和[[实数]]的有序对的类型，它也写为 <math>{\mathbb N}\times{\mathbb R}</math>。再次使用 [[Curry-Howard同构]]，<math>\Sigma</math>-类型也充当建模[[合取]]和[[存在量化]]。

===有限类型===

特别重要的是 <math>0</math> ([[空类型]])、<math>1</math> ([[单位类型]])和 <math>2</math> (布尔值或[[真值]])。再次用到 [[Curry-Howard同构]]，<math>0</math> 表示假而 <math>1</math> 表示真。

使用有限类型，我们可以定义[[否定]]为 <math>\neg A = A \to 0</math>，服从[[Curry-Howard同构]]，[[不相交并集]]也表示[[析取]]，它可以定义为 <math>A+B = \Sigma b:2.\mbox{if}\,b\,\mbox{then}\,A\,\mbox{else}\, B</math>。

===等式类型===

给定 <math>a,b : A</math>，则 <math>a = b</math> 是 <math>a</math> 等于 <math>b</math> 的等式证明。只有一个(规范的) <math>a = b</math> 的居留，并且这是自反性 <math>\mbox{refl} : \Pi a:A.a = a</math> 的证明。

===归纳类型===

归纳类型的基本例子是[[自然数]] <math>\mathbb N</math> 的类型，它是通过 <math>0 : {\mathbb N}</math> 和 <math>\mbox{succ} :{\mathbb N} \to {\mathbb N}</math> 生成的。[[Curry-Howard同构|命题为类型原理]]的一个重要应用是通过对用 <math>n:{\mathbb N}</math> 索引的给定类型 <math>P(n)</math> 的一个消除常量: <math>{\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)</math> 来把(依赖的)[[原始递归函数|原始递归]]和[[数学归纳法|归纳]]同一起来的。在一般的归纳类型中可以被定义为 W-类型，它是[[良基关系|良基的]]树的类型。

一类重要的归纳类型是像上面提及的向量 <math>\mbox{Vec}(A,n)</math> 的归纳类型家族，它们是归纳生成自构造子 <math>\mbox{vnil}:\mbox{Vec}(A,0)</math> 和 <math>\mbox{vcons}:A\to\Pi n:{\mathbb N}.\mbox{Vec}(A,n)\to\mbox{Vec}(A,\mbox{succ}(n))</math>。再次用到[[Curry-Howard同构]]，归纳类型家族对应于归纳定义的关系。

===全集===

全集的一个例子是 <math>U_0</math>，它是所有小类型的全集，它包含前面介绍的所有类型的名字。对于每个名字 <math>a:U_0</math> 我们关联上一个类型 <math>El(a)</math>，这是它的外延或意义。标准上是假定全集的一个直谓性等级: 对于每个自然数 <math>n:{\mathbb N}</math> 的 <math>U_n</math>，这里的全集 <math>U_{n+1}</math> 包含以前的全集的一个代码，就是说，我们通过 <math>El(u_n)=U_n</math> 而有 <math>u_n:U_{n+1}</math>。这个等级经常被假定为是累积性的，就是说来自 <math>U_n</math> 的代码被嵌入了 <math>U_{n+1}</math>。 

已经研究了更强的全集原理，比如超全集和 Mahlo 全集。在 1992 年 Huet 和 Coquand 介入了[[构造演算]]，它是带有非直谓性全集的类型论，从而把类型论同 [[Jean-Yves Girard|Girard]] 的[[系统F]] 合并起来了。这个扩展不被[[直觉主义]]者所普遍接受，因为它允许非直谓性的，就是循环的构造，这经常用经典推理来识别。

==类型论的形式化==

类型论通常表示为依赖的[[有类型 lambda 演算]]，使用判断:
* <math>\vdash \Gamma\, \mbox{Context}</math>，<math>\Gamma</math>类型假定的良好形成的上下文。
* <math>\Gamma\vdash \sigma\, \mbox{Type}</math>，<math>\sigma</math> 在上下文 <math>\Gamma</math> 中的良好形成的类型。
* <math>\Gamma\vdash t : \sigma</math>，<math>t</math> 是在上下文 <math>\Gamma</math> 中的类型<math>\sigma</math> 的良好形成的项。
* <math>\Gamma\vdash \sigma\equiv\tau</math>，<math>\sigma</math> 和 <math>\tau</math> 是在上下文 <math>\Gamma</math> 中的等于类型。
* <math>\Gamma\vdash t \equiv u: \sigma</math>，<math>t</math> 和 <math>u</math> 是在上下文 <math>\Gamma</math> 中的类型 <math>\sigma</math> 的相等项。
特别重要的是转换规则，它声称给定 <math>\Gamma\vdash t : \sigma</math> 和 <math>\Gamma\vdash \sigma\equiv\tau</math> 则 <math>\Gamma\vdash t : \tau</math>。

==外延和内涵==

一个基本区别是外延和内涵的类型论。在外延类型论中定义性(就是计算性)等式不区别于需要证明的命题性等式。作为结论类型检查成为[[不可判定性]]的。相反的，在内涵类型论中，[[类型检查]]是[[可判定性]]的，但是很多数学概念的表达是不标准的，因为缺乏外延推理。这是目前对这种折中是否是不可避免的和在内涵类型论中缺乏外延原理是一个特色还是一个缺陷的讨论的一个主题。

==类型论的实现==

类型论已经被用做很多证明助理的基础，比如 [[NuPRL]]、[[LEGO]]、[[Coq]] 和 [[Agda]]。最近，[[依赖类型]]也作为[[编程语言]]设计的特征，比如[[Dependent ML]] 和 [[Epigram]]。

==参见==
* [[直觉主义]]
* [[BHK释义]]
* [[经典逻辑]]
* [[中间逻辑]]
* [[线性逻辑]]
* [[构造性证明]]
* [[Curry-Howard对应]]
* [[可计算性逻辑]]
* [[博弈语义]]
* [[有类型 lambda 演算]]
* [[Curry-Howard同构]]
* [[直觉逻辑]]
* [[构造演算]]
* [[Per Martin-Löf]]
* [[类型论]]

==外部链接==

* Bengt Nordstr?m; Kent Petersson; Jan M. Smith (1990). ''Programming in Martin-L?f's Type Theory''. Oxford University Press. The book is out of print, but a free version can be picked up from  [http://www.cs.chalmers.se/Cs/Research/Logic/book/ here] {{Wayback|url=http://www.cs.chalmers.se/Cs/Research/Logic/book/ |date=20100212224415 }}.

* Thompson, Simon (1991). ''[http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming] {{Wayback|url=http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ |date=20210323203228 }}'' Addison-Wesley. ISBN 0-201-41667-0.

[[Category:类型论]]
[[Category:數理邏輯|Z]]