函数式编程 - Lambda 演算

Lambda 演算是 Alonzo Church 在 20 世纪 30 年代开发的一个框架，用于研究函数计算。

• 函数创建 − Church 引入了符号 λx.E 来表示一个函数，其中"x"是形式参数，"E"是函数体。 这些函数可以没有名称和单个参数。

• 函数应用 − Church 使用符号 E₁.E₂ 来表示函数 E₁ 对实际参数 E₂ 的应用。 所有的函数都只有一个参数。

Lambda 演算语法

Lambda演算包括三种不同类型的表达式，即，

E :: = x(variables)

| E₁ E₂(function application)

| λx.E(function creation)

其中 λx.E 称为 Lambda 抽象，E 称为 λ-表达式。

评估 Lambda 演算

纯 lambda 演算没有内置函数。 让我们评估以下表达式 −

(+ (* 5 6) (* 8 3)) 

在这里，我们不能以"+"开头，因为它只对数字进行操作。 有两个可约表达式:(* 5 6) 和(* 8 3)。

我们可以先减少其中任何一个。 例如 −

(+ (* 5 6) (* 8 3)) 
(+ 30 (* 8 3)) 
(+ 30 24) 
= 54

β-reduction 规则

我们需要一个归约规则来处理 λs

(λx . * 2 x) 4 
(* 2 4) 
= 8

这称为 β-reduction。

形式参数可以多次使用 −

(λx . + x x) 4 
(+ 4 4) 
= 8

当有多个term时，我们可以这样处理 −

(λx . (λx . + (− x 1)) x 3) 9 

内部x属于内部λ，外部x属于外部。

(λx . + (− x 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
= 11

自由变量和绑定变量

在表达式中，变量的每次出现都是 "free" (to λ) 或 "bound" (to a λ)。

β-reduction of (λx . E) y replaces every x that occurs free in E with y. For Example −

Alpha 缩减

Alpha 缩减非常简单，无需改变 lambda 表达式的含义即可完成。

λx . (λx . x) (+ 1 x) ↔ α λx . (λy . y) (+ 1 x) 

例如 −

(λx . (λx . + (− x 1)) x 3) 9 
(λx . (λy . + (− y 1)) x 3) 9 
(λy . + (− y 1)) 9 3 
+ (− 9 1) 3 
+ 8 3 
11