Λ演算

解释与应用

λ演算是图灵完全的，也就是说，这是一个可以用于模拟任何图灵机的通用模型。 λ也被用在λ表达式和λ项中，用来表示将一个变量绑定在一个函数上。
λ演算可以是有类型或者无类型的，在有类型λ演算中（上文所述是无类型的），函数只能在参数类型和输入类型符合时被应用。有类型λ演算比无类型λ演算要弱——后者是这个条目的主要部分——因为有类型的λ运算能表达的比无类型λ演算少；与此同时，前者使得更多定理能被证明。例如，在简单类型λ演算中，运算总是能够停止，然而无类型λ演算中这是不一定的（因为停机问题）。当前有许多种有类型λ演算的一个原因是它们被期望能做到更多（做到某些以前的有类型λ演算做不到的）的同时又希望能用以证明更多定理。
λ演算在数学、哲学、语言学和计算机科学中都有许多应用。它在编程语言理论中占有重要地位，函数式编程实现了λ演算支持。λ演算在范畴论中也是一个研究热点。

历史

作为对数学基础研究的一部分，数学家阿隆佐·邱奇在20世纪30年代提出了λ演算。 但最初的λ演算系统被证明是逻辑上不自洽的——在1935年Stephen Kleene和J. B. Rosser举出了Kleene-Rosser悖论。
随后，在1936年邱奇把那个版本的关于计算的部分抽出独立发表—现在这被称为无类型λ演算。 在1940年，他创立了一个计算能力更弱但是逻辑上自洽的的系统，这被称为简单类型λ演算。
直到1960年，λ演算与编程语言的关系被确立了；在这之前它只是一个范式。由于Richard Montague和其他语言学家将λ演算应用于自然语言语法的研究，λ演算已经开始在语言学和计算机科学学界拥有一席之地。

lambda演算

lambda演算是由特定形式语法所组成的一种语言，一组转换规则可操作其中的lambda项。这些转换规则被看作是一个等式理论或者一个操作定义。如上节所述，lambda演算中的所有函数都是匿名的，它们没有名称，它们只接受一个输入变量，柯里化用于实现有多个输入变量的函数。

操作函数的函数

在lambda演算中，函数被认为是第一类对象，因此函数可以当作输入，或作为其它函数的输出返回。
例如，表示映射到本身的函数，和表示将这个函数应用于。此外，则表示无论输入为何，始终返回值的常量函数。lambda演算中的函数应用是左结合的，因此表示。
有几个“等价”和“化简”的概念，允许将各个lambda项“缩减”为“相同”的lambda项。

α
      
    
    {\displaystyle \alpha }
  
-等价

对于lambda项，等价的基本形式定义，是-等价。它捕捉了直觉概念，在lambda抽象中一个绑定变量的特别选择（通常）并不重要。
比如，和是-等价的lambda项，它们都表示相同的函数（自映射函数）；但如和项则不是-等价的，因为它们并非以lambda抽象方式绑定的。
在许多演示中，通常会确定-等价的lambda项。
为了能够定义-归约，需要以下定义：

β
      
    
    {\displaystyle \beta }
  
-归约

β-归约规定了形式如的应用，可以化简成项。符号记法用于表示 经过β-归约转换为。例如，对于每个，可转换为。这表明实际上的应用是映射自身函数。同样地，，表明了是一个常量函数。
lambda演算可视为函数式编程语言的理想化版本，如Haskell或ML语言。在这种观点下，β-归约对应于一组计算步骤。
这个步骤重复应用β-转换，一直到没有东西能再被化简。在无类型lambda演算中，如本文所述，这个归约过程可能无法终止，
比如，是个特殊的lambda项。这里

也就是说，该lambda项在一次β-归约中化简到本身，因此归约过程将永远不会终止。
无类型lambda演算的另一方面是它并不区分不同种类的数据。例如，需要编写只针对数字操作的功能。然而，在无类型的lambda演算中，没有办法避免函数被应用于真值、字符串或其它非数字对象。

η-变换

前两条规则之后，还可以加入第三条规则，eta-变换，来形成一个新的等价关系。Eta-变换表达的是外延性的概念，在这里外延性指的是，对于任一给定的参数，当且仅当两个函数得到的结果都一致，则它们将被视同为一个函数。Eta-变换可以令 和  相互转换，只要  不是  中的自由变量。下面说明了为何这条规则和外延性是等价的：
若  与  外延地等价，即， 对所有的 表达式成立，则当取 为在 中不是自由出现的变量时，我们有，因此 ，由eta-变换f == g。所以只要eta-变换是有效的，会得到外延性也是有效的。
相反地，若外延性是有效的，则由beta-归约，对所有的y有(λx .f x) y == f y，可得λx .f x == f，即eta-变换也是有效的。

数据类型的编码

基本的lambda算法可用于建构布尔值，算术，数据结构和递归的模型，如以下各小节所述。

lambda演算中的算术

在lambda演算中有许多方式都可以定义自然数，但最常见的还是邱奇数，下面是它们的定义：
0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))
以此类推。直观地说，lambda演算中的数字n就是一个把函数f作为参数并以f的n次幂为返回值的函数。换句话说，邱奇整数是一个高阶函数 -- 以单一参数函数f为参数，返回另一个单一参数的函数。
(注意在邱奇原来的lambda演算中，lambda表达式的形式参数在函数体中至少出现一次，这使得我们无法像上面那样定义0)在邱奇整数定义的基础上，我们可以定义一个后继函数，它以n为参数，返回n + 1：
SUCC = λn.λf.λx.f(n f x)
加法是这样定义的：
PLUS = λm.λn.λf.λx.m f (n f x)
PLUS可以被看作以两个自然数为参数的函数，它返回的也是一个自然数。你可以试试验证
PLUS 2 3 
与5是否等价。乘法可以这样定义：
MULT = λm.λn.m (PLUS n) 0,
即m乘以n等于在零的基础上m次加n。另一种方式是
MULT = λm.λn.λf.m (n f)
正整数n的前驱元（predecessesor）PRED n = n - 1要复杂一些：
PRED = λn.λf.λx.n(λg.λh.h(g f))(λu.x)(λu.u)
或者
PRED = λn.n(λg.λk.(g 1)(λu.PLUS(g k) 1) k)(λl.0) 0
注意(g 1)(λu.PLUS(g k) 1) k表示的是，当g(1)是零时，表达式的值是k，否则是g(k)+ 1。

附加的编程技术

lambda演算出现在相当大量的编程习惯用法中，其中许多编程语言最初以lambda演算作为语义基础，在此背景下开发的；有效地利用lambda演算作为基底。因为几个编程语言部分含括了lambda演算（或者非常相似的东西），所以这些技术也可以在实际的编程中见到，但有可能被认为是模糊或外来的。

可计算函数和lambda演算

自然数的函数F: N → N是可计算函数，当且仅当存在着一个lambda表达式f，使得对于N中的每对x, y都有F(x) = y当且仅当f x == y，这里的x和y分别是对应于x和y的邱奇数。这是定义可计算性的多种方式之一；关于其他方式和它们的等价者的讨论请参见邱奇-图灵论题。