Lambda 演算

参数和函数体使用 一个点 隔开来，其中参数以 $λ$ 开头，之后跟随的是参数标识符，如： $\lambda x$ 、 $\lambda y$ 甚至是 $\lambda 114514$ 。
因为 λ 演算中你不需要考虑类型转换，因此你的参数标识符可以是 任意字符串，当然前提是你能认得出来你写的是啥。

一个函数可以有多个参数，当你需要多个参数时，只需要粗暴地把参数按顺序堆叠在参数部分就行了：

\lambda x\lambda y.xy

你还可以在每个参数的尾部都使用一个点隔开，这样也可以表示多个参数：

\lambda x.\lambda y.xy

可以发现第二种表达法实际上是 把一个函数给拆分成了两个函数。
上面两种表达法有什么区别？到后面你就知道了。

λ 演算的应用

λ 演算的应用使用 类似于代数计算的乘法 表示：

\begin{align*} (\lambda x.x)a\\ (\lambda x.x)(\lambda y.a) \end{align*}

以上分别表示使用 $a$ 作为参数应用于函数 $\lambda x.x$ ，以及使用 $\lambda y.a$ 作为参数应用于函数 $\lambda x.x$ 。

那么这个函数应用应该怎么计算呢？首先一个最简单的结论：λ 演算的应用实际上就是字符串替换。
所以有：

\begin{align*} (\underline{\lambda x}.x)\underline{a}=a\\ (\underline{\lambda x}.x)\underline{(\lambda y.a)}=\lambda y.a \end{align*}

直接把函数体中对应参数的变量替换为参数即可，我们再来看一个相对复杂的例子：

\begin{align*} &(\lambda x\lambda y.xy)(\lambda x.xa)(\lambda x.xb)\\ =&(\lambda y.\textcolor{red}{(\lambda x.xa)y})(\lambda x.xb)\\ =&(\lambda y.ya)(\lambda x.xb)\\ =&(\lambda x.xb)a\\ =&ab \end{align*}

可以看见，按照从左到右的顺序，依次应用参数，每一步都将函数体使用参数替换作为返回值。
需要注意的是，如果函数体中出现了可以进行计算的部分（如上面的红色部分），那么我们也应该先进行计算，然后再进行外部的应用。

为了严谨定义，对于字符串替换，我们又将其差分为 3 中小操作：

1. α 变换

α 变换是 λ 演算中的一个基础操作，简单来说就是你可以 修改函数中某一个参数的名字，然后对函数体中所有的该参数同样进行改名：

\lambda x.xa\xrightarrow{\alpha}\lambda y.ya

需要注意的是 α 变换是有边界的，它只能对函数自己的参数起作用，而不能对函数内部的其他函数起作用：

\begin{align*} \lambda\textcolor{blue}{x}.(\lambda x\lambda z.zx)\textcolor{blue}{x} &\xrightarrow{\alpha} \lambda\textcolor{blue}{y}.(\lambda x\lambda z.zx)\textcolor{blue}{y}\\ \lambda\textcolor{red}{x}.(\lambda\textcolor{red}{x}\lambda z.z\textcolor{red}{x})\textcolor{red}{x} &\not\xrightarrow{\alpha} \lambda\textcolor{red}{y}.(\lambda\textcolor{red}{y}\lambda z.z\textcolor{red}{y})\textcolor{red}{y} \end{align*}

因为 α 变换最重要的一点是 保证算式变换前后的拓扑关系不变，而超出边界的变换可能会导致拓扑关系被破坏。

2. β 规约

β 规约实际上就是化简运算，将一长串 λ 算式不断使用函数应用，直至不能继续应用为止。

规约的顺序为 从左到右，先算括号：

\begin{align*} &(\lambda x.(\underline{\lambda y}.y)\underline{x})z\\ =&(\underline{\lambda x}.x)\underline{z}\\ =&z \end{align*}

当规约时可能发生语义冲突时，应该先使用 α 变换给有冲突的变量替换名字，然后再进行 β 规约：

