函数式编程的基石 —— Lambda Calculus(Functional Programming)

Y 组合子函数

  • Lambda calculus : λ 定义

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

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

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

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

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

1. λ 表达式/项

 ::=  
          | 
          | ( )
          | (λ .)

其中:

可以是诸如0、1这样的数字,或者预定义的函数: +、-、*等。

是x、y等这样的名字。

( )表示函数调用。 左边的为要调用的函数,右边的为参数。

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

例如:

 lambda  :   

这个定义可以应用到参数上,进行求值。

(lambda x : x + x)(5)
10

(lambda x : (lambda y : x + y))(1)(2)
3

y = 2
(lambda x : x + y)(4)
6

a = 1
(lambda a : a + 1)(2)
3

Beta 规则:

f = (lambda y : (lambda x : x + y))(5)
f(2)
7
f(1)
6

这个例子中, lambda x, y 将x 应用到 y 上. 其中 x 替换成 lambda x : x * x , y 替换成 3.

Beta的严格定义如下:

lambda x . B e = B[x := e] if free(e) /subset free(B[x := e]

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

在lambda演算中只有三种合法表达式( λ-expression or λ-term)存在:

  • 变量(Variable)

    形式: x

    变量名可能是一个字符或字符串,它表示一个参数(形参)或者一个值(实参)。

    e.g.  z   var

  • 抽象(Abstraction)

    形式: λx.M

    它表示获取一个参数x并返回M的lambda函数,M是一个合法lambda表达式,且符号 λ . 表示 绑定变量x于该函数抽象的函数体M 简单来说就是表示一个形参为x的函数M。

    e.g. 
    λx.y
     
    λx.(λy.xy)

    前者表示一个 常量函数(constant function) ,输出恒为y与输入无关; 后者的输出是一个函数抽象 λy.xy ,输入可以是任意的lambda表达式。

    注意: 一个lambda函数的输入和输出也可以是函数。

  • 应用(Application)

    形式: M N

    它表示将函数M应用于参数N,其中M、N均为合法lambda表达式。 简单来说就是给函数M输入实参N。

    e.g. 
    (λx.x) y

    (λx.x) (λx.x)

    前者表示将函数
    λx.x
    应用于变量
    y
    ,得到
    y

    后者表示将函数
    λx.x
    应用于
    λx.x
    ,得到
    λx.x

    函数
    λx.x

    是一个 恒等函数(identity function) ,即输入恒等于输出,它可以用  I 来表示。

这时候可能就有人纳闷儿了, (λx.x) y  意义很明确,但 λy.xy 为什么代表函数抽象而不是将函数 λy.x 应用于 y 的函数应用呢?

为了消除类似的表达式歧义,可以多使用小括号,也有以下几个 消歧约定 可以参考:

  • 一个函数抽象的函数体将尽最大可能向右扩展 ,即:

  • λx.M N

  • 代表的是一个函数抽象

  • λx.(M N)

  • 而非函数应用

  • (λx.M) N

  • 函数应用是左结合的 ,即:

  • M N P

  • 意为

  • (M N) P

  • 而非

  • M (N P)

2. 自由变量和绑定变量

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

  • λx.xy 其中x是绑定变量,y是自由变量;

  • (λy.y)(λx.xy) 这个表达式可以按括号划分为两个子表达式M和N,M的y是绑定变量,无自由变量,N的x是绑定变量,y是自由变量且与M无关;

  • λx.(λy.xyz) 这个表达式中的x绑定于外部表达式,y绑定于内部表达式,z是自由变量。

由于每个lambda函数都只有一个参数,因此也只有一个绑定变量,这个绑定变量随着形参的变化而变化。

我们用 FV 来表示一个lambda表达式中所有自由变量的集合,如:

FV(λx.xy) = {y}

FV((λy.y)(λx.xy)) = FV(λy.y) ∪ FV(λx.xy) = {y}

FV(λx.(λy.xyz)) = FV(λy.xyz) \ x = {x,z} \ x = {z}

3. 柯里化(Currying)

有时候我们的函数需要有多个参数,这太正常不过了,但是lambda函数只能有一个参数怎么办? 解决这个问题的方法就是柯里化(Currying)。

柯里化是用于处理多参数输入情况的方法,我们已经知道 一个lambda函数的输入和输出也可以是函数 ,那么基于它,可以把多参数函数和单参数函数做以下转换:


currying: λx y.xy = λx.(λy.xy)

外层函数接受一个参数x返回一个函数 λy.xy ,这个返回函数(内层函数)又接受一个参数y返回xy,x绑定于外层函数,y绑定于内层函数,这样我们就在满足lambda函数只接受一个参数的约束下实现了多参数函数的功能,这就是柯里化,而 λx y.xy 称为 λx.(λy.xy) 的缩写,为了方便表达,后续会常常出现 λx y.xy 这样的书写方式,需要谨记它只是缩写写法。

lambda | λ 归约

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

1. beta | β 归约

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

  • 替换

    形式:

  • E[V := R]

  • 意为将表达式 E 中的所有 “自由变量”  V 替换为表达式 R 对于变量 x,y 和lambda表达式 M,N ,有以下规则:

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

    形式:

  • β: ((λV.E) E′) ≡ E[V := E′]

  • 其实就是用实参替换函数体中的形参,也就是函数抽象应用(apply)于参数的过程啦,只不过这个参数除了是一个变量还可能是一个表达式。

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

比如以下过程:

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

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

2. alpha | α 转换

这条规则就是说,一个lambda函数抽象在更名绑定变量前后是等价的,即:


α: λx.x ≡ λy.y

其作用就是解决绑定变量与自由变量间的同名冲突问题。

那么对于上面的那个错误归约过程就可以纠正一下了:

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

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

3. eta | η 归约

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

λx.M x

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

λx.M x ≡ M

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

[ https://www.jianshu.com/p/ebae04e1e47c]

λ演算的语法与求值

语法(syntax)

因为λ演算研究的是函数的本质性问题,所以形式极其简单:

E = x           variables
  | λx. E       function creation(abstraction)
  | E1 E2       function application

上面的E称为λ-表达式(expressions)或λ-terms,它的值有三种形式:

  • 变量(variables)。

  • 函数声明或抽象(function creation/abstraction)。 需要注意是的,函数中 有且仅有 一个参数。 在λx. E中,x是参数,E是函数体

  • 函数应用(function application)。 也就是我们理解的函数调用,但官方术语就叫函数应用,本文后面也会采用“应用”的叫法。

  • λ表达式例子

上面就是λ演算的语法了, 下面看几个例子:

  • 恒等函数:

λx.x

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

λy. (λx.x)

可以看到,这里的y参数直接被忽略了。

在使用λ演算时,有一些惯例需要说一下:

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

λx.x λy.x y z

应该理解为

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

函数应用时,遵循左结合。 在举个例子:

x y z

(x y) z

  • Currying:带有多个参数的函数

从上面我们知道,λ演算中函数只有一个参数,那两个参数的函数的是不是就没法表示了呢,那λ演算的功能也太弱了吧,这就是λ的神奇之处,函数在本质上只需要一个参数即可。 如果想要声明多个参数的函数,通过currying技术即可。 下面来说说currying。


λx y. (+ x y)  

=>

λx. (λ y. + x y)

上面这个转化就叫currying,它展示了,我们如何实现加法(这里假设+这个符号已经具有相加的功能,后面我们会讲到如何用λ表达式来实现这个+的功能)。

其实就是我们现在意义上的闭包——你调用一个函数,这个函数返回另一个函数,返回的函数中存储保留了调用函数的变量。 currying是闭包的鼻祖。

如果用Python来表示就是这样的东西:

def add(x):
    return lambda y: x+y

add(4)(3) //return 7

如果用函数式语言clojure来表示就是:

(defn add [x]
  (fn [y] (+ x y)))

((add 4) 3) ;return 7
  • 求值(evaluation)

在λ演算中,有两条求值规则:

  • Alpha equivalence( or conversion )

  • Beta reduction

Alpha equivalence

这个比较简单也好理解,就是说λx.x与λy.y是等价的,并不因为换了变量名而改变函数的意义。

简单并不说这个规则不重要,在一些变量覆盖的场合很重要,如下这个例子:

λx. x (λx. x) 如果你这么写的话,第二个函数定义中的x与第一个函数定义中的x重复了,也就是在第二个函数里把第一个的x给覆盖了。

如果改为
λx. x (λy. y)

就不会有歧义了。

Beta reduction

这个规则是λ演算中函数应用的重点了。 一句话来解释就是,把参数应用到函数体中。 举一个例子:

有这么一个函数应用
(λx.x)(λy.y)
,在这里把
(λy.y)
带入前面函数的x中,就能得到最终的结果
(λy.y)

,这里传入一个函数,然后又返回一个函数,这就是最终的结果。

考虑下面这个函数应用:

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

有两种计算方法,如下图

evaluation-order

可以先计算内层的函数调用再计算外层的函数调用,反之也可。

根据Church–Rosser定理,这两种方法是等价的,最终会得到相等的结果,如上图最后都得到了E。

但如果我们要自己实现一种语言,就有可能必选二选其一,于是有了下面两种方式:

  • Call by Value(Eager Evaluation及早求值)

也就是上图中的inner,这种方式在函数应用前,就计算函数参数的值。 如:

(λy. (λx. x) y) ((λu. u) (λv. v))
(λy. (λx. x) y) (λv. v)
(λx. x) (λv. v)
λv. v
  • Call by Name (Lazy Evaluation惰性求值)

也就是上图中的outer,这种方式在函数应用前,不计算函数参数的值,直到需要时才求值。 如:

(λy. (λx. x) y) ((λu. u) (λv. v)) --->
(λx. x) ((λu. u) (λv. v)) --->
(λu. u) (λv. v) --->
λv. v

值得一提的是,Call by Name这种方式在我们目前的语言中,只有函数式语言支持。

  • λ演算与编程语言的关系

在λ演算中只有函数(变量依附于函数而有意义),如果要用纯λ演算来实现一门编程语言的话,我们还需要一些数据类型,比如boolean、number、list等,那怎么办呢?

λ的强大又再一次展现出来,所有的数据类型都能用函数模拟出来,秘诀就是 不要去关心数据的值是什么,重点是我们能对这个值做什么操作 ,然后我们用合法的λ表达式把这些操作表示出来即可。

听上去很些云里雾里,但看了我下面的讲解以后,你会发现,编程语言原来还可以这么玩,希望我能把这部分讲清楚些,个人感觉这些东西太funny了 🙂

好了,我们先从最简单——boolean的开始。

  • Boolean

Ask: 我们能对boolean值做什么?

Answer:

我们能够进行条件判断,二选其一。

好,知道了能对boolean的操作,下面就用λ表达式来定义它:

true = λx. λy. x
false = λx. λy. y
if E1 then E2 else E3 = E1 E2 E3

来简单解释一下,boolean就是这么一个函数,它有两个参数(通过currying实现),返回其中一个。 下面看个例子:

if true then u else v

可以写成   

(λx. λy. x) u v 
(λy. u) v  
u
  • 自然数

Ask: 我们能对number做什么?

Answer:

我们能够依次遍历这些数字

好,知道了能对number的操作,下面就用λ表达式来定义它:

0 = λf. λs. s
1 = λf. λs. f s
2 = λf. λs. f (f s)
......

解释一下,利用currying,我们知道上面的定义其实相当于一个具有两个参数的函数: 一个函数f,另一个是起始值s,然后不断应用f实现遍历数字的操作。 先不要管为什么这么定义,看了下面我们如何定义加法乘法的例子你应该就会豁然开朗了:

首先我们需要定义一个后继函数(The successor function):

succ n = λf. λs. f (n f s)

例子—— 1+1

add 1 1
1 succ 1
succ 1

λf. λs. f (f s) 2

例子, 2*2

mult 2 2 --->
2 (add 2) 0 --->
(add 2) ((add 2) 0) --->
2 succ (add 2 0) --->
2 succ (2 succ 0) --->
succ (succ (succ (succ 0))) --->
succ (succ (succ (λf. λs. f (0 f s)))) --->
succ (succ (succ (λf. λs. f s))) --->
succ (succ (λg. λy. g ((λf. λs. f s) g y)))

succ (succ (λg. λy. g (g y))) --->...... ---> λg. λy. g (g (g (g y))) = 4

如果想要判断一个数字是否为0,可以这么定义 

iszero n = n (λb. false) true
  • λ-演算与图灵机

λ-演算与图灵机是等价:

在一个不限时间、不限资源的前提下,图灵机通过前进、后退、跳转、输出1或0这四个简单的命令,在一条无限长的纸带上执行事先编好的程序。

根据目前的证明,图灵机是宇宙间最强大的机器(理想中的),我们现有的计算机都没有超过图灵机。

如果说一个语言是图灵完备的,就是说,世界上任何可计算性问题,它都能解决。

我们现有的命令式语言,如C、Java等就是以图灵机为基础的。 如果说这些语言图灵完备,需要具有以下两个特征:

  • 有if、goto语句(或while、for之类的循环语句)

  • 能够进行赋值操作(也就是改变内存状态)

与图灵机对应,λ-演算奠定了函数式编程语言的基础,如Lisp、Haskell等,如果说这些函数式语言图灵完备,需要有以下两个特征:

  • 能够进行函数抽象(也就是函数定义)

  • 能够进行函数应用(也就是函数调用)

鉴别一个语言是不是函数式的标准是: 这个语言能否在运行时创建函数,如果能,就是函数式语言。

λ演算的精髓之处,就是通过一套形式化的规则来描述“计算”。 要知道,这里面的很多东西我们现如今想当然的接受了,但如何让笨重的计算机来理解这个世界呢,这就需要这些形式化的规则来指导了。

我们现在的编程语言趋向于多范式化,像java8,scala,kotlin,python、ruby等等。 因为纯函数式语言不能改变变量状态,这个恐怕在很多场合不适用吧。 纯OO也不好,因为我们大多数程序员,都是用OO的语言来写过程式的程序,看看大家有多少Helper类,Util类就明白了。