直覺類型論

直覺類型論（英語：Intuitionistic type theory），也可簡稱類型論，此外也有構造類型論或馬汀-洛夫類型論稱呼。是基於數學構造主義的函數式程式語言、邏輯和集合論。

直覺類型論由瑞典數學家和哲學家佩爾·馬丁-洛夫於1972年引入。此前馬丁已經多次修改了他的提議，先是非直謂性的而後是直謂性的，先是外延的而後是內涵的類型論變體。直覺類型論基於的是命題和等價類的同一一個命題同一於它的證明的類型。這種同一通常叫做柯里-霍華德同構，它最初公式化了命題邏輯和簡單類型λ演算。

類型論通過介入包含着值的依賴類型把這種同一擴展到謂詞邏輯。類型論內在化了魯伊茲·布勞威爾、阿蘭德·海廷和安德雷·柯爾莫哥洛夫提議的布勞威爾-海廷-柯爾莫哥洛夫釋義的直覺邏輯釋義。類型論的類型扮演了類似於集合在集合論的角色，但是在類型論中的函數總是可計算的。

類型論的連結詞[編輯]

在類型論的語境中，連結詞是使用已給定的類型而構造類型的一種方式。類型論的基本連結詞有:

$\Pi$ -類型[編輯]

$\Pi$ -類型，也叫做依賴函數類型，一般化了普通的函數空間，建模其結果的類型可以隨它們的輸入而變化的函數，比如，對實數的 $n$ -元組寫為 ${\mbox{Vec}}({\mathbb {R} },n)$ ，則 $\Pi n:{\mathbb {N} }.{\mbox{Vec}}({\mathbb {R} },n)$ 表示對給定的自然數返回這個大小的實數元組的函數的類型。在值域類型實際上不依賴於輸入的時候，普通函數空間作為特殊情況出現，比如 $\Pi n:{\mathbb {N} }.{\mathbb {R} }$ 是從自然數到實數的函數的類型，它也寫為 ${\mathbb {N} }\to {\mathbb {R} }$ 。使用 Curry-Howard同構， $\Pi$ -類型還充當建模蘊涵和全稱量化: 比如，具有類型 $\Pi m,n:{\mathbb {N} }.m+n=n+m$ 的一個項，是對任何一對自然數的函數指派加法對這個數對是交換性的證明，並因此可以被當作加法對於所有自然數是交換性的一個證明。

$\Sigma$ -類型[編輯]

$\Sigma$ -類型，也叫做依賴乘積類型，一般化了普通的笛卡爾積，建模第二個構件的類型依賴於第一個構件的有序對，比如類型 $\Sigma n:{\mathbb {N} }.{\mbox{Vec}}({\mathbb {R} },n)$ 表示自然數和這個大小的實數的元組的有序對的類型，就是說，這個類型可以用來建模任意長度的序列(通常叫做列表)。在第二個構件的類型實際上不依賴於第一個構件的時候，常規的笛卡爾積類型作為特殊情況出現，比如 $\Sigma n:{\mathbb {N} }.{\mathbb {R} }$ 是自然數和實數的有序對的類型，它也寫為 ${\mathbb {N} }\times {\mathbb {R} }$ 。再次使用 Curry-Howard同構， $\Sigma$ -類型也充當建模合取和存在量化。

有限類型[編輯]

特別重要的是 $0$ (空類型)、 $1$ (單位類型)和 $2$ (布爾值或真值)。再次用到 Curry-Howard同構， $0$ 表示假而 $1$ 表示真。

使用有限類型，我們可以定義否定為 $\neg A=A\to 0$ ，服從Curry-Howard同構，不相交併集也表示析取，它可以定義為 $A+B=\Sigma b:2.{\mbox{if}}\,b\,{\mbox{then}}\,A\,{\mbox{else}}\,B$ 。

等式類型[編輯]

給定 $a,b:A$ ，則 $a=b$ 是 $a$ 等於 $b$ 的等式證明。只有一個(規範的) $a=b$ 的居留，並且這是自反性 ${\mbox{refl}}:\Pi a:A.a=a$ 的證明。

歸納類型[編輯]