\begin{align*} &(\lambda a\lambda\underline{b}.a\underline{b})b\\ =&(\underline{\lambda a}\lambda\textcolor{blue}{c}.a\textcolor{blue}{c})\underline{b}\\ =&\lambda c.bc \end{align*}

如果强行进行规约，那么就会出现尴尬的事情了：

\begin{align*} &(\underline{\lambda a}\lambda b.ab)\underline{b}\\ =&\lambda b.bb\\ =&??? \end{align*}

3. η 规约

当一个函数的函数体里 没有出现函数的参数 时，那么应用任意的参数到这个函数，函数只会把自己的函数体原原本本地返回：

(\lambda a.x)b=x

这是一个非常显然的结论。

柯里化

之前我们将函数参数的时候说过，当有多个参数时，以下两种写法等价：

\begin{align*} \lambda x\lambda y.xy\\ \lambda x.\lambda y.xy \end{align*}

实际上就类似于这两种 JS 函数定义：

const func1 = (x, y) => x(y);
const func2 = (x) => (y) => x(y);

在 λ 演算中，我们允许只提供部分参数，函数只进行部分演算，然后返回一个新的函数来接收其他参数，直到所有的参数都接受完成。
这就是 柯里化 的概念。

当然在如上的 JS 代码中 func1 并不满足这个条件，它必须同时接收两个参数，因此实际上 λ 演算中的函数都是以 func2 形式进行执行的。

λ 演算中所有的函数都是柯里化执行的，因此你可以在任何时候代入部分参数进行部分演算，以获得新的函数作为结果。

λ 演算的图灵完备性

λ 演算是图灵完备的，也就是说我们可以使用 λ 演算构建出任何使用其他编程语言所编写的程序，并能够实现任何图灵机可以实现的功能。

在现实生活中，如果我们能够成功用 λ 演算表达出 真、假值 以及 与或非 操作，那么通过组合这些基本元素，我们就能知道 λ 演算是图灵完备的，因为现实中的计算机就是由这些基础元素搭建出来的。

真假值与条件函数

定义如下：

\begin{align*} \mathrm{True}=&\lambda x\lambda y.x\\ \mathrm{False}=&\lambda x\lambda y.y\\ \mathrm{If}=&\lambda b\lambda t\lambda f.btf \end{align*}

条件函数有三个参数，分别是条件、真分支 和 假分支，通过分别带入真值和假值，我们能够很容易地验证条件函数的正确性：

\begin{align*} &(\mathrm{If})(\mathrm{True})\\ =&(\underline{\lambda b}\lambda t\lambda f.btf)\underline{(\lambda x\lambda y.x)}\\ =&\lambda t\lambda f.(\underline{\lambda x\lambda y}.x)\underline{tf}\\ =&\lambda t\lambda f.t \end{align*}

\begin{align*} &(\mathrm{If})(\mathrm{False})\\ =&(\underline{\lambda b}\lambda t\lambda f.btf)\underline{(\lambda x\lambda y.y)}\\ =&\lambda t\lambda f.(\underline{\lambda x\lambda y}.y)\underline{tf}\\ =&\lambda t\lambda f.f \end{align*}

由于这里所说的分支实际上还是一个函数，其实条件函数更像是一个 三目运算符。

与或非

当有了真假值和三目运算符，与或非操作当然也就非常好定义了：

\begin{align*} \mathrm{AND}=&\lambda a\lambda b.(\mathrm{IF})ab(\mathrm{False})\\ \mathrm{OR}=&\lambda a\lambda b.(\mathrm{IF})a(\mathrm{True})b\\ \mathrm{NOT}=&\lambda a.(\mathrm{IF})a(\mathrm{False})(\mathrm{True}) \end{align*}

我们将对应的函数代入化简一下：

\begin{align*} \mathrm{AND}=&\lambda a\lambda b.\underline{(\mathrm{IF})}ab(\mathrm{False})\\ =&\lambda a\lambda b.(\underline{\lambda b\lambda t\lambda f}.btf)\underline{ab(\mathrm{False})}\\ =&\lambda a\lambda b.ab(\mathrm{False}) \end{align*}

