类型和程序设计语言

在互联网行业中，每个人都希望自己的系统是能够水平扩展的，系统的计算能力也是如此。随着实践的深入，大家发现函数式编程能够天然得实现计算的并行化，实际上Map-reduce这样的并行框架本质上都是函数式编程思想下的产物。于是近些年来，Scala，Erlang这样的函数式编程语言越来越受到追捧，搞得程序员不会上个一两门函数式语言都不好意思出门打招呼。博主也不能免俗，准备也花点时间研究一下函数式编程，就从scala入手吧。在触及到具体的语言之前，我觉得还是很有必要先做一些理论储备，每一门计算机语言其实背后都蕴含着某一种思想的光芒。如果能够对这些基本的理论有一点体会或者理解，那么对于程序员提高自己的境界还是很有帮助的，至少在看到网上的大牛们讨论的时候不会一头雾水，经验上可能跟不上这些大牛，但思想一定要跟得上。函数式编程背后的理论基础就是Lambda calculus。作者花了点时间翻阅了一下维基百科http://en.wikipedia.org/wiki/Lambda_calculus，觉得有点体会，这里做个翻译点评。实际上维基百科中文也对该词条进行了翻译，但感觉中文只是英文词条的一个直译，很多东西含混不清，博主在这里对其进行一个评注，便于像我这样数学功底比较差的同仁们理解。

首先解释一下什么是Lambda caculus，Lambda 演算实际上是一套形式化系统，它的主要目的就是通过变量绑定以及代入的方法来表达计算，也就是说它能够从本质上来分析计算。正是因为如此，它在计算机理论界被广泛采用，成为设计函数式编程语言的理论工具。了解一点lamda演算，有助于你从本质上理解函数编程语言考虑问题和看待世界的方式。如果你能够理解到这个层次，也许你也能够在函数式编程思想的启迪下提出actor model这样的并行模型，成为万人膜拜的一代大牛。（憧憬一下....）

Lamda演算的概念十分重要，实际上Lambda 演算系统也不只一个，有uptyped Lambda calculus和typed Lambda calculus的区别，这两个演算系统实际上是不同的变种，至于到底有什么区别，我也不是很清楚，大概的意思是untyped Lambda calculus中的函数没有什么限制，而typed lamada calculus 中的函数所能接受的数据类型是有限制的。具体的区别，得靠理论界的专业人士来普及了，我也就不班门弄斧了。

Lambda演算的开山鼻祖是Alonzo Church，上个世纪30年代的大师。让我们记住他的名字吧。（好吧，只是记住他的名字，其实我也不知道他到底有多牛）

动机

首先来谈谈动机，Lambda演算到底想干什么。关键词就是函数function。我们知道在计算机语言中有一个很基本的概念就是递归函数，这个递归函数很烦人。记得在本科时学习C语言时，如果掌握了递归函数的写法，那C语言就算是基本入门了。而Lambda演算则为各式各样复杂的计算（包括递归计算）提供了一个统一的，简单的语义，从而使得我们能够正式得分析计算的各种特性。否则，计算只是一个口头上笼统的概念，有了Lambda演算，我们就有一个形式化系统来完整的分析到底什么是计算，它到底干了些什么，有什么特性。

首先让我们来看一个函数，identity function：

Id(x) = x

这个函数很简单，输入一个x，马上就返回这个输入值x。接下来再看另外一个函数，平方和函数：

Sqsum(x,y) = x*x + y*y

这个函数输入x,y，返回值是x和y的平方和x*x + y*y。

这是两个很简单的函数，通过观察这两个函数，我们可以观察到一些有用的东西，而这些观察正是Lambda演算主要思想的灵感来源。

首先第一个观察是，函数是不需要一个显式的名字的，比如函数

Sqsum(x,y) = x*x + y*y

其实可以写成一个匿名函数

(x,y) -> x*x +y*y

用专业一点的说法，这个函数可以表述成：

X，y对被映射成x*x + y*y。同样，类似的

Id(x) = x

也可以被写成一个匿名函数 x->x：输入被简单得映射成了自身。

第二个观察就是函数的参数（自变量）的名字是无关紧要的，这也就说

