why lambda?
Nuclear_Fish_cyq
·
·
算法·理论
:::epigraph[——沃茨基·硕德]
哥们就爱整点抽象的，lambda 怎么你了。
:::
Part 0 引入
大家或多或少都见过现代 C++ 的 lambda 语法，这里要讲的是它的老祖宗 \lambda（即 lambda）演算。
Lambda 演算（lambda calculus, λ-calculus），最初由阿隆佐·邱奇（Alonzo Church）提出，是世界上最小的编程语言。 尽管没有数字、字符串、布尔或者任何非函数的数据类型，lambda 演算仍可以表示任何图灵机。
摘抄自 learn x in y minutes。
lambda 演算是一套从数学逻辑中发展，以变量绑定和替换的规则，来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。它由数学家阿隆佐·邱奇在 20 世纪 30 年代首次发表。lambda 演算作为一种广泛用途的计算模型，可以清晰地定义什么是一个可计算函数，而任何可计算函数都能以这种形式表达和求值，它能模拟单一磁带图灵机的计算过程；尽管如此，lambda 演算强调的是变换规则的运用，而非实现它们的具体机器。
lambda 演算可比拟最根本的编程语言，它包括了一条变换规则（变量替换）和一条将函数抽象化定义的方式。因此普遍公认是一种更接近软件而非硬件的方式。对函数式编程语言造成很大影响，比如 Lisp、ML 语言和 Haskell 语言。在 1936 年邱奇利用 Lambda 演算给出了对于判定性问题（Entscheidungsproblem）的否定：关于两个 lambda 表达式是否等价的命题，无法由一个“通用的算法”判断，这是不可判定性能够证明的头一个问题，甚至还在停机问题之先。
摘抄自维基百科。
可以看到，\lambda 演算就是计算机科学界的原始古神。
本文较为抽象，建议阅读时间十五分钟以上。
Part 1 基础
语法
这里介绍的是最常见的无类型 \lambda 演算。
由于 \lambda 演算过于抽象，以下几乎所有\lambda语句都会给出一段自创的伪代码，主要亮点在于其具有缩进。
| 语法 |
说明 |
伪代码 |
| \lambda x.x+y |
一个函数，给定x，返回x+y。这里的y被称为自由变量，具体值根据外部环境决定。注意到这里的函数是没有名字的（x,y 本质上也只是临时的名字，后面会讲），这一点在后面会讲到。伪代码中为了便于理解函数可以拥有名字。 |
func : (x){return x + y} |
| fx |
将x带入f，等价于f(x)。需要注意的是这里的x 也是一个函数，在\lambda演算中数据类型只有函数，函数可以进行代入、运算，等等。 |
f(k) |
理论上每层语法外面都要叠一层括号，但是由于过于麻烦，删去不造成歧义的括号会被省略。
### 柯里化（Currying）
不难发现用原生语法无法直接表达拥有多个参数的函数，我们可以用像这样的方法解决：$\color{green}\lambda x.(\color{orange}\lambda y.(x+y)\color{green})$，例：$\color{green}\lambda x.(\color{orange}\lambda y.(x+y)\color{green})\color{black}\ 2\ 4=\color{orange}\lambda y.(2+y)\color{black}\ 4=2+4=6$。
```
f = func : (x){
return func : (y){
return x + y
}
}
f(2)(4)=(func:(y){2+y})(4)=2+4=6
```
当然这样子太不简洁了，于是后面我们会直接缩写为 $\lambda xy.(x+y)\ 2\ 4=6$，这个过程被称为柯里化。这个东西实际上不对 $\lambda$ 演算能干的事进行干扰，归根结底只是一个语法糖。化简的过程中运用了接下来讲的 $\beta$-规约，如有不理解可在学习后重看一遍。
大部分情况下 $\lambda x.\lambda y.$ 与 $\lambda xy.$ 可以互换使用，这样会方便理解部分函数。有时拆开写 $\lambda x.\lambda y.$ 是为了表明层次，或者返回值是用 $\lambda$ 定义的函数（此时通常会加括号）。
### $\beta$-规约
细说有点复杂，可以当作“代入”操作来理解。例：$(\lambda x.x)\ y=x[x\rightarrow y]=y$，这里的 $\rightarrow$ 的意思是“被定义为”。有时规约的东西里面还套着东西，需要一并替换。
```
f = func : (x){return x}
f(y)=y
```
刚才柯里化的函数也可以作为一个例子。
一个复杂的式子可能可以多次规约，不能继续规约的式子被称为 $\beta$-范式。每个 $\lambda$ 表达式不一定存在属于自己的 $\beta$-范式，如存在一定只有一个本质相同的。一个不存在 $\beta$-范式的例子如 $\Omega=\omega\omega$，其中 $\omega=\lambda x.(xx)$，可以自己试一试，其在一次 $\beta$-规约后得到自己。$\Omega_3=\omega_3\omega_3$ 会无限变长，其中 $\omega_3=\lambda x.(xxx)$。一个式子也可能有多个 $\beta$-规约的方式，可能有的方式能规约完毕有的不能。仔细展开是一个很长的话题，还和停机问题等有很大的关系（尽管这玩意比停机问题早许多）。
```
omega = func : (x){
return x(x)
}
Omega = omega(omega)
// TLE!
```
### $\alpha$-变换
不咋重要。
思想大概是函数参数的名字无关函数的本质，例如 $\lambda x.x^2=\lambda y.y^2$。
```
f = func : (x){return x * x}
g = func : (y){return y * y}
//f和g显然本质相同
```
也有形参匿名的 $\lambda$ 演算语法，此处按下不表。
### $\eta$-变换
主要有以下两点：
- 只要 $x$ 不是 $f$ 的自由参数，$\lambda x.fx=f$。很好理解，“给你一个 $x$，返回 $f(x)$”的函数不就是 $f$ 自己嘛。
```
g = func(x){return f(x)}
//疑似洗钱行为
```
- 对于 $f,g$，如果对于所有 $x$ 都有 $fx=gx$，那么 $f=g$。
这两点是等价的，想一想。
## Part 2 数数
注意到 $\lambda$ 演算中所有东西都是函数，这很难不令人好奇 $\operatorname{true},\operatorname{false},0,1,2,3,\cdots$ 对应的是什么。
### 布尔代数
布尔，同 bool。
定义 $\operatorname{true}$ 和 $\operatorname{false}$ 的方法有非常多种，这里采用最常用的。你也可以尝试定义自己的！
$\operatorname{true}=\lambda xy.x$，意思是给两个数，返回前面那个。
```
true = func : (x, y){return x}
```
同理，$\operatorname{false}=\lambda xy.y$，意思是给两个数，返回后面那个。
```
false = func : (x, y){return y}
```
有了这两，我们就可以快快乐乐的定义 $\operatorname {if}$ 函数了：$\operatorname {if}=\lambda pxy.pxy$，其中 $x,y$ 是 $p$ 的参数（缩写柯里化的一点坏处是调用函数的时候不小心就会把参数套一起，最好像这样加个说明）。
```
if = func : (p, x, y){return p(x,y)}
//return : if p then x else y
//使用选择器做true和false的一点好处是if很好写
```
有了 $\operatorname {if}$ 剩下的布尔代数都简单了，$\operatorname {and},\operatorname {or},\operatorname {not}$ 的实现留给读者。一些运算可能会有别的等价表达方式，可以争取让自己的表达方式算起来最快。
### 自然数
由于这段过于复杂，公式看不懂代码也没啥帮助，故不提供伪代码。
这里同样使用最常见的方法。
$0 = \lambda fx.x = \operatorname{false}
$2 = \lambda fx.f(f(x))
3 = \lambda fx.f(f(f(x)))
以此类推。
后继数运算：
\operatorname{SUCC}(x) = \lambda x.(\lambda fy.f((xf)y)$。例：$\operatorname{SUCC}(3) = \lambda fy.f((3f)y) = \lambda fy.f((\lambda gx.g(g(g(x)))f)y)=\lambda fy.f(\lambda x.f(f(f(x)))y)=\lambda fy.f(f(f(f(y))))=4
虽然有点复杂但只要一步一步走就能做出来。五个等号分别进行的操作是：代入 \operatorname{SUCC} 的定义，代入 3 的定义，进行 \beta-约简（将 f 代入 \lambda gx.，如果严谨一点在这之前还要去 \lambda gx. 的柯里化变为 \lambda g.\lambda x. 再计算），再次进行 \beta-约简（将 y 代入 \lambda x.），代入 4 的定义。也可以自己找个数试一试，会对这个定义的理解有很大的提升。或者你也可以创造自己的实现！\lambda 演算的自由度非常高，很快就会出现例子。
利用数的定义，可以很快速的用后继数定义出加法：+(a,b)=\lambda ab. (a\ \operatorname{SUCC})\ b。注意 a\ \operatorname{SUCC} 代表把 \operatorname{SUCC} 代入 a 的定义 而非反过来。大家可以试试展开这个式子，不过最好不要把 \operatorname{SUCC} 的定义代入进去，免得被长式子击败。
同理加法也可以定义乘法，但是后缀已经是史山了加法更是一坨，这再套层不得起飞啊？于是我们还有另外一种表达方式：\times(a,b)=\lambda ab.(\lambda fx.a(bf)x)，不过 \lambda x.x 看着实在有点怪，所以这里一般反柯里化一下然后 \eta-变换成 \lambda abf .a(bf))。
\times \,\,2\,\,3 =(\lambda abc.a(bc)) (\lambda sz.s(s(z))) (\lambda xy.x(x(x(y))))\\= \lambda c.(\lambda sz.s(s(z)))((\lambda xy.x(x(x(y))))c)\\= \lambda cz.((\lambda xy.x(x(x(y))))c)(((\lambda xy.x(x(x(y))))c)(z)) \\= \lambda cz.(\lambda y.c(c(c(y)))) (c(c(c(z)))) \\= \lambda cz.c(c(c(c(c(c(z)))))) \\= 6 \\
具体过程就不细说了。这段 \LaTeX 来源于这位老哥，写的也十分不错。
类似的可以化简式子的还有幂，它的式子惊人的短：\operatorname{pow}(a,b)=\lambda ab.b\ a，但具体过程也十分惨不忍睹。\operatorname{pow}(3,2)=(\lambda fx.f(f(f(x))))(\lambda gy.g(g(y)))=\lambda x.\lambda gy.g(g(y))(\lambda gy.g(g(y))(\lambda gy.g(g(y))x))=\lambda x.\lambda gy.g(g(y))(\lambda gy.g(g(y))\lambda y.x(x(y)))=\cdots
实在化简不下去了。上面这段如有错误请勿指出。
减法也是惊人的屎山，接下来是那位老哥给出的未化简完毕的：
\displaystyle-(x,y)=\lambda xy.y(\lambda n.(\lambda p.p(F))(n(\lambda p. (\lambda a\lambda b.(\lambda s.s(a)(b)))(\lambda n\lambda f\lambda x.f(n(f)(x))((\lambda p.p(T))(p)))((\lambda p.p(T)))(p)))((\lambda a\lambda b.(\lambda s.s(a)(b)))(0)(0))))(x)
其中 F=\operatorname{false},T=\operatorname{true}。
不过要做到更简单的减法，我们还是要从前驱定义起，不过具体细节交给大家，实在不想碰这坨屎山了。如果真的好奇答案，请看维基百科。
Part 3 组合子
这里面的内容甚至会更屎山。
在别的文章里面这一点内容可能会出现一些约定俗成的记号，这里先放作参考。本文内不会未经声明地使用这些记号。
::::info[常用组合子]{open}
有些 \lambda 表达式有约定俗成的名字。
I = \lambda x.x
K = \lambda xy.x
S = \lambda xyz.xz(yz)
B = \lambda xyz.x(yz)
C = \lambda xyz.xzy
U = \lambda xy.y(xxy)
\omega = \lambda x.xx
\Omega = \omega \omega
Y = \lambda g.(\lambda x.g(xx))(\lambda x.g(xx))
其中很多都用于消除 \lambda 抽象，例如 2 = S (S (K S) (S (K K) (SKK))) (S (S (K S) (S (K K) (SKK))) (K (SKK)))
事实上还有更简洁的表示方法，细说的话这篇文章写不完了。
::::
我们考虑阶乘函数。在伪代码中，我们可以很简洁的定义函数：
fac = func : (x){return if(IS_ZERO(x), 1, x * fac(x-1))}
IS_ZERO 的实现是简单的，留给大家思考。
可是在 \lambda 演算中所有函数都是匿名函数，我们应该如何实现呢？
::::warning
接下来的内容较为抽象，建议放慢时间阅读。
::::
\operatorname{fac'}=\lambda fx.\operatorname{if}\ \operatorname{IS\_ZERO}\ x\ \operatorname{then}\ 1\ \operatorname{else} \ x \times f(x-1)
这样我们就用参数的形式表示递归了。我们需要的 \operatorname{fac} = \operatorname{fac'}\operatorname{fac}，还是有点问题，不过不要紧。相信大家做高中题时都遇见过“不动点”吧，我们在前面提到了 Y 组合子（又称不动点组合子）：Y = \lambda g.(\lambda x.g(xx))(\lambda x.g(xx))，注意到 Yf=(\lambda x.f(xx))(\lambda x.f(xx))=f((\lambda x.f(xx))(\lambda x.f(xx)))=f(Yf)，因此有 \operatorname{fac}=\operatorname{fac'}\operatorname{fac}=\operatorname{fac'}(Y\operatorname{fac'})=Y\operatorname{fac'}，这样就得到闭合形式了。
可以注意到这个函数也是前面提到“一个式子也可能有多个 \beta-规约的方式，可能有的方式能规约完毕有的不能。”的式子之一。
Part 4 结语
这么快就要结束了啊。
> Lambda 演算（lambda calculus, λ-calculus），最初由阿隆佐·邱奇（Alonzo Church）提出，是世界上最小的编程语言。 尽管没有数字、字符串、布尔或者任何非函数的数据类型，lambda 演算仍可以表示任何图灵机。
>
> 摘抄自 [learn x in y minutes](https://learnxinyminutes.com/zh-cn/lambda-calculus/)。
> lambda 演算是一套从数学逻辑中发展，以变量绑定和替换的规则，来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。它由数学家阿隆佐·邱奇在 20 世纪 30 年代首次发表。lambda 演算作为一种广泛用途的计算模型，可以清晰地定义什么是一个可计算函数，而任何可计算函数都能以这种形式表达和求值，它能模拟单一磁带图灵机的计算过程；尽管如此，lambda 演算强调的是变换规则的运用，而非实现它们的具体机器。
>
> lambda 演算可比拟最根本的编程语言，它包括了一条变换规则（变量替换）和一条将函数抽象化定义的方式。因此普遍公认是一种更接近软件而非硬件的方式。对函数式编程语言造成很大影响，比如 Lisp、ML 语言和 Haskell 语言。在 1936 年邱奇利用 Lambda 演算给出了对于判定性问题（Entscheidungsproblem）的否定：关于两个 lambda 表达式是否等价的命题，无法由一个“通用的算法”判断，这是不可判定性能够证明的头一个问题，甚至还在停机问题之先。
>
> 摘抄自[维基百科](https://zh.wikipedia.org/wiki/%CE%9B%E6%BC%94%E7%AE%97)。
:::epigraph[——沃茨基·硕德]
哥们就爱整点抽象的，lambda 怎么你了。
:::
最后作为读了这么久抽象玩意之后的小放松，讲一下 $\lambda$ 符号的传说来历：
据说最开始这个符号在手稿上是长这样的：$\hat{f}$，后面小尖尖在印刷时被单独弄出去了：$\wedge f$，最后又给抄错了，变成了 $\lambda f$。
::::info[推荐阅读]
列举一些学习中用到的资料。
[Y 分钟速成 lambda 演算](https://learnxinyminutes.com/zh-cn/lambda-calculus/) 这篇文章讲了一些组合子演算。
[维基百科：λ 演算](https://zh.wikipedia.org/wiki/%CE%9B%E6%BC%94%E7%AE%97) 讲了一些更全的东西。
[维基百科：邱奇数](https://zh.wikipedia.org/wiki/%E9%82%B1%E5%A5%87%E6%95%B0) 里面有关于各种加减乘除更详细的说明。
[这篇知乎文章](https://zhuanlan.zhihu.com/p/565089428) 还额外讲了一些更抽象的内容，例如图灵机，还有 python 的代码。
[这篇知乎回答](https://www.zhihu.com/question/21099081/answer/23893046) 教会了我使用 $Y$ 不动点组合子。本文 Part 3 很多都是参考他的。
[2swap 的油管视频](https://www.youtube.com/watch?v=RcVA8Nj6HEo) 这篇文章的灵感，多讲了一个很神秘的图表。ta d所有视频都是艺术品级别的，推荐观看。
::::
---
断断续续写了 9000+ 字，如果喜欢可以在[知乎](https://zhuanlan.zhihu.com/p/1958133095459983422)上点赞同收藏什么的，或者看我知乎主页里的其他文章。不建议在知乎上阅读，知乎的阅读体验绝对更差。