\begin{align*} \mathrm{OR}=&\lambda a\lambda b.\underline{(\mathrm{IF})}a(\mathrm{True})b\\ =&\lambda a\lambda b.(\underline{\lambda b\lambda t\lambda f}.btf)\underline{a(\mathrm{True})b}\\ =&\lambda a\lambda b.a(\mathrm{True})b \end{align*}

\begin{align*} \mathrm{NOT}=&\lambda a.\underline{(\mathrm{IF})}a(\mathrm{False})(\mathrm{True})\\ =&\lambda a.(\underline{\lambda b\lambda t\lambda f}.btf)\underline{a(\mathrm{False})(\mathrm{True})}\\ =&\lambda a.a(\mathrm{False})(\mathrm{True}) \end{align*}

简单代入几个值进行计算：

\begin{align*} &(\mathrm{AND})(\mathrm{True})(\mathrm{True})\\ =&(\underline{\lambda a\lambda b}.ab(\mathrm{False}))\underline{(\lambda x\lambda y.x)(\lambda x\lambda y.x)}\\ =&(\underline{\lambda x\lambda y}.x)\underline{(\lambda x\lambda y.x)(\mathrm{False})}\\ =&\lambda x\lambda y.x\\ =&\mathrm{True} \end{align*}

\begin{align*} &(\mathrm{OR})(\mathrm{False})(\mathrm{False})\\ =&(\underline{\lambda a\lambda b}.a(\mathrm{True})b)\underline{(\lambda x\lambda y.y)(\lambda x\lambda y.y)}\\ =&(\underline{\lambda x\lambda y}.y)\underline{(\mathrm{True})(\lambda x\lambda y.y)}\\ =&\lambda x\lambda y.y\\ =&\mathrm{False} \end{align*}

\begin{align*} &(\mathrm{NOT})(\mathrm{True})\\ =&(\underline{\lambda a}.a(\mathrm{False})(\mathrm{True}))\underline{(\lambda x\lambda y.x)}\\ =&(\underline{\lambda x\lambda y}.x)\underline{(\mathrm{False})(\mathrm{True})}\\ =&\mathrm{False} \end{align*}

用 λ 演算存储数据

你可能会摸不着头脑，但是 λ 演算的确可以表示出一个能存储数据的结构，而它实际上只是一个简单的条件函数！

考虑链表的建立方式，对于每个存储单元我们需要两个字段，一个是字段，另一个是 Next 指针。
指针对于 λ 演算来说太复杂了，那么我们可以考虑一种套娃的形式 —— 在 Next 指针存储另一个完整的链表，最终变成这样：

((((), d_1), d_2), d_3)

这样一来，我们就能构建一系列的操作了：

\begin{align*} \mathrm{NULL}=&\lambda x.x\\ \mathrm{EMPTY\_LIST}=&\lambda b.(\mathrm{IF})b(\mathrm{NULL})(\mathrm{NULL})\\ \mathrm{GET\_DATA}=&\lambda l.l(\mathrm{True})\\ \mathrm{GET\_NEXT}=&\lambda l.l(\mathrm{False})\\ \mathrm{PUSH\_DATA}=&\lambda l\lambda d\lambda b.(\mathrm{IF})bdl \end{align*}

这个链表看起来更像一个栈结构了，你可以通过应用函数来验证其正确性：

\begin{align*} &(\mathrm{PUSH\_DATA})(\underline{(\mathrm{PUSH\_DATA})}(\mathrm{EMPTY\_LIST})(\mathrm{True}))(\mathrm{False})\\ =&(\mathrm{PUSH\_DATA})((\underline{\lambda l\lambda d}\lambda b.(\mathrm{IF})bdl)\underline{(\mathrm{EMPTY\_LIST})(\mathrm{True})})(\mathrm{False})\\ =&\underline{(\mathrm{PUSH\_DATA})}(\lambda b.(\mathrm{IF})b(\mathrm{True})(\mathrm{EMPTY\_LIST}))(\mathrm{False})\\ =&(\underline{\lambda l\lambda d}\lambda b.(\mathrm{IF})bdl)\underline{(\lambda b.(\mathrm{IF})b(\mathrm{True})(\mathrm{EMPTY\_LIST}))(\mathrm{False})}\\ =&\lambda b.(\mathrm{IF})b(\mathrm{False})(\lambda b.(\mathrm{IF})b(\mathrm{True})(\mathrm{EMPTY\_LIST})) \end{align*}

