译者注：
      本文译自Raúl Rojas, A Tutorial Introduction to the Lambda Calculus, Freie Universität Berlin, WS-97/98。囿于译者自身能力，本文注定存在诸多错误，望方家斧正。

/******************************

************************

******************************** 废话与译文的分割线 

*****************************

************************

********************************/

Lambda算子简介

此论文是一篇简短无痛的lambda算子简介。lambda算子最初为了研究有效可计算函数的某些数学特性而作，此形式已经为函数编程语言族供了一个强大的理论基础。在此演示了使用lambda演算子实行某些数学运算的方法以及定义递归函数的方法，尽管lambda演算子中的函数是匿名的并且因此它们不能被显示引用，我们仍然可以定义递归函数。


1  定义

lambda演算子可以说是世界上最小的通用编程语言。lambda演算子由一个单一转换规则(变量替换)和一个单一函数定义系统构成。它在1930年代被Alonzo Church作为一个方法引入有效计算能力的概念的形式化中。lambda演算子是通用的是因为任意可计算函数可以使用此形式表达和求值。因此它等价与图灵机。但是，lambda演算子强调的是对转换规则的使用而且不关心实际机器对其实现的方式。这是一个更接近软件而不是硬件的方法。

lambda演算子的核心概念是“表达式”。一个“名字”，也被叫做“变量”，是一个标示符，它可以是任意字母a, b, c... 表达式被第归的定义如下：

 <expression>   := <name> | <function> | <application>
      <function>   := λ <name>.<expression>
 <application>    := <expression><expression>

为了清晰，可以使用括号包围表达式，也就是说，如果E是一个表达式，那么(E)是同一个表达式。“

λ”和“.”是这个语言里仅有的表达式。为了避免使用过多括号，我们采用函数左结合的习惯，也就是说，表达式：

E1E2E3En

采用以下方式求值：

(((E1E2)E3)En)

就像可以被从

前文出现的lambda表达式的定义看出来的一样，一个单独的标示符就是一个lambda表达式。下面是一个函数的例子：

λx.x

这个表达式定义了单位函数。

λ后的名字是这个函数参数的标示符。点后的表达式(在这个例子里是一个单独的x)叫做定义的函数体。
函数可以作用于表达式。一个程序的例子是：

(λx.x)y

这就是单位函数作用于y。括号的作用是使程序清晰，避免二义性。函数程序以替换函数体内参数x的值(在这个例子里是y)的方式被求值，例如：

(λx.x)y = [y/x]x = y

这个转换中记号[y/x]表示在右边的表达式中所有出现的x都被替换成y。

函数定义中参数的名字本身没有任何意义。它们仅仅是“占位符”，也就是说，当函数被求值时它们被用于指定重新安排函数参数的方法。因此

(λz.z) ≡ (λy.y) ≡ (λt.t) ≡ (λu.u)

等等。我们使用符号“

≡“表示如果A 

≡ B成立，那么A仅仅是B的一个别名。

1.1 自由与受限变量在lambda算子里所有的名字对于定义来说都是局部的。在函数

λx.x里我们说x是受限的因为它出现在函数体里之前，先出现了λx。没有跟在

λ之后出现的名字叫做自由变量。在表达式
中x是受限变量，y是自由变量。在表达式

(λx.x)(λy.yx)

中，左边表达式函数体中的x受限于左边的

λ。右边表达式函数体中的y受限于右边的

λ，而x是自由变量。非常重要的一点是，右边表达式中的x与左边表达式中的x完全无关。

正式的，当以下3个条件之一成立时，我们说变量<name>在一个表达式中是自由变量：

• <name>在<name>中是自由变量。
• 如果<name>≠<name1>并且<name>在<exp>中是自由变量，那么<name>在
  λ<name1>.<exp>中是自由变量。
• 如果<name>在E_1，E₂两者之一中是自由变量，那么<name>在
  E₁E₂中是自由变量。

当以下2个条件之一成立时，<name>是受限变量：

• 如果<name>=<name1>或者<name>在<exp>中是受限变量，那么<name>在
  λ<name1>.<exp>中是受限变量。
• 如果<name>在E_1，E₂两者之一中是
  受限变量，那么<name>在
  E₁E₂中是
  受限变量。

必须强调的是，同一个变量在同一个表达式中可能同时是自由变量和受限变量。在表达式：

(λx.xy)(λy.y)

中左边表达式中的y是自由变量，右边表达式中的y是受限变量。因此在整个表达式中y既是自由变量又是受限变量。

1.2 替换
lambda算子更令人费解的部分，对于第一次接触它的人来说，是我们没有给函数起名字这个事实。当我们想要使用一个函数的时候，我们写出整个函数，然后对它求值。为了简化这些符号，我们使用大写字母，数字和其它符号作为某些函数的别名。举例来说，单位函数(

λx.x)可以被记作I。

