Let's build our mathematics by using lambda calculus && church encoding!

· · 算法·理论

致谢

Gemini 2.5 Pro 0325 && 0506：文本润色、事实正确性审查，以及帮助我学习、理解和回忆这些内容。

myster1ous： 给予我巨大的启发，帮助我构建出 prev 函数。

前言

本文的目的是带领大家踏上一段奇妙的旅程：我们将使用 λ 演算（Lambda Calculus）这一极简的计算模型，并通过丘奇编码（Church Encoding）这一巧妙的技术，一步步构建出我们日常编程中熟悉和依赖的计算体系，例如数字、布尔逻辑乃至更复杂的数据结构。

为了方便演示和实践，本文中的所有代码示例都将使用 Scheme 语言。Scheme 是 Lisp 家族的一员，它的语法是 S-表达式 (Symbolic Expressions)。S-表达式不仅简洁优雅，而且其结构与 λ 演算的表达方式惊人地契合。

在我们开始之前，让我们先快速了解一下 S-表达式：

例如，表达式 (+ 1 (* 2 3)) 在 Scheme 中表示数学上的 1 + (2 * 3)。 这里：

  1. 最外层的 (+ 1 (* 2 3)) 是一个 S-表达式。+ 是操作符，1 和 (* 2 3) 是它的参数。
  2. (* 2 3) 本身也是一个 S-表达式。* 是操作符，2 和 3 是它的参数。执行它会得到 6。
  3. 所以整个表达式 (+ 1 6) 最终会计算得到 7。

理解了 S-表达式，我们就可以更顺畅地进入 λ 演算的世界了。

λ 演算：计算的本质

λ 演算（Lambda Calculus）由阿隆佐·丘奇在 20 世纪 30 年代提出，它是一个极其简洁却具有图灵完备计算能力的数学形式系统。这意味着任何可计算的函数都可以用 λ 演算来表达和计算。

λ 演算的核心要素出奇地少，主要包括：

  1. 变量 (Variables): 如 x, y, f 等，用作参数名或函数本身的占位符。
  2. 函数抽象 (Function Abstraction): 这是定义一个新（通常是匿名的）函数的过程。
  3. 函数应用 (Function Application): 这是将一个函数作用于其参数（即调用函数）的过程。

让我们逐一来看。

1. 函数抽象 (定义函数)

在传统的数学或 λ 演算表示法中，一个接受参数 x 并返回表达式 E 的函数可以写为 \lambda x.E。 在 Scheme (以及本文的 S-表达式) 中，我们这样表示：

(lambda (x) E)

这里的 lambda 是一个特殊的关键字，表示我们正在定义一个匿名函数。(x) 是参数列表（这里只有一个参数 x），而 E 是函数体，代表函数要执行的计算并返回的结果。

例如，一个接受参数 x 并简单返回 x 本身的函数 (称为恒等函数)：

(lambda (x) x)

这是一个非常基础但重要的函数。

再举一个例子，一个接受参数 x 并期望返回 x+1 的函数：

(lambda (x) (+ x 1))

请注意： 在这个例子中，我们暂时借用了 Scheme 中预定义的 + 操作符和数字 1。这有助于我们直观地理解函数定义。然而，在纯粹的 λ 演算中，并不存在预定义的数字或算术运算符。一切——包括数字、布尔值和运算——都需要从最基本的函数抽象和应用来构建。这正是我们稍后将通过“丘奇编码”来实现的迷人之处！现在，请将注意力集中在 lambda 如何定义一个接受输入、进行处理、然后输出结果的“黑盒子”。

这些用 lambda 定义的函数都是匿名函数，它们没有名字。

2. 函数应用 (调用函数)

定义了函数，我们自然需要调用它。在传统表示法中，将函数 f 应用于参数 a 通常写作 f(a) 或 f\;a。 在 S-表达式中，函数应用的形式非常统一：

(f a)

其中 f 是要应用的函数，a 是传递给函数的参数。

如果我们想直接应用一个匿名函数，可以这样做：

((lambda (x) (+ x 1)) 5)

这个表达式的含义是：将匿名函数 (lambda (x) (+ x 1)) 应用于参数 5。计算过程（我们稍后会详细讨论其规则）会得到 6。

虽然纯粹的 λ 演算主要处理匿名函数，但在像 Scheme 这样的编程语言中，为了代码的清晰和可重用性，我们通常会给函数命名。这可以通过 define 实现：

(define inc (lambda (x) (+ x 1)))

这里，我们将前面定义的“加一”函数命名为 inc。现在，我们可以通过名字来调用它：

(inc 5) ; 这将返回 6
(inc 10) ; 这将返回 11

需要强调的是，define 并不是 λ 演算本身的一部分，它是 Scheme 提供的用于绑定名称到值的便利工具。在 λ 演算的理论探讨中，我们更多关注匿名函数及其组合。

3. 万物皆函数：λ 演算的核心思想

λ 演算最令人着迷的一点或许是它的极简主义哲学：在纯粹的 λ 演算中，一切皆是函数。 我们通常认为理所当然存在的数字 (0, 1, 2...)、布尔值 (真/假)、条件判断 (if-then-else)、数据结构 (如列表) 等等，在 λ 演算的宇宙中，都是通过巧妙地组合和嵌套函数来表达的。

这意味着，理论上我们只需要“定义函数”和“应用函数”这两个基本操作，就能构建出整个可计算的世界。这听起来可能有些抽象和不可思议，但别担心，本文的后半部分将通过丘奇编码来具体展示如何用函数来表示数字和布尔值，并在此基础上进行运算。

λ 演算的运算法则

λ 演算有几条基本的变换规则，它们定义了表达式如何被“计算”或“简化”。最重要的规则有：

a. α-变换 (Alpha Conversion / α-renaming)

α-变换指的是，在不改变函数行为的前提下，可以对函数定义中的绑定变量（即参数名）进行重命名。

例如，以下两个函数定义是完全等价的：

(lambda (x) (+ x 1))

和

(lambda (y) (+ y 1))

（用传统符号表示即 \lambda x.x+1 等价于 \lambda y.y+1）

只要新的参数名不与函数体内的自由变量（即那些不是由当前 lambda 定义的参数，而是来自外部作用域的变量）冲突，这种重命名就是有效的。α-变换告诉我们，参数的具体名字是什么并不重要，重要的是函数的结构和行为。

b. β-规约 (Beta Reduction)

β-规约是 λ 演算的“引擎”，它描述了函数应用（调用）是如何执行的，其本质就是代入 (substitution)。

当一个形如 ((lambda (v) E_body) E_arg) 的表达式出现时（即一个 lambda 函数紧接着被一个参数应用），β-规约允许我们将函数体 E_body 中所有出现的绑定变量 v 都替换成实际参数 E_arg 的（经过求值的）副本。

例如，对于表达式：

((lambda (x) (+ x 1)) 5)

根据 β-规约：

  1. 找到 lambda 的参数 x 和函数体 (+ x 1)。
  2. 找到实际传入的参数 5。
  3. 将函数体 (+ x 1) 中的所有（自由出现的）x 替换为 5。
  4. 得到新的表达式：(+ 5 1)。

在 Scheme 环境下，这个表达式 (+ 5 1) 会被进一步求值为 6。β-规约是实现计算的核心步骤。

c. η-变换 (Eta Conversion / η-reduction)

η-变换表达了函数外延性的概念：如果两个函数对于所有可能的输入都产生相同的结果，那么它们就是等价的。

