函数式编程 - λ演算
λ演算是由Alonzo Church在20世纪30年代开发的一个框架，用于研究函数的计算。
函数创建 − Church引入了λx.E 表示法来表示函数，其中'x'是形式参数，'E'是函数体。这些函数可以是无名函数，并且只有一个参数。
函数应用 − Church使用E1.E2表示法来表示将函数E1应用于实际参数E2。所有函数都只有一个参数。
λ演算的语法
λ演算包括三种不同的表达式，即：
E :: = x(变量)
| E1 E2(函数应用)
| λx.E(函数创建)
其中λx.E称为λ抽象，E称为λ表达式。
λ演算的求值
纯λ演算没有内置函数。让我们求值以下表达式：
(+ (* 5 6) (* 8 3))
这里，我们不能从'+'开始，因为它只对数字进行操作。有两个可约表达式：(* 5 6) 和 (* 8 3)。
我们可以先约简其中一个。例如：
(+ (* 5 6) (* 8 3)) (+ 30 (* 8 3)) (+ 30 24) = 54
β-归约规则
我们需要一个归约规则来处理λ。
(λ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。例如：
α-归约
α-归约非常简单，可以在不改变λ表达式的含义的情况下完成。
λ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
Church-Rosser定理
Church-Rosser定理陈述如下：
如果E1 ↔ E2，则存在一个E，使得E1 → E 且 E2 → E。“以任何方式归约最终都可以产生相同的结果。”
如果E1 → E2，并且E2是范式，则存在E1到E2的正规序归约。“如果存在范式，则正规序归约将始终产生范式。”
广告