以上函数组合出了一个如下的链表：

(((), \mathrm{True}), \mathrm{False})

我想要取出数据：

\begin{align*} &\underline{(\mathrm{GET\_DATA})}(\lambda b.(\mathrm{IF})b(\mathrm{False})(\lambda b.(\mathrm{IF})b(\mathrm{True})(\mathrm{EMPTY\_LIST})))\\ =&(\underline{\lambda l}.l(\mathrm{True}))\underline{(\lambda b.(\mathrm{IF})b(\mathrm{False})(\lambda b.(\mathrm{IF})b(\mathrm{True})(\mathrm{EMPTY\_LIST})))}\\ =&(\underline{\lambda b}.(\mathrm{IF})b(\mathrm{False})(\lambda b.(\mathrm{IF})b(\mathrm{True})(\mathrm{EMPTY\_LIST})))\underline{(\mathrm{True})}\\ =&\underline{(\mathrm{IF})(\mathrm{True})(\mathrm{False})}(\lambda b.(\mathrm{IF})b(\mathrm{True})(\mathrm{EMPTY\_LIST}))\\ =&\mathrm{False} \end{align*}

当然这样做还是比较抽象的，因为我们还没有定义整数，所以如果需要提取深层数据，只能不停的重复调用。

λ 演算的自然数定义与演算

想要用 λ 演算这种抽象算式来数数，最好的方法就是用 皮亚诺公理 了，我们来复习一下公理内容：

$0$ 是自然数
每一个确定的自然数 $a$ ，都具有确定的后继数 $a'$ ， $a'$ 也是自然数
$0$ 不是任何自然数的后继数
不同的自然数有不同的后继数，如果自然数 $b$ 、 $c$ 的后继数都是自然数 $a$ ，那么 $b=c$
设 $S\sube\N$ ，且满足2个条件（i） $0\in S$ ；（ii）如果 $\forall n\in S$ ，那么 $n'\in S$ 。则 $S$ 是包含全体自然数的集合，即 $S=\N$ 。

用皮亚诺公理数数

要利用皮亚诺公理，我们需要定义两个东西 —— 0 和 后继数。
有了他们我们就可以从 0 开始一直数数下去了。

在 λ 演算中，他们被定义为：

\begin{align*} 0=&\lambda s\lambda x.x\\ \mathrm{S}=&\lambda n\lambda s\lambda x.s(nsx) \end{align*}

我们如果想要数 1，那么就将后继操作应用于 0：

\begin{align*} 1=&(\mathrm{S})(0)\\ =&(\underline{\lambda n}\lambda s\lambda x.s(nsx))\underline{(\lambda s\lambda x.x)}\\ =&\lambda s\lambda x.s((\underline{\lambda s\lambda x}.x)\underline{sx})\\ =&\lambda s\lambda x.sx \end{align*}

数 2 也是同理：

\begin{align*} 2=&(\mathrm{S})(1)\\ =&(\underline{\lambda n}\lambda s\lambda x.s(nsx))\underline{(\lambda s\lambda x.sx)}\\ =&\lambda s\lambda x.s((\underline{\lambda s\lambda x}.sx)\underline{sx})\\ =&\lambda s\lambda x.s(sx) \end{align*}

发现了一个规律，数多少个自然数，实际上就是在 λ 算式里套娃多少个 s：

\begin{align*} 0=&\lambda s\lambda x.x\\ 1=&\lambda s\lambda x.sx\\ 2=&\lambda s\lambda x.s(sx)\\ 3=&\lambda s\lambda x.s(s(sx))\\ \cdots \end{align*}

后继函数利用 λ 演算本质上就是字符串替换的特性巧妙地实现了这一点。

这一种对自然数的特殊编码方式被称为 丘奇编码。

加法

在知道了自然数与 s 的关系之后，加法操作就很简单了，只需要将两个数字的 s 部分拼接在一起就行：