形式上，如果 F 是一个函数，且变量 x 在 F 中不是自由变量 (not free in F)，那么： (lambda (x) (F x)) 等价于 F。 （用传统符号表示即 \lambda x.(F\;x) 等价于 F，如果 x \notin FV(F)）

这意味着，如果一个函数的唯一作用就是将其参数传递给另一个函数 F 并返回结果，那么这个外层包裹的函数实际上就是 F 本身。

例如，如果我们有函数 inc (定义为 (lambda (z) (+ z 1)))，那么： (lambda (y) (inc y)) 就 η-等价于 inc 本身。

α-变换、β-规约和（可选的）η-变换共同构成了 λ 演算的计算基础。对于构建我们的计算体系而言，β-规约是最直接相关的“执行”规则。

柯里化 (Currying)：用一元函数模拟多元函数

你可能已经注意到，在纯粹的 λ 演算定义中，函数抽象（lambda）一次只绑定一个参数。例如我们前面看到的 (lambda (x) x)（\lambda x.x）或 (lambda (x) (+ x 1))（\lambda x.x+1）。那么，我们如何表示需要多个参数的函数呢，比如一个计算两数之积的函数，直觉上可能会写成类似 (lambda (x y) (* x y))（或 \lambda xy. x \times y）的形式？

在纯粹的 λ 演算中，函数严格来说只接受一个参数。但是，通过一种称为柯里化 (Currying) 的巧妙技巧（以逻辑学家哈斯凯尔·柯里命名），我们可以用这些一元函数来优雅地实现多元函数的效果。

这里的关键在于 λ 演算中的一个核心特性：函数是“一等公民”。这意味着函数可以作为参数传递给其他函数，也可以作为其他函数的返回值。能够接受函数作为参数或返回函数的函数，我们称之为高阶函数 (Higher-Order Functions)。

柯里化的思想很简单： 要模拟一个接受多个参数（比如 n 个）的函数，我们可以：

  1. 定义一个一元函数，它接受第一个参数。
  2. 这个函数返回一个新的一元函数，这个新函数接受第二个参数。
  3. 这个新函数又返回一个更新的一元函数，接受第三个参数...
  4. 如此往复，直到所有 n 个参数都被逐个接受。最后一个返回的函数才会最终计算并返回结果。

让我们看一个例子。假设我们想实现一个两数相乘的函数 multiply(x, y)。通过柯里化，它可以表示为：

\lambda x . (\lambda y . x \times y)

在 Scheme 中，这对应于：

(lambda (x)
  (lambda (y)
    (* x y)))

这个表达式做了什么？

我们如何使用这个柯里化的乘法函数呢？

; 定义柯里化的乘法函数
(define curried-mult
  (lambda (x)
    (lambda (y)
      (* x y))))

; 应用第一个参数
(define times-three (curried-mult 3))
; (curried-mult 3) 返回的是 (lambda (y) (* 3 y))
; times-three 现在就是这个新函数

; 应用第二个参数
(display (times-three 5)) ; 输出 15

; 或者一步到位地调用
(display ((curried-mult 3) 5)) ; 输出 15

通过柯里化，我们成功地用一系列只接受单个参数的函数模拟了多参数函数的功能。这在 λ 演算的理论框架中至关重要，因为它表明仅用一元函数就足以表达所有计算。在很多函数式编程语言中，虽然它们可能提供了直接定义多参数函数的语法，但其底层有时就是通过柯里化来实现或解释的，或者柯里化本身就是一种推荐的编程范式。

一层又一层抽象：构建复杂性的阶梯

计算机科学与工程的伟大之处，很大程度上在于其精妙的抽象分层 (Layers of Abstraction)。我们从最底层的物理现象开始：

每一层都依赖于其下一层提供的功能，同时向上一层隐藏了不必要的复杂细节。这使得我们能够专注于当前层次的问题，而不必每次都从最原始的元素（比如电子的运动）开始思考。

在本文探索 λ 演算和丘奇编码的旅程中，我们也将采用类似的方法。 一旦我们成功地用 λ 演算定义了一个概念（比如布尔值、数字或某个运算），在后续的构造中，我们就会把它当作一个已知的、可以直接使用的“基本构建块”或“新定义的原语 (primitive)”。 我们不会在每次使用时都将其完全展开回最原始的 lambda 表达式形态（除非为了阐释特定原理）。

例如，一旦我们用 λ 表达式定义了数字 ZERO、ONE 和加法运算 ADD：

这样做可以让我们保持思路清晰，逐步构建更复杂的系统，而不至于迷失在无尽的 lambda 嵌套中。

现在，我们已经了解了 λ 演算的基本规则和柯里化这一重要技巧（它让我们能方便地处理多“参数”的函数），是时候开始用这些积木搭建我们计算世界的第一块基石了！

构建数学与计算体系的开始：基本元素

正如我们之前讨论的，纯粹的 λ 演算只拥有函数抽象（定义函数）和函数应用（调用函数）这两个基本构建块。我们日常编程中习以为常的“数字”、“自然数”、“加法运算”，乃至“字符”、“布尔值”（真/假）等等，在 λ 演算的原始宇宙中并不直接存在。

显然，如果缺少这些基本的数据类型和运算，我们很难用常规的思路来编写程序。

然而，λ 演算的强大之处在于，我们可以完全利用其自身的体系来构造出这些常用的对象。换句话说，我们可以为这些概念找到它们在 λ 演算世界中的函数式对应物 (functional counterparts)。

这个将数据类型和运算用纯函数来表达和实现的过程，正是丘奇编码 (Church Encoding) 的核心思想，由阿隆佐·丘奇本人开创。

让我们从最基本、也可能是最简单的概念开始：布尔值 (Booleans)。

布尔值 (Booleans) 与逻辑运算

布尔逻辑是计算的基石，它处理的是“真”与“假”这两个基本值。在丘奇编码中，这两个值被巧妙地定义为两个不同的选择函数：

这两个定义的神奇之处在于，它们内在地编码了条件选择的行为，这正是 if-then-else 语句的核心！ 如果我们有一个丘奇布尔值 condition，以及两个表达式 then-expr 和 else-expr，那么： (condition then-expr else-expr) 这个表达式本身就会根据 condition 是 true 还是 false 来求值：

