類型論
維基百科,自由的 encyclopedia
類型論,數學、邏輯和電腦科學以下的一個分支,是研究不同類型系統及其表達形式的學科。某些類型系統適合用作數學基礎,取代數學家一般使用的集合論,其中最具影響力的有阿隆佐·邱奇的有類型λ演算和佩爾·馬丁-洛夫的直覺類型論。許多函式語言和電腦協助定理驗證(英語:Proof assistant)工具都建立在類型論的基礎上,如Agda、Coq、Idris、Lean等等。
類型論的核心概念是,每一條合乎語法規則的表達式(或稱「項」)都有其所屬的「類型」。通過結合多個基礎類型,可以定義更加複雜的類型。如此得出的類型可以代表林林總總的數學結構,如自然數、群、拓撲空間等等。在集合論中,這些結構都是含有元素(或稱成員)的集合,它的定義純粹就是指定其所含的所有元素。在類型論中,這些結構的定義並不羅列屬於它的所有項,而是指定如何建構它的項的一套規則。
集合論建基於一階邏輯,有「集合」和「命題」兩個主要概念。任何一套集合論公理(如策梅洛-弗蘭克爾集合論)和命題都是以一階邏輯的語言所表達。類型論則只有「類型」的概念,每一條邏輯命題都是一個類型。要證明任何一條命題,就需要建構屬於此類型的項,是為命題為類型原理。換言之,證明定理的過程只不過是建構符合指定數學結構的數學物件的過程的一個特例。[1]