同倫類型論
在數理邏輯與計算機科學中，同倫類型論（homotopy type theory，縮寫 HoTT）是一套旨在於同倫論的大框架下構建內涵類型論語義的理論，尤指Quillen模型範疇和弱分解系統。反而言之，內涵類型論則為同倫理論提供了一套邏輯語言。類型論在絕大多數計算機證明輔助系統中被用作集合論的替代理論，因為集合論的語言難以轉化成計算機證明輔助的形式語言。[1]
歷史
1908年，恩斯特·策梅洛提出了被稱作策梅洛-弗蘭克爾集合論（或ZFC）的公理化集合論。該理論採用了選擇公理，並作為數學的基礎理論存在，因所有的數學物件均可通過集合論中的概念來解釋。[1]而英國哲學家和邏輯學家伯特蘭·羅素則提出了類型論作為集合論的替代理論。[1]
同倫理論在2002年菲爾茲獎獲得者、弗拉基米爾·沃埃沃德斯基關於米爾諾猜想的工作中發揮了重要作用。 沃埃沃德斯基近年來致力於使用一價語義構造新數學基礎的理論體系 UniMath，利用證明輔助工具 Coq 實現。[1]
普林斯頓高等研究院從2012-2013年間開始致力於同倫類型論的開發，組織者包括 Steve Awodey、Thierry Coquand 和沃埃沃德斯基等人，吸引了大量數學家和計算機科學家加入。
目前該領域亟待解決的問題包括同倫類型論的計算釋義，以及開發新的、能夠更好支持同倫類型論的計算機證明輔助系統。
定理證明
數學定理的證明必須遵從邏輯的原則，從公理或已證明的命題推導。而數學基礎研究之終極目的是形式化一切公理，從而使所有數學定理能夠精確、無二義性地推導得出。[1]
HoTT 簡化了證明助手將數學證明翻譯到電腦程式語言的步驟，這為計算機檢定複雜的證明提供了一條簡單易行的途徑。[1]
HoTT 引入了泛等公理（univalence axiom），將同倫論與邏輯命題的等價性聯繫起來。該等價性同樣適用於數學和計算機語言的釋義，它在同倫論中能夠更好地被形式化。
Homotopy Type Theory
作為該理論研究的產物，一本開放源碼的書籍 Homotopy Type Theory: Univalent Foundations of Mathematics（同倫類型論：數學的泛等基礎） （頁面存檔備份，存於網際網路檔案館） 得以公開發布。作為一部純數學作品，它非常罕見地在 GitHub 上通過社區合作的方式進行創作，並使用 Creative Commons 授權，從而允許任何人免費下載或選擇購買紙質版。
參見
擴展閱讀
- Homotopy Type Theory: Univalent Foundations of Mathematics （頁面存檔備份，存於網際網路檔案館）. The Univalent Foundations Program. Institute for Advanced Study.
- Awodey, Steve. Type theory and homotopy. Dybjer, P.; Lindström, Sten; Palmgren, Erik; Sundholm, G. (編). Epistemology versus Ontology (PDF). Logic, Epistemology, and the Unity of Science. Springer Netherlands. 2012: 183–201 [2014-09-15]. ISBN 978-94-007-4434-9. doi:10.1007/978-94-007-4435-6_9. （原始內容存檔 (PDF)於2019-07-13）.
- Martin Hofmann and Thomas Streicher (1996), The groupoid interpretation of type theory （頁面存檔備份，存於網際網路檔案館）, in Sambin, Giovanni (ed.) et al., Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, October 19–21, 1995.
- Michael A. Warren (2008), Homotopy theoretic aspects of constructive type theory （頁面存檔備份，存於網際網路檔案館）, Ph.D. thesis, Carnegie Mellon University.
- S. Awodey and M. A. Warren (2009), Homotopy theoretic models of identity types （頁面存檔備份，存於網際網路檔案館）, Mathematical Proceedings of the Cambridge Philosophical Society.
- Egbert Rijke (2012) Homotopy Type Theory （頁面存檔備份，存於網際網路檔案館）, Masters Thesis, Utrecht University.
參考文獻
外部連結
- Homotopy Type Theory （頁面存檔備份，存於網際網路檔案館）
- Vladimir Voevodsky's webpage on the Univalent Foundations （頁面存檔備份，存於網際網路檔案館）
- Homotopy Type Theory and the Univalent Foundations of Mathematics （頁面存檔備份，存於網際網路檔案館） by Steve Awodey
- "Constructive Type Theory and Homotopy" （頁面存檔備份，存於網際網路檔案館） – Video lecture by Steve Awodey at the Institute for Advanced Study
- Homotopy Type Theory Google GroupPortuguese Web Archive的存檔，存檔日期2011-01-22
- Homotopy Type Theory IRC channel