x->x

和

y->y

实际上表达的是同样的函数：identity function

类似的

(x,y) ->x*x + y*y 和

(u,v)->u*u + v*v

实际上表达的也是同一个函数。

最后一个观察就是，任何有两个自变量的函数，比如前面提到的sqsum函数，可以被重新写成另外一种形式的函数，这种新形式的函数只有一个输入变量，但输出返回的却是另外一个函数，而这个返回的函数同样也具有一个输入变量，输出返回另外一个函数，依次类推，直至终结。这有点和递归类似。举个例子吧，

(x,y) -> x*x + y*y

可以被写成

x->(y->x*x+y*y)

这种变化被称之为柯里化。有了柯里化，一个普通的具有多个输入自变量的函数都可以被转化成一系列的，只具有一个输入自变量的函数，这一系列的函数推导也被称之为partial application（片面应用）。

以上面的sqsum的例子而言，如果我们的输出参数是（5，2）我们可以进行如下推导：

((x,y) ->x*x + y*y)(5,2) = 5*5 + 2*2 = 29

如果使用了柯里化，则有

((x->(y->x*x+y*y))(5))(2)

=(y->5*5 + y*y)(2)

=5*5 + 2*2 = 29

我们看到柯里化和之前的函数都得到了一致的结果。需要注意的是，在函数链的第一个函数完成参数代入（x）之后，x*x就变成了一个常量。

Lambda演算

Lamda演算的描述是通过一种专门的Lambda词汇，这套词汇实际上定义了一种语法，以及基于该语法的一系列变换规则，这套规则可以操作Lambda词汇。这种变换规则可以被看作一种等价理论。正如上面所描述的，Lambda演算中的所有函数都是匿名函数，这些函数只有一个输入自变量，因为柯里化可以把多输入自变量的函数变换成只含有一个输入自变量的函数。

Lambda词汇

Lambda演算的语法定义了哪些表达式是有效的Lambda演算声明，同时也定义了哪些表达式不是有效的Lambda演算声明。就像C语言定义了哪些字符串是有效的C语言程序语法，哪些不是。一个有效的Lamda变化表达式被称之为一个Lambda词汇（Lambdaterm）。

下面的三条规则给出了一套归纳定义（递归定义），所有语法有效的Lambda词汇从根本上都源于这套归纳定义：

l 一个变量x，本身就是一个有效的Lambda词汇

l 如果t是一个Lambda词汇，x是一个变量，那么也是一个有效的Lambda词汇（也称之为Lambda抽象）

l 如果t和s都是Lambda词汇，那么ts也是一个有效的Lambda词汇（称之为application，中文叫应用）

任何其它的表达式都不是一个有效的Lambda词汇。如果一条表达式能够通过上述三条原则进行分解，那么这个表达式也可以称之为有效的Lambda词汇。

一个Lamda抽象实际上是一个匿名函数的定义，该函数接受一个输入自变量x，然后将x代入到表达式t中。举个例子，就是一个函数的Lamda抽象，表达式实际上就是t。Lamda抽象只不过建立了一个函数，但并没有调用这个函数，相当于函数声明。

而一个application ts表达的就是一种调用动作，就是把s作为输入代入到函数t中，从而产生t(s)，相当于函数调用。

在Lambda演算中没有变量声明的概念。比如一个函数声明，Lambda演算就把y当作一个还没有定义的变量。Lambda抽象在语法上是有效的，它代表一个函数，这个函数的行为就是把输入变量x和一个暂时还未知的变量y相加。

Lambda词汇也利用括号来区分词条。比如和表示的就是不同的词条。

函数

在Lambda演算中，函数是所谓的一等公民，也就说它和值本质上是一样的，函数可以作为输入，函数也可以作为其它函数的返回值出现。

还是举例子吧，代表着identical 函数。而表示的是把identical函数应用到y上。另外一个例子，代表的是constant函数（函数永远返回y，不管输入x是什么）。

在Lambda演算中，函数的application是左优先的，也就说实际上意味着.

在Lambda演算中，有所谓的“等价”和“推导”的概念，这两个概念可以把某个Lambda词汇通过“推导”变成“等价”的Lambda词汇。

