查看“︁有类型λ演算”︁的源代码

{{Unreferenced|time=2017-04-05T18:16:07+00:00}}
{{NoteTA
|G1 = IT
}}
'''有类型lambda演算'''是使用lambda符号（<math>\lambda</math>）指示[[匿名函数]]抽象的一种有类型的形式化。有类型lambda演算是基础[[编程语言]]并且是有类型的[[函数式编程语言]]如[[ML语言|ML]]和[[Haskell]]和更间接的[[指令式编程语言]]的基础。它们通过[[Curry-Howard同构]]密切关联于[[直觉逻辑]]并可以被认为是[[范畴论 (数学)|范畴]]的类的内部语言，比如简单类型lambda演算是[[笛卡儿闭范畴|笛卡尔闭范畴]]（CCC）的语言。

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

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

某些有类型lambda演算介入“[[子类型]]”的概念，就是说如果<math>A</math>是<math>B</math>的子类型，则类型<math>A</math>的所有项也有类型<math>B</math>。带有子类型的有类型lambda演算是带有合取类型和<math>F^\leq</math>（F-sub）的简单类型lambda演算。

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

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

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

==参见==
*[[简单类型lambda演算]]
*[[系统F]]
*[[逻辑框架]]
*[[构造演算]]
*[[直觉类型论]]

[[Category:Lambda演算]]
[[Category:类型论]]