+=\lambda a\lambda b\lambda s\lambda x.as(bsx)

这里的 $bsx$ 实则是将 $b$ 的函数体完整返回，而 $as(bsx)$ 则是保留 $a$ 的 $s$ 字符串，将最末尾的 $x$ 给替换成 $b$ ，这样一来实际上就是把两数的 s 进行了拼接。

所以有：

\begin{align*} (+)(2)(3)=&(\underline{\lambda a\lambda b}\lambda s\lambda x.as(bsx))\underline{(\lambda s\lambda x.s(sx))(\lambda s\lambda x.s(s(sx)))}\\ =&\lambda s\lambda x.(\lambda s\lambda x.s(sx))s((\underline{\lambda s\lambda x}.s(s(sx)))\underline{sx})\\ =&\lambda s\lambda x.(\underline{\lambda x}.s(sx))\underline{(s(s(sx)))}\\ =&\lambda s\lambda x.s(s(s(s(sx))))\\ =&5 \end{align*}

乘法

小学数学学过，乘法实际上就是多次加法，但是在 λ 演算的世界里，乘法要简单的多，只需要 将一个数中所有的 s 替换成另一个数 就行了，因此有：

\times=\lambda a\lambda b\lambda s.a(bs)

这里的 $a(bs)$ 实际上就是将 $a$ 中的 $s$ 全部替换成 $bs$ ，这就隐含了将 $b$ 中的 $s$ 重复 $a$ 次这个乘法语义。

所以有：

\begin{align*} (\times)(2)(3)=&(\underline{\lambda a\lambda b}\lambda s.a(bs))\underline{(\lambda s\lambda x.s(sx))(\lambda s\lambda x.s(s(sx)))}\\ =&\lambda s.(\lambda s\lambda x.s(sx))((\underline{\lambda s}\lambda x.s(s(sx)))\underline{s})\\ =&\lambda s.(\underline{\lambda s}\lambda x.s(sx))\underline{(\lambda x.s(s(sx)))}\\ =&\lambda s\lambda x.(\lambda x.s(s(sx)))((\underline{\lambda x}.s(s(sx)))\underline{x})\\ =&\lambda s\lambda x.(\underline{\lambda x}.s(s(sx)))\underline{(s(s(sx)))}\\ =&\lambda s\lambda x.s(s(s(s(s(sx)))))\\ =&6 \end{align*}

幂次

如果将乘法执行多次，那么得到的就是幂次，按照替换方法，在 λ 演算中实现也非常简单：

\mathrm{POW}=\lambda a\lambda b.ba

这里计算 $a^b$ 只需要将 $b$ 中的 $s$ 全部替换成 $a$ ，就隐含了将 $a$ 中的 $s$ 重复 $b$ 次的语义。

跟乘法不同，幂次没有引入 $s$ 变量，因为我们实际上是以递归的形式计算幂次，需要将每一步计算得到的新结果再进行 s 替换，而不像乘法一样进行一次替换就行。

所以有：

\begin{align*} (\mathrm{POW})(2)(3)=&(\underline{\lambda a\lambda b}.ba)\underline{(\lambda s\lambda x.s(sx))(\lambda s\lambda x.s(s(sx)))}\\ =&(\underline{\lambda s}\lambda x.s(s(sx)))\underline{(\lambda s\lambda x.s(sx))}\\ =&\lambda \underline{x}.(\lambda s\lambda x.s(sx))((\lambda s\lambda x.s(sx))((\lambda s\lambda x.s(sx))\underline{x}))\\ =&\lambda t.(\lambda s\lambda x.s(sx))((\lambda s\lambda x.s(sx))((\underline{\lambda s}\lambda x.s(sx))\underline{t}))\\ =&\lambda t.(\lambda s\lambda x.s(sx))((\underline{\lambda s}\lambda x.s(sx))\underline{(\lambda x.t(tx))})\\ =&\lambda t.(\lambda s\lambda x.s(sx))(\lambda x.(\lambda x.t(tx))((\underline{\lambda x}.t(tx))\underline{x}))\\ =&\lambda t.(\lambda s\lambda x.s(sx))(\lambda x.(\underline{\lambda x}.t(tx))\underline{(t(tx))})\\ =&\lambda t.(\underline{\lambda s}\lambda x.s(sx))\underline{(\lambda x.t(t(t(tx))))}\\ =&\lambda t.\lambda x.(\lambda x.t(t(t(tx))))((\underline{\lambda x}.t(t(t(tx))))\underline{x})\\ =&\lambda t.\lambda x.(\underline{\lambda x}.t(t(t(tx))))\underline{(t(t(t(tx))))}\\ =&\lambda \underline{t}.\lambda x.\underline{t}(\underline{t}(\underline{t}(\underline{t}(\underline{t}(\underline{t}(\underline{t}(\underline{t}x)))))))\\ =&\lambda s\lambda x.s(s(s(s(s(s(s(sx)))))))\\ =&8 \end{align*}