Alpha等价

Alpha等价是Lambda词汇中定义的一个基本的等价形式。这个思路很简单，在Lambda抽象中变量名的选择实际上是无关紧要的。比如，λx.x和λy.y是alpha等价的Lambda词汇，它们实际上表示的都是一个函数。但Lambda词汇x和y则不是alpha等价的，因为他们并未绑定到一个Lambda抽象中。

接下来一个重要的概念就是beta推导，要理解beta推导则需要首先理解下面这几个概念。

自由变量

Lambda词汇的自由变量指的是还没有被绑定到某一个Lambda抽象中的这些变量。某一个表达式的自由变量集可以定义如下

x的自由变量就是x
λx.t的自由变量集就是t的自由变量集（x被排除在外）
ts的自由变量集就是t的自由变量集和s的自由变量集的union。

例如， λx.x没有任何自由变量，而 λx.x+y的自由变量就是y。

Capture-avoiding替换

Capture-avoiding这个名词可能有点难于理解，简单解释一下。在Lamda演算中，正如前面提到的，变量名实际上是无关紧要的，比如(λx.(λy.yx))实际上和 (λa.(λb.ba))本质上是一样的函数。但这并不意味着这种变量名字的替换是没有约束的。看(λx.(λy.yx))的里面那个Lamda抽象：

(λy.yx)

从这个表达式来看，x是自由变量（未绑定任何Lamda抽象），如果按照上述原则（变量名无关），把y换成x，那么它可以被替换成：

(λx.xx)

但显然这么做是不可以的，这种替换下，最后一个x（原来的自由变量）被capture了，它此时被绑定到某一个Lamda抽象中去了。

因此替换一定要避免自由变量被capture，这就是所谓的Capture-avoided的由来。

假如t，s和r都是lamda词汇，而x，y都是变量，那么表示的就是以capture-avoiding的方式将t中的x替换成r，给予这个定义，则有：

如果
如果x不等於y并且y不是r的自由变量

那么基于第5条的定义，

是一个成功的capture-avoiding替换，

也是一个capture-avoiding的很好的例子。

在定义5中，y不是r的自由变量，因此也被称之为y对于r来讲是fresh的，这个条件非常关键，这就确保了替换式capture-avoiding的，不会改变函数的含义。如果没有这个条件，则有，这就把一个常量函数变成了一个identical函数。

通常来讲，如果你发现fresh条件无法满足时，你可能需要进行一些重命名工作来获得。比如可以利用一个第三者自由变量z来重新命名，就可以得到

Beta推导

有了前面的准备我们就可以来定义beta推导了。Beta推导规则可以让一个(λx.t)s 形式的应用推导成词汇t[x := s]. 那么 (λx.t)s → t[x := s]就用来表示(λx.t)s beta推导成t[x := s]。举个例子，对于每个s，则有(λx.x)s → x[x := s] = s。这就意味着λx.x 真的是一个将x映射x的一个函数。类似的则有(λx.y)s → y[x := s] = y，这也揭示了常量函数λx.y的特性。因此beta推导可以用来揭示函数的特性。

Lambda演算可以看作一个理想的函数式编程语言，就像Haskell。基于这种视角，beta推导对应着一个计算步骤。这个计算步骤不断得被重复，直到没有更多的application可以进一步beta推导。

在untyped Lambda演算中（就是我们目前讨论的Lambda演算），推导过程未必可以终止（也就说满足没有更多的application可以进一步beta推导这个条件）。举例而言，(λx.xx)(λx.xx)，我们对这个Lambda词汇应用beta推导，就可以得到(λx.xx)(λx.xx) → (xx)[x := λx.xx] = (x[x := λx.xx])(x[x := λx.xx]) = (λx.xx)(λx.xx). 这就意味着，这个词条通过一步beta推导又变成了自身，因此这个词条永远没有终止条件。Untyped Lambda演算的另外一个方面就是演算不区分不同种类的数据，例如，你也许写了一个函数只用来操作数字，但是在untyped Lambda演算中，这个函数也可以用来处理真假值（true/false），string或者非数字的对象，这个函数可以处理任何类型的数据。

