在数理逻辑与计算机科学中，同伦类型论（homotopy type theory，缩写 HoTT）是一套旨在于同伦论的大框架下构建内涵类型论语义的理论，尤指Quillen模型范畴和弱分解系统。反而言之，内涵类型论则为同伦理论提供了一套逻辑语言。类型论在绝大多数计算机证明辅助系统中被用作集合论的替代理论，因为集合论的语言难以转化成计算机证明辅助的形式语言。而英国哲学家和逻辑学家伯特兰·罗素则提出了类型论作为集合论的替代理论。
同伦理论在2002年菲尔兹奖获得者、弗拉基米尔·沃埃沃德斯基关于米尔诺猜想的工作中发挥了重要作用。 沃埃沃德斯基近年来致力于使用一价语义构造新数学基础的理论体系 UniMath，利用证明辅助工具 Coq 实现。
普林斯顿高等研究院从2012-2013年间开始致力于同伦类型论的开发，组织者包括 Steve Awodey、Thierry Coquand 和沃埃沃德斯基等人，吸引了大量数学家和计算机科学家加入。
目前该领域亟待解决的问题包括同伦类型论的计算释义，以及开发新的、能够更好支持同伦类型论的计算机证明辅助系统。
定理证明
数学定理的证明必须遵从逻辑的原则，从公理或已证明的命题推导。而数学基础研究之终极目的是形式化一切公理，从而使所有数学定理能够精确、无二义性地推导得出。
HoTT 简化了证明助手将数学证明翻译到计算机程序语言的步骤，这为计算机检验复杂的证明提供了一条简单易行的途径。
HoTT 引入了泛等公理（univalence axiom），将同伦论与逻辑命题的等价性联系起来。该等价性同样适用于数学和计算机语言的释义，它在同伦论中能够更好地被形式化。
同名著作
作为该理论研究的产物，一本开放源码的书籍 [http://homotopytypetheory.org/book/ Homotopy Type Theory: Univalent Foundations of Mathematics]（同伦类型论：数学的泛等基础） 得以公开发布。作为一部纯数学作品，它非常罕见地在 GitHub 上通过社区合作的方式进行创作，并使用 Creative Commons 授权，允许任何人免费下载或选择购买纸质版。
参见
- 泛等基础
- 数学基础
- 同伦论
- Coq
- 弗拉基米尔·沃埃沃德斯基 – UniMath（Univalent Foundations of Mathematics） 研究项目的发起人。
- 构造演算
- 直觉类型论
- 柯里-霍华德同构
扩展阅读
- [http://homotopytypetheory.org/book/ Homotopy Type Theory: Univalent Foundations of Mathematics] . The Univalent Foundations Program. Institute for Advanced Study.
*
- Martin Hofmann and Thomas Streicher (1996), [http://www.mathematik.tu-darmstadt.de/~streicher/venedig.ps.gz 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), [http://www.andrew.cmu.edu/user/awodey/students/warren.pdf Homotopy theoretic aspects of constructive type theory] , Ph.D. thesis, Carnegie Mellon University.
- S. Awodey and M. A. Warren (2009), [http://www.andrew.cmu.edu/user/awodey/preprints/homotopy.pdf Homotopy theoretic models of identity types] , Mathematical Proceedings of the Cambridge Philosophical Society.
- Egbert Rijke (2012) [http://hottheory.files.wordpress.com/2012/08/hott2.pdf Homotopy Type Theory] , Masters Thesis, Utrecht University.
参考文献
外部链接
- [http://www.homotopytypetheory.org/ Homotopy Type Theory]
- [http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html Vladimir Voevodsky's webpage on the Univalent Foundations]
- [http://www.andrew.cmu.edu/user/awodey/htt.html Homotopy Type Theory and the Univalent Foundations of Mathematics] by Steve Awodey
- [http://video.ias.edu/univalent/awodey "Constructive Type Theory and Homotopy"] – Video lecture by Steve Awodey at the Institute for Advanced Study
- [https://groups.google.com/forum/#!forum/homotopytypetheory Homotopy Type Theory Google Group]
- [https://web.archive.org/web/20160821090906/http://irc.freenode.net/#hott Homotopy Type Theory IRC channel]
评论 (0)