前驱

光有加法乘法和幂次可不够，我们还希望有减法，在这之前，我们需要获取一个自然数的前驱值。

在丘奇编码中，前驱值就比较复杂了：

\mathrm{P}=\lambda n\lambda s\lambda x.n(\lambda g\lambda h.h(gs))(\lambda u.x)(\lambda u.u)

光看可分析不出啥，我们来演算一下：

\begin{align*} (\mathrm{P})(2)=&(\underline{\lambda n}\lambda s\lambda x.n(\lambda g\lambda h.h(gs))(\lambda u.x)(\lambda u.u))\underline{(\lambda s\lambda x.s(sx))}\\ =&\lambda s\lambda x.(\underline{\lambda s\lambda x}.s(sx))\underline{(\lambda g\lambda h.h(gs))(\lambda u.x)}(\lambda u.u)\\ =&\lambda s\lambda x.((\lambda g\lambda h.h(gs))((\underline{\lambda g}\lambda h.h(gs))\underline{(\lambda u.x)}))(\lambda u.u)\\ =&\lambda s\lambda x.((\lambda g\lambda h.h(gs))(\lambda h.h((\underline{\lambda u}.x)\underline{s})))(\lambda u.u)\\ =&\lambda s\lambda x.((\underline{\lambda g}\lambda h.h(gs))\underline{(\lambda h.hx)})(\lambda u.u)\\ =&\lambda s\lambda x.(\lambda h.h((\underline{\lambda h}.hx)\underline{s}))(\lambda u.u)\\ =&\lambda s\lambda x.(\underline{\lambda h}.h(sx))\underline{(\lambda u.u)}\\ =&\lambda s\lambda x.(\underline{\lambda u}.u)\underline{(sx)}\\ =&\lambda s\lambda x.sx\\ =&1 \end{align*}

为了把一个 s 给去掉，我们要花费这么多步……
其实观察计算步骤，我们还是能看出来演算做了什么的，无非重新从 0 开始数数，直到 n-1 的时候停止返回。

那么如果我们想要求 0 的前驱？

\begin{align*} (\mathrm{P})(0)=&(\underline{\lambda n}\lambda s\lambda x.n(\lambda g\lambda h.h(gs))(\lambda u.x)(\lambda u.u))\underline{(\lambda s\lambda x.x)}\\ =&\lambda s\lambda x.(\underline{\lambda s\lambda x}.x)\underline{(\lambda g\lambda h.h(gs))(\lambda u.x)}(\lambda u.u)\\ =&\lambda s\lambda x.(\underline{\lambda u}.x)\underline{(\lambda u.u)}\\ =&\lambda s\lambda x.x\\ =&0 \end{align*}

当然是算不出来的了，因为自然数中没有负数。

减法

有了前驱之后，减法定义就相对容易了：

-=\lambda a\lambda b.b(\mathrm{P})a

当 $a\ge b$ 时计算得到 $a-b$ 否则计算得 0。

如：

