类型论概论与Curry-Howard对应

plus_comm =

fun nm :nat =＞

nat_ind(fun n0 :nat =＞ no + m=m +n0)

(plus_n_0 m)

(fun (y :nat)(H:y + m=m+y)=＞

eq_ind(S(m + y))

(fun no :nat =＞ S (y +m)=n0)

(f_equal S H)

(m + S y)

(plus_n_Sm m y)）n

：forallnm:nat.n+m=m+n

一 数学的根基是什么？

数学的根基是什么？这是数学家们一直在追寻的问题。我们公认的基础是形式系统。把数学公式的书写从意义独立出来，以此来保持数学本身的严谨性。而公式的意义可以在严谨的推理之后在去赋予。我们举个非常简单的形式系统的例子[1]：

pq形式系统：

1 ‘pyq‘y 是一个公式，其中 y 表示任意数量的 ‘ 。

2 如果 xpyqz 是公式，其中 x，y，z 表示任意数量的 ‘ ，那么 ‘xpyq‘z 也是一个公式。

我们来推导一些定理吧（定理指的是可以由形式系统的规则推出的公式）。

pq定理1： ‘p‘q‘‘ 是公式。

证明：在规则1中令 y＝‘ 即可。

到目前为止，这个形式系统只是一串没有意义的符号罢了。但是，我们马上就可以赋予它意义。事实上，这个形式系统刻画的是正整数的加法。p代表plus（加），q代表equal（等于）。

当然，我们还可以赋予它其他的意义，比如p代表“是相反数”，q代表“减”。

通常，我们先把逻辑推演先以形式系统的方式定义好，然后定义我们想要研究的对象（譬如自然数、四则运算）。这些对象满足一些公理。

集合论是其中一种：由空集开始，把各种数学概念编码成集合的结构。从这一点出发数学家提出了很多套集合论的公理。这在后面的文章里会讲到。

另一种可以作为数学根基的便是类型论。至于它有什么特别之处，以后便会讲到。

二 类型论与编程

我们先来看看编程中的类型系统。这方面比较接近Martin-Löf的理论的语言有ML类（比如OCaML）、Haskell与Lisp（这个不太清楚）。我们直接拿Haskell做例子。

我们可以很自然的引出函数类型：给一个 A 类型的元素，返回一个 B 类型的元素。记作 A → B 。换成代码就是：

f :: A -＞ B

那么如果

x :: A

就有

f x :: B

同样自然地可以得到积类型：一个有序对，其中前一项是 A 类型，后一项是 B 类型。记作 A × B 。这在Haskell（以及大部分支持元组的编程语言中）就是

a :: A

b :: B

(a, b) :: (A, B)

不过这里用同样的记号表示元素与类型，私以为不好。

我们常用的None（Python），属于Nonetype，就是只能有一个值的类型，称为1类型。在Haskell中，可以用空元组表示（事实上，这是积类型的单位元，也就是它称为1的原因）：

()

但是一般语言中没有的特性是依赖类型，这在后面的文章中会介绍。

三 类型论与逻辑

那么类型论怎么充当数学根基的角色呢？

举个例子，如果A 能推出 B，这相当于“给我一个 A 的证明，我就能给出一个 B 的证明”，这是不是类似函数类型？受此启发，我们提出把命题作为类型的思想：如果 P 是一个命题，我们把它当做一个类型，而如果 p 是这个类型的，我们解读为“ p 是 P 的证明”。接下来的一切，都在这个思想下讨论。

四 类型论的形式化

我们以推理规则的形式简单写写类型论的框架。

首先，α 是 A 类型，可以写作 α：A 。注意，这不是一个命题，而是一个判断！这一点的区别在于，这种东西是不能被像命题一样操作的：比如，你无法否定它（“α 不是 A 类型”这句话根本就是不符合语法的），因此写出一个判断，就代表它是对的，而认定它正确性的就是推理规则。命题与判断的区别，在讲相等类型的时候还会遇到。

如果从一些判断（用Γ 代指）出发，可以用推理规则直接得到另一个判断 J ，我们写作 Γ ⊢ J。譬如：

α：A，b：B ⊢ (α，b)：A × B

树形

α：A，b：B

─────── prod-intro

(α，b)：A × B

右边就是推理规则的名称。

References

[1] Douglas Hofstader,Gödel, Escher, Bach: an Eternal Golden Briad.

[2] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics.