直覺類型論

直覺類型論、或構造類型論、或Martin-Löf 類型論、或就叫類型論是基於數學構造主義的函式式程式語言、邏輯和集合論。直覺類型論由瑞典數學家和哲學家 Per Martin-Löf 在1972年提出的。 Martin-Löf 已經多次修改了它的提議；先是非直謂性的而後是直謂性的，先是外延的而後是內涵的類型論變體。

基本介紹

• 中文名：直覺類型論
• 外文名：intuitionistic type theory
• 學科：計算機科學
• 定義：基於數學構造主義的集合論
• 提出時間：1972
• 類別：構造類型論

簡介

構造類型論為計算機科學家提供了一個框架，以一種優雅和靈活的方式把邏輯和程式設計語言結合起來：在同一形式系統中，可以同時表達規約和（函式式語言）程式，從證明規則可以導出正確的程式，並驗證程式具有某種性質，從而在同一系統內完成程式的開發和驗證。構造類型論的三大理論基石是：直覺類型論和構造數學、弄演算和函式式語言程式設計與實現、證明論和Curry-Howard同態。直覺類型論為構造數學提供直覺解釋。它是一個邏輯框架，可表達和解釋其它邏輯或理論。從它的規範化證明立即得出其所表達理論的規範化。直覺類型論基於的是命題和類型的同一: 一個命題同一於它的證明的類型。這種同一通常叫做Curry-Howard同構，它最初公式化了命題邏輯和簡單類型 lambda演算。類型論通過介入包含著值的依賴類型把這種同一擴展到謂詞邏輯。類型論內在化了 Brouwer、Heyting 和 Kolmogorov 提議的叫做 BHK釋義的直覺邏輯釋義。類型論的類型扮演了類似於集合在集合論的角色，但是在類型論中的函式總是可計算的。

直覺類型論的連結詞

在直覺類型論的上下文中，連結詞是可能使用已給定的類型而構造類型的一種方式。類型論的基本連結詞有：

-類型

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

-類型

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

有限類型

特別重要的是 (空類型)、 (單位類型)和 (布爾值或真值)。再次用到 Curry-Howard同構， 表示假而 表示真。使用有限類型，我們可以定義否定為 ，服從Curry-Howard同構，不相交並集也表示析取，它可以定義為 。

等式類型

給定 ，則 是 等於 的等式證明。只有一個(規範的) 的居留，並且這是自反性 的證明。

歸納類型

歸納類型的基本例子是自然數 的類型，它是通過和生成的。命題為類型原理的一個重要套用是通過對用索引的給定類型的一個消除常量：來把(依賴的)原始遞歸和歸納同一起來的。在一般的歸納類型中可以被定義為 W-類型，它是良基的樹的類型。

一類重要的歸納類型是像上面提及的向量的歸納類型家族，它們是歸納生成自構造子 和 。再次用到Curry-Howard同構，歸納類型家族對應于歸納定義的關係。

全集

全集的一個例子是，它是所有小類型的全集，它包含前面介紹的所有類型的名字。對於每個名字 我們關聯上一個類型，這是它的外延或意義。標準上是假定全集的一個直謂性等級: 對於每個自然數，這裡的全集包含以前的全集的一個代碼，就是說，我們通過而有。這個等級經常被假定為是累積性的，就是說來自的代碼被嵌入了。已經研究了更強的全集原理，比如超全集和 Mahlo 全集。在 1992 年 Huet 和 Coquand 介入了構造演算，它是帶有非直謂性全集的類型論，從而把類型論同 Girard 的系統F 合併起來了。這個擴展不被直覺主義者所普遍接受，因為它允許非直謂性的，就是循環的構造，這經常用經典推理來識別。

外延和內涵

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