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

举个例子，如果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.

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