同伦类型论
哲学园 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 全体连续函数的集合)上的等价关系。同伦的初步应用之一,是借由环路的同伦定义何谓单连通。
相对同伦
是连续函数,固定子空间
;若存在前述同伦映射
,满足:
同伦到
的恒等映射
。
同伦到
的恒等映射
。
一个平面上的圆或椭圆同伦等价到 ,即去掉一点的平面。
线段 、闭圆盘及闭球间两两同伦等价,它们皆同伦等价于一个点。
对所有 ,映射
是个同胚映射。
相对于
同伦。若取
,则回到原先的同伦定义。
空间的同伦等价
空间的连续变化:咖啡杯与甜甜圈
与
,我们称之同伦等价(或称具相同伦型),当且仅当存在两个连续映射
与
,使得:
同痕
和
是同胚,并要求两者间可用一族同胚映射相连。
与
被称为同痕的,当且仅当存在连续映射
使之满足: