Lambda 学习笔记

历史

莱布尼茨曾有过以下两个想法：

1. 创造一门‘形式语言’，来描述所有可能的问题
2. 找到一种方法，可以解决所有该形式语言描述的问题

第二个问题被称为Entscheidungsproblem（可判定性）。
1936年，Turing 和 Church 分别推出了两种不同的模型来解决可计算问题。
Church 提出了一个形式系统叫做 lambda 演算，并通过这一系统定义了可计算函数的符号表示。
Turing 提出了图灵机模型。

依据图灵机模型，冯诺依曼型计算机被创造。指令式语言，如 Fortran，Pascal 等都是以图灵机为基础，他们都依赖于状态序列。
而函数式语言，如 ML，Lisp，Haskell等则是以 lambda 演算为基础。

Lambda

Lambda 演算由3个部分（lambda terms)组成：expressions, variables, abstractions.
lambda terms 定义如下：

<expression> := <name>|<function>|<application>
<function>   := λ <name>.<expression>  (also called abstraction)
<application>:= <expression><expression>

• name(variables) 为一个无限长的标识符集合，如 V = {v,v',v'',v'''...}
• 表达式是可以是一个标识符或者一个函数抽象或者是两者的组合
• 函数抽象由两部分组成：头部和函数体。头部为 λ 加上一个标识符，body 为一个表达式。使用 . 进行分隔。一个简单的例子：λx.x

函数应用

我们把 FA 称为函数应用，把表达式 F 看做是一个算法，而表达式 A 看做一个输入。
表达式可以自己应用自己, FF，这样可以实现递归。
函数应用默认为左结合，即 E1E2E3 . . . En == ((E1E2)E3). . . En)

Free and bound variables

在函数抽象中，如果函数体中存在的标识符存在于头部, 称为绑定标识符（bound variables）。在函数应用中，输入会被代换到绑定的标识符上。
不存在于头部的，称为自由标识符（free variables)。
比如下面这个表达式中，x 为 bound variable，y 为 free variable
λx.xy
注意 λx.xy 与 λx.xz 并不等价，因为 y 和 z 可能不相等。而 λxy.xy 与 λab.ab 是等价的，我们可以通过下面的 alpha 替换得到。

Alpha 替换

我们可以在命名不冲突的情况下，把表达式中绑定的标识符替换为其他标识符。

(λz.z) ≡ (λy.y) ≡ (λt.t) ≡ (λu.u)

Beta 化简

在函数应用中，我们用输入的表达式代入到函数体中绑定的标识符上，这一过程称为 Beta 化简。

 (λx.xy)z   
 [x:=z]   把 z 代入到函数体中的 x
 zy

一个复杂的例子：

 ((λx.x)(λy.y))z 
[x:=(λy.y)]
(λy.y)z
[y:=z]
z

柯理化

当我们的表达式有多个参数的时候，可以以柯理化的方式表示:
λxy.xy 与 λx.(λy.xy) 是等价的。

(λxy.xy)wz ≡ (λx.(λy.xy))wz ≡ wz

(λx.(λy.xy))wz
[x:=w]
(λy.wy)z
[y:=z]
wz

Normal form

我们可以通过 Beta 化简不断使用一个表达式去替换另一个表达式，重复这一过程，直到无法再替换后所得到的表达式称为 normal form。
一个例子, 2000/100 并不是 normal form，而完全计算后的 2 是 normal form。
另一个例子， λx.x 为 normal form， 而 (λx.x)z 不是 normal form，它可以被化简为 z，这才是 normal form。
并不是所有的表达式都能化简到 normal form 的。比如下面这个例子：

(λx.xx)(λx.xx)
[x:=(λx.xx)]
(λx.xx)(λx.xx)