有了 true 和 false 这两个基本构建块，我们就可以定义出标准的逻辑运算符：

  1. 逻辑非 (NOT): (not x) not 应该将 true 变为 false，将 false 变为 true。 我们可以这样定义 not：

    (define (not x)
  ; x 是一个选择函数，它会从后面两个参数中选一个
  ; 如果 x 是 true, 它选择第一个参数 (false)。
  ; 如果 x 是 false, 它选择第二个参数 (true)。
  (x false true))

    验证：

    • (not true) 会展开为 (true false true)，根据 true 的定义，返回 false。
    • (not false) 会展开为 (false false true)，根据 false 的定义，返回 true。

  2. 逻辑与 (AND): (and p q) p AND q 为真，当且仅当 p 和 q 都为真。

    (define (and p q)
  ; 如果 p 是 true，则 AND 的结果取决于 q (实际上是 q 本身)
  ; 如果 p 是 false，则 AND 的结果一定是 false
  (p q false)) ; 注：这里 q 必须也是一个丘奇布尔值

    解释：

    • 如果 p 是 true：表达式变为 (true q false)。true 选择第一个参数，即 q。所以 (and true q) 的结果就是 q。
      • 若 q 是 true，结果是 true。
      • 若 q 是 false，结果是 false。
    • 如果 p 是 false：表达式变为 (false q false)。false 选择第二个参数，即 false。所以 (and false q) 的结果总是 false。 这完全符合 AND 的逻辑。 (你原文中的 (p (q true false) false) 也是完全正确的，它更明确地将 q 的结果约束在 true 或 false 上，如果 q 本身已经是丘奇布尔值，(q true false) 就等价于 q。)

  3. 逻辑或 (OR): (or p q) p OR q 为真，只要 p 或 q 中至少一个为真。

    (define (or p q)
  ; 如果 p 是 true，则 OR 的结果一定是 true
  ; 如果 p 是 false，则 OR 的结果取决于 q (实际上是 q 本身)
  (p true q)) ; 注：这里 q 必须也是一个丘奇布尔值

    解释：

    • 如果 p 是 true：表达式变为 (true true q)。true 选择第一个参数，即 true。所以 (or true q) 的结果总是 true。
    • 如果 p 是 false：表达式变为 (false true q)。false 选择第二个参数，即 q。所以 (or false q) 的结果就是 q。
      • 若 q 是 true，结果是 true。
      • 若 q 是 false，结果是 false。 这完美符合 OR 的逻辑。 (同样，你原文的 (p true (q true false)) 也是正确的。)

阿隆佐·丘奇选择用“选择函数”来代表布尔值，这无疑是一个天才般的洞察。“选择”这一行为完美地概括了我们通常使用布尔值所做的核心操作——基于条件做出决策——这也使得后续逻辑运算的定义变得异常简洁和优雅。我们仅仅通过函数定义和应用，就凭空创造出了逻辑系统！

小扩展：更直观的 if 结构

既然我们的丘奇布尔值 true 和 false 本身就是选择函数，我们自然可以定义一个更符合我们日常编程直觉的 if 控制结构。这个 if 函数将接受三个参数：一个条件 (丘奇布尔值)，一个“then”分支的表达式，以及一个“else”分支的表达式。

(define (if-then-else condition then-branch else-branch)
  (condition then-branch else-branch))

你可能会问，这和直接写 (condition then-branch else-branch) 有什么本质区别呢？确实，通过我们前面讨论过的 η-变换 (Eta Conversion)，(lambda (c t e) (c t e)) 其实就等价于一个直接接受 c, t, e 并应用的结构（在Scheme中，多参数函数可以看作是柯里化的一种语法糖）。 然而，定义这样一个 if-then-else 函数的好处在于：

  1. 可读性： (if-then-else hungry? (eat food) (sleep)) 比 (hungry? (eat food) (sleep)) 更明确地表达了条件判断的意图，尤其是当 hungry? 本身也是一个复杂表达式时。
  2. 抽象的体现： 它再次强调了我们可以通过函数封装来构建我们熟悉的编程构造。这更像是一种“语法糖”，它向我们展示了如何将底层的函数式构造包装成更易读、更符合特定编程范式的形式。

这再次提醒我们，λ 演算的表达能力是灵活的，我们可以基于核心规则构建出我们需要的抽象层次。

自然数 (Natural Numbers)：函数的重复应用

继布尔值之后，下一个重要的基石是自然数 (Natural Numbers)，如 0, 1, 2, ... 与布尔值通过“选择”来定义不同，自然数的丘奇编码抓住的是“重复”或“迭代”这一核心概念。

阿隆佐·丘奇的天才之处在于他意识到，数字可以被表示为高阶函数，其含义是“一个函数被应用的次数”。

具体来说，一个丘奇数 n 是一个函数，它接受两个参数：

  1. 一个函数 f (代表要被重复应用的操作)。
  2. 一个初始值 x (代表该操作的起点，或者说被操作的对象)。

这个丘奇数 n 会将 f 应用到 x 上恰好 n 次。

“重复应用 n 次”如何用纯函数定义呢？ 我们没有循环语句，也没有内置的计数器。 答案在于巧妙地利用函数本身的结构，类似于数学中从 0 和后继操作构建自然数的皮亚诺公理 (Peano Axioms)。

数字 零 (ZERO)

数字 零 (ZERO) 就代表“将函数 f 应用零次”。这意味着无论 f 是什么，初始值 x 都原封不动地返回。 其定义如下：

ZERO := \lambda f . \lambda x . x

在 Scheme 中：

(define ZERO
  (lambda (f)      ; ZERO 接受一个函数 f
    (lambda (x)    ; 并返回一个新的函数，这个新函数接受 x
      x)))         ; 然后直接返回 x (f 应用了0次)

这里的 ZERO 是一个柯里化的函数。它首先接受一个函数 f，然后返回另一个函数。这个内部函数接受初始值 x 并直接返回 x，完美体现了 f 被应用了零次。

例如，如果我们有一个函数 inc (加一) 和一个值 10： ((ZERO inc) 10)

  1. (ZERO inc) 会返回 (lambda (x) x) （因为 f 是 inc，但没有被使用）。
  2. 然后 ((lambda (x) x) 10) 会返回 10。 这正是我们期望的“对 10 加一 0 次”的结果。

后继函数 (Successor Function, S)

有了 ZERO，我们如何得到其他数字呢？我们需要一个后继函数 (Successor Function)，通常表示为 S。S 接受一个丘奇数 n 作为输入，并返回代表 n+1 的丘奇数。

如果丘奇数 n 代表“将 f 应用 n 次”，那么 (S n)（即 n+1）就应该代表“将 f 应用 n+1 次”。 这可以这样理解：要将 f 应用 n+1 次到 x 上，我们可以先将 f 应用 n 次到 x 上得到一个中间结果，然后再对这个中间结果额外应用一次 f。

形式化地，后继函数 S 定义为：

S := \lambda n . \lambda f . \lambda x . f ( (n f) x )

在 Scheme 中：

(define S
  (lambda (n)          ; S 接受一个丘奇数 n
    (lambda (f)        ; 返回一个新函数 (代表 n+1)，它接受 f
      (lambda (x)      ; 再返回一个新函数，它接受 x
        (f             ; 将 f 应用于...
         ((n f) x)))))) ; ...n 将 f 应用于 x 的结果

让我们仔细解读一下 S 的定义：

  1. S 接受一个丘奇数 n (例如 ZERO)。
  2. 它返回一个新的函数，这个函数就是代表 n+1 的丘奇数。这个新函数也遵循丘奇数的规范，所以它也期望接受一个函数 f 和一个值 x。
  3. 当这个代表 n+1 的函数被 f 和 x 调用时，它的行为是 (f ((n f) x))：
    • (n f): 首先，我们将输入的丘奇数 n 应用于 f。回忆一下，丘奇数 n 本身是 (lambda (f_inner) (lambda (x_inner) ...)) 的形式。所以 (n f) 会返回一个“准备好对某个 x_inner 应用 f_inner（这里是 f）n 次”的函数。
    • ((n f) x): 接着，我们将上面返回的函数应用于 x。这就完成了 f 在 x 上的 n 次应用。
    • (f ((n f) x)): 最后，我们将 f 再额外应用一次到 ((n f) x) 的结果上。这就构成了 f 的 n+1 次应用。

这种从 ZERO 和后继函数 S 出发来构造所有自然数的方法，其思想与数学中的皮亚诺公理 (Peano Axioms) 定义自然数的方式高度相似（皮亚诺公理：① 0 是自然数；② 每个自然数 a 都有一个后继数 S(a)；...）。

