这篇博客对 Lambda-Calculus and Combinator § 4C Theorem 4.20 的 proof 部分做一些补充，证明的整体意图是证明符合 Definition 4.18 的全称递归函数可以用组合子来表示. 这里对该证明的关键部分，即迭代组合子的构造，做简要的陈述. 也可以理解为：在 Pure Lambda Calculus 中编写一个具有特定终止条件的迭代程序.

递归与迭代：在 $R_{\text{Bernays}}$ 递归组合子的构造中，求解某个递归函数 $\phi $ 的值 $ \phi(n) $，一种可行的方法是，从 $ \phi(0) $ 开始，做 $n$ 次迭代得到 $ \phi(n) $（大致如下：记递归步更新函数为 $\chi$，$\phi(n) = \chi^n \phi(0)$）. 迭代和递归是正向与逆向的区别. 本文中的"递归"意在描述"调用自身" 的结构特点，探讨的中心问题还是对迭代（$0 \rightarrow 1 \rightarrow … \rightarrow n$）问题的求解.

构造目标

假设有一个检查函数 $X$，迭代的终止条件为 $XY=_{\beta,w}\bar{0}$, 我们希望构造一个组合子 $P$,得到最小的符合终止条件的 $Y$. 即从 $Y = \bar{0}$ 开始，检查 $(XY) = _{\beta,w}? \bar{0}$ ，若条件满足，则返回值为此 $Y$，否则继续检查 $X(\bar{\sigma}Y)$，我们希望构造一个组合子 $P$ 自动化此检查过程，形式化地，我们预期 $P$ 的行为如下:

$$ PXY =_{\beta,w}Y \quad \text{, if } XY = _{\beta,w}\bar{0};$$

$$ PXY =_{\beta,w}PX(\bar{\sigma}Y), \text{ otherwise} $$

完全尊重预期，写一个 $P$ 组合子：$P \equiv \lambda xy.\textbf{D}y(Px(\bar{\sigma}y))(xy)$，其中 $\textbf{D}=\lambda xyz.z(\textbf{K}y)x$, 可以用 $\textbf{Y}$ 组合子来 fix 这个 $P$（$P \equiv \textbf{Y}(\lambda pxy.\textbf{D}y(px(\bar{\sigma}y))(xy))$），使用 $\textbf{Y} $ 组合子求解出的 $P$ 没有 normal form，这里不采用此 $P$，我们尝试逐层构造一个具备 normal form 的 $P$ 组合子.

构造过程

基本结构

用高级语言的伪代码表示现有的 $P$:

combinator p(x,y):            // L1: define p
    if (xy == 0):
        return const(y)                     
    else:
        return p(x, σ y)       // L5: call p

递归的 $\lambda $，形如 $P \equiv \lambda x. MPN $，像这样的 $\lambda$-term，符合我们在高级语言程序设计的经验，但是不符合 Lambda Calculus 中的规范，因为 Lambda Calculus 对 $\lambda$-term 的归纳定义并不包含为 abstraction 赋标识符的规则，我们写 $P$ 等标识符的目的只在于提升可读性和明确表达式结构，而不是借助标识符的复用来像高级语言编程一样定义递归函数. 一个细节是，我们在书里看到的为某个 $\lambda$-term 记标识符用的符号是 $\equiv$ 而不是 $=$.

我们不能通过标识符的复用定义递归不意味着我们不能定义递归，只是我们需要依赖多一层的抽象来构造出 形式上的非递归，事实意义上的递归.

从高级语言编程的角度出发，如果我们希望用某种方式取代 L5 中对 p 自身的调用，我们可以如下修改我们的代码. 为了两个分支的结构一致，我们设计一个函数列表 t，t 中的两个函数对应两个分支，函数 getCurrentY 将返回当前 y 值，recursion_p 将承担递归的工作：（这里先不考虑函数的具体结构和参数设计/参数传递的问题，后面总有办法的，这里我们只关心整体结构）

t = [getCurrentY, recursion_p]      // list of functions

combinator p(x,y):            
    if (xy == 0):
        return t[0]                     
    else:
        return t[1]    

如何在 Lambda Calculus 中表达以上的代码？为了专注于我们目前处理的抽象层次，先将 $P \equiv \lambda xy.\textbf{D}y(Px(\bar{\sigma}y))(xy)$ 的结构简化为 $P \equiv \lambda xy.\textbf{D}AB(xy)$

根据预期 / 上面的伪代码，我们可以写出大致的 $\lambda $ 框架如下:

$$ P \equiv \lambda xy. T(xy)[params] $$ $$ T \equiv \textbf{D}AB $$ $$ A \equiv \lambda [params]. \dots$$ $$ B \equiv \lambda [params]. …$$

此时 $PXY = _{\beta,w} T(XY) $，$ XY = _{\beta, w} \bar{0} \longrightarrow PXY = A; XY \neq _{\beta, w} \bar{0} \longrightarrow PXY = B $ .

我们预期：将分支的具体逻辑放在 $T$ 中，将分支的选择和分支函数参数传递放在 $P$ 中.

具体细节

上面我们忽略了许多细节，现在是考虑细节的时候了 :)

首先注意一个事实：我们将分支函数参数传递的工作放在 $P$ 中，意味着无论当前 $P$ 中的 $(xy)$ 将导向哪个分支，我们传递的参数列表都是一致的 / 都只能是一致的. 因为 $(xy) = _{\beta,w}\bar{0}$ 对应的情况更简单，只需返回当前 $y$，所以我们延后考虑这一情况，先考虑 $(xy) ≠ _{\beta,w}\bar{0}$ 的情况，让前者迁就后者（，因为两个分支都与 $y$ 有关，所以参数列表中必然有 $y$，在这一点上两个分支是有共性的；另一方面，我们甚至可以两个分支函数对应的参数并列传递，然后在 $A$,$B$ 的具体实现中 不对与本分支无关的参数进行绑定）.