歸納類型的基本例子是自然數 $\mathbb {N}$ 的類型，它是通過 $0:{\mathbb {N} }$ 和 ${\mbox{succ}}:{\mathbb {N} }\to {\mathbb {N} }$ 生成的。命題為類型原理的一個重要應用是通過對用 $n:{\mathbb {N} }$ 索引的給定類型 $P(n)$ 的一個消除常量: ${\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-類型，它是良基的樹的類型。

一類重要的歸納類型是像上面提及的向量 ${\mbox{Vec}}(A,n)$ 的歸納類型家族，它們是歸納生成自構造子 ${\mbox{vnil}}:{\mbox{Vec}}(A,0)$ 和 ${\mbox{vcons}}:A\to \Pi n:{\mathbb {N} }.{\mbox{Vec}}(A,n)\to {\mbox{Vec}}(A,{\mbox{succ}}(n))$ 。再次用到Curry-Howard同構，歸納類型家族對應於歸納定義的關係。

全集[編輯]

全集的一個例子是 $U_{0}$ ，它是所有小類型的全集，它包含前面介紹的所有類型的名字。對於每個名字 $a:U_{0}$ 我們關聯上一個類型 $El(a)$ ，這是它的外延或意義。標準上是假定全集的一個直謂性等級: 對於每個自然數 $n:{\mathbb {N} }$ 的 $U_{n}$ ，這裏的全集 $U_{n+1}$ 包含以前的全集的一個代碼，就是說，我們通過 $El(u_{n})=U_{n}$ 而有 $u_{n}:U_{n+1}$ 。這個等級經常被假定為是累積性的，就是說來自 $U_{n}$ 的代碼被嵌入了 $U_{n+1}$ 。

已經研究了更強的全集原理，比如超全集和 Mahlo 全集。在 1992 年 Huet 和 Coquand 介入了構造演算，它是帶有非直謂性全集的類型論，從而把類型論同 Girard 的系統F 合併起來了。這個擴展不被直覺主義者所普遍接受，因為它允許非直謂性的，就是循環的構造，這經常用經典推理來識別。

類型論的形式化[編輯]

類型論通常表示為依賴的有類型 lambda 演算，使用判斷:

$\vdash \Gamma \,{\mbox{Context}}$ ， $\Gamma$ 類型假定的良好形成的上下文。
$\Gamma \vdash \sigma \,{\mbox{Type}}$ ， $\sigma$ 在上下文 $\Gamma$ 中的良好形成的類型。
$\Gamma \vdash t:\sigma$ ， $t$ 是在上下文 $\Gamma$ 中的類型 $\sigma$ 的良好形成的項。
$\Gamma \vdash \sigma \equiv \tau$ ， $\sigma$ 和 $\tau$ 是在上下文 $\Gamma$ 中的等於類型。
$\Gamma \vdash t\equiv u:\sigma$ ， $t$ 和 $u$ 是在上下文 $\Gamma$ 中的類型 $\sigma$ 的相等項。

特別重要的是轉換規則，它聲稱給定 $\Gamma \vdash t:\sigma$ 和 $\Gamma \vdash \sigma \equiv \tau$ 則 $\Gamma \vdash t:\tau$ 。

外延和內涵[編輯]

一個基本區別是外延和內涵的類型論。在外延類型論中定義性(就是計算性)等式不區別於需要證明的命題性等式。作為結論類型檢查成為不可判定性的。相反的，在內涵類型論中，類型檢查是可判定性的，但是很多數學概念的表達是不標準的，因為缺乏外延推理。這是目前對這種折中是否是不可避免的和在內涵類型論中缺乏外延原理是一個特色還是一個缺陷的討論的一個主題。

類型論的實現[編輯]

類型論已經被用做很多證明助理的基礎，比如 NuPRL、LEGO、Coq 和 Agda。最近，依賴類型也作為程式語言設計的特徵，比如Dependent ML 和 Epigram。

參見[編輯]

外部連結[編輯]

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 here （頁面存檔備份，存於互聯網檔案館）.

Thompson, Simon (1991). Type Theory and Functional Programming （頁面存檔備份，存於互聯網檔案館） Addison-Wesley. ISBN 0-201-41667-0.