Shellex.info

在SICP的练习2.6 提到了Church计数，也就是将数据和操作引入Lambda演算，告诉我们，一旦拥有Lambda，别无所求。这些搞数学的家伙总是喜欢把可以不要的东西全全都去掉，然后用2.6这样的习题中表现出来的能力彻底雷到我。所以像我一样数学只有半桶水的同学先看看维基总是比较好：( http://en.wikipedia.org/wiki/Lambda_calculus )

Wiki：

lambda演算，也称为λ-演算，作为一个形式定义系统去研究函数定义、实现、递归。也是Lisp这类语言计算模型。

定义

一个Lambda 表达式应该由以下的东东构成

变量： v1, v2, . . .
符号：λ 和 .
括号组：( 和 )

一个合法的Lambda 表达式<expression>可以按照如下递归定义：

• <expression>  = <variable> | <function> | <application>
• <function>  = λ <variable>.<expression>
• <application> = (<expression> <expression>)

Lambda表达式记号法

对于Lambda表达式M和N，

• 最外层括号可以省略:  (M N) 可以表示成 M N.
• (λx. M)这样的表达式 被称为函数抽象，原因是它常常就是一个函数的定义，函数的参数就是变量x，函数体就是M，而函数名称则是匿名的。你可以认为它就是f(x)=M，匿名就意味这函数名’f'是不存在的，存在的仅仅是x映射到M这个过程。
• 函数应用采用左结合: M N P 表示 (M N) P.
• Lambda表达式在记法上使用贪婪扩展: 也就是说 λ x. M N 表示 (λ x.M N) ，而不是(λ x. M) N
• Lambda表达式序列: λ x λ y λ z. N 可以简写为 λ x y z . N

λ表达式中的自由变量和约束变量

对于函数抽象操作符λ，能够綁定任何出现在函数抽象体中的变量。如果一个变量处于lambda表达式的作用域内，则称该变量是受约束的。否则，则该变量是自由的。

比如说，对于表达式λ y . x x y，y是一个被λ约束变量，而x则是自由变量。
直观的理解就是y是有MM的，λ是y的MM；x是单身的，想砸酒瓶就砸酒瓶，想攒烟头就攒烟头。

由一系列自由变量组成的Lambda表达式M可以表示成 FV(M)并且得到递归定义如下：

• FV( x ) = {x}, 其中x是自由变量
• FV ( λ x . M ) = FV ( M ) – {x}
• FV ( M N ) = FV ( M ) ∪ FV ( N )

而不包含自由变量的Lambda表达式则被称为是闭合的。

归约方法

• α变换：说白了就是符号替换。没什么意思，就是进行归约的时候如果出现符号名冲突时可以对符号进行重命名。不过α变换只在当前域中有效。对表达式 λ x x. x，可以变换成λy x. x，而不可以变换成λy x.y。因为名字本身在lambda表达式中是不重要的。
• 替换：E[V:=E']表示变量V可以用E’来替换，如果E’在E中是自由的。
  比如 (λx. y)[y:=x]得出(λx. x)是错误的。因为x在λ下受到约束。正确的方法是通过α变换成(λz. y)[y:=x] 得到(λz.x)
• β归约：表达了一种函数应用的思想。对于表达式(M N)来说含义就是将函数M应用到N上。也就是说N作为形参传入函数M，作为M的约束变量在M中实现。
  用上面的定义，β归约(λ v. m) n 可以表示成 m[v:=n]
  比如说如果存在函数λ x. (+ x 2)，而且+这个操作已经实现，那么(λ x. (+ x 2)) 3的结果就是(+ 3 2)=5
• η变换：表达了“外延性”的思想。如果说两个函数是等价的，那么它们必须对所有传入的参数都能得到一致的结果。也就是对这两个函数，作β归约或者α变换得到的lambda表达式一致。

好了，现在可以开始玩λ演算了。别忘了，我们除了上面所说的东东以外什么都没有。包括’数’这个概念。so首先是自然数的定义：

0:= λ f x. f
1:= λ f x. f x
2:= λ f x. f (f x)
3:= λ f x. f (f (f x))
n:= λ f x. f^n x

可以看出，对自然数n的表示就是函数f对参数应用n次得到的lambda表达式。为了获取到整个自然数域，可以定义出INC过程用于给当前自然数n加上1：

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

同理，加法PLUS m n过程可以认为是函数应用m次再应用n次=m+n次的结果：

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

当然，也可以利用INC来对PLUS进行定义，认为是m 加一这个过程进行n次的结果：PLUS:=λ m n. n INC m

例如求解(PLUS 2 3)的过程如下

(PLUS 2 3)
(PLUS 2 3):= (((λ m n f x. n f (m f x)) 2 ) 3)
:= ((λ m n f x. n f (m f x)) (λ f x. f (f x)) (λ f x. f (f (f x))))
    其中，(m f x) [m:=λ f x. f (f x)]
    -> (λ f x. f (f x)) f x
    -> (λ x. f' (f' x)[f':= f] ) x
    -> λ x. f (f x) x
    -> f (f x')[x':=x]
    -> f (f x)
∴ (2 f x) := f (f x)
∴ PLUS 2 3 := (λ n f x. n f (f (f x))) (λ f x. f (f (f x)))
   其中 (n f)[n := λ f x. f (f (f x))]
    -> (λ f x. f (f (f x))) f
    -> (λ x. f' (f' (f' x)))[f':=f]
    -> (λ x. f (f (f x)))
∴ PLUS 2 3 := (λ f x. (λ x. f (f (f x))) (f (f x)))
∵ (λ x. f (f (f x))) (f (f x))
    -> f’ (f‘ (f’ x‘))[x’ := (f (f x))]
    -> f‘ (f‘ (f’ (f (f x))))
    ∵ f 是 λ 下的约束变量
    ∴ f'== f;
∴ PLUS 2 3 := f (f (f (f (f x)))) ＝ 5

同样可以定义出其他算术运算和逻辑运算（http://en.wikipedia.org/wiki/Church_numeral），有了这些东西，牛奶，面包，魔兽3，RMB，MM，俯卧撑，都有了咯。感谢Church，给我们建立了这个世界。

答案for SICP练习2.6:

(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))
(define (add n m)
  (lambda (f) lambda (x) ((n f) ((m f) x))))