类型论

维基百科，自由的百科全书

在最广泛的层面上，类型论是关注把实体分类到叫做类型的搜集中的数学和逻辑分支。在这种意义上，它与类型的形而上学概念有关。现代类型论在部分上是响应罗素悖论而发明的，并在伯特兰·罗素和 Alfred North Whitehead 的《数学原理》中起到重要作用。

在计算机科学分支中的编程语言理论中，类型论提供了设计分析和研究类型系统的形式基础。实际上，很多计算机科学家使用术语“类型论”来称呼对编程语言的类型语言的形式研究，尽管有些人把它限制于对更加抽象的形式化如有类型 lambda 演算的研究。

[编辑] 简单的类型论

下面的系统是 Mendelson 的(1997: 289-93) ST。量化的域被划分成上升的类型层次，带有所有的个体都被指派了一个类型。量化的变量确立范围只在一个类型上；所以底层逻辑是一阶逻辑。ST是"简单的" (相对于《数学原理》中的类型论)主要是因为任何关系的域和陪域的所有成员都必须是同一个类型的。

有一个最低的类型，它的个体没有成员并且是次最低类型的成员。最低类型的个体对应于特定集合论中的基本元素(urelement)。每个类型都有一个更高的类型，类似于在皮亚诺算术中后继者。ST 对是否有极大类型保持沉默，形成超限数个类型没有困难。这些因素，和回应于皮亚诺公理，使它方便和习惯于指派自然数到每个类型，开始于 0 给最低类型。这个类型论不要求自然数的先决定义。

ST 的特有符号是加右上角标的变量和中缀 $\in$ 。在任何给定的公式中，无角标的变量都有相同的类型，而有角标的变量( $x'$ )取值于更高的类型上。ST 的原子公式与两种形式， $x = y$ (同一性) 和 $y \in x'$ 。中缀符号 $\in$ 暗示了预想的释义，集合成员关系。

出现在同一性定义和外延和概括公理中所有变量都取值于连贯的两个类型之上。一个"低层"类型和另一个"高层"类型。取值于高层类型上的变量加角标；而取值于低层类型的变量不加。ST的一阶公式化排除在类型上的量化。所以每对连续的类型都要求它自己的外延和概括公理，如果“外延”和“概括”公理采用公理模式的方式取值于类型上就是可能的。

同一性定义: $x=y \Leftrightarrow \forall z' [x \in z' \leftrightarrow y \in z']$ 。

外延公理模式: $\forall x[x \in y' \leftrightarrow x \in z'] \Rightarrow y'=z'$ 。

设 Φ(x) 表示包含自由变量 x 的任何一阶公式。

概括公理模式: $\exists z' \forall x[x \in z' \leftrightarrow \Phi(x)]$ 。

备注: 相同类型的元素的任何搜集都可以形成更高类型的一个对象。概括公理有关于 $Φ(x)$ 也有关于类型。

无穷公理。存在着在最低层类型的个体之上的非空二元关系 R，它是反自反的、传递的和强连接的( $\forall x ,y [xRy \lor yRx]$ )。

备注: 无穷公理是 ST 的唯一真正的，并且本质上完全是数学的公理。R 也是一个严格全序，带有同一的域和陪域。如果 0 被指派给最低层类型(依次 1 是对(双元素集合，单元素集合)，2 是有序对)，R 的类型是 3。这个公理强迫一个无穷集合的存在，因为只有 R 的(陪)域是无穷的时候它才可以被满足。如果关系以有序对的方式定义，这个公理要求有序对的先决定义； ST 接受 Kuratowski 的定义。文献没有给出 ZFC 和其他集合论的无穷公理(存在归纳集合)不能结合于 ST 的理由。

ST 披露了类型论可以制定得何其类似于公理化集合论。而 ST 更加精致的本体论，根源于现在所谓的“集合的迭代构想”，导致了远比有着更简单的本体论的常规集合论如ZFC简单得多的公理(模式)。公理化集合论起步于类型论，但是它的公理、本体论和术语不同于上面所述 ST 系统，还包括新基础和Scott-Potter 集合论。

[编辑] 参见

[编辑] 进一步阅读

Andrews, Peter B., 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, 2nd ed. Kluwer Academic Publishers.
Cardelli, Luca, 1997, "Type Systems," in Allen B. Tucker, ed., The Computer Science and Engineering Handbook. CRC Press: 2208-2236.
Mendelson, Elliot, 1997. Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
Pierce, Benjamin, 2002. Types and Programming Languages. MIT Press. ISBN 0-262-16209-1)
Thompson, Simon, 1991. Type Theory and Functional Programming. Addison-Wesley. ISBN 0-201-41667-0.
Winskel, Glynn, 1993. The Formal Semantics of Programming Languages, An Introduction. MIT Press. ISBN 0-262-23169-7.

[编辑] 外部链接

Stanford Encyclopedia of Philosophy: Type Theory" -- by Thierry Coquand.
National Institute of Standards and Technology: Abstract data type
A summary paper on the formal basis of ADTs, relationship to category theory, and list of good references. Pages 3-4 appear relevant. Reference number [6] looks good, but it may not be available online.
Constable, Robert L., 2002, "Naïve Computational Type Theory," in H. Schwichtenberg and R. Steinbruggen (eds.), Proof and System-Reliability: 213-259.
The Nuprl Book: "Introduction to Type Theory."