\begin{align*} (-)(5)(2)=&(\underline{\lambda a\lambda b}.b(\mathrm{P})a)\underline{(5)(\lambda s\lambda x.s(sx))}\\ =&(\underline{\lambda s\lambda x}.s(sx))\underline{(\mathrm{P})(5)}\\ =&(\mathrm{P})(\underline{(\mathrm{P})(5)})\\ =&\underline{(\mathrm{P})(4)}\\ =&3 \end{align*}

可以看出减法实际上就是将减数的 s 替换成了前驱操作，通过对 $a$ 做 $b$ 次前驱操作实现的。

比较运算

在有了如上的基本代数工具之后，是时候将数字和真假值联系起来了，这时候我们就需要一系列比较运算了，一切的基础都要从与 0 比较开始：

\mathrm{IS\_ZERO}=\lambda n.n(\lambda x.(\mathrm{False}))(\mathrm{True})

这个函数可太直观了，记得一些自然数的丘奇编码如下：

\begin{align*} 0=&\lambda s\lambda x.x\\ 1=&\lambda s\lambda x.sx\\ 2=&\lambda s\lambda x.s(sx)\\ 3=&\lambda s\lambda x.s(s(sx))\\ \cdots \end{align*}

如果将 0 应用于这个函数，则很明显会返回一个真值，又由于 s 被传入一个永远返回假值的函数，所以只要数字的丘奇编码中出现了 s，那么它永远返回假。

那么接下来要比较两个数是否小于等于关系，就可以简单表示如下：

\mathrm{LEQ}=\lambda a\lambda b.(\mathrm{IS\_ZERO})((-)ab)

只要 $a-b\leq0$ 那么这个函数就将返回真。

有了这个基本比较，其他的比较函数也容易得到了：

\begin{align*} \mathrm{LEQ}=&\lambda a\lambda b.(\mathrm{IS\_ZERO})((-)ab)\\ \mathrm{GEQ}=&\lambda a\lambda b.(\mathrm{IS\_ZERO})((-)ba)\\ \mathrm{EQ}=&\lambda a\lambda b.(\mathrm{AND})((\mathrm{LEQ})ab)(\mathrm{GEQ}ab)\\ \mathrm{NEQ}=&\lambda a\lambda b.(\mathrm{NOT})((\mathrm{EQ})ab)\\ \mathrm{LT}=&\lambda a\lambda b.(\mathrm{NOT})((\mathrm{GEQ})ab)\\ \mathrm{GT}=&\lambda a\lambda b.(\mathrm{NOT})((\mathrm{LEQ})ab) \end{align*}

Y 组合子

考虑计算阶乘，用 λ 演算可以这样表示：

\mathrm{FACT}=\lambda n.(\mathrm{IF})((\mathrm{IS\_ZERO})n)(1)((\times)n((\mathrm{FACT})((P)n)))

如计算 $3!$ ，有：

