有类型λ演算

维基百科,自由的百科全书
跳转至: 导航搜索

有类型 lambda 演算是使用 lambda 符号(\lambda)指示匿名函数抽象的一种有类型的形式化。有类型 lambda 演算是基础编程语言并且是有类型的函数式编程语言MLHaskell 和更间接的指令式编程语言的基础。它们通过 Curry-Howard同构密切关联于直觉逻辑并可以被认为是范畴的类的内部语言,比如简单类型 lambda 演算是笛卡尔闭范畴(CCC)的语言。

传统上,有类型 lambda 演算被看作无类型lambda演算的精细化。更现代的观点把有类型 lambda 演算看做更基础的理论,而把无类型 lambda 演算看作它的只有一个类型的特殊情况。

种类[编辑]

已经研究了各种有类型 lambda 演算。简单类型lambda演算的类型只是基本类型(或类型变量)和函数类型 \sigma\to\tau系统T 向简单类型 lambda 演算扩展了自然数类型和更高阶的原始递归函数;在这个系统中在可证明在皮亚诺算术中是递归函数的所有函数都是可定义的。系统F 通过在所有类型上的全称量化允许多态性;从逻辑的观点看它可以描述可证明在二阶逻辑中是全函数的所有函数。有依赖类型的 lambda 演算是直觉类型论构造演算逻辑框架(LF)的基础,它是带有依赖类型的纯 lambda 演算。基于 Berardi 的工作,Barendregt 提议了 Lambda立方体来系统化纯有类型 lambda 演算(包括简单类型 lambda 演算,系统 F,LF 和构造演算)之间的关系。

某些有类型 lambda 演算介入“子类型”的概念,就是说如果 AB 的子类型,则类型 A 的所有项也有类型 B。带有子类型的有类型 lambda 演算是带有合取类型和 F^\leq (F-sub) 的简单类型 lambda 演算。

迄今提到的所有西,除了无类型 lambda 演算是例外,都是“强规范化”的:所有计算都会终止。结论是他们作为逻辑都是自恰的,就是说这里有无居留(uninhabited)类型。但是存在着不是强规范化的有类型 lambda 演算。比如带有所有类型的一个类型(Type : Type)的依赖类型 lambda 演算由于Girard悖论而不是强规范化的。这个系统也是最简单的纯类型系统,它是推广 Lambda立方体的一种形式化。有明确的递归组合子的系统,比如 Gordon Plotkin 的 PCF,不是规范化的,但是它们不意图被解释为逻辑。实际上,PCF(可计算函数的编程语言)是元典型(prototypical)的有类型的函数式编程语言,这里的类型被用来确保程序是有良好行为的而不必須是终止的。

应用[编辑]

有类型 lambda 演算在为编程语言设计新类型系统的时候扮演了关键性角色;这里类型能力通常捕获了程序想要的性质,比如程序不会导致内存访问违规。

编程中,强类型编程语言的例程(函数,过程,方法)密切关联于有类型 lambda 表达式。Eiffel 有一个“内线代理”概念,使得有可能直接定义和操纵有类型 lambda 表达式,通过这种表达式如 agent (p: PERSON): STRING do Result := p.spouse.name end,指示表示返回一个人配偶的名字的一个函数的一个对象。

参见[编辑]