哲学园 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 全体连续函数的集合）上的等价关系。同伦的初步应用之一，是借由环路的同伦定义何谓单连通。

相对同伦

为定义高阶基本群，必须考虑相对于一个子空间的同伦概念。这是指能在不变动该子空间的状况下连续变化，正式定义是：设

是连续函数，固定子空间

；若存在前述同伦映射

，满足：

• 
• 
则称

相对于

同伦。若取

，则回到原先的同伦定义。

空间的同伦等价



空间的连续变化：咖啡杯与甜甜圈

给定两个拓扑空间

与

，我们称之同伦等价（或称具相同伦型），当且仅当存在两个连续映射

与

，使得：
• 

  同伦到

  

  的恒等映射

  

  。
• 

  同伦到

  

  的恒等映射

  

  。
同胚蕴含同伦，反之则不然，详见以下例子：
例三：
• 一个平面上的圆或椭圆同伦等价到

  

  ，即去掉一点的平面。
• 线段

  

  、闭圆盘及闭球间两两同伦等价，它们皆同伦等价于一个点。
同伦等价是个拓扑空间之间的等价关系。许多代数拓扑学里的性质均在同伦等价下不变，包括有：单连通、同调群及上同调群等等。

同痕

同痕是同伦的加细版；我们进一步要求所论的函数

和

是同胚，并要求两者间可用一族同胚映射相连。
定义如次：

与

被称为同痕的，当且仅当存在连续映射

使之满足：
• 
• 
• 对所有

  

  ，映射

  

  是个同胚映射。
同痕的概念在纽结理论中格外重要：若两个结同痕，则我们视之相等；换言之，可以在不使结扯断或相交的条件下彼此连续地变形。






Coq
Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言执行检查、帮助构造形式化的证明、并从其形式化描述的构造性证明中提取出可验证的（certified）程序。Coq 的理论基础是归纳构造演算（calculus of inductive constructions）、一种构造演算（calculus of constructions）的衍生理论。Coq 并非一个自动化定理机器证明语言；然而，它提供了自动化定理证明的策略（tactics）和不同的决策过程。


Coq 同时还是一个依赖类型的函数式编程语言[1]。它由法国PPS实验室的PI.R2团队研究开发[2]，该团队由INRIA、巴黎综合理工学院、巴黎第十一大学、巴黎第七大学和法国国家科学研究中心组成。此前里昂高等师范学校亦曾参与开发。Coq 项目当前由 Gérard Huet、Christine Paulin 和 Hugo Herbelin领导。Coq 使用 OCaml 以及少部分 C 实现。


单词 coq 在法语中意为'公鸡'，此命名体现了法国在研究活动中使用动物名称命名工具的传统。[3] 最初，它被简单地称作 Coc，意即构造演算（calculus of constructions）的缩写，同时也暗含了 Thierry Coquand（与 Gérard Huet 共同提出了前述的构造演算）的姓氏。
Coq 自身提供了一套规范语言 Gallina[4] 。使用 Gallina 书写的程序具有规范化性质——它们总是会终止。此性质使之避开了停机问题 [5]。同时，这也使得 Coq 语言本身并非图灵完全。

打开APP，阅读全文并永久保存 查看更多类似文章 更多类似文章 >>