Λ演算 λ演算（英语：lambda calculus，λ-calculus）是一套从数学逻辑中发展，以变数绑定和替换的规则，来研究函式如何抽象化定义、函式如何被应用以及递回的形式系统。它由数学家阿隆佐·邱奇在20世纪30年代首次发表。lambda演算作为一种广泛用途的计算模型，可以清晰地定义什么是一个可计算函式，而任何可计算函式都能以这种形式表达和求值，它能模拟单一磁带图灵机的计算过程；尽管如此，lambda演算强调的是变换规则的运用，而非实现它们的具体机器。 lambda演算可比拟是最根本的编程语言，它包括了一条变换规则（变数替换）和一条将函式抽象化定义的方式。因此普遍公认是一种更接近软体而非硬体的方式。对函数式编程语言造成很大影响，比如Lisp、ML语言和Haskell语言。在1936年邱奇利用λ演算给出了对于判定性问题（Entscheidungsproblem）的否定：关于两个lambda运算式是否等价的命题，无法由一个「通用的演算法」判断，这是不可判定效能够证明的头一个问题，甚至还在停机问题之先。 lambda演算包括了建构lambda项，和对lambda项执行归约的操作。在最简单的lambda演算中，只使用以下的规则来建构lambda项： 产生了诸如：(λx.λy.(λz.(λx.zx)(λy.zy))(x y))的表达式。如果表达式是明确而没有歧义的，则括号可以省略。对于某些应用，其中可能包括了逻辑和数学的常量以及相关操作。 本文讨论的是邱奇的“无类型lambda演算”，此后，已经研究出来了一些有类型lambda演算。 解释与应用. λ演算是图灵完备的，也就是说，这是一个可以用于模拟任何图灵机的通用模型。 λ也被用在λ表达式和λ项中，用来表示将一个变量绑定在一个函数上。 λ演算可以是有类型或者无类型的，在有类型λ演算中（上文所述是无类型的），函数只能在参数类型和输入类型符合时被应用。有类型λ演算比无类型λ演算要弱——后者是这个条目的主要部分——因为有类型的λ运算能表达的比无类型λ演算少；与此同时，前者使得更多定理能被证明。例如，在简单类型λ演算中，运算总是能够停止，然而无类型λ演算中这是不一定的（因为停机问题）。目前有许多种有类型λ演算的一个原因是它们被期望能做到更多（做到某些以前的有类型λ演算做不到的）的同时又希望能用以证明更多定理。 λ演算在数学、哲学、语言学和计算机科学中都有许多应用。它在程式语言理论中占有重要地位，函数式编程实现了λ演算支持。λ演算在范畴论中也是一个研究热点。 历史. 作为对数学基础研究的一部分，数学家阿隆佐·邱奇在20世纪30年代提出了λ演算。 但最初的λ演算系统被证明是逻辑上不自洽的——在1935年斯蒂芬·科尔·克莱尼和J. B. Rosser举出了。 随后，在1936年邱奇把那个版本的关于计算的部分抽出独立发表—现在这被称为无类型λ演算。 在1940年，他创立了一个计算能力更弱但是逻辑上自洽的系统，这被称为简单类型λ演算。 直到1960年，λ演算与编程语言的关系被确立了；在这之前它只是一个范式。由于理查德·蒙塔古和其他语言学家将λ演算应用于自然语言语法的研究，λ演算已经开始在语言学和计算机科学学界拥有一席之地。 至于为何邱奇选择λ作为符号，连他本人的解释也互相矛盾：最初是在1964年的一封信中，他明确解释称这是来源于《数学原理》一书中的类抽象符号（脱字符），为了方便阅读，他首先将其换成逻辑与符号（formula_1）作为区分，然后又改成形状类似的λ。他在1984年又重申了这一点，但再后来他又表示选择λ纯粹是偶然。 非形式化的直觉描述. 在λ演算中，每个表达式都代表一个函数，这个函数有一个参数，并且会返回一个值。不论是参数和返回值，也都是一个单参的函数。可以这么说，λ演算中只有一种“类型”，那就是这种单参函数。函数是通过λ表达式匿名地定义的，这个表达式说明了此函数将对其参数进行什么操作。 例如，“加2”函数f(x)= x + 2可以用lambda演算表示为λx.x + 2（或者λy.y + 2，参数的取名无关紧要），而f(3)的值可以写作(λx.x + 2) 3。函数的应用（application）是左结合的：f x y =(f x) y。 考虑这么一个函数：它把一个函数作为参数，这个函数将被作用在3上：λf.f 3。如果把这个（用函数作参数的）函数作用于我们先前的“加2”函数上：(λf.f 3)(λx.x+2)，则明显地，下述三个表达式： (λf.f 3)(λx.x+2) 与 (λx.x + 2) 3 与 3 + 2 是等价的。有两个参数的函数可以通过lambda演算这样表达：一个单一参数的函数，它的返回值又是一个单一参数的函数（参见柯里化）。例如，函数f(x, y) = x - y可以写作λx.λy.x - y。下述三个表达式： (λx.λy.x - y) 7 2 与 (λy.7 - y) 2 与 7 - 2 也是等价的。然而这种lambda表达式之间的等价性，无法找到某个通用的函数来判定。 并非所有的lambda表达式都能被归约至上述那样的确定值，考虑 (λx.x x)(λx.x x) 或 (λx.x x x)(λx.x x x) 然后试图把第一个函数作用在它的参数上。(λx.x x)被称为ω 组合子，((λx.x x)(λx.x x))被称为Ω，而((λx.x x x) (λx.x x x))被称为Ω2，以此类推。若仅形式化函数作用的概念而不允许lambda表达式，就得到了组合子逻辑。 动机. 在数学和计算机科学中，「可计算的」函式是基础观念。对于所谓的可计算性，λ-演算提供了一个简单明确的语义，使计算的性质可以被形式化研究。λ-演算结合了两种简化方式，使得这个语义变得简单。第一种简化是不给予函式一个确定名称，而“匿名”地对待它们。例如，两数的平方和函式 formula_2 可以用匿名的形式重新写为： formula_3（理解成一包含x和y的数组被映射到formula_4） 同样地， formula_5 可以用匿名的形式重新写为： formula_6（即输入是直接对应到它本身。） 第二个简化是λ演算只使用单一个参数输入的函数。如果普通函数需要两个参数，例如formula_7函数，可转成接受单一参数，传给另一个函数中介，而中介函数也只接受一个参数，最后输出结果。例如， formula_3 可以重新写成： formula_9 这是称为柯里化的方法，将多参数的函数转换成为多个中介函数的复合链，每个中介函数都只接受一个参数。 将formula_7函数应用于参数(5,2)，直接产生结果 formula_11 formula_12 formula_13, 而对于柯里化转换版的评估，需要再多一步： formula_14 formula_15 //在内层表达式中formula_16的定义为formula_17，这就像β-归约一样。 formula_18 //formula_19的定义为formula_20，再次如同β-归约。 formula_13 得出相同结果。 lambda演算. lambda演算是由特定形式语法所组成的一种语言，一组转换规则可操作其中的lambda项。这些转换规则被看作是一个等式理论或者一个操作定义。如上节所述，lambda演算中的所有函数都是匿名的，它们没有名称，它们只接受一个输入变量，柯里化用于实现有多个输入变量的函数。 lambda项. lambda演算的语法将一些表达式定义为有效的lambda演算式，而某一些表达式无效，就像C编程语言中有些字串有效，有些则不是。有效的lambda演算式称为“lambda项”。 以下三个规则给出了语法上有效的lambda项，如何建构的归纳定义： 其它的都不是lambda项。因此，lambda项若且唯若可重复应用这三个规则取得时，才是有效的。一些括号根据某些规则可以省略。例如，最外面的括号通常不会写入。 “lambda抽象”是指一个匿名函数的定义，它将单一输入的formula_29替换成formula_23的表达式，所以产生了一个匿名函数，它采用formula_16的值并返回formula_23。例如，formula_33是表示使用函数formula_34作为formula_23项的一个lambda抽象。lambda抽象只是先“设置”了函数定义，还没使用它。这个抽象在formula_23项中绑定了变量formula_16。一个应用formula_38表示将函数formula_23应用在输入formula_27，亦即对输入formula_27使用函数formula_23产生formula_43。 lambda演算中并没有变量声明的概念。如formula_44（即formula_45）的定义中，lambda演算将formula_19当作尚未定义的变量。lambda抽象formula_47在语法上是有效的，并表示将其输入添加到未知formula_19的函数。 可用圆括弧对来消除歧义。例如，formula_49和formula_50表示不同的项（尽管它们刚好化简到相同值）。这里第一个例子定义了一个包含子函数的抽象，并将子函数应用于x（先应用后传回）的结果；而第二个例子定义了一个传回任何输入的函数，然后在应用过程中传回对输入为x的应用（返回函数然后应用）。 操作函数的函数. 在lambda演算中，函数被认为是头等物件，因此函数可以当作输入，或作为其它函数的输出返回。 例如，formula_51表示映射到本身的函数，formula_6和formula_53表示将这个函数应用于formula_19。此外，formula_55则表示无论输入为何，始终返回formula_19值的常数函数formula_57。lambda演算中的函数应用是左结合的，因此formula_58表示formula_59。 有几个“等价”和“化简”的概念，允许将各个lambda项“缩减”为“相同”的lambda项。 α-等价. 对于lambda项，等价的基本形式定义，是formula_60-等价。它捕捉了直觉概念，在lambda抽象中一个绑定变量的特别选择（通常）并不重要。 比如，formula_51和formula_62是formula_60-等价的lambda项，它们都表示相同的函数（自映射函数）；但如formula_16和formula_19项则不是formula_60-等价的，因为它们并非以lambda抽象方式绑定的。 在许多演示中，通常会确定formula_60-等价的lambda项。 为了能够定义formula_68-归约，需要以下定义： 自由变量. 所谓的自由变量是那些在lambda抽象不受到绑定的变量。表达式中的一组自由变量定义归纳如下： 例如，代表映射自身的formula_51，其中的lambda项没有自由变量，但是在函数formula_78中的lambda项，有一个自由变量formula_19。 避免捕获的替换记法. 假设formula_23，formula_27和formula_82是lambda项，而formula_16和formula_19是变量。如果写成formula_85是一种"避免被捕获"的记法方式，表示在formula_23这个lambda项中，以formula_82来替换formula_16变量的值。这定义为： 例如，formula_100 和formula_101。 新鲜度条件（要求formula_19不在lambda项formula_82中的自由变量中）对于确保替换不会改变函数的意义很重要。例如，忽视新鲜度条件的替代：formula_104。此替换会将原本意义为常量函数的formula_105，转换成意义为映射自身函数的formula_51。 一般来说，在无法满足新鲜度条件的情况，可利用formula_60-重新命名使用一个合适的新变量来补救，切换回正确的替换概念；比如在formula_108中，使用一个新变量formula_109重新命名这个lambda抽象，获取formula_110，则替换就能保留原本函数的义涵。 β-归约. β-归约规定了形式如formula_111的应用，可以化简成formula_112项。符号记法formula_113用于表示formula_114 经过β-归约转换为formula_115。例如，对于每个formula_27，可转换为formula_117。这表明formula_118实际上的应用是映射自身函数。同样地，formula_119，表明了formula_120是一个常量函数。 lambda演算可视为函数式编程语言的理想化版本，如Haskell或ML语言。在这种观点下，β-归约对应于一组计算步骤。 这个步骤重复应用β-转换，一直到没有东西能再被化简。在无型别lambda演算中，如本文所述，这个归约过程可能无法终止， 比如formula_121，是个特殊的lambda项。这里 formula_122 也就是说，该lambda项在一次β-归约中化简到本身，因此归约过程将永远不会终止。 无型别lambda演算的另一方面是它并不区分不同种类的资料。例如，需要编写只针对数字操作的功能。然而，在无型别的lambda演算中，没有办法避免函数被应用于真值、字串或其它非数字物件。 形式化定义. 形式化地，我们从一个标识符（identifier）的可数无穷集合开始，比如{a, b, c, ..., x, y, z, x1, x2, ...}，则所有的lambda表达式可以通过下述以BNF范式表达的上下文无关文法描述： 头两条规则用来生成函数，而第三条描述了函数是如何作用在参数上的。通常，lambda抽象（规则2）和函数作用（规则3）中的括弧在不会产生歧义的情况下可以省略。如下假定保证了不会产生歧义：（1）函数的作用是左结合的，和（2）lambda操作符被绑定到它后面的整个表达式。例如，表达式 (λx.x x)(λy.y) 可以简写成λ(x.x x) λy.y 。 类似λx.(x y)这样的lambda表达式并未定义一个函数，因为变量y的出现是自由的，即它并没有被绑定到表达式中的任何一个λ上。一个lambda表达式的自由变量的集合是通过下述规则（基于lambda表达式的结构归纳地）定义的： 例，对于表达式λx.x（我们将第一个x视作变量，第二个x视作表达式），其中表达式x中，由1，它的自由变量集合是x，又由2，表达式λx.x的自由变量的集合是表达式x的自由变量集合减去变量x。所以对于表达式λx.x，它的自由变量集合是空。 例，对于表达式λx.x x由形式化描述的第3点，我们把它看作((λx.x)(x))，(λx.x)和(x)分别为表达式，由上一例知道(λx.x)的自由变量集合为空，表达式(x)的变量集合为变量x，所以对于λx.x x，它的自由变量集合为x与空的并，即x。 在lambda表达式的集合上定义了一个等价关系(在此用==标注)，“两个表达式其实表示的是同一个函数”这样的直觉性判断即由此表述，这种等价关系是通过所谓的“alpha-变换规则”和“beta-归约规则”。 归约. 归约的操作包括： α-变换. Alpha-变换规则表达的是，被绑定变量的名称是不重要的。比如说λx.x和λy.y是同一个函数。尽管如此，这条规则并非像它看起来这么简单，关于被绑定的变量能否由另一个替换有一系列的限制。 Alpha-变换规则陈述的是，若V与W均为变量，E是一个lambda表达式，同时E[V:=W]是指把表达式E中的所有的V的自由出现都替换为W，那么在W不是 E中的一个自由出现，且如果W替换了V，W不会被E中的λ绑定的情况下，有 λV.E == λW.E[V:=W] 这条规则告诉我们，例如λx.(λx.x) x这样的表达式和λy.(λx.x) y是一样的。 β-归约. Beta-归约规则表达的是函数作用的概念。它陈述了若所有的E'的自由出现在E [V:=E']中仍然是自由的情况下，有 ((λV.E) E') == E [V:=E'] 成立。 ==关系被定义为满足上述两条规则的最小等价关系（即在这个等价关系中减去任何一个映射，它将不再是一个等价关系）。 对上述等价关系的一个更具操作性的定义可以这样获得：只允许从左至右来应用规则。不允许任何beta归约的lambda表达式被称为Beta范式。并非所有的lambda表达式都存在与之等价的范式，若存在，则对于相同的形式参数命名而言是唯一的。此外，有一个算法用户计算范式，不断地把最左边的形式参数替换为实际参数，直到无法再作任何可能的规约为止。这个算法当且仅当lambda表达式存在一个范式时才会停止。Church-Rosser定理说明了，当且仅当两个表达式等价时，它们会在形式参数换名后得到同一个范式。 η-变换. 前两条规则之后，还可以加入第三条规则，eta-变换，来形成一个新的等价关系。Eta-变换表达的是外延性的概念，在这里外延性指的是，对于任一给定的参数，当且仅当两个函数得到的结果都一致，则它们将被视同为一个函数。Eta-变换可以令 formula_123 和 formula_124 相互转换，只要 formula_16 不是 formula_124 中的自由变量。下面说明了为何这条规则和外延性是等价的： 若 formula_124 与 formula_128 外延地等价，即，formula_129 对所有的 formula_130 表达式 formula_131成立，则当取 formula_131 为在 formula_124 中不是自由出现的变量 formula_16时，我们有formula_135，因此 formula_136，由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 注意codice_1表示的是，当codice_2是零时，表达式的值是codice_3，否则是codice_4。 逻辑与谓词. 习惯上，下述两个定义（称为邱奇布尔值）被用作TRUE和FALSE这样的布尔值： TRUE := λx.λy.x FALSE := λx.λy.y (注意FALSE等价于前面定义邱奇数零) 接着，通过这两个λ-项，我们可以定义一些逻辑运算： AND := λp q.p q FALSE OR := λp q.p TRUE q NOT := λp.p FALSE TRUE IFTHENELSE := λp x y.p x y 我们现在可以计算一些逻辑函数，比如： AND TRUE FALSE ≡(λp q.p q FALSE) TRUE FALSE →β TRUE FALSE FALSE ≡(λx y.x) FALSE FALSE →β FALSE 我们见到AND TRUE FALSE等价于FALSE。 “谓词”是指返回布尔值的函数。最基本的一个谓词是ISZERO，当且仅当其参数为零时返回真，否则返回假： ISZERO := λn.n (λx.FALSE) TRUE 运用谓词与上述TRUE和FALSE的定义，使得"if-then-else"这类语句很容易用lambda演算写出。 有序对. 有序对（2-元组）数据类型可以用TRUE、FALSE和IF来定义。 CONS := λx y.λp.IF p x y CAR := λx.x TRUE CDR := λx.x FALSE 链表数据类型可以定义为，要么是为空列表保留的值（e.g.FALSE），要么是CONS一个元素和一个更小的列表。 附加的编程技术. lambda演算出现在相当大量的编程习惯用法中，其中许多编程语言最初以lambda演算作为语义基础，在此背景下开发的；有效地利用lambda演算作为基底。因为几个编程语言部份含括了lambda演算（或者非常相似的东西），所以这些技术也可以在实际的编程中见到，但有可能被认为是模糊或外来的。 命名常数. 在lambda演算中，函式库将采用预先定义好的函数集合，其中lambda项仅仅是特定的常量。纯粹的lambda演算法并不具有命名常数的概念，因为所有的原子λ项都是变量；但是在程序主体中，我们可将一个变量当成常量的名称，利用lambda抽象把这个变量绑定，并将该lambda抽象应用于预期的定义，来模拟命名常量的作法。因此在"N"（“主程序”的另一个lambda项）中，要以"f"来表示"M"（一些明确的lambda项），则写成如下： (λ"f"."N") "M" 作者经常引入类似如let的语法糖，允许以更直观的次序撰写上述内容： let "f" = "M" in "N" 通过等号链接这个命名常数，即可将lambda演算“编程”的一个lambda项，写为零或多个函数的定义，而使用构成程序主体的那些函数。这个let显著的限制，是在"M"中并没有定义"f"名称，因为"M"不在绑定"f"的lambda抽象范畴之内；这意味著递归函数定义不能以let来使用"M"。更进步的letrec语法糖允许以直觉的方式编写递归函数定义，而不需用到不动点组合子。 递归与不动点. 递归是使用函数自身的函数定义；在表面上，lambda演算不允许这样。但是这种印象是误解。考虑个例子，阶乘函数f(n)递归的定义为 f(n):= if n = 0 then 1 else n·f(n-1)。 在lambda演算中，你不能定义包含自身的函数。要避免这样，你可以开始于定义一个函数，这里叫g，它接受一个函数f作为参数并返回接受n作为参数的另一个函数： g := λf n.(if n = 0 then 1 else n·f(n-1))。 函数g返回要么常量1，要么函数f对n-1的n次应用。使用ISZERO谓词，和上面描述的布尔和代数定义，函数g可以用lambda演算来定义。 但是，g自身仍然不是递归的；为了使用g来建立递归函数，作为参数传递给g的f函数必须有特殊的性质。也就是说，作为参数传递的f函数必须展开为调用带有一个参数的函数g -- 并且这个参数必须再次f函数! 换句话说，f必须展开为g(f)。这个到g的调用将接着展开为上面的阶乘函数并计算下至另一层递归。在这个展开中函数f将再次出现，并将被再次展开为g(f)并继续递归。这种函数，这里的f = g(f)，叫做g的不动点，并且它可以在lambda演算中使用叫做悖论算子或不动点算子来实现，它被表示为Y -- Y组合子： Y = λg.(λx.g(x x))(λx.g(x x)) 在lambda演算中，Y g是g的不动点，因为它展开为g(Y g)。现在，要完成我们对阶乘函数的递归调用，我们可以简单的调用 g(Y g)n，这里的n是我们要计算它的阶乘的数。 比如假定n = 5，它展开为： (λn.(if n = 0 then 1 else n·((Y g)(n-1)))) 5 if 5 = 0 then 1 else 5·(g(Y g，5-1)) 5·(g(Y g)4) 5·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 4) 5·(if 4 = 0 then 1 else 4·(g(Y g，4-1))) 5·(4·(g(Y g)3)) 5·(4·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 3)) 5·(4·(if 3 = 0 then 1 else 3·(g(Y g，3-1)))) 5·(4·(3·(g(Y g)2))) 等等，递归的求值算法的结构。所有递归定义的函数都可以看作某个其他适当的函数的不动点，因此，使用Y所有递归定义的函数都可以表达为lambda表达式。特别是，我们现在可以明晰的递归定义自然数的减法、乘法和比较谓词。 标准化的组合子名称. 某一些lambda项有普遍接受的名称： I := λ"x"."x" K := λ"x".λ"y"."x" S := λ"x".λ"y".λ"z"."x" "z" ("y" "z") B := λ"x".λ"y".λ"z"."x" ("y" "z") C := λ"x".λ"y".λ"z"."x" "z" "y" W := λ"x".λ"y"."x" "y" "y" U := λ"x".λ"y"."y" ("x" "x" "y") ω := λ"x"."x" "x" Ω := ω ω Y := λ"g".(λ"x"."g" ("x" "x")) (λ"x"."g" ("x" "x")) 其中有几个在“消除lambda抽象”中有直接的应用，将lambda项变为组合演算的术语。 消除lambda抽象. 如果"N"是一个没有λ-抽象的lambda项，但可能包含了命名常量（组合子），则存在一个lambda项"T"("x","N")，这相同于一个缺少λ-抽象（除了作为命名常量的一部份，如果这些被认为是非原子的）的λ"x"."N"；也可以被视为匿名变量，就如同"T"("x","N")从"N"之中删除所有出现的"x"，同时仍然允许在"N"包含"x"的位置替换参数值。 转换函数"T"可由下式定义： "T"("x", "x") := I "T"("x", "N") := K "N" if "x" is not free in "N". "T"("x", "M" "N") := S "T"("x", "M") "T"("x", "N") 在这两种情况下，形式"T"("x","N")"P"可借由使初始的组合子I，K或S获取参数"P"而化简， 就像(λ"x"."N") "P"经过β-归约一样。I返回那个参数。K则将参数抛弃，就像(λ"x"."N")，如果"x"在"N"中不是以自由变量出现。S将参数传递给应用程序的两个子句，然后将第一个结果应用到第二个的结果之上。 组合子B和C类似于S，但把参数传递给应用的一个子项（B传给“参数”子项，而C传给“函数”子项），如果子项中没有出现"x"，则保存后续的K。与B和C相比，S组合子实际上混合了两个功能： 重新排列参数，并复制一个参数，以便它可以在两个地方使用。W组合子只做后者，产生了SKI组合子演算的B，C，K，W系统。 可计算函数和lambda演算. 自然数的函数F: N → N是可计算函数，当且仅当存在着一个lambda表达式f，使得对于N中的每对x, y都有F(x) = y当且仅当f x == y，这里的x和y分别是对应于x和y的邱奇数。这是定义可计算性的多种方式之一；关于其他方式和它们的等价者的讨论请参见邱奇-图灵论题。 lambda演算与编程语言. 匿名函数. 比如计算平方的函数 square 在 Lisp 中可以表示为如下的 lambda 表达式 符号 lambda 创建一个匿名函数，给定参数列表 (x) ，以及一个作为函数体的表达式 (* x x)。 匿名函数有时称为 lambda 表达式。 很多命令式语言都有函数指针或者类似的机制。但是函数指针并不是类型中的一等公民，函数是一等公民当且仅当函数可以在运行时创建。 下面一些语言支持函数的运行时创建： Smalltalk、 JavaScript、 Kotlin、 Scala、 Python3、 C# ("delegates")、 C++11等。