learnxinyminutes-docs/zh-cn/lambda-calculus.md
2024-12-08 23:21:12 -07:00

221 lines
6.2 KiB
Markdown
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

---
contributors:
- ["Max Sun", "http://github.com/maxsun"]
- ["Yan Hui Hang", "http://github.com/yanhh0"]
translators:
- ["Maoyin Sun", "https://github.com/simonmysun"]
---
# Lambda 演算
Lambda 演算(lambda calculus, λ-calculus),
最初由[阿隆佐·邱奇][]([Alonzo Church][])提出,
是世界上最小的编程语言.
尽管没有数字, 字符串, 布尔或者任何非函数的数据类型,
lambda 演算仍可以表示任何图灵机.
[阿隆佐·邱奇]: https://zh.wikipedia.org/wiki/%E9%98%BF%E9%9A%86%E4%BD%90%C2%B7%E9%82%B1%E5%A5%87
[Alonzo Church]: https://en.wikipedia.org/wiki/Alonzo_Church
Lambda 演算由三种元素组成: **变量**(variables)、**函数**(functions)和**应用**(applications)。
| 名称 | 语法 | 示例 | 解释 |
|------|----------------------|-----------|--------------------------------------------------|
| 变量 | `<变量名>` | `x` | 一个名为"x"的变量 |
| 函数 | `λ<参数>.<函数体>` | `λx.x` | 一个以"x"(前者)为参数、以"x"(后者)为函数体的函数 |
| 应用 | `<函数><变量或函数>` | `(λx.x)a` | 以"a"为参数调用函数"λx.x" |
最基本的函数为恒等函数: `λx.x`, 它等价于`f(x) = x`.
第一个"x"为函数的参数, 第二个为函数体.
## 自由变量和约束变量:
- 在函数`λx.x`中, "x"被称作约束变量因为它同时出现在函数体和函数参数中.
- 在`λx.y`中, "y"被称作自由变量因为它没有被预先声明.
## 求值:
求值操作是通过[β-归约][]([β-Reduction][])完成的,
它本质上是词法层面上的替换.
[β-归约]: https://zh.wikipedia.org/wiki/%CE%9B%E6%BC%94%E7%AE%97#'%22%60UNIQ--postMath-0000006F-QINU%60%22'-%E6%AD%B8%E7%B4%84
[β-Reduction]: https://en.wikipedia.org/wiki/Lambda_calculus#Beta_reduction
当对表达式`(λx.x)a`求值时, 我们将函数体中所有出现的"x"替换为"a".
- `(λx.x)a`计算结果为: `a`
- `(λx.y)a`计算结果为: `y`
你甚至可以创建高阶函数:
- `(λx.(λy.x))a`计算结果为: `λy.a`
尽管 lambda 演算传统上仅支持单个参数的函数,
但我们可以通过一种叫作[柯里化][]([Currying][])的技巧创建多个参数的函数.
[柯里化]: https://zh.wikipedia.org/wiki/%E6%9F%AF%E9%87%8C%E5%8C%96
[Currying]: https://en.wikipedia.org/wiki/Currying
- `(λx.λy.λz.xyz)`等价于`f(x, y, z) = ((x y) z)`
有时`λxy.<body>`与`λx.λy.<body>`可以互换使用.
----
认识到传统的 **lambda 演算没有数字, 字符或者任何非函数的数据类型**很重要.
## 布尔逻辑:
在 lambda 演算中没有"真"或"假". 甚至没有 1 或 0.
作为替换:
`T`表示为: `λx.λy.x`
`F`表示为: `λx.λy.y`
首先, 我们可以定义一个"if"函数`λbtf`, 它当`b`为真时返回`t`,
`b`为假时返回`f`
`IF`等价于: `λb.λt.λf.b t f`
通过`IF`, 我们可以定义基本的布尔逻辑运算符:
`a AND b`等价于: `λab.IF a b F`
`a OR b`等价于: `λab.IF a T b`
`NOT a`等价于: `λa.IF a F T`
*注意: `IF a b c`本质上指: `IF((a b) c)`*
## 数字:
尽管 lambda 演算中没有数字,
我们还可以用[邱奇编码][]([Church numerals][])将数字嵌入到 lambda 演算中.
[邱奇编码]: https://zh.wikipedia.org/wiki/%E9%82%B1%E5%A5%87%E7%BC%96%E7%A0%81
[Church numerals]: https://en.wikipedia.org/wiki/Church_encoding
对于任意数字 n: <code>n = λf.f<sup>n</sup></code> 所以:
`0 = λf.λx.x`
`1 = λf.λx.f x`
`2 = λf.λx.f(f x)`
`3 = λf.λx.f(f(f x))`
要增加一个邱奇数, 我们使用后继函数`S(n) = n + 1`:
`S = λn.λf.λx.f((n f) x)`
使用后继函数, 我们可以定义加法:
`ADD = λab.(a S)b`
**挑战**: 试定义乘法函数!
## 变得更小: SKI, SK 和 Iota
### SKI 组合子演算
令 S, K, I 为下列函数:
`I x = x`
`K x y = x`
`S x y z = x z (y z)`
我们可以将 lambda 演算中的表达式转换为 SKI 组合子演算中的表达式:
1. `λx.x = I`
2. `λx.c = Kc`
3. `λx.(y z) = S (λx.y) (λx.z)`
以邱奇数 2 为例:
`2 = λf.λx.f(f x)`
对于里面的部分 `λx.f(f x)`:
```
λx.f(f x)
= S (λx.f) (λx.(f x)) (case 3)
= S (K f) (S (λx.f) (λx.x)) (case 2, 3)
= S (K f) (S (K f) I) (case 2, 1)
```
所以:
```
2
= λf.λx.f(f x)
= λf.(S (K f) (S (K f) I))
= λf.((S (K f)) (S (K f) I))
= S (λf.(S (K f))) (λf.(S (K f) I)) (case 3)
```
对于第一个参数`λf.(S (K f))`有:
```
λf.(S (K f))
= S (λf.S) (λf.(K f)) (case 3)
= S (K S) (S (λf.K) (λf.f)) (case 2, 3)
= S (K S) (S (K K) I) (case 2, 3)
```
对于第二个参数`λf.(S (K f) I)`有:
```
λf.(S (K f) I)
= λf.((S (K f)) I)
= S (λf.(S (K f))) (λf.I) (case 3)
= S (S (λf.S) (λf.(K f))) (K I) (case 2, 3)
= S (S (K S) (S (λf.K) (λf.f))) (K I) (case 1, 3)
= S (S (K S) (S (K K) I)) (K I) (case 1, 2)
```
综上:
```
2
= S (λf.(S (K f))) (λf.(S (K f) I))
= S (S (K S) (S (K K) I)) (S (S (K S) (S (K K) I)) (K I))
```
如果展开这个表达式, 我们最终又会得到邱奇数 2 的相同的表达式.
### SK 组合子演算
SKI 组合子演算还可以进一步简化. 我们可以通过`I = SKK`移除 I 组合子.
我们可以将所有的 `I` 替换为 `SKK`.
### ι 组合子
SK 组合子仍不是最简的. 定义:
```
ι = λf.((f S) K)
```
我们有:
```
I = ιι
K = ι(ιI) = ι(ι(ιι))
S = ι(K) = ι(ι(ι(ιι)))
```
## 更多阅读:
1. [A Tutorial Introduction to the Lambda Calculus](http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf)(英文)
2. [Cornell CS 312 Recitation 26: The Lambda Calculus](https://courses.cs.cornell.edu/cs312/2008sp/recitations/rec26.html)(英文)
3. [Wikipedia - Lambda Calculus](https://en.wikipedia.org/wiki/Lambda_calculus)(英文)
4. [Wikipedia - SKI combinator calculus](https://en.wikipedia.org/wiki/SKI_combinator_calculus)(英文)
5. [Wikipedia - Iota and Jot](https://en.wikipedia.org/wiki/Iota_and_Jot)(英文)
6. [λ演算 - 维基百科,自由的百科全书](https://zh.wikipedia.org/wiki/SKI%E7%BB%84%E5%90%88%E5%AD%90%E6%BC%94%E7%AE%97)
7. [SKI组合子演算 - 维基百科,自由的百科全书](https://zh.wikipedia.org/wiki/SKI%E7%BB%84%E5%90%88%E5%AD%90%E6%BC%94%E7%AE%97)