递归（迭代）分支的构造

目标是：$XY \neq _{\beta, w} \bar{0} \longrightarrow PXY = B \xlongequal{\text{expected}} PX(\bar{\sigma}Y) $，我们希望函数 $B$ 与 $P$ 中传递的 $[params]$ 应用后得到的 $\lambda$-term 和 $PXY$ 具备一样的结构（注意不是 $B$ 和 $P$ 两个 abstraction 本身结构一致），只是 $Y$ 位置的值替换成了 $(\bar{\sigma}Y)$，为了得到和 $P$ 一样的结构，最简单的方法是——把 $P$ 现有的组件作为 $[params]$ 传递到 $B$（，当然也传递到了 $A$），然后在 $B$ 中把这些组件重组成 $P$ 的结构：

$$ P \equiv \lambda xy. T(xy)Txy $$ $$ T \equiv \textbf{D}AB $$ $$ A \equiv \lambda tuv. \dots$$ $$ B \equiv \lambda tuv. q(uv) $$

（$ T \mapsto t, x \mapsto u, y \mapsto v$）

由于 $[params]$ 的传递，现在 $P$ 的结构发生了改变，我们需要让 $B$ 与新的 $P$ 结构同步；另一方面，我们需要在 $B$ 的内部将传递进来的 $y$ （由 $v$ 绑定）变为 $\bar{\sigma}y$：

$$ P \equiv \lambda xy. T(xy)Txy $$ $$ T \equiv \textbf{D}AB $$ $$ A \equiv \lambda tuv. \dots$$ $$ B \equiv \lambda tuv. q(u(\bar{\sigma}v))qu(\bar{\sigma}v) $$

做一个检查：当 $XY \neq _{\beta, w} \bar{0}$：

$ \quad PXY $
$ = _{\beta,w} T(XY)TXY $
$ = _{\beta,w} BTXY $
$ = _{\beta,w} T(X(\bar{\sigma}Y))TX(\bar{\sigma}Y) $
$ = _{\beta,w} PX(\bar{\sigma}Y) $

符合我们的预期，至此，迭代分支的构造就完成了.

迭代终止分支的构造

目标是：$XY = _{\beta, w} \bar{0} \longrightarrow PXY = A \xlongequal{\text{expected}} Y $，在 $B$ 的构造过程中，我们已有的参数列表是 $ t \mapsto T, u \mapsto x, v \mapsto y$，在 $A$ 中，我们只需要把 $y$ 提取出来即可，所以 $A = \lambda tuv.v$ ，如果你希望和 Definition 4.8 的记法保持一致，那么 $A = \Pi^3_3$.

完整 $\lambda$

$$ P \equiv \lambda xy. T(xy)Txy $$ $$ T \equiv \textbf{D}AB $$ $$ A \equiv \lambda tuv. v (= _{\beta,w} \Pi^3_3) $$ $$ B \equiv \lambda tuv. q(u(\bar{\sigma}v))qu(\bar{\sigma}v) $$

LCaC Theorem 4.20 中的 $P$ 简述

LCaC Theorem 4.20 中给出的 $P$ 定义如下：

$$ T \equiv \lambda x.\textbf{D}\bar{0}(\lambda uv.u(x(\bar{\sigma}v))u(\bar{\sigma}v)) $$ $$ P \equiv \lambda xy.Tx(xy)(Tx)y $$

以与前文一致的格式转写：

$$ P \equiv \lambda xy.Tx(xy)(Tx)y $$ $$ T \equiv \lambda x.\textbf{D}AB $$ $$ A \equiv \bar{0} $$ $$ B \equiv \lambda uv.u(x(\bar{\sigma}v))u(\bar{\sigma}v) $$

在一些时刻把 $(Tx)$ 作为一个整体，让表达式更简洁了一些，同时让 $x$ 和 $T$ 有绑定关系（$T \equiv \lambda x….$），在 $T$ 的内部依然可以单独地拿出 $x$ 使用；$P$ 中的 $(Tx)$ 闭包，使得传参的形态是 $B(Tx)y$ —— 而不是 $BTxy$ ——让 $A$ 的设计更简洁了，$A \equiv \bar{0}$.

虽然在细节上略有差别，但是整体结构与本文给出的 $P$ 是一致的.

其他

尝试着展开上面的 $P$:

$$ \lambda xy.\lambda x.\textbf{D}\bar{0}(\lambda uv.u(x(\bar{\sigma}v))u(\bar{\sigma}v))x(xy)(\lambda x.\textbf{D}\bar{0}(\lambda uv.u(x(\bar{\sigma}v))u(\bar{\sigma}v))x)y$$

如果你愿意把以下也全部展开：
$ \textbf{D} = _{\beta, w} \lambda xyz.z(\textbf{K}y)x, \quad \textbf{K} = _{\beta, w} \lambda xy.x $
$ \bar{0} = _{\beta, w} \lambda xy.y $
$ \bar{\sigma} = _{\beta, w} \lambda nfz. f (n f z)$

$$ \lambda xy.\lambda x.(\lambda xyz.z((\lambda xy.x)y)x)(\lambda xy.y)(\lambda uv.u(x(\lambda nfz. f (n f z)))u(\lambda nfz. f (n f z)))x(xy)(\lambda x.(\lambda xyz.z((\lambda xy.x)y)x)(\lambda xy.y)(\lambda uv.u(x(\lambda nfz. f (n f z)))u(\lambda nfz. f (n f z)))x)y$$

可以说，我们用这一堆符号 + Pure Lambda Culculus 的演算规则完成了一个迭代程序的构造——Programming in Pure Lambda Calculus.