abstract.tex

\documentclass[UTF8, zihao=-4]{ctexart}
\usepackage[T1]{fontenc}
\usepackage[b5paper]{geometry}
\usepackage{graphicx}
\usepackage[dvipsnames]{xcolor}
\usepackage{amssymb,amsmath,amsthm}
\usepackage{fancyhdr}
\usepackage{biblatex}
\usepackage{hyperref}
\usepackage{quiver}

\newcommand\myshade{85}
\colorlet{mylinkcolor}{violet}
\colorlet{mycitecolor}{orange}
\colorlet{myurlcolor}{Aquamarine}

\hypersetup{
  linkcolor  = mylinkcolor!\myshade!black,
  citecolor  = mycitecolor!\myshade!black,
  urlcolor   = myurlcolor!\myshade!black,
  colorlinks = true,
}

\newcommand{\cons}[1]{\textsf{#1}}
\newcommand{\slogan}[1]{\begin{center}%
  \fcolorbox{red!80!green}{red!10}{%
    \large\textbf{#1}%
  }%
\end{center}}

\theoremstyle{plain}
\newtheorem*{lemma}{引理}
\newtheorem*{theorem}{定理}
\newtheorem*{corollary}{推论}

\theoremstyle{definition}
\newtheorem*{definition}{定义}

\theoremstyle{remark}
\newtheorem*{remark}{注}

\addbibresource{history.bib}

% \pagestyle{fancy}
% \fancyhead[L]{\nouppercase{\kaishu\rightmark}}
% \fancyhead[R]{\nouppercase{\kaishu\leftmark}}
% \setlength{\headheight}{14pt}
\title{类型论简史 (摘要)}
\date{}
\author{Trebor}
\begin{document}
\maketitle

2020年12月, Peter Scholze发布了\href{https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/}{一项挑战}.
在他的凝聚态数学前沿研究中有一条技术性定理, 对于这个领域有
至关重要的作用：
\begin{theorem}[Clausen, Scholze]
设 \(0 < p' < p \le 1\) 为实数, 令 \(S\) 为投射有限集,
\(V\) 为 \(p\)-Banach 空间. 记 \(\mathcal M_{p'}(S)\)
为 \(S\) 上的 \(p'\)-测度构成的空间. 那么对于 \(i \ge 1\) 有
\[\mathrm{Ext}_{\mathsf{Cond}(\mathsf{Ab})}^i(
  \mathcal M_{p'}(S), V
) = 0.\]
\end{theorem}
Scholze希望这条定理的证明可以被完全严格形式化, 并且通过
计算机的检查. 2022年7月, Lean
社区\href{https://leanprover-community.github.io/blog/posts/lte-final/}{宣布}这个挑战正式完成.
换句话说, 即使是数学最尖端的结论, 也可以在一年半的时间内
被转化成计算机可以理解并验证的代码.
这种成就是如何达成的呢? 答案是Lean的类型论.

在类型论中, 一切数学对象的含义都由它们从属的类型决定.
如类型 \(\mathbb N\) 的元素是自然数, 而类型 \(\alpha \times \beta\)
的元素是有序对, 类型 \(\alpha \to\beta\) 的元素
是映射, 等等. 而这些类型可以相互组合, 表达出复杂的含义,
这使得类型论有能力作为数学的基础, 与集合论的地位类似.
另一方面, 计算机科学中也有利用类型描述程序的传统. 因此, 类型论
可以看作是数学与计算机之间的桥梁. 这也使得计算机定理
验证成为了有可行性的工作: 传统的使用一阶逻辑与集合论数学
基础中, 一个初等的定理也可能需要冗长的说明才能完全
严格的写出来, 因此只有理论上的可能性.
类型论的定理验证不仅可以验证数学定理,
在实际应用上还可以验证各种需要低出错率的
软硬件(如军事、医用、宇航电子仪器)设计无误.


这篇文章的主要目的是以历史作为连贯的主线将类型论的知识
串联在一起, 为中文学习者提供些微的参考价值. 同时, 文章中
介绍各个领域时都会提及其中优秀的参考书目, 供希望进一步了解
的读者阅读.

文章不要求任何类型论的前置知识, 并且尽量避免范畴论知识的
使用, 但是会援引一般数学中的许多例子. 同时, 每一节的内容
相对独立, 因此如果某一部分使用的范畴论知识较多, 读者可以直接
跳过, 不影响后续阅读.

\section*{简单类型论}
类型论是Russell在1903年为了解决以他命名的悖论而提出的.
如果有集合 \(R = \{x \mid x \notin x\}\), 那么考察
\(R \in R\) 的真假就会发现矛盾. 为了解决这个矛盾,
Russell提出了类型的概念.

我们可以发现, 数学中我们根本不会需要讨论 \(x \in x\) 这样的
命题. 实数 \(x\) 属于实数集 \(\mathbb R\), 而一些实数的
集合 (如开集) 构成集合族 \(\Omega\). 这些数学对象之间都有明确的层级,
层级混乱的命题一般没有数学意义.
更严格来说, 对象之间是有分类的. 譬如虽然二维的点 \((\pi, 3)\)
和三维空间的点 \((0,1,-1)\) 都是同一个层级的, 但是我们也基本不会
把它们放在同一个集合中.

从这个观察出发, 我们可以把这种分类的概念严格化. 我们设当前研究
的最基本的个体的分类称作 \(\iota\). 如我们研究数论的时候
\(\iota\) 代表全体自然数, 研究分析学的时候就是全体实数, 等等.
其次我们需要有一类数学对象表示命题, 因此我们把所有命题构成的分类
称作 \(o\).
其次, 我们需要从基本的分类出发组成更复杂的分类. 譬如说可以用
\(\iota \to \iota\) 表示自然数到自然数的函数.
最后, 我们引入各种逻辑连词, 如 \(\wedge : o \to o \to o\),
\(\forall : (\iota \to o) \to o\)  等等, 并且
添加相关的推理规则. 这样就得到了简单类型论的逻辑系统.

人们依据这种形式系统, 写出了计算机程序 Isabelle,
用计算机的准确性验证数学证明. 已经有不少数学理论被 Isabelle 形式化.
譬如质数定理. 这说明类型论与集合论一样, 有形式化数学的基本能力.

\section*{Curry--Howard 对应}
观察类型系统的规则,
假如我们有 \(f : \alpha \to \beta\), 以及 \(a : \alpha\),
那么我们就能求值得到 \(f(a) : \beta\). 这其实和逻辑里
最古老的推理有些相像： 假如我们证明了 \(p\Rightarrow q\),
并且我们证明了 \(p\), 那么我们就可以证明 \(q\).
在1934年, Curry 注意到了这一相似之处. 随后越来越多
的对应关系表明, 逻辑中的命题与类型论中的类型表现得非常
相似. 这就是 Curry--Howard 对应. 因此, 如果我们为
每一种逻辑关系找到对应的类型, 那么就不需要再额外添加推理
规则, 直接使用类型作为命题即可.

1967年, 利用这些想法, Nicolaas Govert de Bruijn
设计了一门依值类型论的计算机语言, 称为 Automath.
1976年, Jutting 在学位论文中使用 Automath
形式化了 Landau 的《分析学基础》． Automath 没有
被大规模使用, 不过它的设计影响到了许多后继的类型论.

F系统在 1972 年由逻辑学家 Jean-Yves Girard
与 1974 年由计算机科学家 J. C. Reynolds 独立发现.
这说明 Curry--Howard 对应不仅仅是一个刻意构造的对应,
而是深刻而直接地影响到了两个学科的发展.

\section*{同伦类型论}

1998年, Hofmann给出了类型论的群胚模型. 这为类型论
的发展提供了新的启示, 最终产生了同伦类型论的概念.

基于拓扑空间的同伦论中, 拓扑空间不满足许多理应满足的性质.
譬如连续函数构成的空间并不一定能使得求值态射
\(\cons{ev} : [(X \Rightarrow Y) \times X] \to Y\) 连续;
不是所有空间都有万有覆叠, 等等. 因此使用拓扑空间时
必须花费精力将性质不好的部分剔除.

同伦类型论则从全新的角度解决了这个问题. 正如《几何原本》并不是
利用实数构造坐标系来研究几何, 而是直接从一系列基本的事实
出发推导复杂的定理, 同伦类型论不使用实数区间 \([0,1]\) 而是
直接从类型规则出发刻画同伦的概念. 譬如
\(\pi_4(\mathbb S^3) = \mathbb Z/2\mathbb Z\)
等性质可以直接在同伦类型论中得到证明. 目前有许多同伦论的
结论已经可以在同伦类型论中复现.

2012--2013年, 由Princeton高等研究院发起了
“泛等数学基础特别年”, 邀请了拓扑学、计算机科学、范畴论、逻辑学
等等领域的数学家参加. 其中由 Peter Aczel 提议, 尝试使用
同伦类型论书写非形式化的数学. 这次尝试很快获得了
初步成功, 最终写出了《同伦类型论：泛等数学基础》这本书.
它从零出发, 整理了泛等数学基础中的结论, 从同伦类型论
的角度重新叙述了集合论与范畴论, 并且给出了
实数的定义与主要性质的证明.

\section*{类型论的语义}

语法与语义, 是类型论理论研究的中心. 起初, 类型论的语义
常常使用的是一阶逻辑和集合论现成的语义学工具. 1984年,
Seely在一篇文章中指出, 局部积闭范畴可以和
类型论中的许多东西找到对应. 随后, 范畴论与类型论之间的
关联逐步被发展起来. 各种不同的类型论可以视作是各类不同
的范畴的语言. 它们之间的关系可以画成图表:

\[\begin{tikzcd}
{\text{范畴论}} && {\text{类型论}}
\arrow[""{name=0, anchor=center, inner sep=0}, "{\text{内语言}}"', shift right=1, curve={height=6pt}, from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\text{语法范畴}}"', shift right=1, curve={height=6pt}, from=1-3, to=1-1]
\arrow["\bot"{description}, draw=none, from=1, to=0]
\end{tikzcd}\]

类型论的语法规定了语义的结构, 而另一方面
语义研究的发展又促使新的语法规则的形成. 二者构成对立统一,
矛盾运动的关系.

\vspace*{\fill}

\emph{参考文献见完整版.}
\end{document}