现在，我们可以定义其他数字了：

例如，ONE 的展开会是：

(define ONE (S ZERO))
;; ONE 展开为：
;; (lambda (f)
;;   (lambda (x)
;;     (f ((ZERO f) x))))
;; 由于 ((ZERO f) x) 会返回 x，所以 ONE 进一步简化为：
;; (lambda (f)
;;   (lambda (x)
;;     (f x)))

这完美符合“将 f 应用一次到 x”的定义。

同样，TWO 会展开为 (lambda (f) (lambda (x) (f (f x))))，即 f 应用两次。

通过 ZERO 和 S，我们已经用纯粹的函数构建了整个自然数体系的“骨架”！下一步，我们将探索如何在这些丘奇数上进行算术运算，比如加法和乘法。

算术运算 (Arithmetic Operations): 加法与乘法

有了代表自然数的丘奇编码，我们自然想在它们之上定义算术运算，比如加法和乘法。

熟悉皮亚诺公理 (Peano Axioms) 的朋友可能还记得它们是如何递归定义加法和乘法的：

直接将这些递归定义转换为纯 λ 演算（尤其是没有显式递归操作符如 Y 组合子的情况下）会有些棘手，特别是处理像 S(n) 这样需要“分解”参数的模式，或者找到一个数的前驱。

幸运的是，丘奇编码的本质——“将一个函数应用特定次数”——为我们提供了一条更直接、更优雅的路径。

加法 (Addition): m + n

思考一下加法 m + n 的含义：它可以被看作是从数字 m 开始，连续应用“加一”（即后继函数 S）操作 n 次。

这完美契合了丘奇数 n 的定义！回忆一下，丘奇数 n 是一个函数 (lambda (f) (lambda (x) ...))，它会将 f 应用到 x 上 n 次。

所以，m + n 可以通过将丘奇数 n 应用于后继函数 S 和初始值 m 来实现： ((n S) m)

因此，我们可以定义一个柯里化的加法函数 PLUS (或者叫 ADD)：

PLUS := \lambda m . \lambda n . ( (n S) m )

在 Scheme 中：

(define PLUS
  (lambda (m)      ; PLUS 接受第一个加数 m
    (lambda (n)    ; 返回一个函数，该函数接受第二个加数 n
      ((n S) m)))) ; 将 S 应用到 m 上 n 次

让我们来验证一下 (PLUS ONE TWO) 是否等于 THREE：

加法的定义就是如此简洁！它直接利用了丘奇数 n 作为“迭代器”的特性。

乘法 (Multiplication): m × n

乘法 m × n 又如何用类似的思想表达呢？ 它可以被看作是将“加 m”这个操作，应用 n 次，并且从 ZERO 开始累加。 也就是说： m \times n = \underbrace{m + m + \dots + m}_{n \text{ times}}。

所以，m × n 可以通过将丘奇数 n 应用于“加 m”这个函数 (PLUS m) 和初始值 ZERO 来实现： ((n (PLUS m)) ZERO)

因此，柯里化的乘法函数 TIMES (或者叫 MULTIPLY) 定义为：

TIMES := \lambda m . \lambda n . ( (n (PLUS \ m)) ZERO )

在 Scheme 中：

(define TIMES
  (lambda (m)          ; TIMES 接受第一个乘数 m
    (lambda (n)        ; 返回一个函数，该函数接受第二个乘数 n
      ((n (PLUS m))    ; 将 (PLUS m) 这个“加m”的函数...
       ZERO))))        ; ...应用 n 次到 ZERO 上

这里的 (PLUS m) 是一个函数，它等待另一个参数 k 来计算 m+k。丘奇数 n 正好可以将这个“加 m”的函数重复作用。

例如，思考 (TIMES TWO THREE):

  1. (TIMES TWO) 返回 (lambda (n) ((n (PLUS TWO)) ZERO))。
  2. 将其应用于 THREE： ((THREE (PLUS TWO)) ZERO)。
  3. THREE 会将 (PLUS TWO) 这个函数应用 3 次到 ZERO 上：
    • 第一次：((PLUS TWO) ZERO) 结果是 TWO (0 + 2 = 2)
    • 第二次：((PLUS TWO) TWO) 结果是 FOUR (2 + 2 = 4) (假设我们已经定义了 FOUR)
    • 第三次：((PLUS TWO) FOUR) 结果是 SIX (4 + 2 = 6) (假设我们已经定义了 SIX) 这正是 2 \times 3 = 6。

通过这些定义，我们看到丘奇编码不仅能表示数字，还能以一种非常优雅和本质的方式来定义它们之间的运算，这一切都仅仅建立在函数抽象和应用之上！

进入更深层次的构造：比较与减法

我们已经成功地用纯函数定义了布尔逻辑、自然数以及基本的加法和乘法运算。这本身已经是一个了不起的成就，展示了 \lambda 演算惊人的表达能力。现在，我们将继续沿着这条道路前进，构建更复杂的计算工具，首当其冲的是如何比较两个数字，以及如何定义减法。

正如你可能预料到的，这些操作的定义会比加法和乘法稍微复杂一些，它们需要我们更深入地挖掘丘奇编码的潜力，并引入一些新的辅助函数。

减法 · 引入

按照四则运算的顺序，接下来我们要构造的就是减法，它是加法的逆运算。

面对这个问题，你第一时间的想法是什么？很有可能你会想到“前驱函数”（即找到 n-1），然后思考“如何从 n 次函数应用中去除一次”。

这听起来似乎直接，例如通过求反函数。然而，并非所有函数都拥有反函数，且求取反函数本身也相当复杂。我们需要另辟蹊径。

从“加法的逆运算”这个角度思考 n-m：我们是否可以枚举一个数 k (从 0 到 n)，检查 k+m 是否等于 n？如果相等，则 k 就是 n-m 的值。如果找不到这样的 k，则 n-m 在自然数内无解。

然而，这又引入了一个新问题：我们如何判断两个丘奇数是否“相等”？这是一个我们尚未定义的关键谓词。

有人可能会说：“如果 n-m=0，那么 n 不就等于 m 了吗？”或者“如果 n \ge m 且 n \le m，那么 n=m。” 但这又会使我们陷入对减法或比较运算的循环定义中。

别担心，我们将逐步解决这些问题。

判断是否为零 (ZERO?)：一个重要的边界条件

要判断任意两个自然数是否相等，或者进行更复杂的算术运算，我们至少需要能够判断一个数是否为零。这是许多递归定义和条件判断的基础。

我们可以通过以下方式巧妙地定义 ZERO? 谓词：

\text{ZERO? predicated} := \lambda n . (n \ (\lambda x . \text{FALSE})) \ \text{TRUE}

在 Scheme 中：

(define ZERO?
  (lambda (n)
    ((n (lambda (x) FALSE)) TRUE)))

这个定义的巧妙之处在于它利用了丘奇数自身的特性：

这样，我们就得到了一个可靠的 ZERO? 测试。

构造数据结构的基础——丘奇对 (Church Pairs)

在定义更复杂的操作（如前驱函数）之前，我们需要一种方式来将两个值组合成一个单一的复合数据单元。丘奇对 (Church Pairs) 提供了这样的机制，它类似于许多编程语言中的 pair 或二元元组。

