同倫類型論

同倫類型論

同倫類型論（homotopy type theory，縮寫HoTT）是一套旨在於同倫論的大框架下構建內涵類型論語義的理論，尤指Quillen模型範疇和弱分解系統。

基本介紹

  • 中文名：同倫類型論
  • 外文名：homotopy type theory
  • 縮寫：HoTT
  • 代指：Quillen模型範疇和弱分解系統
  • 套用領域：數理邏輯與計算機科學
  • 相關術語：類型論
描述,歷史,定理證明,相關書籍,參見,

描述

在數理邏輯與計算機科學中，同倫類型論（homotopy type theory，縮寫HoTT）是一套旨在於同倫論的大框架下構建內涵類型論語義的理論，尤指Quillen模型範疇和弱分解系統。反而言之，內涵類型論則為同倫理論提供了一套邏輯語言。類型論在絕大多數計算機證明輔助系統中被用作集合論的替代理論，因為集合論的語言難以轉化成計算機證明輔助的形式語言。

歷史

1908年，恩斯特·策梅洛提出了被稱作策梅洛-弗蘭克爾集合論（或ZFC）的公理化集合論。該理論採用了選擇公理，並作為數學的基礎理論存在，因所有的數學對象均可通過集合論中的概念來解釋。而英國哲學家和邏輯學家伯特蘭·羅素則提出了類型論作為集合論的替代理論。
同倫理論在2002年菲爾茲獎獲得者、弗拉基米爾·沃埃沃德斯基關於米爾諾猜想的工作中發揮了重要作用。 沃埃沃德斯基近年來致力於使用一價語義構造新數學基礎的理論體系 UniMath，利用證明輔助工具Coq實現。
普林斯頓高等研究院從2012-2013年間開始致力於同倫類型論的開發，組織者包括 Steve Awodey、Thierry Coquand 和沃埃沃德斯基等人，吸引了大量數學家和計算機科學家加入。
目前該領域亟待解決的問題包括同倫類型論的計算釋義，以及開發新的、能夠更好支持同倫類型論的計算機證明輔助系統。

定理證明

數學定理的證明必須遵從邏輯的原則，從公理或已證明的命題推導。而數學基礎研究之終極目的是形式化一切公理，從而使所有數學定理能夠精確、無二義性地推導得出。
HoTT 簡化了證明輔助工具將數學證明翻譯到電腦程式語言的步驟，這為計算機檢驗複雜的證明提供了一條簡單易行的途徑。
HoTT 引入了一價公理（univalence axiom），將同倫論與邏輯命題的等價性聯繫起來。該等價性同樣適用於數學和計算機語言的釋義，它在同倫論中能夠更好地被形式化。

相關書籍

作為該理論研究的產物，一本開放源碼的書籍
《Homotopy Type Theory:Univalent Foundations of Mathematics》得以公開發布。作為一部純數學作品，它非常罕見地在GitHub上通過社區合作的方式進行創作，並使用Creative Commons授權，從而允許任何人免費下載或選擇購買紙質版。

參見

相關詞條

熱門詞條

聯絡我們