lambda calculus:Introduction

首先，λ演算的提出者 丘奇(Alonzo Church) 是普林斯顿大学的教授。1935年，丘奇发表论文使用λ演算证明基本数论中存在不可解决的问题。1936年4月，丘奇指出自己的那篇论文可以推论出著名的 判定性问题(Hilbert Decision-problem) 是不可解决的。1936年5月，图灵发表论文使用他自己假想的计算机器(后被称为图灵机)证明了同一个问题。当时丘奇几乎是世界上唯一能够验证这篇论文正确性的人。因此丘奇将图灵收入门下读博士。之后他们共同提出了 邱奇-图灵论题(Church–Turing thesis) ，该论题的核心思想是

如果某个算法是 可计算的(Computability) ，那这个算法同样可以被图灵机，以及λ演算所实现，图灵机与λ演算是等价的。

这意味着假如你现在要自己设计一套编程语言，如果你的语言能做到图灵机或λ演算同样的事情，那么你的语言就可以解决所有的可计算问题。这时，你可以声称它是一门 图灵完备 的编程语言。下面来看看图灵机与λ演算能做什么事情

• 图灵机的基本思想大概是这样：

  1. 一条无限长的纸带TAPE。纸带被划分为一个接一个的小格子，每个格子上包含一个来自有限字母表的符号，字母表中有一个特殊的符号表示空白。纸带上的格子从左到右依次被编号为0, 1, 2, ...，纸带的右端可以无限伸展。
  2. 一个读写头HEAD。该读写头可以在纸带上左右移动，它能读出当前所指的格子上的符号，并能改变当前格子上的符号。
  3. 一套控制规则TABLE。它根据当前机器所处的状态以及当前读写头所指的格子上的符号来确定读写头下一步的动作，并改变状态寄存器的值，令机器进入一个新的状态。
  4. 一个状态寄存器。它用来保存图灵机当前所处的状态。图灵机的所有可能状态的数目是有限的，并且有一个特殊的状态。称为停机状态。

  这样一台机器就能实现目前人类已知的任何可行算法，以c为代表的命令式编程就是以这种假想模型作为理论基础。

• λ演算的基本思想大概是这样：

  1. 可以定义函数(function abstraction)
  2. 可以调用函数(function application)

  一门语言只要能做到以上两点，就可以实现任何可行算法，以lisp为代表的函数式编程以λ演算作为理论基础。

可以看到λ演算的概念要比图灵机更加简洁明了，顺便再对比一下c与lisp，以下引用 《黑客与画家》 中的描述

如果使用Lisp语言，能让程序变得多短？以Lisp和C的比较为例，我听到的大多数说法是C代码的长度是Lisp的7倍到10倍。但是最近，New Architect杂志上有一篇介绍ITA软件公司的文章，里面说"一行Lisp代码相当于20行C代码"，因为此文都是引用ITA总裁的话，所以我想这个数字来自ITA的编程实践。 如果真是这样，那么我们可以相信这句话。ITA的软件，不仅使用Lisp语言，还同时大量使用C和C++，所以这是他们的经验谈。

最后说说我自己对丘奇和图灵两位伟人的一些感想。两个同样高智商的天才，如果其中一个有情商缺陷，那么那个有情商缺陷的人智商总是会被莫名其妙的放大，这也许就是为什么影视剧作品中总是要以低情商来塑造一个天才（参照福尔摩斯与谢尔顿·库珀）再加上如果某个人的一生以悲剧结尾，那么人们将进一步放大他所做的贡献。关于丘奇与图灵的更多内容可以阅读 图灵的光环 。

二.λ演算的语法

1.λ表达式

λ表达式只遵循以下三条规则：

1. 变量，比如 x 就是合法的λ表达式
2. 如果y是λ表达式，x是变量，则 λx.y 是合法的λ表达式（又称为函数声明或lambda abstraction），它代表输入x返回y的匿名函数。等价的js(本文均指 ecmascript6 )写法是 x=>y 。 λx.x+y 也是合法的，它表示一个函数输入x，返回x与未知的y的和。
3. 如果t和s都是λ表达式，则 (t s) 也是λ表达式（又称为函数应用或application），它代表使用参数s调用函数t，等价的js写法是 t(s) 。

所有合法的λ表达式都是通过重复这三条规则得到的，不过为了保持表达式的整洁，大家一般遵循以下惯例（暂时看不明白也没关系）:

1. 最外层的括号可以省略， (M N) 可以写成 M N 。
2. 函数应用左聚合， (M N) P 可以写成 M N P 。
3. 函数定义时，函数体尽可能向右扩展， λx.M N 应该解释为 λx.(M N) 而不是 (λx.M) N 。
4. 函数定义序列可以被合并表达， λx.λy.λz.N 可以被缩写为 λxyz.N

2.绑定变量与自由变量

如果一个变量是一个λ表达式的参数，则称该变量绑定到该λ上，比如说 λx.x+y 中，x是绑定变量，y则称为自由变量。更详细的规则如下：

• λ表达式 x 中的自由变量就是x
• λ表达式 λx.t 中的自由变量，是t中的自由变量但不包括x，结合第一条规则来看， λx.x 的自由变量为空
• λ表达式 ts 中的自由变量，是t中的自由变量与s中的自由变量的并集，结合前两条规则， λx.x x 的自由变量是x与空集的并集，即x。

3.化简规则

下面是化简规则的“官方描述”(如果在阅读时出现恶心，头晕等不良反应，可以切换到最后的草根版本)：

