類型論：一類新的數學
以下視頻轉自：遇見數學
遇見數學翻譯小組
哲學園鳴謝
隨著計算機越來越多地被用來互動式數學證明，是時候進一步研究計算機科學對數學的貢獻，比如在計算機實現了用類型論求解數學問題的系統。
請看托爾斯滕·阿爾滕基奇博士討論類型論與集合論的視頻。
翻譯 @ 小魚：[遇見數學翻譯小組] 核心成員
同倫類型論
哲學園
2014-12-25
素材來源於網路
哲學園鳴謝
在數理邏輯與計算機科學中，同倫類型論（homotopy type theory，縮寫 HoTT）是一套旨在於同倫論的大框架下構建內涵類型論語義的理論，尤指Quillen模型範疇和弱分解系統。反而言之，內涵類型論則為同倫理論提供了一套邏輯語言。類型論在絕大多數計算機證明輔助系統中被用作集合論的替代理論，因為集合論的語言難以轉化成計算機證明輔助的形式語言。
Homotopy Type Theory 的封面
歷史
1908年，恩斯特·策梅洛提出了被稱作策梅洛-弗蘭克爾集合論（或ZFC）的公理化集合論。該理論採用了選擇公理，並作為數學的基礎理論存在，因所有的數學對象均可通過集合論中的概念來解釋。而英國哲學家和邏輯學家伯特蘭·羅素則提出了類型論作為集合論的替代理論。
同倫理論在2002年菲爾茲獎獲得者、弗拉基米爾·沃埃沃德斯基關於米爾諾猜想的工作中發揮了重要作用。沃埃沃德斯基近年來致力於使用一價語義構造新數學基礎的理論體系 UniMath，利用證明輔助工具Coq實現。
普林斯頓高等研究院從2012-2013年間開始致力於同倫類型論的開發，組織者包括 Steve Awodey、Thierry Coquand 和沃埃沃德斯基等人，吸引了大量數學家和計算機科學家加入。
目前該領域亟待解決的問題包括同倫類型論的計算釋義，以及開發新的、能夠更好支持同倫類型論的計算機證明輔助系統。
定理證明
數學定理的證明必須遵從邏輯的原則，從公理或已證明的命題推導。而數學基礎研究之終極目的是形式化一切公理，從而使所有數學定理能夠精確、無二義性地推導得出。
HoTT 簡化了證明輔助工具將數學證明翻譯到計算機程序語言的步驟，這為計算機檢驗複雜的證明提供了一條簡單易行的途徑。[1]
HoTT 引入了一價公理（univalence axiom），將同倫論與邏輯命題的等價性聯繫起來。該等價性同樣適用於數學和計算機語言的釋義，它在同倫論中能夠更好地被形式化。
Homotopy Type Theory
作為該理論研究的產物，一本開放源碼的書籍Homotopy Type Theory: Univalent Foundations of Mathematics（同倫類型論：數學的一價語義基礎）得以公開發布。作為一部純數學作品，它非常罕見地在GitHub上通過社區合作的方式進行創作，並使用 Creative Commons 授權，從而允許任何人免費下載或選擇購買紙質版。
相關知識
數學基礎
數學上，數學基礎一詞有時候用於數學的特定領域，例如數理邏輯，公理化集合論，證明論，模型論，和遞歸論。但是尋求數學的基礎也是數學哲學的中心問題：在什麼終極基礎上命題可以稱為真?
目前占統治地位的數學範式是基於公理化集合論和形式邏輯的。實際上，幾乎所有現在的數學定理都可以表述為集合論下的定理。在這個觀點下，所謂數學命題的真實性，不過就是該命題可以從集合論公理使用形式邏輯推導出來。
這個形式化的方法不能解釋一些問題：為什麼我們應沿用現行的公理而不是別的，為什麼我們應沿用現行的邏輯規則而不是別的，為什麼"真"數學命題（例如，算術領域的皮亞諾公理）在物理世界中似乎是真的。這被尤金·維格納在1960年叫做「數學在自然科學中無理由的有效性」（The unreasonable effectiveness of mathematics in the natural sciences）。
上述的形式化真實性也可能完全沒有意義：有可能所有命題，包括自相矛盾的命題，都可以從集合論公理導出。而且，作為歌德爾第二不完備定理的一個結果，我們永遠無法排除這種可能性。
在數學實在論（有時也叫柏拉圖主義）中，獨立於人類的數學對象的世界的存在性被作為一個基本假設；這些對象的真實性由人類發現。在這種觀點下，自然定律和數學定律有類似的地位，因此"有效性"不再"無理由"。不是我們的公理，而是數學對象的真實世界構成了數學基礎。但，顯然的問題在於，我們如何接觸這個世界？
一些數學哲學的現代理論不承認這種數學基礎的存在性。有些理論傾向於專註數學實踐，並試圖把數學家的實際工作視為一種社會群體來作描述和分析。也有理論試圖創造一個數學認知科學，把數學在"現實世界"中的可靠性歸結為人類的認知。這些理論建議只在人類的思考中找到基礎。
同倫論
在數學中，同倫（Homotopy）的概念在拓撲上描述了兩個對象間的「連續變化」。
兩條路徑的同倫
函數的同倫
給定兩個拓撲空間和。考慮兩個連續函數，若存在一個連續映射使得
·
·
則稱（在里）同倫。
換言之：每個參數對應到一個函數；隨著參數值從 0 到 1 變化，連續地從變化到
另一種觀點是：對每個，函數定義一條連接與的路徑：
例一：取,,及。則與透過下述函數在中同倫。
（注意到此例子不依賴於變數，通常並非如此。）
註：「在中同倫」的說法提示一個重點：在例一中若將代為子空間，則雖然與仍取值在，但此時它們並不同倫。此點可藉中間值定理驗證。
例二：取、、及.描繪一個以原點為圓心之單位圓；停在原點。與透過下述連續函數同倫：
幾何上來看，對每個值，函數描繪一個以原點為圓心，半徑的圓。
函數間的同倫是（即從 X 到 Y 全體連續函數的集合）上的等價關係。同倫的初步應用之一，是藉由環路的同倫定義何謂單連通。
相對同倫
為定義高階基本群，必須考慮相對於一個子空間的同倫概念。這是指能在不變動該子空間的狀況下連續變化，正式定義是：設是連續函數，固定子空間；若存在前述同倫映射，滿足：
則稱相對於同倫。若取，則回到原先的同倫定義。
空間的同倫等價
空間的連續變化：咖啡杯與甜甜圈
給定兩個拓撲空間與，我們稱之同倫等價（或稱具相同倫型），當且僅當存在兩個連續映射與，使得：
同倫到的恆等映射。
同倫到的恆等映射。
同胚蘊含同倫，反之則不然，詳見以下例子：
例三：
一個平面上的圓或橢圓同倫等價到，即去掉一點的平面。
線段、閉圓盤及閉球間兩兩同倫等價，它們皆同倫等價於一個點。
同倫等價是個拓撲空間之間的等價關係。許多代數拓撲學裡的性質均在同倫等價下不變，包括有：單連通、同調群及上同調群等等。
同痕
同痕是同倫的加細版；我們進一步要求所論的函數和是同胚，並要求兩者間可用一族同胚映射相連。
定義如次：與被稱為同痕的，當且僅當存在連續映射使之滿足：
對所有，映射是個同胚映射。
同痕的概念在紐結理論中格外重要：若兩個結同痕，則我們視之相等；換言之，可以在不使結扯斷或相交的條件下彼此連續地變形。
Coq
Coq 是一個互動式的定理證明輔助工具。它允許用戶輸入包含數學斷言的表達式、機械化地對這些斷言執行檢查、幫助構造形式化的證明、並從其形式化描述的構造性證明中提取出可驗證的（certified）程序。Coq 的理論基礎是歸納構造演算（calculus of inductive constructions）、一種構造演算（calculus of constructions）的衍生理論。Coq 並非一個自動化定理機器證明語言；然而，它提供了自動化定理證明的策略（tactics）和不同的決策過程。
Coq 同時還是一個依賴類型的函數式編程語言[1]。它由法國PPS實驗室的PI.R2團隊研究開發[2]，該團隊由INRIA、巴黎綜合理工學院、巴黎第十一大學、巴黎第七大學和法國國家科學研究中心組成。此前里昂高等師範學校亦曾參與開發。Coq 項目當前由 Gérard Huet、Christine Paulin 和 Hugo Herbelin領導。Coq 使用 OCaml 以及少部分 C 實現。
單詞 coq 在法語中意為"公雞"，此命名體現了法國在研究活動中使用動物名稱命名工具的傳統。[3] 最初，它被簡單地稱作 Coc，意即構造演算（calculus of constructions）的縮寫，同時也暗含了 Thierry Coquand（與 Gérard Huet 共同提出了前述的構造演算）的姓氏。
Coq 自身提供了一套規範語言 Gallina[4] 。使用 Gallina 書寫的程序具有規範化性質——它們總是會終止。此性質使之避開了停機問題 [5]。同時，這也使得 Coq 語言本身並非圖靈完全。
應用
四色定理：在2004年九月使用 Coq 完成正式的證明。
法伊特－湯普森定理：在2012年九月使用 Coq 完成正式的證明。
弗拉基米爾·沃埃沃德斯基 – UniMath（Univalent Foundations of Mathematics） 研究項目的發起人。
構造演算
直覺類型論
柯里-霍華德同構
TAG:哲學園 |