直觉类型论
維基百科,自由的 encyclopedia
直觉类型论(英語:Intuitionistic type theory),也可简称类型论,此外也有构造类型论或马汀-洛夫类型论称呼。是基于数学构造主义的函数式编程语言、逻辑和集合论。
直觉类型论由瑞典数学家和哲学家 佩尔·马丁-洛夫于1972年引入。此前马丁已经多次修改了他的提议,先是非直谓性的而后是直谓性的,先是外延的而后是内涵的类型论变体。直觉类型论基于的是命题和等价类的同一一个命题同一于它的证明的类型。这种同一通常叫做柯里-霍华德同构,它最初公式化了命题逻辑和简单类型λ演算。
类型论通过介入包含着值的依赖类型把这种同一扩展到谓词逻辑。类型论内在化了 鲁伊兹·布劳威尔、阿兰德·海廷 和 安德雷·柯爾莫哥洛夫提议的布劳威尔-海廷-柯尔莫哥洛夫释义的直觉逻辑释义。类型论的类型扮演了类似于集合在集合论的角色,但是在类型论中的函数总是可计算的。