与图灵机具有相同的运算能力还不够伟大?那么 Lambda 演算可以做到“虚无生两极,两极生四象,四象生八卦”,感谢 Church,我们最终获得世界万物。

Lambda 演算,也称为λ-演算,是一个形式定义系统去,我们用它研究函数定义、实现、递归,也是函数语言的计算模型。

定义

一个 λ 表达式应该由以下的部分构成

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

一个合法的 λ 表达式可以按照如下递归定义:

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

λ表达式记号法

对于 λ 表达式 M 和 N,

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

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

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

比如说,对于表达式 λ y . x x yy是一个被λ约束的变量,而x则是自由变量。

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

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

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

归约方法

α变换

就是符号替换。没什么意思,就是进行归约的时候如果出现符号名冲突时可以对符号进行重命名。不过α变换只在当前域中有效。对表达式 λ x x. x,可以变换成 λy x. x,而不可以变换成 λy x.y。因为名字本身在λ表达式中是不重要的。

替换: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

η变换

表达了“外延性”的思想。

如果说两个函数是等价的,那么它们必须对所有传入的参数都能得到一致的结果。也就是对这两个函数,作β归约或者α变换得到的λ表达式一致。

从0到世界万物

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

1
2
3
4
5
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)的过程如下

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
(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

同样可以定义出其他算术运算和逻辑运算

再次感谢Church,给我们建立了这个世界。

附 SICP 练习 2.6 的答案:

1
2
3
4
(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))))