lambda 演算学习

guitarhua 2013-08-21

展开全文

前言

因为最近在学习组合范畴文法，也就是CCG（combinatory categorial grammar）。这种文法在表达语义的过程中使用到一些关于lambda演算的一些知识，所以在网上找到一些资料错略的学习了一下。在这里把所学习的内容整理一下以便以后学习参考。

lambda演算（lambda calculus 或者 λ-calculus）

先简单介绍一下历史。当年莱布尼茨leibniz有两个理想：（1）希望能够创造一种能够描述任何问题的语言，（2）找到一种能够解决用这种通用语言描述的问题的通用方法，这个问题也就是Entscheidungsproblem （这是德语，其实就是decision problem，我们经常说的判定问题）。对于第二个遐想，1936年Church发明了一种形式系统也就是lambda calculus，并指出判定问题是无解的。lambda演算还能够清晰的定义什么是一个可计算的函数。之后，lambda演算对函数式的编程语言（如 Lisp）的发展有很重要的影响，并且在λ-演算的基础上，发展起来的π-演算、χ-演算，成为近年来的并发程序的理论工具之一，许多经典的并发程序模型就是以π-演算为框架的。

1 lambda演算是什么？

lambda演算是一个形式系统（形式系统主要是由形式语言加上推理规则或转换规则构成的集合），它主要是被用来研究函数定义，函数应用和递归。简单点说，lambda演算就是一个小的形式系统，它主要表达了计算机计算中两个概念：“代入”和“置换”。“代入”通俗点解释就是和我们平常接触的函数调用类似，比如用实参代入到形参。“置换”一般理解为变量换名规则。“代入”就是后面要讲到的lambda演算中的β-规约，而“置换”相当于lambda 演算中的α--变换。

2 lambda演算相关的概念和定义

lambda表达式主要由以下元素构成：

变量： v₁, v₂, ..., v_n, ...

抽象符号： λ 和 . （一个点）

左右括号 ( )

还有两个:规约：→ 和等价：=

lambda表达式的集合 Λ, 递归定义如下：

(1)如果x是一个变量，那么 x ∈ Λ

(2)如果 x 是一个变量，且 M ∈ Λ, 那么 (λx.M) ∈ Λ

(3)如果 M, N ∈ Λ, 那么 (M N) ∈ Λ

λ-项
λ-项在一些文章中也称为λ表达式（lambda expression），它是由上面字母表中的合法字符组成的表达式，合法的表达式组成规则如下：

1. 任一个变元是一个项

2. 若M，N是项，则（MN）也是一个项（function application，函数应用）

3. 若M是一个项，而x是一个变元，则（λx.M）也是一个项（function abstraction，函数抽象）

4. 仅仅由以上规则归纳定义得到的符号串是项

说明1：λ-项是左结合的，意思就是若f x y都是λ-项，那么f x y＝(f x) y

说明2：(λx.M)这样的λ-项被称为函数抽象，原因是它常常就是一个函数的定义，函数的参数就是变量x，函数体就是M，而函数名称则是匿名的。用一个不恰当的比喻来说，我们通常认为的函数f(x)=x+2，可以被表达为λx.x+2。因为＋是未定义的，所以这个比喻只是为了方便理解而已。

说明3：MN这样的λ-项被称为函数应用，原因是它表达了将M这个函数应用到N这个概念。沿用上面的例子f(x)=x+2，那么f(2)=2+2；同样的λx.x+2表达了f(x)的概念，那么（λx.x+2）2表达了f(2)的概念。其中M＝λx.x+2，N＝2，所以MN＝（λx.x+2）2。

说明4：注意说明3只是为了方便理解，但是还存在很多与直观理解不符合的地方。例如xy也是一个合法的λ-项，它们也是MN形式的，不过x和y都仅仅是一个变量而已，谈不上函数代入。

上面是λ-项的形式化定义，有一些是可以与函数理论直观联系的，而另一些只是说明这个λ-项是合法的，不一定有直观的字面意义。

λ-项中的自由变量（free variable）和绑定变量（bond variable）
在一个λ-项中，变量要么是自由出现的，要么是被一个λ符号绑定的。还是以函数的方式来理解变量的自由出现和绑定。例如 f(x)=xy这个函数，我们知道x是和函数f相关的，因为它是f的形参，而y则是和f无关的。那么在λx.xy这个λ-项中，x就是被λ绑定的，而y则是自由出现的变量。

直观的理解，被绑定的变量就是作为某个函数形参的变量，而自由变量则是不作为任何函数形参的变量。

Lambda变量绑定规则：

（1）在表达式x中，如果x本身就是一个变量，那么x就是一个单独的自由出现。

（2）在表达式λ x. E中，自由出现就是E中所有的除了x的自由出现。这种情况下在E中所有x的出现都称为被表达式中x前面的那个λ所绑定。

（3）在表达式(MN )中，变量的自由出现就是M和N中所有变量的自由出现。

另一种关于变量的自由出现的规则也许更直接：

（1）free(x) = x

（2） free(MN) = free(M) ∪ free(N)

（3） free(λx ? M) = free(M) – {x}

为什么要花大力气来给出变量自由出现的规则，是因为后面的很多地方要用到变量的自由出现的概念。例如α-变换和β-归约。

例子：分析λf.λx.fx中变量的自由出现和绑定状况。

λf.λx.fx =λf.E, E=λx.fx

E=λx.A, A=A1A2, A1=f, A2=x

所以在A中f和x都是自由出现的，

所以E中x是绑定λ x

所以整个公式中f是绑定第一个λ f的。

注意：如果一个λ-项中没有自由变量，那个这个λ-项是闭合的（closed，也可称为：组合子combinator）

α-变换（α-conversion）（置换，换名）

α-变换规则试图解释这样一个概念，λ演算中约束变量的名称是不重要的，例如λx.x和λy.y是相同的函数。因此，将某个函数中的所有约束变量全部换名是可以的。但是，换名需要遵循一些约束。

首先是一个说明：如果M，N是λ-项，x在M中有自由出现，若以N置换M中所有x的自由出现（M中可能含有x的约束出现），我们得到另一个λ-项，记为M[x/N]。

α-变换规则如下：

λx.M=λy.M[x/y] 如果y没有在M中自由出现，并且只要y替换M中的x，都不会被M中的一个λ绑定。

例子：λx.( λx.x)x = λy(λx.x)y

1.	((λ x x) x)	α-reduction on "(λ x x)", substituting "y1" for "x" ==>
	((λ y1 y1) x)
2.	((λ x x)(λ x (x x)))	α-reduction on "(λ x x)", substituting "y1" for "x" ==>
	((λ y1 y1)(λ x (x x)))
3.	(λ x (λ x (x x)))	α-reduction on "(λ x (λ x (x x)))", substituting "y1" for "x" ==>
	(λ y1 (λ x (x x)))