单位函数作用于它自身的程序是：

II ≡ (λx.x)(λx.x)

这个表达式里左边括号里的x与右边括号里的x是相互独立的。事实上我们可以把上面的表达式重写为：

II ≡ (λx.x)(λz.z)

单位函数作用于它自身

II ≡ (λx.x)(λz.z)

替换为

[λz.z/x]x = λz.z ≡ I

也就是单位函数本身。

做替换时我们必须小心地避免搞混自由变量和受限变量。在表达式：

(λx.(λy.xy))y

中，内嵌的

lambda表达式包含一个受限的y变量，而整个表达式最右边的y是自由变量。不正确的替换可能会搞混这两个变量而导致错误结果：

(λy.yy)

简单的将受限的y变量改名为t我们可以得到：

(λx.(λt.xt))y = (λt.yt)

这是正确的结果，与上一个完全不同。

因此，如果函数

λx.<exp>作用于E，我们用E替换所有<exp>中出现的自由变量x。如果替换引入了

一个E中的与<exp>中某个受限变量重名的自由变量，我们在替换之前先改掉<exp>中受限变量的名字。举例来说，在表达式：

(λx.(λy.(x(λx.xy))))y

中，我们应该把最外层lambda表达式的参数x替换成y。在函数体：

(λy.(x(λx.xy)))

中，仅有第一个x是自由变量，可以被替换。然而在替换之前，我们须要改变变量y的名字以避免它和自由变量冲突:

[y/x](λt.(x(λx.xt))) = (λt.(y(λx.xt)))

按照一般的化简顺序我们总是尝试从一个程序最左边的表达式开始，直到无法进一步化简。


2 算术

我们期望编程语言可以做算术运算。可以使用lambda演算子表示数字，从0开始，然后“suc(zero)”表示1，“suc(suc(zero))”表示2，等等。使用lambda演算子我们唯一能做的事是定义新函数。数字将会用以下方法先函数一样被定义：0被定义为：

λs.(λz.z)

这个函数接受两个参数s和z，我们缩写这样的表达式为

λsz.z

这样的形式被理解为在求值过程中s是第一个被替换的参数，z是第二个。使用这种记号，前几个自然数可以被表示为：

1 ≡ λsz.s(z)
2 ≡ λsz.s(s(z))
3 ≡ λsz.s(s(s(z)))

等等。

我们第一个有趣的函数是后继函数。这个函数可以定义为：

S ≡ λwyx.y(wyx)

将这个后继函数作用于我们代表0的函数，展开为：

S0 ≡ (λwyx.y(wyx))(λsz.z)

在左边表达式的函数体内我们用(

λsz.z)替换所有的w得到：

(λwyx.y(wyx))(λsz.z) = λyx.y((λsz.z)yx) = λyx.y((λz.z)x) = λyx.y(x) ≡ 1

也就是说，我们得到了表示1的函数(请注意函数参数没有意义)。

后继函数作用于1得到：

S1 ≡ (λwyx.y(wyx))(λsz.s(z)) = λyx.y((λsz.s(z))yx) = λyx.y(y(x)) ≡ 2

请注意将数字(

λsz.s(z))作用于参数y和x的唯一目的在于“重命名”我们的数字函数中用到的变量。
2.1 加法
注意到我们定义的数字1的函数体sz可以被解释为将函数s作用于z，加法函数可以立刻通过相似的方法得到。如果想要计算2加3，我们就把后继函数2次作用于3：

2S3 ≡ (λsz.s(sz))(λwyx.y(wyx))(λuv.u(u(uv)))

恒等式右边第一个表达式是2，第二个是后继函数，第三个是3(已经修改了变量名)。上面的表达式化简为：

(λsz.s(sz))(λwyx.y(wyx))(λuv.u(u(uv))) = (λwyx.y(wyx))((λwyx.y(wyx))(λuv.u(u(uv)))) ≡ S(S3) = S4 = 5

2.2 乘法
两个数字x与y相乘可以使用以下方程计算。

(λxyz.x(yz))

2乘2的积就是：

(λxyz.x(yz))22 = (λz.2(2z)) ≡ (λz.2((λuv.u(uv))z)) = (λz.2(λv.z(zv))) ≡ (λz.(λxy.x(xy))(λv.z(zv))) 
                                                                                    = (λz.(λy.(λv.z(zv))((λv.z(zv))y))) = (λzy.(λv.z(zv))(z(zy))) = (λzy.z(z(z(zy)))) ≡ 4

3 条件

我们引入以下2个函数分别表示逻辑真与逻辑假：

T ≡ λxy.x
F ≡ λxy.y

第一个函数接受2个参数并返回其中第一个，第二个函数接受2个参数并返回其中第二个。

3.1 逻辑运算
现在可以使用表示真或假的函数定义逻辑运算。

