直覺類型論
維基百科,自由的 encyclopedia
直覺類型論(英語:Intuitionistic type theory),也可簡稱類型論,此外也有構造類型論或馬汀-洛夫類型論稱呼。是基於數學構造主義的函數式程式語言、邏輯和集合論。
直覺類型論由瑞典數學家和哲學家 佩爾·馬丁-洛夫於1972年引入。此前馬丁已經多次修改了他的提議,先是非直謂性的而後是直謂性的,先是外延的而後是內涵的類型論變體。直覺類型論基於的是命題和等價類的同一一個命題同一於它的證明的類型。這種同一通常叫做柯里-霍華德同構,它最初公式化了命題邏輯和簡單類型λ演算。
類型論通過介入包含著值的依賴類型把這種同一擴展到謂詞邏輯。類型論內在化了 魯伊茲·布勞威爾、阿蘭德·海廷 和 安德雷·柯爾莫哥洛夫提議的布勞威爾-海廷-柯爾莫哥洛夫釋義的直覺邏輯釋義。類型論的類型扮演了類似於集合在集合論的角色,但是在類型論中的函數總是可計算的。