Formal定义

对于上面的概念，Lamda演算有一套完备严谨的书面定义，这就是通常说的formal definition。这就过于理论化了，这里就不多说了，反正说的就是上面的那么个意思，作为一般非学界的码农，也就没有必要纠结于这些形式化定义了。

推导

Lamda演算的关键就是推导，存在3种推导形式：

Alpha变换
Beta推导
Eta变换

通常我们也会把上面的三种推导说成等价，比如如果两个表达式可以通过beta推导变成相同的表达式，我们就可以称之为这两个表达式是beta等价的，同理alpha等价，eta等价也是类似的定义。

关于推导，有一个专有名词redex，它是reducible expression的缩写。指的是那些可以利用上述3种规则进行推导的表达式，例如，(λx.M) N就是一个beta-redex，而如果x不是M的自由变量，λx.M x 就是eta-redex（这个会再后边解释）。Redex推导之后变成的表达式被称之为reduct。以前面刚刚提到的两个例子而言，各自对应的reduct就分别是 M[x:=N] 和M。

Alpha变换

这个概念前面已经提到过，就是说函数与具体的变量名称无关。两个函数如果是alpha等价的，那这两个函数本质上你可以认为是完全等价的。

实际上alpha变化还是有些需要注意的地方在里面。比如，当你对某一个Lambda抽象进行alpha变换时，发生重命名的变量一定是被绑定到同一个Lambda抽象中的。比如，λx.λx.x 的alpha变化可以是λy.λx.x，但不能是λy.λx.y，因为第一个x和第三个x没有被绑定到同一个Lambda抽象中去。

第二个需要注意的是capture avoiding的原则，这个在前面提到过，也不赘述。

在函数式编程语言中，alpha变化可以避免命名解析的一些问题。比如我们知道在编程语言中一般都有隐藏的概念（java，隐藏），通过alpha变化就可以把函数的变量换成各自不同的，这就避免了编程语言为了实现隐藏带来的复杂性，不会发生某一个变量名屏蔽了另外的变量名，这对具体编程语言的实现是很有意义的。

代入

代入被写作E[V := R]，就是将E中所有变量v出现的地方都用R代替。Lambda演算中的词汇的代入通过递归定义的方式来定义的：

x[x := N] ≡ N

y[x := N] ≡ y, if x ≠ y

(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])

(λx.M)[x := N] ≡ λx.M

(λy.M)[x := N] ≡ λy.(M[x := N]), if x ≠ y, provided y 不属于 FV(N)

为了代入Lamda抽象，有时候还必须得对表达式进行一下alpha变换。举个例子来说吧，代入(λx.y)[y := x]得到(λx.x)就是不对的，因为代入的x本来是个自由变量，结果一代入就被绑定了。正确的代入结果应该是(λz.x)，有点像是对Lambda抽象进行了一个alpha变化，但需要注意的是alpha变化和代入的定义是完全不同的。

Beta推导

Beta推导其实前面也讲过，它是为了揭示函数application的特性。Beta推导的定义是通过代入来定义的：

((λV.E) E′)的beta推导就是E[V := E′].

举例，有一个2，7，x的编码函数((λn.n×2) 7)，其beta推导就有((λn.n×2) 7) → 7×2.

Eta变换

Eta变换是为了揭示扩展性，它是说当且仅当两个函数对所有的参数都能产生相同的结果的时候，我们才认为这两个函数是相同的。如果x是f中的变量且不是自由变量，λx.(f x)可以Eta变换成f。

Notation:

为了保证Lambda表示式的简洁明快，会有如下的约定：

不保留最外层的括号：MN实际上就是(MN)
Application是左优先的：MNP实际上就是(MN)P
Lambda抽象的函数体是尽可能向右衍生的：λx.M N实际上是λx.(M N) 而并不是(λx.M) N
多个连续的Lambda抽象是可以缩减的：λx.λy.λz.N可以缩减为λxyz.N

Lambda演算的应用

有了上面这些定义，我们就可以利用Lambda演算来做一些推导，来看看函数式编程语言的一些特性如何来用Lambda演算来进行表达。

自然数

比如自然数0，1，2，3可以如下定义：