AND运算可以定义为：

OR

运算可以定义为：

∪ ≡ λxy.x(λuv.u)y ≡ λxy.xTy

NOT

运算可以定义为：

~ ≡ λx.x(λuv.v)(λab.a) ≡ λx.xFT

这些函数的意义很明显，不再赘述。

3.2 条件测试
编程语言中如果有这样一个函数会很方便：接受一个数值参数，当参数值为0时返回true否则返回false。下面的函数Z的满足此需求：

Z ≡ λx.xF~F

为了理解这个函数怎么工作，请注意：

0fa ≡ (λsz.z)fa = a

也就是说，函数f被作用在a上0次的结果是a。另一方面，函数F作用于任意参数可以得到单位函数I：

Fa ≡ (λxy.y)a = (λy.y) ≡ I

我们现在来检查Z是否正确。此函数作用于0得到：

Z0 ≡ (λx.xF~F)0 = 0F~F = ~F = T

而作用于其它数字N得到：

ZN ≡ (λx.xF~F)N = NF~F

然后，F被连续N次作用于~。由于F作用于任意值的结果都是I，所以以上表达式结果为：

NF~F = IF = F

3.3 前驱函数
我们现在可以将之前介绍过的函数组合起来以定义前驱函数。计算n的前驱时，一般的策略是创建一对数(n, n - 1)，然后去其中第二个数作为结果。

lambda算子可以用函数表示一对对象，并分别使用T和F取得其中第一和第二个对象：

(λz.zab)
(λz.zab)T = Tab = a
(λz.zab)F = Fab = b

下面的函数从数对(n, n - 1)(参数p表示这个数对)生成(n + 1, n)

Φ ≡ (λpz.z(S(pT))(pT))

其中子表达式pT取得数对中的第一个数。新的数对从这个数产生，方法是将此数加1作为新数对的第1个元素并且将此数直接用作新数对第二个元素。

计算n的前驱的方法是将Φ函数n此作用于数对(λz.z00)并取出新数对的第二个元素。

P ≡ (λn.nΦ(λz.z00)F)

请注意使用此函数计算0的前驱结果是0。这个特性在定义其它函数的时候有用。

3.4 相等于不等
以前驱函数为基础，我们现在可以定义函数以监测x是否大于y或者是否等于y。

G ≡ (λxy.Z(xPy))
E ≡ (λxy.∩(Gxy)(Gyx))

如果将前驱函数x次作用于y得到0，那么x >= y。如果x >= y且y >= x，那么x == y。用类似的方法还可以定义>, <和!=函数。


4 递归

lambda演算子借助一个特殊函数可以实现递归函数，这个特殊函数调用一个函数y然后生成它自身。为了帮助理解，请参考以下函数Y:

Y ≡ (λy.(λx.y(xx))(λx.y(xx)))

将函数Y作用于任意R得到

YR ≡ (λy.(λx.y(xx))(λx.y(xx)))R = (λx.R(xx))(λx.R(xx)) = R((λx.R(xx))(λx.R(xx))) ≡ R(YR)

也就是说，函数R递归的使用YR作为第一个参数被求值。

举个例子，假如我们想要求前n个自然数的和，我们使用递归的定义Σ_i=[0..n] i = n + 

Σ_i=[0..n-1] i， 然后

定义函数R

R ≡ (λrn.Zn0(nS(r(Pn))))

这个实现先检查n：如果n为0那么和也是0。否则，后继函数被n次作用在以n的前驱为参数的递归调用(即r(Pn))上。

既然lambda算子里的函数没有名字，如何能够确定以上表达式中的r在递归调用R？我们无法确定，而这恰恰是我们使用递归操作符Y的原因。假定我们想要计算0到3的和，方法是：

YR3 =                R(YR)3    =             Z30(3S(YR(P3)))      =          3S(YR2) 
      =           3S(R(YR)2)   =         3S(Z20(2S(YR(P2))))    =      3S(2S(YR1))
      =      3S(2S(R(YR)1))  =     3S(2S(Z10(1S(YR(P1)))))   = 3S(2S(1S(YR0))) 
      = 3S(2S(1S(R(YR)0))) = 3S(2S(1S(Z00(0S(YR(P0)))))) = 3S(2S(1S(0))) 
      = 6

5 习题

• 1，定义“小于”函数和“大于”函数。
• 2，使用自然数对定义正整数和负整数。
• 3，定义正负整数加减法。
• 4，定义递归函数计算正整数除法。
• 5，定义递归函数计算自然数阶乘。
• 6，使用整数对定义自然数。
• 7，定义自然数的四则运算。
• 8，定义函数表示数的列表。
• 9，定义函数取出列表中第一个数。
• 10，定义递归函数计算列表长度。
• 11，你能使用lambda演算子模拟图灵机吗？

6 References
略