• α变换(Alpha conversion)
  α变换简单理解就是λ表达式中的绑定变量可以替换变量名，例如 λx.x 与 λy.y 是α等价(Alpha equivalence)的，将 λx.x 替换成 λy.y 就称为α变换。这条规则虽然简单，但仍然要小心一些陷阱。考虑下面这个例子，对 λx.λx.x 进行α变换可以得到 λy.λx.x 但是不能得到 λy.λx.y 。其次，当α变换会导致变量被不同的函数绑定时，不允许进行变换，比如 λx.λy.x 就不能被替换成 λy.λy.y 。

• β归约(Beta reduction)

  在理解β归约之前，我们先来定义一个变量替换(substitution)操作符，假设M,N是任意λ表达式，x,y是变量，M[x:=N]表示将M中的所有自由变量x替换成表达式N，下面是一些例子：

  • 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)

  这项操作又称之为Capture-avoiding substitution，因为它必须确保变量替换后不能成为一个绑定变量，比如说 (λx.y)[y := x]=λx.x 就是不正确的，必须先对 λx.y 进行α变换，改变绑定变量名得到 λz.y ，之后再进行[y := x]操作得到 λz.x 。了解了变量替换后，β归约可以被简单的定义成：

  ((λV.E) E') = E [V:=E']

• η变换(Eta-conversion)

  η变换指的是当且仅当两个函数对所有的输入，返回同样的输出时，两个函数是相等的，这意味这x只要不是f中的自由变量，f就可以转换成 λx.f x ，一些在急性求值(eager evalution)环境下无法正常调用的函数，需要通过这条规则来进行转换，这条规则在后面学习 Y-combinator 的时候会用到，这里大致有个印象就可以了。

草根版本：

• α变换
  函数在不引发变量名冲突的情况下可以修改形参变量名，即 x=>x+y 等价于 z=>z+y
• β归约
  函数可以将实参代入函数体，即 (x=>(y=>x+y))(z) 等价于 y=>z+y ，但是如果是 (x=>(y=>x+y))(y) 则需要先进行α变换得到 (x=>(z=>x+z))(y) ，再进行β归约得到 z=>y+z ，而不是直接代入得到 y=>y+y
• η变换
  如果f是一个函数，那么 f 等价于 x=>f(x) ，因为对于任意变量 v ， f(v) 总是等于 (x=>f(x))(v)

三.简单的运算规则

1.逻辑运算

在进行逻辑运算之前，需要先定义什么是真，什么是假。下面的定义称为丘奇布尔值(Church booleans)

• TRUE = λx.λy.x 对应的js代码是 x=>(y=>x) ，柯里化之前是 (x,y)=>x （等价于丘奇数0）
• FALSE = λx.λy.y 对应的js代码是 x=>(y=>y) ，柯里化之前是 (x,y)=>y

从柯里化之前的js代码来看，丘奇布尔值就是一个接受两个参数的函数，如果为真则返回第一个参数，否则返回第二个(因为合法的λ表达式只接收一个参数，所以才写成了这种形式 λx.λy.x ，如果你还记得上面介绍的λ表达式的惯例，那么你应该知道 λx.λy.x 可以简写成 λxy.x )。有了布尔值，下面就可以在它的基础上定义出逻辑运算：

• AND = λp.λq.p q p
• OR = λp.λq.p p q
• NOT = λp.p FALSE TRUE
• IFTHENELSE = λp.λa.λb.p a b

下面简单验证 AND 表达式的正确性，尝试化简 AND TRUE FALSE

1. 第一步得到 (λp.(λq.((p q) p))) TRUE FALSE
2. 第一次β归约得到 (λq.((TRUE q) TRUE) FALSE
3. 第二次β归约得到 TRUE FALSE TRUE 即 ((λx.λy.x) FALSE) TRUE
4. 第三次β归约得到 (λy.FALSE) TRUE 即 FALSE

2.算术运算

λ演算中有多种方法可以用来定义自然数，如下定义又称为丘奇数(Church numerals)，是使用最广泛的定义方式

• 0 = λf.λx.x 对应的js代码是 f=>(x=>x) ，柯里化之前是 (f,x)=>x
• 1 = λf.λx.f x 对应的js代码是 f=>(x=>f(x)) ，柯里化之前是 (f,x)=>f(x)
• 2 = λf.λx.f (f x) 对应的js代码是 f=>(x=>f(f(x)) ，柯里化之前是 (f,x)=>f(f(x))
• 3 = λf.λx.f (f (f x)) 对应的js代码是 f=>(x=>f(f(f(x))) ，柯里化之前是 (f,x)=>f(f(f(x)))

同样从柯里化之前的js代码来看，丘奇数是一个接受两个参数的函数，对于任意数字n，它把第一个参数应用到第二个参数上n次。根据这样的思路，可以轻松实现自增函数(输入n，返回n+1的函数)

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

上面的实现思路是输入丘奇数n，在n的基础上再调用一次函数f，就能得到n+1。可以将上面的丘奇数代入该函数进行验算（跟上面的验算步骤一样，不断进行β归约即可）。有了自增函数，就可以在它的基础上继续定义加法与乘法函数：

• PLUS = λm.λn.λf.λx.m f (n f x) n+m 可以看做是在n的基础上调用m次自增函数
• MULT = λm.λn.m (PLUS n) 0 m*n 可以看做是使用丘奇数0调用m次加n函数

四.总结

上面演示的功能相当的naive，但从中已经可以领略到λ演算的思想，即先定义最简单的lambda term(函数)，之后通过将简单的表达式不断的组合来实现复杂的算法。下篇文章我打算继续学习如何使用λ演算实现递归函数，换句话说如何使用匿名函数来实现递归?

参考链接：

• Lambda_calculus
• My Favorite Calculus: Lambda (part 1)
• 图灵的光环