The Lambda Calculus

Syntax

Lambda演算的基本语法像这样：

1
(+ 4 5)

运算符用前缀记法来表示。嵌套的运算则这样表示：

1
(+ (* 2 4) (* 3 8))

要注意的是这里的求值顺序实际上是不确定的，比如我们可以

1
2
3
4
(+ (* 2 4) (* 3 8))
(+ 8       (* 3 8))
(+ 8       24     )
32

也可以

1
2
3
4
(+ (* 2 4) (* 3 8))
(+ (* 2 4) 24     )
(+ 8       24     )
32

求值顺序的不确定将在后面的章节探讨。

PS. 这里的语法和Lisp好像。

函数和柯里化

函数应用在函数式语言中太重要了以至于这里省略了括号（是的！）

1
f x

表示“函数f应用到参数x”。但是多个参数怎么办呢？当然我们可以写(f (x,y))，不过我们可以利用柯里化

1
((+3) 4)

一次只应用一个参数。

括号

没有歧义的情况下，我们可以省略不必要的括号

1
2
(+ 2 3)
+ 2 3

lambda抽象

定义一个函数很简单，只需要

1
(λx . + x 1)

定义了一个函数以x为参数，将x加一。

总结

Lambda演算有这样的文法

1
2
3
4
<exp> ::= <constant>            内建常数
      |   <variable>            变量名字
      |   <exp> <exp>           函数应用
      |   λ <variable> . <exp>  Lambda抽象(函数定义)

之后我们将使用小写字母来表示变量，单个大写字母表示Lambda表达式(Lambda expression E)，
大写字母表示内置的函数名。

Lambda Calculus的操作语义

Lambda Calculus之所以叫做这个名字是因为可以做”Calculate”，换句话说就是转换规则。
在这之前，先介绍一些术语。

约束和自由变量

自由出现的定义:

  • x在x中自由出现(但并不在其他变量或常量中)
  • x在(E F)中自由出现 当且仅当 x在E中自由出现 或 x在F中自由出现
  • x在λy.E 中自由出现 当且仅当 x在E中自由出现 且 x和y是不同的变量

约束出现的定义:

  • x在(E F)中约束出现 当且仅当 x在E中约束出现 且 x在F中约束出现
  • x在λy.E 中约束出现 当且仅当 x在E中约束出现 或 x和y是相同变量且x在E中自由出现

Beta转换

1
2
(λx . + x 1) 4        <->        (+ 4 1)
                Beta-conversion

后面的章节很多是在讨论这个过程的高效实现。

Alpha转换

1
2
(λx . + x 1)        <->        (λy . + y 1)
              Aplha-conversion

Eta转换

1
2
3
4
5
6
7
8
(λx . + 1 x)        <->        (+ 1)
               Eta-conversion
               
(λx . F x)          <->        F
               Eta-conversion
               
      F             <->        (λx . F x)
               Eta-conversion

一个新符号

1
(λx . E) M        ==        E[M/x]

表示将所有约束出现的x替换为M。

化简规则

Normal Reduction Order被证明足够良好。
所谓Normal Order，就是从左到右依次求值。

递归函数

Y

我们可以抽象出组合子Y来表达递归，使得

1
Y H = H (Y H)

Y的纯Lambda演算定义

1
Y＝ (λh. (λx. h (x x)) (λx. h (x x)))

Lambda演算的表示语义

Eval函数

Eval函数用来将表达式转换为值，若E1 <-> E2，则Eval[E1] == Eval[E2]。