Church 计数和 Lambda 演算

src

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

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

定义

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

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

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

<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 y，y是一个被λ约束的变量，而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到世界万物

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

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

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

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

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