类型论概论与Curry-Howard对应 (2-1)

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的原因）：

()

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

三 类型论与逻辑

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

数学联邦政治世界观提示您：看后求收藏（同人小说网http://tongren.me），接着再看更方便。