λ 演算
大约 2 分钟
本文是 λ 演算的介绍。
1. 什么是 λ 演算
λ 演算（lambda calculus，λ-calculus）是一套从数学逻辑中发展，以变量绑定和替换的规则，来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。它由数学家 阿隆佐·邱奇 在 20 世纪 30 年代首次发表。λ 演算作为一种广泛用途的计算模型，可以清晰地定义什么是一个可计算函数，而任何可计算函数都能以这种形式表达和求值，它能模拟单一磁带图灵机的计算过程；尽管如此，λ 演算强调的是变换规则的运用，而非实现它们的具体机器。[1]
lambda 演算包括了建构 lambda 项，和对 lambda 项执行归约的操作。在最简单的 lambda 演算中，只使用以下的规则来建构 lambda 项：
| 语法 | 名称 | 描述 |
|---|---|---|
x | 变量 | 用字符或字符串来表示参数或者数学上的值或者表示逻辑上的值 |
(λx.M) | 抽象化 | 一个完整的函数定义（M 是一个 lambda 项），在表达式中的 x 都会绑定为变量 x |
(M N) | 应用 | 将函数 M 作用于参数 N，M 和 N 是 lambda 项 |
产生了诸如 λf.λx.(f (f x)) 的表达式。如果表达式是明确而没有歧义的，则括号可以省略。
为了方便理解，我们使用 JavaScript 的箭头函数来表示 lambda 演算中的抽象化和应用：
f => x => f(f(x))邱奇编码（Church Encoding）
为了更方便地进行下面的讨论，我们可以给一个λ项命名，例如：
swap := λx.λy.y x那么
swap a b ≡ (λx.λy.y x) a b → b aΛ 演算，维基百科，https://zh.wikipedia.org/wiki/Λ演算 ↩︎