一个丘奇对通过一个高阶函数来表示，这个高阶函数接受一个“选择器”函数作为参数。当我们用两个值 a 和 b 构造一个序对时，这个序对函数会“包裹”住 a 和 b。当它被一个选择器函数 s 调用时，它会将 a 和 b 传递给 s，即执行 (s a b)。

构造序对的函数 CONS 定义如下：

\text{CONS} := \lambda a . \lambda b . \lambda s . (s \ a \ b)

在 Scheme 中：

(define CONS
  (lambda (first-element)
    (lambda (second-element)
      (lambda (selector-function)
        (selector-function first-element second-element)))))

要从序对中提取元素，我们需要合适的选择器。丘奇布尔值 TRUE (\lambda t . \lambda f . t) 和 FALSE (\lambda t . \lambda f . f) 正好可以胜任：

前驱函数 (PRED)：寻找 n-1

前驱函数 PRED 的目标是计算 n-1。对于丘奇数 ZERO，其前驱仍然是 ZERO (即 \text{PRED ZERO} = \text{ZERO} )。

直接从丘奇数“减去”一次函数应用是困难的。但我们有一个巧妙的思路：考虑一个序列，例如 (0, 0, 1, 2, 3, \dots) 。如果我们能通过某种方式定位到这个序列的第 n 项（0-indexed），那么这一项的值恰好是 n 的前驱（当 n=0 时为 0，当 n=1 时为 0，当 n=2 时为 1，以此类推）。

我们不必实际构造一个无穷列表。关键在于定义一个状态转换函数，该函数接受当前状态（一个序对），并返回序列中的下一个状态。丘奇数 n 可以将这个状态转换函数应用 n 次。

我们将状态表示为一个序对 (current-predecessor-value, flag):

初始状态为 (CONS ZERO ZERO)。 状态转换函数 PHI_PRED_STEP 定义为：

\Phi_{\text{PRED\_STEP}} := \lambda p . (\text{ZERO?} \ (\text{CDR}\ p)) \ (\text{CONS}\ \text{ZERO}\ \text{ONE}) \ (\text{CONS}\ (\text{S}\ (\text{CAR}\ p))\ \text{ONE})

在 Scheme 中：

(define PHI_PRED_STEP
  (lambda (p) ; p 是形如 (current-predecessor-value, flag) 的序对
    ((ZERO? (CDR p))          ; 检查 flag 是否为 ZERO
     (CONS ZERO ONE)          ; 如果是，下一个状态是 (ZERO, ONE)
     (CONS (S (CAR p)) ONE)))) ; 否则，下一个状态是 (S current-predecessor-value, ONE)

这个转换逻辑是：

  1. 如果 flag 是 ZERO（初始状态，意味着我们正在处理输入为 ZERO 或 ONE 的情况的“第一步迭代”）：下一个状态的 current-predecessor-value 保持 ZERO，并将 flag 置为 ONE。
  2. 如果 flag 是 ONE（后续状态）：下一个状态的 current-predecessor-value 是前一个值的后继 (S (CAR p))，flag 保持 ONE。

有了初始状态和转换函数，PRED n 就是将 PHI_PRED_STEP 应用 n 次到初始状态 (CONS ZERO ZERO) 上，然后取结果序对的第一个元素：

\text{PRED} := \lambda n . \text{CAR} \ (n \ \Phi_{\text{PRED\_STEP}} \ (\text{CONS ZERO ZERO}))

在 Scheme 中：

(define PRED
  (lambda (n)
    (CAR ((n PHI_PRED_STEP) (CONS ZERO ZERO)))))

让我们验证一下：

这完美地实现了前驱函数的功能。

减法 · 截断减法 (SUB)

有了前驱函数 PRED，定义减法就变得直接了。我们要实现的是截断减法 (Truncating Subtraction)，即 m-n。如果 m \ge n，结果是 m-n；如果 m < n，结果是 0（因为我们只处理自然数）。

