函数式编程的基石——LambdaCalculus（FunctionalProgramming）

在lambda演算中&＃xff0c;函数是一等公民。可以把函数作为参数传入或返回&＃xff0c;把函数赋值给一个变量等等。

                                                          Y 组合子函数

通过 lambda , currying, closure, alpha, beta 可以定义出一个"完备"的计算体系.

在此之上,我们可以构造出任意复杂的程序.

要描述一个形式系统&＃xff0c;我们首先需要约定用到的基本符号&＃xff0c;对于本系列所介绍的lambda演算&＃xff0c;其符号集包括λ . ()和变量名(x, y, z, etc.)。

1. λ 表达式/项

::&＃61; | | ( )| (λ .)


其中&＃xff1a;

可以是诸如0、1这样的数字&＃xff0c;或者预定义的函数: &＃43;、-、*等。

是x、y等这样的名字。

( )表示函数调用。左边的为要调用的函数&＃xff0c;右边的为参数。

(λ .)被称为lambda抽象(lambda abstraction)&＃xff0c;用以定义新的函数。

例如&＃xff1a;

lambda <参数> : <函数体>  

这个定义可以应用到参数上&＃xff0c;进行求值。

(lambda x : x &＃43; x)(5)
10(lambda x : (lambda y : x &＃43; y))(1)(2)
3y &＃61; 2
(lambda x : x &＃43; y)(4)
6a &＃61; 1
(lambda a : a &＃43; 1)(2)
3

Beta 规则&＃xff1a;

f &＃61; (lambda y : (lambda x : x &＃43; y))(5)
f(2)
7
f(1)
6

这个例子中, lambda x, y 将x 应用到 y 上. 其中 x 替换成 lambda x : x * x , y 替换成 3.
Beta的严格定义如下&＃xff1a;

