fbpx
维基百科

同伦类型论

二月 09, 2023

在数理逻辑与计算机科学中，同伦类型论（homotopy type theory，缩写 HoTT）是一套旨在于同伦论的大框架下构建内涵类型论语义的理论，尤指Quillen模型范畴和弱分解系统。反而言之，内涵类型论则为同伦理论提供了一套逻辑语言。类型论在绝大多数计算机证明辅助系统中被用作集合论的替代理论，因为集合论的语言难以转化成计算机证明辅助的形式语言。[1]

Homotopy Type Theory 的封面

历史

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.

参考文献

  1. ^ 1.0 1.1 1.2 1.3 1.4 1.5 Meyer, Florian. A new foundation for mathematics. R&D Magazine. 9/3/14 [9/6/14]. （原始内容于2015-09-24）. 

外部链接

  • 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

二月 09, 2023
同伦类型论, 在数理逻辑与计算机科学中, homotopy, type, theory, 缩写, hott, 是一套旨在于同伦论的大框架下构建内涵类型论语义的理论, 尤指quillen模型范畴和弱分解系统, 反而言之, 内涵类型论则为同伦理论提供了一套逻辑语言, 类型论在绝大多数计算机证明辅助系统中被用作集合论的替代理论, 因为集合论的语言难以转化成计算机证明辅助的形式语言, homotopy, type, theory, 的封面, 目录, 历史, 定理证明, homotopy, type, theory, 参见,. 在数理逻辑与计算机科学中 同伦类型论 homotopy type theory 缩写 HoTT 是一套旨在于同伦论的大框架下构建内涵类型论语义的理论 尤指Quillen模型范畴和弱分解系统 反而言之 内涵类型论则为同伦理论提供了一套逻辑语言 类型论在绝大多数计算机证明辅助系统中被用作集合论的替代理论 因为集合论的语言难以转化成计算机证明辅助的形式语言 1 Homotopy Type Theory 的封面 目录 1 历史 2 定理证明 3 Homotopy Type Theory 4 参见 5 扩展阅读 6 参考文献 7 外部链接历史 编辑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 授权 从而允许任何人免费下载或选择购买纸质版 参见 编辑数学基础 同伦论 Coq 弗拉基米尔 沃埃沃德斯基 UniMath Univalent Foundations of Mathematics 研究项目的发起人 构造演算 直觉类型论 柯里 霍华德同构扩展阅读 编辑Homotopy Type Theory Univalent Foundations of Mathematics 页面存档备份 存于互联网档案馆 The Univalent Foundations Program Institute for Advanced Study Awodey Steve Type theory and homotopy Dybjer P Lindstrom 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 参考文献 编辑 1 0 1 1 1 2 1 3 1 4 1 5 Meyer Florian A new foundation for mathematics R amp D Magazine 9 3 14 9 6 14 原始内容存档于2015 09 24 请检查 access date date 中的日期值 帮助 外部链接 编辑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 取自 https zh wikipedia org w index php title 同伦类型论 amp oldid 67302883, 维基百科，wiki，书籍，书籍，图书馆，

文章

，阅读，下载，免费，免费下载，mp3，视频，mp4，3gp， jpg，jpeg，gif，png，图片，音乐，歌曲，电影，书籍，游戏，游戏。