0 := λf.λx.x

1 := λf.λx.f x

2 := λf.λx.f (f x)

3 := λf.λx.f (f (f x))

怎么理解呢？先看0：

λf.λx.x := f -> (x->x)

也就说变量f在Lambda抽象中没有起到任何作用，这就是0。

再看1：

λf.λx.f x := f->(x->f(x))

fx是一个函数调用，表示的是把x应用到f得到f(x)。那整个表达式的意思就是描述这么一个函数，输入变量f，x（f，x可能是表达式，是合法的Lambda词汇）得到f（x）这样的效果，f进行了一次递归运算。

接着就是2：

λf.λx.f (f x) ：= f->(x->f(f(x)))

这里输入f，x得到f(f(x))，f进行了两次递归运算。

这个定义很晦涩，f的参与递归运算次数（阶数）就是自然数，这其实某种程度上反映了自然数的本质，2实际上就是1的二阶。

操作符

接下来，看看自增（++）函数的操作定义：

SUCC := λn.λf.λx.f (n f x)

自增函数以n作为输入，返回n+1. 这个定义看起来也很是晦涩，但实际上基于前面的定义，SUCC的推导是很完备的。首先看nfx, 基于前面的定义，其中f总共出现了n次。将n代入nfx则有：

将nfx代入SUCC的定义，则有:

这下f总共出现n+1次，根据上面的定义，这不就是n+1嘛。

PLUS的定义也很简单：

PLUS := λm.λn.λf.λx.m f (n f x)

首先看nfx，前面推导过了，有

再看mf(nfx)，则有：

将前面得到的nfx代入mf(nfx)，则有：

这样f就一共出现了m+n次，那最终则有：

这就是m+n。呵呵，很完美吧。

逻辑判断

接下来看看逻辑判断的例子：

TRUE := λx.λy.x

FALSE := λx.λy.y

AND := λp.λq.p q p

上面这三个定义是正确的，为什么是正确的呢？下面的推导可以帮助你理解它的正确性：

AND TRUE FALSE

≡ (λp.λq.p q p) TRUE FALSE →β TRUE FALSE TRUE

≡ (λx.λy.x) FALSE TRUE →β FALSE

递归函数

最后来看看递归函数的例子，递归函数也可以归结为Lambda演算。根据递归的概念，递归函数需要使用递归函数自身。如果用Lambda演算表示这种概念，一个直接的想法是递归函数也许可以表示成这种形式：(λx.x x) y 。xx表示的是把自身作为输入又传递给自身，由于两个x都指向的是y，那么y一定有一个特殊的能力：将Lambda表达式自身作为参数传递给自己。

举个阶乘的例子吧，阶乘的递归定义大家都很清楚，可以写成这样：

F(n) = 1, if n = 0; else n × F(n − 1).

为了描述这个函数，需要引入一个中间Lambda词汇r：

G := λr. λn.(1, if n = 0; else n × (r (n−1)))

其中r能将自身作为输入传递给自身。什么样的Lambda词汇这么神奇，能够具有这样的特性呢？答案就是Fix-Point combinator。怎么理解这个东西呢？大家可能知道函数的fix-point，所谓函数的fix-point指的是函数f的某一个或几个值点x，使得f(x) = x。比如x^2的fix-point就是0和1，因为0^2 = 0，1 ^2 =1。这是值域空间的fix-point，如果x可以是函数的话，这就是所谓的Fix-point combinator，它的特性就是Yg = g（其中Y就是Fix-Point combinator）。找到了Y（Fix-point comibnator），把Y作为r代入到G中，就可以得到阶乘函数的最终定义。因此基于上面的定义，就可以得到阶乘函数F的Lambda演算定义:

F(n) =(YG)n

其中G := λr. λn.(1, if n = 0; else n × (r (n−1)))

至于Y，实际上有很多可能的定义满足这样Fix-point combinator的特性，最简单的就是

Y := λg.(λx.g (x x)) (λx.g (x x))

通过上面的描述，我们可以得出，任何递归函数都可以归结为一个Lambda application （YG），其中G和具体的函数相关，而Y则是统一的，和具体的函数无关。通过分析递归函数的Lambda演算形式，可以帮助我们分析递归函数的本质特性，同时也有助于我们在设计函数式语言时考虑递归的实现。