lambda x . B e &＃61; B[x :&＃61; e] if free(e) /subset free(B[x :&＃61; e]

这条规则是为了保证出现命名冲突的时候,先进行 alpha 替换,然后再应用 beta 简化.

小结

在lambda演算中只有三种合法表达式&＃xff08;也可以称之为项&＃xff1a;λ-expression or λ-term&＃xff09;存在&＃xff1a;

• 变量(Variable)
  形式&＃xff1a;x
  变量名可能是一个字符或字符串&＃xff0c;它表示一个参数&＃xff08;形参&＃xff09;或者一个值&＃xff08;实参&＃xff09;。
  e.g. z var
• 抽象(Abstraction)
  形式&＃xff1a;λx.M
  它表示获取一个参数x并返回M的lambda函数&＃xff0c;M是一个合法lambda表达式&＃xff0c;且符号λ和.表示绑定变量x于该函数抽象的函数体M。简单来说就是表示一个形参为x的函数M。
  e.g. λx.y λx.(λy.xy)
  前者表示一个常量函数(constant function)&＃xff0c;输出恒为y与输入无关&＃xff1b;后者的输出是一个函数抽象λy.xy&＃xff0c;输入可以是任意的lambda表达式。
  注意&＃xff1a;一个lambda函数的输入和输出也可以是函数。
• 应用(Application)
  形式&＃xff1a;M N
  它表示将函数M应用于参数N&＃xff0c;其中M、N均为合法lambda表达式。简单来说就是给函数M输入实参N。
  e.g. (λx.x) y, (λx.x) (λx.x)
  前者表示将函数λx.x应用于变量y&＃xff0c;得到y&＃xff1b;后者表示将函数λx.x应用于λx.x&＃xff0c;得到λx.x。函数λx.x是一个恒等函数(identity function)&＃xff0c;即输入恒等于输出&＃xff0c;它可以用 I 来表示。

这时候可能就有人纳闷儿了&＃xff0c;(λx.x) y意义很明确&＃xff0c;但λy.xy为什么代表函数抽象而不是将函数λy.x应用于y的函数应用呢&＃xff1f;为了消除类似的表达式歧义&＃xff0c;可以多使用小括号&＃xff0c;也有以下几个消歧约定可以参考&＃xff1a;

• 一个函数抽象的函数体将尽最大可能向右扩展&＃xff0c;即&＃xff1a;λx.M N代表的是一个函数抽象λx.(M N)而非函数应用(λx.M) N。
• 函数应用是左结合的&＃xff0c;即&＃xff1a;M N P意为(M N) P而非M (N P)。

2. 自由变量和绑定变量

前面提到在函数抽象中&＃xff0c;形参绑定于函数体&＃xff0c;即形参是绑定变量&＃xff0c;相对应地&＃xff0c;不是绑定变量的自然就是自由变量。咱们来通过几个例子来理解这个关系&＃xff1a;

• λx.xy&＃xff1a;其中x是绑定变量&＃xff0c;y是自由变量&＃xff1b;
• (λy.y)(λx.xy)&＃xff1a;这个表达式可以按括号划分为两个子表达式M和N&＃xff0c;M的y是绑定变量&＃xff0c;无自由变量&＃xff0c;N的x是绑定变量&＃xff0c;y是自由变量且与M无关&＃xff1b;
• λx.(λy.xyz)&＃xff1a;这个表达式中的x绑定于外部表达式&＃xff0c;y绑定于内部表达式&＃xff0c;z是自由变量。

由于每个lambda函数都只有一个参数&＃xff0c;因此也只有一个绑定变量&＃xff0c;这个绑定变量随着形参的变化而变化。
我们用FV来表示一个lambda表达式中所有自由变量的集合&＃xff0c;如&＃xff1a;

FV(λx.xy) &＃61; {y}
FV((λy.y)(λx.xy)) &＃61; FV(λy.y) ∪ FV(λx.xy) &＃61; {y}
FV(λx.(λy.xyz)) &＃61; FV(λy.xyz) \ x &＃61; {x,z} \ x &＃61; {z}


3. 柯里化(Currying)

有时候我们的函数需要有多个参数&＃xff0c;这太正常不过了&＃xff0c;但是lambda函数只能有一个参数怎么办&＃xff1f;解决这个问题的方法就是柯里化(Currying)。
柯里化是用于处理多参数输入情况的方法&＃xff0c;我们已经知道一个lambda函数的输入和输出也可以是函数&＃xff0c;那么基于它&＃xff0c;可以把多参数函数和单参数函数做以下转换&＃xff1a;
currying: λx y.xy &＃61; λx.(λy.xy)
外层函数接受一个参数x返回一个函数λy.xy&＃xff0c;这个返回函数&＃xff08;内层函数&＃xff09;又接受一个参数y返回xy&＃xff0c;x绑定于外层函数&＃xff0c;y绑定于内层函数&＃xff0c;这样我们就在满足lambda函数只接受一个参数的约束下实现了多参数函数的功能&＃xff0c;这就是柯里化&＃xff0c;而λx y.xy称为λx.(λy.xy)的缩写&＃xff0c;为了方便表达&＃xff0c;后续会常常出现λx y.xy这样的书写方式&＃xff0c;需要谨记它只是缩写写法。

我们已经知道了lambda表达式的基本定义与语法&＃xff0c;下面将介绍如何对一个lambda表达式进行归约(reduction)。

1. beta | β 归约

对于一个函数应用(λx.x) y&＃xff0c;它意为将函数应用λx.x应用于y&＃xff0c;等价于x[x:&＃61;y]&＃xff0c;即结果是y。在这个过程中&＃xff0c;(λx.x) y ≡ x[x:&＃61;y]一步就叫做beta归约&＃xff0c;x[x:&＃61;y] ≡ y一步称作替换(substitution)&＃xff0c;[x:&＃61;y]意为将表达式中的自由变量x替换为y。

• 替换
  形式&＃xff1a;E[V :&＃61; R]
  意为将表达式E中的所有 “自由变量” V替换为表达式R。对于变量x,y和lambda表达式M,N&＃xff0c;有以下规则&＃xff1a;

x[x :&＃61; N] ≡ N
y[x :&＃61; N] ≡ y //注意 x ≠ y
(M1 M2)[x :&＃61; N] ≡ (M1[x :&＃61; N]) (M2[x :&＃61; N])
(λx.M)[x :&＃61; N] ≡ λx.M //注意 x 是绑定变量无法替换
(λy.M)[x :&＃61; N] ≡ λy.(M[x :&＃61; N]) //注意 x ≠ y, 且表达式N的自由变量中不包含 y 即 y ∉ FV(N)


• beta归约
  形式&＃xff1a;β: ((λV.E) E′) ≡ E[V :&＃61; E′]
  其实就是用实参替换函数体中的形参&＃xff0c;也就是函数抽象应用(apply)于参数的过程啦&＃xff0c;只不过这个参数除了是一个变量还可能是一个表达式。

细心的话可以注意到&＃xff0c;替换规则中特别标注了一些x ≠ y或者y ∉ FV(N)等约束条件&＃xff0c;它们的意义在于防止lambda表达式的归约过程中出现歧义。
比如以下过程&＃xff1a;

(λx.(λy.xy)) y
&＃61; (λy.xy)[x:&＃61;y] //beta归约&＃xff1a;注意 y ∈ FV(y) 不满足替换的约束条件
&＃61; λy.yy //替换&＃xff1a;绑定变量y与自由变量y同名出现了冲突


可以看出在不满足约束条件的情况强行替换造成了错误的结果&＃xff0c;那么对于这种情况该如何处理呢&＃xff1f;那就需要alpha转换啦。

2. alpha | α 转换

这条规则就是说&＃xff0c;一个lambda函数抽象在更名绑定变量前后是等价的&＃xff0c;即&＃xff1a;
α: λx.x ≡ λy.y
其作用就是解决绑定变量与自由变量间的同名冲突问题。
那么对于上面的那个错误归约过程就可以纠正一下了&＃xff1a;

(λx.(λy.xy))y
&＃61; (λy.xy)[x:&＃61;y] //beta归约&＃xff1a;注意 y ∈ FV(y) 不满足替换的约束条件
&＃61; (λz.xz)[x:&＃61;y] //alpha转换&＃xff1a;因为绑定变量y将与自由变量x&＃xff08;将被替换为y&＃xff09;冲突&＃xff0c;所以更名为z
&＃61; λz.yz


Perfect&＃xff01;这样对于lambda演算最基础的定义与归约规则已经介绍完毕了&＃xff0c;虽然内容很简单&＃xff0c;但是却很容易眼高手低&＃xff0c;要试着练习喔。

3. eta | η 归约

灵活运用alpha和beta已经可以解决所有的lambda表达式归约问题&＃xff0c;但是考虑这样一个表达式&＃xff1a;

λx.M x


将它应用于任意一个参数上&＃xff0c;比如(λx.M x) N&＃xff0c;进行beta归约和替换后会发现它等价于M N&＃xff0c;这岂不是意味着

λx.M x ≡ M


没错&＃xff0c;对于形如λx.M x&＃xff0c;其中表达式M不包含绑定变量x的函数抽象&＃xff0c;它是冗余的&＃xff0c;等价于M&＃xff0c;而这就是eta归约&＃xff0c;它一般用于清除lambda表达式中存在的冗余函数抽象。

[原文&＃xff1a;https://www.jianshu.com/p/ebae04e1e47c]

[https://liujiacai.net/blog/2014/10/12/lambda-calculus-introduction/]

Lambda calculus我们一般称为λ演算&＃xff0c;最早是由邱奇&＃xff08;Alonzo Church&＃xff0c;图灵的博导&＃xff09;在20世纪30年代引入&＃xff0c;当时的背景是解决函数可计算的本质性问题&＃xff0c;初期λ演算成功的解决了在可计算理论中的判定性问题&＃xff0c;后来根据Church–Turing thesis&＃xff0c;证明了λ演算与图灵机是等价的。

好了&＃xff0c;经过上边简单的介绍&＃xff0c;大家应该对λ演算有了初步印象。下面我将重点介绍λ演算的具体内容&＃xff0c;并且阐述λ演算是如何奠基了我们现在常用的编程语言&＃xff08;如&＃xff1a;Java、python、Lisp等&＃xff09;。

λ演算的语法与求值

语法(syntax)

因为λ演算研究的是函数的本质性问题&＃xff0c;所以形式极其简单&＃xff1a;

E &＃61; x variables| λx. E function creation(abstraction)| E1 E2 function application


上面的E称为λ-表达式(expressions)或λ-terms&＃xff0c;它的值有三种形式&＃xff1a;

1. 变量(variables)。
2. 函数声明或抽象(function creation/abstraction)。需要注意是的&＃xff0c;函数中有且仅有一个参数。在λx. E中&＃xff0c;x是参数&＃xff0c;E是函数体
3. 函数应用(function application)。也就是我们理解的函数调用&＃xff0c;但官方术语就叫函数应用&＃xff0c;本文后面也会采用“应用”的叫法。

λ表达式例子

上面就是λ演算的语法了&＃xff0c;很是简单吧。下面看几个例子&＃xff1a;

• 恒等函数

λx.x

• 一个返回恒等函数的函数

λy. (λx.x)

可以看到&＃xff0c;这里的y参数直接被忽略了。

在使用λ演算时&＃xff0c;有一些惯例需要说一下&＃xff1a;

函数声明时&＃xff0c;函数体尽可能的向右扩展。什么意思呢&＃xff0c;举个例子大家就明白了&＃xff1a;

λx.x λy.x y z


应该理解为

λ x. (x (λy. ((x y) z)))

函数应用时&＃xff0c;遵循左结合。在举个例子&＃xff1a;

x y z

为

(x y) z

Currying带有多个参数的函数

从上面我们知道&＃xff0c;λ演算中函数只有一个参数&＃xff0c;那两个参数的函数的是不是就没法表示了呢&＃xff0c;那λ演算的功能也太弱了吧&＃xff0c;这就是λ的神奇之处&＃xff0c;函数在本质上只需要一个参数即可。如果想要声明多个参数的函数&＃xff0c;通过currying技术即可。下面来说说currying。
λx y. (&＃43; x y)---->λx. (λ y. &＃43; x y)
上面这个转化就叫currying&＃xff0c;它展示了&＃xff0c;我们如何实现加法&＃xff08;这里假设&＃43;这个符号已经具有相加的功能&＃xff0c;后面我们会讲到如何用λ表达式来实现这个&＃43;的功能&＃xff09;。
其实就是我们现在意义上的闭包——你调用一个函数&＃xff0c;这个函数返回另一个函数&＃xff0c;返回的函数中存储保留了调用函数的变量。currying是闭包的鼻祖。
如果用Python来表示就是这样的东西&＃xff1a;

def add(x):return lambda y: x&＃43;yadd(4)(3) //return 7


如果用函数式语言clojure来表示就是&＃xff1a;

(defn add [x](fn [y] (&＃43; x y)))((add 4) 3) ;return 7


求值(evaluation)

在λ演算中&＃xff0c;有两条求值规则&＃xff1a;

1. Alpha equivalence( or conversion )
2. Beta reduction

Alpha equivalence

这个比较简单也好理解&＃xff0c;就是说λx.x与λy.y是等价的&＃xff0c;并不因为换了变量名而改变函数的意义。
简单并不说这个规则不重要&＃xff0c;在一些变量覆盖的场合很重要&＃xff0c;如下这个例子&＃xff1a;
λx. x (λx. x)如果你这么写的话&＃xff0c;第二个函数定义中的x与第一个函数定义中的x重复了&＃xff0c;也就是在第二个函数里把第一个的x给覆盖了。
如果改为λx. x (λy. y)就不会有歧义了。

Beta reduction

这个规则是λ演算中函数应用的重点了。一句话来解释就是&＃xff0c;把参数应用到函数体中。举一个例子&＃xff1a;
有这么一个函数应用(λx.x)(λy.y)&＃xff0c;在这里把(λy.y)带入前面函数的x中&＃xff0c;就能得到最终的结果(λy.y)&＃xff0c;这里传入一个函数&＃xff0c;然后又返回一个函数&＃xff0c;这就是最终的结果。

考虑下面这个函数应用&＃xff1a;

(λ y. (λ x. x) y) E


有两种计算方法&＃xff0c;如下图