$$ \text{SUB} := \lambda m . \lambda n . (n \ \text{PRED} \ m) $$ 在 Scheme 中： ```lisp (define SUB (lambda (m) (lambda (n) ((n PRED) m)))) ; 计算 m - n ``` 例如 `(SUB FIVE TWO)` 会将 `PRED` 应用 2 次到 `FIVE` 上，得到 `THREE`。而 `(SUB TWO FIVE)` 会得到 `ZERO`。 #### 关系运算符 基于 `SUB` 和 `ZERO?`，我们可以构建各种关系运算符： 1. **小于或等于 (`IS_LEQ?`)**: $m \le n$ 当且仅当 $m-n = 0$ (在截断减法中)。 $$ \text{IS\_LEQ?} := \lambda m . \lambda n . \text{ZERO?} \ (\text{SUB}\ m \ n) $$ ```lisp (define IS_LEQ? (lambda (m) (lambda (n) (ZERO? (SUB m n))))) ``` 2. **大于 (`IS_GT?`)**: $m > n$ 当且仅当 $m-n \neq 0$ (且 $m-n > 0$)，也即 $m \not\le n$。 $$ \text{IS\_GT?} := \lambda m . \lambda n . \text{NOT} \ (\text{IS\_LEQ?}\ m \ n) $$ 或者，更直接地：$m > n$ 当且仅当 $m-n$ 的结果不是 $ZERO$ (在我们的自然数和截断减法定义下，这意味着 $m-n$ 是一个正数)。 $$ \text{IS\_GT?}_{\text{alt}} := \lambda m . \lambda n . \text{NOT} \ (\text{ZERO?} \ (\text{SUB}\ m \ n)) $$ *(注：使用 $\text{IS\_GT?}_{\text{alt}}$ 定义，则 $m>n$ 为真。若 $m \le n$, $\text{SUB}\ m\ n$ 为 $\text{ZERO}$, $ZERO?$ 为 $\text{TRUE}$, $\text{NOT}$ 为 $\text{FALSE}$)* 3. **等于 (`IS_EQ?`)**: $m = n$ 当且仅当 $m \le n$ 并且 $n \le m$。 $$ \text{IS\_EQ?} := \lambda m . \lambda n . \text{AND} \ (\text{IS\_LEQ?}\ m \ n) \ (\text{IS\_LEQ?}\ n \ m) $$ ```lisp (define IS_EQ? (lambda (m) (lambda (n) (AND (IS_LEQ? m n) (IS_LEQ? n m))))) ``` 另一种思路是：$m=n$ 当且仅当 $m-n=0$ 且 $n-m=0$。所以 $(\text{SUB } m n)$ 和 $(\text{SUB } n m)$ 都必须是 `ZERO`。 4. **小于 (`IS_LT?`)**: $m < n$ 当且仅当 $n > m$。 $$ \text{IS\_LT?} := \lambda m . \lambda n . \text{IS\_GT?}\ n \ m $$ 或者 $m < n$ 当且仅当 $m \not\ge n$ (即 $\neg(n \le m)$)。 $$ \text{IS\_LT?}_{\text{alt}} := \lambda m . \lambda n . \text{NOT} \ (\text{IS\_LEQ?}\ n \ m) $$ 5. **大于或等于 (`IS_GEQ?`)**: $m \ge n$ 当且仅当 $n \le m$。 $$ \text{IS\_GEQ?} := \lambda m . \lambda n . \text{IS\_LEQ?}\ n \ m $$ 通过这些定义，我们已经构建了一套完整的基于丘奇编码的自然数关系运算。 #### 一点关于时间复杂度分析与计算模型的声明 我们发现，刚刚实现的算术运算（尤其是乘法、前驱、减法）的过程，如果完全展开成 $\beta$-规约，其步骤数会相当可观，效率较低。但是，$\lambda$ 演算主要是一个用于研究计算理论、证明计算完备性的数学工具，其直接实现的效率并非首要考量。在实际编程中，我们当然会使用硬件直接支持的、高度优化的原生数字类型和运算。 如果追求“高效的算术”，我们可以探索例如二进制表示的丘奇数。不过，这会引入显著的复杂性，超出了本文旨在演示如何用 $\lambda$ 演算构建一个完备计算体系的目标。 与此相对，我们将采取另一种视角。正如我们在前文“一层又一层抽象”中所讨论的，为了能够清晰地构建和分析更复杂的算法，我们将把这些已经定义的丘奇编码实体（如 `ZERO`, `PLUS`, `IF-THEN-ELSE`, `PRED`, `SUB`, `IS_LEQ?` 等）视为我们新的**抽象原语 (abstract primitives)**。 在后续的算法讨论和复杂度分析中，除非特别指出，我们将假设对这些抽象原语的一次调用（例如，执行一次 `(PLUS church_num1 church_num2)` 或一次 `(IS_LEQ? church_num1 church_num2))`) 构成一个基本计算步骤，其开销计为常数时间 $O(1)$（或者说，我们统计的是这些高级原语被调用的次数）。 这样做使我们能够专注于算法本身的逻辑和结构，而不必每次都回溯到底层的 $\lambda$-规约。这与我们在高级编程语言中分析算法时，将整数加法或比较视为 $O(1)$ 操作的做法是相通的。 --- 我们还缺乏一种重要的算术运算：除法。但是它的实现比较复杂，需要一些额外的工具。在下一节中，我们将引入这些必要的工具。 ## 递归：让函数调用自身 到目前为止，我们已经用 λ 演算构建了布尔逻辑、自然数、算术运算乃至简单的数据结构（丘奇对）。然而，你可能已经敏锐地注意到，我们似乎还缺少一个在编程中至关重要的工具：**循环或迭代**。我们用丘奇数 `n` 实现了将某个操作重复 `n` 次，但这更像是一个固定次数的 `for` 循环。对于更一般的情况，比如“当条件满足时重复执行某个操作”（类似 `while` 循环），或者像阶乘那样需要根据输入值决定计算深度的场景，我们目前的工具还不够。 在大多数编程语言中，这类重复性的任务通常通过递归（函数调用自身）或循环结构（`for`, `while`）来解决。循环结构本质上也可以看作是递归的一种特定模式或语法糖。因此，关键在于如何在 λ 演算这个纯粹的函数世界中实现递归。 让我们先看看在 Scheme 中，递归是如何轻易实现的。比如，计算阶乘的函数： ```lisp (define (factorial n) (if (= n 0) 1 (* n (factorial (- n 1))))) (factorial 5) ; 计算结果为 120 ``` 在这里，`define` 允许我们将函数命名为 `factorial`，然后在 `factorial` 的函数体内部，我们可以再次通过这个名字 `factorial` 来调用它自身。 但问题来了：在纯粹的 λ 演算中，函数通常是**匿名**的。回忆一下，我们定义的 `TRUE`、`ZERO`、`PLUS` 等都是 `(lambda (...) ...)` 这样的匿名函数，只是为了方便讨论，我们才用 `define` 给它们起了名字。如果一个函数没有名字，它如何在自己的定义中引用自己呢？这就好比写一封匿名信，却想在信的内容里提及“写这封信的我”——我们该如何指代这个匿名的“我”？ 这正是 λ 演算实现递归所面临的核心挑战。我们需要一种方法，让一个匿名函数能够获得对自身的引用。 ### “手动”实现递归：将函数作为参数传递 一种直观的想法是：如果一个函数 `g` 需要调用自身，我们可以修改 `g` 的定义，让它多接受一个参数，这个参数就是 `g` 自身（或者一个行为与 `g` 等同的函数）。 让我们尝试为一个“准阶乘函数”`almost-factorial` 这样做。这个 `almost-factorial` 期望接收一个 `self` 参数（代表它自己）和一个数字 `n`： ```lisp (define almost-factorial (lambda (self n) ; self 是期望中的递归调用 (if (= n 0) 1 (* n (self self (- n 1)))))) ; 注意这里：用 (self self ...) 来进行递归调用 ``` 要使用它，我们需要某种方式把 `almost-factorial` 这个函数本身传递给它自己的第一个参数 `self`： ```lisp (almost-factorial almost-factorial 5) ; 结果是 120 ``` 这种模式 `(f f x)` 有一个专门的名字，叫做 **U 组合子**（或模拟 U 组合子的行为），即 `U f = f f`。我们通过 `(almost-factorial almost-factorial ...)` 使得 `almost-factorial` 的第一个参数 `self` 确实是 `almost-factorial` 本身。在 `almost-factorial` 内部，当它需要递归调用时，它就调用 `(self self (- n 1))`，这实际上又变回了 `(almost-factorial almost-factorial (- n 1))`，递归得以实现！ 这种“将函数自身作为参数传递给自身”的技巧虽然可行，但每次调用时都需要重复写 `(f f x)` 这样的结构，显得有些笨拙。我们更希望有一个“魔法函数”，能够自动帮我们处理这种“自我引用”的传递。 ### 不动点组合子：Y 组合子与 Z 组合子 这个“魔法函数”就是**不动点组合子 (Fixed-Point Combinator)**。在数学中，函数 `f` 的一个不动点 `x` 是指满足 `f(x) = x` 的点。在计算理论中，递归函数可以被看作是某个高阶函数的不动点。 假设我们有一个函数生成器 `G`。`G` 接受一个函数 `h`（代表递归调用）作为参数，并返回一个新的函数，这个新函数就是我们想要定义的递归函数的“单步版本”。例如，对于阶乘，`G` 可以这样定义（这里暂时借用 Scheme 的数字和运算以便理解）： ```lisp (define G-factorial (lambda (h) ; h 是用于递归调用的函数 (即阶乘函数本身) (lambda (n) ; 返回的是阶乘函数的一步 (if (= n 0) 1 (* n (h (- n 1))))))) ; 这里用 h 来进行递归调用 ``` 我们希望找到一个函数 `factorial`，使得 `factorial` 等价于 `(G-factorial factorial)`。也就是说，`factorial` 是 `G-factorial` 这个高阶函数的不动点。 **Y 组合子**正是这样一个神奇的函数，它能为任何给定的函数生成器 `G` 找到其不动点。即 `(Y G)` 会产生一个函数 `f_rec`，这个 `f_rec` 满足 `f_rec = (G f_rec)`。 Y 组合子的经典定义是： $$ Y := \lambda g . (\lambda x . g (x \ x)) (\lambda x . g (x \ x)) $$ 在 Scheme 中表示为： ```lisp (define Y (lambda (g) ((lambda (x) (g (x x))) (lambda (x) (g (x x)))))) ``` 于是，` (Y G-factorial)` 就会是上面我们用 `define` 直接定义的那个 `factorial` 函数！我们不再需要在调用时手动传递 `factorial` 给自身了，Y 组合子帮我们完成了这个绑定。 --- **补充：Y 组合子如何工作：不动点属性的推导** Y 组合子的神奇之处在于它如何构造出这个不动点。让我们手动展开 `(Y G)` 的求值过程（使用 β-规约）来看看它是如何工作的。 回顾 Y 组合子的定义： ```lisp (define Y (lambda (g) ((lambda (x) (g (x x))) ; 我们将这个内部的 (lambda (x) ...) 称为 omega-maker (lambda (x) (g (x x)))))) ; 这是传递给 omega-maker 的参数，形式与 omega-maker 自身相同 ``` 为了方便推导，我们定义一个辅助函数 `omega_g` (或者叫 `make-omega-for-g`)，它依赖于 `g`： `omega_g := (lambda (x) (g (x x)))` 那么，Y 组合子可以看作是： `Y := (lambda (g) (omega_g omega_g))` 现在，我们将 Y 应用于我们的函数生成器 `G`： `(Y G)` 根据 Y 的定义，这会进行一次 β-规约，将 `G` 替换掉 Y 定义中的 `g`： `(Y G) evaluates-to (omega_G omega_G)` 这里 `omega_G` 就是 `(lambda (x) (G (x x)))` (即把 `g` 换成了具体的 `G`)。 接下来，我们来看 `(omega_G omega_G)` 是什么： `(omega_G omega_G)` `= ((lambda (x) (G (x x))) omega_G)` (将第一个 `omega_G` 展开) 现在，我们再次进行 β-规约：将 `omega_G` 这个实际参数替换掉 `(lambda (x) ...)` 中的形式参数 `x`。 `((lambda (x) (G (x x))) omega_G)` `evaluates-to (G (omega_G omega_G))` 我们得到了： 1. `(Y G) = (omega_G omega_G)` 2. `(omega_G omega_G) = (G (omega_G omega_G))` 综合这两步，我们可以通过代换得到： `(Y G) = (G (omega_G omega_G))` 现在，注意到等式右边的 `(omega_G omega_G)` 正是我们在第一步中定义的 `(Y G)`！ 所以，我们可以将 `(Y G)` 代换回去： `(Y G) = (G (Y G))` 这正是我们期望的不动点属性！ `(Y G)` 这个表达式本身（我们称之为 `f_rec`）等于将 `G` 应用于 `(Y G)`（即 `(G f_rec)`）。Y 组合子通过这种巧妙的自我应用结构，成功地为一个“期望接收自身作为参数”的函数生成器 `G` 创造了一个可以直接调用的递归函数 `(Y G)`，而这个递归函数 `(Y G)` 确实是 `G` 的不动点。 这就是为什么 Y 组合子能够在纯 λ 演算中实现递归的魔力所在。它构建了一个表达式，该表达式在求值时会“展开”成将生成器 `G` 应用于该表达式自身的形式。 --- 然而，Y 组合子的这个经典定义在严格求值/应用序求值（Applicative Order Evaluation，即函数参数在函数体执行前就被完全求值）的语言（如 Scheme）中直接使用时会遇到问题：`(x x)` 这一部分会导致无限递归求值，从而使程序无法终止。 为了解决这个问题，在应用序求值语言中，我们通常使用 **Z 组合子**，它是 Y 组合子的一个变体，通过引入一个额外的 `lambda` 来延迟 `(x x)` 的求值： $$ Z := \lambda g . (\lambda x . g (\lambda v . ((x \ x) v))) (\lambda x . g (\lambda v . ((x \ x) v))) $$ 在 Scheme 中： ```lisp (define Z (lambda (g) ((lambda (x) (g (lambda (v) ((x x) v)))) (lambda (x) (g (lambda (v) ((x x) v))))))) ``` 现在，我们可以用 Z 组合子和我们之前定义的 `G-factorial` 来构造阶乘函数： ```lisp (define factorial-via-Z (Z G-factorial)) (factorial-via-Z 5) ; 计算结果为 120 ``` 这里，`factorial-via-Z` 就是一个完全由 λ 演算（加上 Z 组合子）构造出来的递归阶乘函数。在纯 λ 演算的语境下，`G-factorial` 中的 `if`、`=`、`0`、`1`、`*`、`-` 当然也需要用我们之前讨论过的丘奇编码来定义。 不动点组合子（如 Y 或 Z）是 λ 演算中一个深刻而强大的概念。它们揭示了即使在这样一个极简的系统中，我们也能通过纯粹的函数抽象和应用来构建出递归这一复杂的控制结构。这为 λ 演算的图灵完备性提供了关键的一环，也意味着我们几乎拥有了构建任何可计算过程所需的所有理论工具。 有了递归，我们的 λ 演算工具箱才算真正强大起来，能够去定义和执行那些需要自我参照和重复计算的复杂算法了。 我们很快就会看到它们的威力。在下一节中，我们将应用它们来构造之前我们暂时搁置的算术逻辑：除法。 ### 更进一步的算术：除法 (`DIV`) 在构建了加法、减法和乘法之后，自然会想到四则运算的最后一个基本操作：**除法**。我们将在这里实现整数除法，即计算 $m \div n$ 的商 $q$。 与加法和乘法不同，除法的计算过程（重复从被除数中减去约数，直到余数小于约数）通常不依赖于一个固定的、由输入数字直接决定的迭代次数。这暗示了我们需要使用递归来实现它。 #### 除法的核心逻辑：重复减法与递归 整数除法 $m \div n$ 的商 $q$ 可以通过以下递归过程找到： 1. **基本情况**：如果 $m < n$，那么我们无法再从中减去 $n$ 了，此时累积的商就是最终结果。 2. **递归步骤**：如果 $m \ge n$，那么我们可以从 $m$ 中减去一个 $n$，然后对新的 $m' = m-n$ 和原始的 $n$ 再次进行除法过程，同时将累积的商加一。 我们需要一个辅助的递归函数，它会跟踪当前的被除数、原始的除数以及到目前为止累积的商。 #### 构造除法的递归辅助函数生成器 (`G_DIV_LOOP`) 让我们定义一个函数生成器 `G_DIV_LOOP`。它接受一个参数 `self_div_loop`（代表递归调用自身），并返回一个执行单步除法逻辑的函数。这个单步函数接受三个参数： * `current_m`：当前的被除数。 * `original_n`：原始的（保持不变的）除数。 * `current_q`：到目前为止累积的商。 $$ \begin{aligned} \text{G\_DIV\_LOOP} := \lambda \text{self\_div\_loop} . \lambda \text{current\_m} . \lambda \text{original\_n} . \lambda \text{current\_q} . \\ \quad (\text{IS\_LT?} \ \text{current\_m} \ \text{original\_n}) \\ \quad \quad \text{current\_q} \\ \quad \quad (\text{self\_div\_loop} \ (\text{SUB} \ \text{current\_m} \ \text{original\_n}) \ \text{original\_n} \ (\text{S} \ \text{current\_q})) \end{aligned} $$ 在 Scheme 中（使用我们之前定义的 `IF-THEN-ELSE` 的等价结构，即丘奇布尔值直接作为选择器）： ```lisp (define G_DIV_LOOP (lambda (self_div_loop) (lambda (current_m) (lambda (original_n) (lambda (current_q) ((IS_LT? current_m original_n) ; If current_m < original_n current_q ; Then: return current_q (self_div_loop (SUB current_m original_n) ; Else: recurse original_n (S current_q)))))))) ``` 这里我们使用了之前定义的 `IS_LT?` (小于)，`SUB` (截断减法)，和 `S` (后继函数)。 #### 使用 Z 组合子实现递归循环 现在，我们可以使用 Z 组合子来从 `G_DIV_LOOP` 生成实际的递归辅助函数 `DIV_LOOP`： $$ \text{DIV\_LOOP} := \text{Z} \ \text{G\_DIV\_LOOP} $$ ```lisp (define DIV_LOOP (Z G_DIV_LOOP)) ``` `DIV_LOOP` 现在是一个柯里化的函数，它接受 `current_m`、`original_n` 和 `current_q`，并递归地计算直到 `current_m < original_n`。 #### 定义主除法函数 `DIV` 主除法函数 `DIV` 将接受两个参数：被除数 `m` 和除数 `n`。它会调用 `DIV_LOOP`，并将初始商设为 `ZERO`。 $$ \text{DIV} := \lambda m . \lambda n . (\text{DIV\_LOOP} \ m \ n \ \text{ZERO}) $$ 在 Scheme 中： ```lisp (define DIV (lambda (m) (lambda (n) (DIV_LOOP m n ZERO)))) ``` **注意：** 此定义假设除数 `n` 不为 `ZERO`。如果 `n` 是 `ZERO` (且 `m` 非 `ZERO`)，` (IS_LT? current_m ZERO)` 永远为假，而 `(SUB current_m ZERO)` 结果仍是 `current_m`，这将导致无限递归（不终止）。 #### 示例 让我们尝试计算 `(DIV SIX TWO)`（假设 `SIX` 是丘奇数 6，`TWO` 是丘奇数 2）： 1. `(DIV_LOOP SIX TWO ZERO)` * `IS_LT? SIX TWO` 为 `FALSE`。 * 递归调用 `(DIV_LOOP (SUB SIX TWO) TWO (S ZERO))` 即 `(DIV_LOOP FOUR TWO ONE)`。 2. `(DIV_LOOP FOUR TWO ONE)` * `IS_LT? FOUR TWO` 为 `FALSE`。 * 递归调用 `(DIV_LOOP (SUB FOUR TWO) TWO (S ONE))` 即 `(DIV_LOOP TWO TWO TWO)`。 3. `(DIV_LOOP TWO TWO TWO)` * `IS_LT? TWO TWO` 为 `FALSE` (因为 `TWO` 不小于 `TWO`)。 * 递归调用 `(DIV_LOOP (SUB TWO TWO) TWO (S TWO))` 即 `(DIV_LOOP ZERO TWO THREE)`。 4. `(DIV_LOOP ZERO TWO THREE)` * `IS_LT? ZERO TWO` 为 `TRUE`。 * 返回当前的商 `THREE`。 因此，`(DIV SIX TWO)` 的结果是 `THREE`，这符合预期。 同样，`(DIV SEVEN THREE)` 会返回 `TWO`。 #### 获取余数 (Remainder) (可选扩展) 上面的 `DIV` 函数只返回商。如果我们也想得到余数，该怎么办呢？ 余数其实就是在递归的**基本情况**下（即当 `current_m < original_n` 时）的 `current_m` 的值。 我们可以修改 `G_DIV_LOOP`，使其返回一个包含商和余数的**丘奇对 `(CONS quotient remainder)`**。 $$ \begin{aligned} \text{G\_DIV\_REM\_LOOP} := \lambda \text{self\_div\_loop} . \lambda \text{current\_m} . \lambda \text{original\_n} . \lambda \text{current\_q} . \\ \quad (\text{IS\_LT?} \ \text{current\_m} \ \text{original\_n}) \\ \quad \quad (\text{CONS} \ \text{current\_q} \ \text{current\_m}) \\ \quad \quad (\text{self\_div\_loop} \ (\text{SUB} \ \text{current\_m} \ \text{original\_n}) \ \text{original\_n} \ (\text{S} \ \text{current\_q})) \end{aligned} $$ ```lisp (define G_DIV_REM_LOOP (lambda (self_div_loop) (lambda (current_m) (lambda (original_n) (lambda (current_q) ((IS_LT? current_m original_n) (CONS current_q current_m) ; 返回 (商, 余数) (self_div_loop (SUB current_m original_n) original_n (S current_q)))))))) (define DIV_REM_LOOP (Z G_DIV_REM_LOOP)) (define DIV_AND_REMAINDER (lambda (m) (lambda (n) (DIV_REM_LOOP m n ZERO)))) ``` 然后，我们可以定义分别获取商和余数的函数： $$ \text{QUOTIENT} := \lambda m . \lambda n . \text{CAR} \ (\text{DIV\_AND\_REMAINDER} \ m \ n) $$ $$ \text{REMAINDER} := \lambda m . \lambda n . \text{CDR} \ (\text{DIV\_AND\_REMAINDER} \ m \ n) $$ ```lisp (define QUOTIENT (lambda (m) (lambda (n) (CAR (DIV_AND_REMAINDER m n))))) (define REMAINDER (lambda (m) (lambda (n) (CDR (DIV_AND_REMAINDER m n))))) ``` 例如，`(DIV_AND_REMAINDER SEVEN THREE)` 会返回一个序对，其中 `CAR` 是 `TWO` (商)，`CDR` 是 `ONE` (余数)。 通过这种方式，我们利用递归和之前构建的算术及逻辑原语，成功地扩展了我们的 $\lambda$ 演算计算体系，使其包含了基本的除法运算。这进一步展示了该计算模型的图灵完备性。 ## 结语 在上文中，我们已经成功地用 λ 演算构建了基本的计算逻辑、自然数算术以及强大的递归机制。这为我们打开了通往更广阔计算世界的大门。 在实际的编程中，除了原始的数据类型和运算，我们还需要各种**数据结构**来有效地组织和管理信息，例如链表、栈、队列、树、图、哈希表等等。没有这些，许多复杂的算法都将无从谈起。 利用我们已经掌握的丘奇对 (可以看作是构造其他数据结构的基础单元) 和递归思想，我们完全有能力在纯 λ 演算的框架内逐步构建出这些复杂的数据结构。 例如，**链表 (Linked List)** 作为最基础也最常用的数据结构之一，它与 λ 演算的递归特性天然契合。我们可以设想用嵌套的丘奇对来表示链表节点，其中每个节点包含一个数据元素和一个指向下一个节点的“指针”（即另一个链表或代表列表末尾的特殊值）。 ``` (define MY-NIL (lambda (f) (lambda (x) x))) ; 例如，用 ZERO 或一个特定的选择函数代表空列表 (define MY-CONS CONS) ; 丘奇对就是我们的 cons (define MY-CAR CAR) (define MY-CDR CDR) ; 一个包含 1, 2, 3 的列表可以表示为： ; (MY-CONS ONE (MY-CONS TWO (MY-CONS THREE MY-NIL))) ``` 对这些数据结构的操作（如插入、删除、查找、遍历）也都可以通过定义相应的 λ 函数来实现，这些函数通常会利用递归来处理链表的递归定义。 由于篇幅和精力的限制，本文不再详细展开这些数据结构的具体实现。但我们强烈鼓励充满好奇心的读者，以本文介绍的原理和方法为基础，亲自动手尝试去构建它们。这将会是一段极具启发性和挑战性的旅程，能让你更深刻地理解计算的构造性和 λ 演算的强大威力。 同样，对于数系的扩展，例如从自然数到整数（如何表示负数？）、再到有理数（如何表示分数并进行运算？），甚至是实数的某些计算特性，也都是值得探索的领域。 希望本文能为你打开一扇窗，让你窥见计算世界最纯粹、最本源的构造之美。