Lambda演算与函数式语言的关系

讲了这么多，有人可能会问？Lambda演算和函数式编程语言到底有什么关系?

实际上你可以认为任何面向过程的编程语言（包括函数式编程语言）都是某种形式的Lambda演算，只不过这些语言同时又提供了一些额外的过程抽象。

Lambda演算重新精炼了函数的概念，并且使得函数像值一样成为“一等公民”，但这也大大增加了函数式编程语言实现的复杂性。

匿名函数

在古老的Lisp语言中，平方函数可以被表示成如下的一个Lambda表达式：

(lambda (x) (*xx))

上面的例子是一个表达式用来演算一个函数。符号Lambda创建了一个匿名函数，这个函数的参数是x，而表达式（*xx）是函数体。其它的函数式语言比如Haskell的匿名函数创建也采用了同样的语法，因此，匿名函数有时候也被称之为Lamda表达式。

像Pascal这样的命令式语言很早就支持通过函数指针把子程序当作参数传递给其他的子程序。但是仅仅有函数指针还不够，要想让函数成为编程语言的“一等公民”，必须要让函数的新的实例在runtime时可以被动态创建。函数的动态创建在C++，Scala，C#等语言中已经得以支持。

推导策略

对于函数式编程语言而言，其实质都是Lamda演算，函数式语言的语法都对应着相应的Lambda词汇。根据前面的定义，这些Lamda词汇在编译执行的时候往往都需要进行推导，比如beta推导，eta推导，alpha推导等等，这些推导什么时候进行，这就是各个函数式语言需要考虑的问题，有的函数式语言是eager evaluation的策略，而有的函数式语言采用的则是lazy evaluation的策略。这些具体的策略有什么不同，这里就不赘述了，作为码农大概了解一下即可。

关于复杂度

Beta推导的思想看起来很简单，但它并不是一个原子的过程，那么这就意味着在估计计算复杂度时它的代价是颇为可观的，并不能忽略不计。为了精确估计复杂度，编译器需要找出绑定变量V在表达式E中出现的所有位置，这就意味着时间开销，编译器同时又必须用某种方法来存放这些绑定变量的位置，这就意味着空间开销。如果简单的搜索表达式E中V出现的位置，这是一个o(n)的复杂度（其中n为E的长度）。Lambda演算采用了一些特殊的方法来搜索并保存这些绑定变量的出现位置，比如explicit substitution和director strings等等，这里就不再赘述。

并发

Lambda演算的特性决定了演算（beta推导）可以以任何顺序被执行，甚至是并行。这就意味着各种推导策略之间实际上相互之间是有关联的。Lambda演算没有为并行提供一种显式的支持，函数式语言可以为Lambda演算添加类似Future之类的支持，实际上还有其他的并发机制被开发出来并添加到Lambda演算。

语义

最后的问题是，Lambda词汇的语义到底是什么？你可以理解为寻找集合D，该集合D和将函数自身作为输入参数的函数的空间D->D是同构的。（好吧，原谅无知的我，我终究没看懂这一段。。。但其大概意思就是说Lambda词汇的目的就是寻找一个集合D，而且70年代又有大牛理论证明这个集合是存在的，从而使得Lambda演算的理论模型得以成立）

总结下，通过Lambda演算，你可以理解函数式语言的实现，理解函数式语言为什么能够并发。当然，对于一般码农来讲，理解这个似乎也不能帮助你的工作，但多一点深入的理解总没有什么坏处。

标签：函数,演算,评论,收藏,赞同,类型,程序设计,Lambda,语言
来源： https://www.cnblogs.com/cx2016/p/11373601.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。

ICode9

类型和程序设计语言

当前标签：简单易懂的程序语言入门小册子

当前标签：简单易懂的程序语言入门小册子

你好，类型：

zzfx：我的最爱Lambda 演算

积分与排名

随笔分类 (5508)

Lambda Calculus + 新浪：http://blog.sina.com.cn/s/blog_68ffc7a4010169rl.html

Lambda Calculus