函数式编程 - Lambda 演算

---

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

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

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

Lambda 演算的语法

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

E :: = x（变量）

| E ₁ E ₂（功能应用）

| λxE（函数创建）

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

评估 Lambda 演算

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

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

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

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

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

β-减少规则

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

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

这称为β-还原。

形式参数可以使用多次 -

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

当有多个术语时，我们可以按如下方式处理它们 -

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

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

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

自由变量和绑定变量

在表达式中，变量的每次出现都是“自由”（对于 λ）或“绑定”（对于 λ）。

(λx . E) y的 β-约简将E中自由出现的每个x替换为y。例如 -

阿尔法减少

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 

丘奇-罗瑟定理

丘奇-罗瑟定理指出以下内容 -

• 如果 E1 ↔ E2，则存在一个 E，使得 E1 → E 和 E2 → E。“以任何方式减少最终都可以产生相同的结果。”

• 如果 E1 → E2，并且 E2 是正规形式，则存在 E1 到 E2 的正规阶约简。“如果存在的话，正规阶约简总是会产生一种正规形式。”