\begin{align*} (\mathrm{FACT})(3)=&(\underline{\lambda n}.(\mathrm{IF})((\mathrm{IS\_ZERO})n)(1)((\times)n((\mathrm{FACT})((P)n))))\underline{(3)}\\ =&(\mathrm{IF})(\underline{(\mathrm{IS\_ZERO})(3)})(1)((\times)(3)((\mathrm{FACT})(\underline{(P)(3)})))\\ =&\underline{(\mathrm{IF})(\mathrm{False})}(1)\underline{((\times)(3)((\mathrm{FACT})(2)))}\\ =&(\times)(3)((\underline{\mathrm{FACT}})(2))\\ =&(\times)(3)((\underline{\lambda n}.(\mathrm{IF})((\mathrm{IS\_ZERO})n)(1)((\times)n((\mathrm{FACT})((P)n))))\underline{(2)})\\ =&(\times)(3)((\mathrm{IF})(\underline{(\mathrm{IS\_ZERO})(2)})(1)((\times)(2)((\mathrm{FACT})(\underline{(P)(2)}))))\\ =&(\times)(3)(\underline{(\mathrm{IF})(\mathrm{False})}(1)\underline{((\times)(2)((\mathrm{FACT})(1)))})\\ =&(\times)(3)((\times)(2)((\underline{\mathrm{FACT}})(1)))\\ =&(\times)(3)((\times)(2)((\underline{\lambda n}.(\mathrm{IF})((\mathrm{IS\_ZERO})n)(1)((\times)n((\mathrm{FACT})((P)n))))\underline{(1)}))\\ =&(\times)(3)((\times)(2)((\mathrm{IF})(\underline{(\mathrm{IS\_ZERO})(1)})(1)((\times)(1)((\mathrm{FACT})(\underline{(P)(1)})))))\\ =&(\times)(3)((\times)(2)(\underline{(\mathrm{IF})(\mathrm{False})}(1)\underline{((\times)(1)((\mathrm{FACT})(0)))}))\\ =&(\times)(3)((\times)(2)((\times)(1)(\underline{(\mathrm{FACT})}(0))))\\ =&(\times)(3)((\times)(2)((\times)(1)((\underline{\lambda n}.(\mathrm{IF})((\mathrm{IS\_ZERO})n)(1)((\times)n((\mathrm{FACT})((P)n))))\underline{(0)})))\\ =&(\times)(3)((\times)(2)((\times)(1)((\mathrm{IF})(\underline{(\mathrm{IS\_ZERO})(0)})(1)((\times)(0)((\mathrm{FACT})((P)(0)))))))\\ =&(\times)(3)((\times)(2)((\times)(1)(\underline{(\mathrm{IF})(\mathrm{True})(1)}((\times)(0)((\mathrm{FACT})((P)(0)))))))\\ =&(\times)(3)((\times)(2)(\underline{(\times)(1)(1)}))\\ =&(\times)(3)(\underline{(\times)(2)(1)})\\ =&\underline{(\times)(3)(2)}\\ =&6 \end{align*}

我们使用递归操作，让函数不断地调用自己实现了阶乘计算，但是如果我们的函数没有名字呢？
当涉及到匿名函数递归时，我们就需要一个工具来帮助我们调用函数自己，而它就是 Y 组合子。

Y 组合子的定义如下：

\mathrm{Y}=\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))

Y 组合子接收一个函数作为参数，且对于任意函数 $f$ ，显然有：

\begin{align*} (\mathrm{Y})f=&(\underline{\lambda f}.(\lambda x.f(xx))(\lambda x.f(xx)))\underline{f}\\ =&(\underline{\lambda x}.f(xx))\underline{(\lambda x.f(xx))}\\ =&f(\underline{(\lambda x.f(xx))(\lambda x.f(xx))})\\ =&f((\mathrm{Y})f)\\ =&f(f((\mathrm{Y})f))\\ =&f(f(f(\cdots f((\mathrm{Y})f)\cdots))) \end{align*}

我们得到了一个可以无限自展开的新函数！

那么这样一来，我们就可以定义新的阶乘函数了：

\mathrm{FACT}=(\mathrm{Y})(\lambda f\lambda n.(\mathrm{IF})((\mathrm{IS\_ZERO})n)(1)((\times)n(f((P)n))))

计算展开过程过于复杂，这里就不展示了，不过要使用 Y 组合子进行递归展开需要满足一个条件，那就是最终函数应该展开至一个 不动点，即：

x=f(x)

此时就算无穷展开下去函数值也不会发生改变，那么就可以停止展开，开始回溯计算值。
如果函数无法满足这个条件，也就意味着无穷展开没有边界了，自然运算永远也不会停下。

小结

λ 演算大道至简，没有什么乱七八糟的概念，虽然是计算机世界中的一块基石，但是更多的反而是面向数学而非计算机。

想要给 λ 演算写一个编译器/解释器很容易，但是想拿它来写程序那就大可不必了。

函数式编程就大量借鉴了 λ 演算的思路与想法，到时候再写文章讨论吧。

什么是 Lambda 演算

λ 演算的基本要素

1. 变量

2. 函数

3. 应用

λ 演算的函数

λ 演算的应用

1. α 变换

2. β 规约

3. η 规约

柯里化

λ 演算的图灵完备性

真假值与条件函数

与或非

更多的逻辑运算

用 λ 演算存储数据

λ 演算的自然数定义与演算

用皮亚诺公理数数

加法

乘法

幂次

前驱

减法

比较运算

Y 组合子

小结