-
直覺類型論
鎖定
- 中文名
- 直覺類型論
- 外文名
- intuitionistic type theory
- 學 科
- 計算機科學
- 定 義
- 基於數學構造主義的集合論
- 提出時間
- 1972年
- 類 別
- 構造類型論
直覺類型論簡介
構造類型論為計算機科學家提供了一個框架,以一種優雅和靈活的方式把邏輯和程序設計語言結合起來:在同一形式系統中,可以同時表達規約和(函數式語言)程序,從證明規則可以導出正確的程序,並驗證程序具有某種性質,從而在同一系統內完成程序的開發和驗證。構造類型論的三大理論基石是:直覺類型論和構造數學、弄演算和函數式語言程序設計與實現、證明論和Curry-Howard同態。直覺類型論為構造數學提供直覺解釋。它是一個邏輯框架,可表達和解釋其它邏輯或理論
[1]
。從它的規範化證明立即得出其所表達理論的規範化。直覺類型論基於的是命題和類型的同一: 一個命題同一於它的證明的類型。這種同一通常叫做Curry-Howard同構,它最初公式化了命題邏輯和簡單類型 lambda演算。類型論通過介入包含着值的依賴類型把這種同一擴展到謂詞邏輯。類型論內在化了 Brouwer、Heyting 和 Kolmogorov 提議的叫做 BHK釋義的直覺邏輯釋義。類型論的類型扮演了類似於集合在集合論的角色,但是在類型論中的函數總是可計算的。
直覺類型論直覺類型論的連結詞
在直覺類型論的上下文中,連結詞是可能使用已給定的類型而構造類型的一種方式。類型論的基本連結詞有:
有限類型
特別重要的是
(空類型)、
(單位類型)和
(布爾值或真值)。再次用到 Curry-Howard同構,
表示假而
表示真。使用有限類型,我們可以定義否定為
,服從Curry-Howard同構,不相交併集也表示析取,它可以定義為
。
等式類型
給定
,則
是
等於
的等式證明。只有一個(規範的)
的居留,並且這是自反性
的證明。
歸納類型
歸納類型的基本例子是自然數
的類型,它是通過
和
生成的。命題為類型原理的一個重要應用是通過對用
索引的給定類型
的一個消除常量:
來把(依賴的)原始遞歸和歸納同一起來的。在一般的歸納類型中可以被定義為 W-類型,它是良基的樹的類型。
一類重要的歸納類型是像上面提及的向量
的歸納類型家族,它們是歸納生成自構造子
和
。再次用到Curry-Howard同構,歸納類型家族對應于歸納定義的關係。
全集
全集的一個例子是
,它是所有小類型的全集,它包含前面介紹的所有類型的名字。對於每個名字
我們關聯上一個類型
,這是它的外延或意義。標準上是假定全集的一個直謂性等級: 對於每個自然數
,這裏的全集
包含以前的全集的一個代碼,就是説,我們通過
而有
。這個等級經常被假定為是累積性的,就是説來自
的代碼被嵌入了
。已經研究了更強的全集原理,比如超全集和 Mahlo 全集。在 1992 年 Huet 和 Coquand 介入了構造演算,它是帶有非直謂性全集的類型論,從而把類型論同 Girard 的系統F 合併起來了。這個擴展不被直覺主義者所普遍接受,因為它允許非直謂性的,就是循環的構造,這經常用經典推理來識別。
直覺類型論外延和內涵
一個基本區別是外延和內涵的類型論。在外延類型論中定義性(就是計算性)等式不區別於需要證明的命題性等式。作為結論類型檢查成為不可判定性的。相反的,在內涵類型論中,類型檢查是可判定性的,但是很多數學概念的表達是不標準的,因為缺乏外延推理。這是對這種折中是否是不可避免的和在內涵類型論中缺乏外延原理是一個特色還是一個缺陷的討論的一個主題。