类型论
维基百科,自由的 encyclopedia
类型论,数学、逻辑和电脑科学以下的一个分支,是研究不同类型系统及其表达形式的学科。某些类型系统适合用作数学基础,取代数学家一般使用的集合论,其中最具影响力的有阿隆佐·邱奇的有类型λ演算和佩尔·马丁-洛夫的直觉类型论。许多函数语言和电脑协助定理验证(英语:Proof assistant)工具都建立在类型论的基础上,如Agda、Coq、Idris、Lean等等。
类型论的核心概念是,每一条合乎语法规则的表达式(或称“项”)都有其所属的“类型”。通过结合多个基础类型,可以定义更加复杂的类型。如此得出的类型可以代表林林总总的数学结构,如自然数、群、拓扑空间等等。在集合论中,这些结构都是含有元素(或称成员)的集合,它的定义纯粹就是指定其所含的所有元素。在类型论中,这些结构的定义并不罗列属于它的所有项,而是指定如何建构它的项的一套规则。
集合论建基于一阶逻辑,有“集合”和“命题”两个主要概念。任何一套集合论公理(如策梅洛-弗兰克尔集合论)和命题都是以一阶逻辑的语言所表达。类型论则只有“类型”的概念,每一条逻辑命题都是一个类型。要证明任何一条命题,就需要建构属于此类型的项,是为命题为类型原理。换言之,证明定理的过程只不过是建构符合指定数学结构的数学对象的过程的一个特例。[1]