The Nerve Blog Learning

By Matthew Prast 08 Apr 2025 — 19 min read

从零开始构建 Y Combinator，第一部分

我的一个教学上的痛点是，一些技术概念仅仅以完全开发完成的状态被列出，而缺乏足够的动机、推导或历史背景。我认为这就像出版一本充满精美蛋糕图片的食谱，却没有配方。 我推出 “从零开始构建 ” 系列的目标不仅是描述 what，还有 how 和 why，希望这能带来更丰富、更持久的理解。

著名的 Y combinator

这篇文章是关于 Y combinator 的。不是 Y Combinator 这个加速器，而是以它命名的数学结构 - the Y combinator。 Y combinator 看起来像这样： Y=λf.(λx.f(xx))(λx.f(xx))

面对这个定义，你可能会问自己：

  1. 它为什么长这样？
  2. 它是用来做什么的？
  3. 为什么人们还在谈论它？
  4. (Combinator 到底是什么玩意？)

对所有这些问题的一句话回答是：“Y combinator 在不允许显式自引用的函数式语言中实现递归”，但值得更深入地探讨。在我看来，从根本上理解 Y combinator 是 什么的最简单方法是关注它如何产生不动点。理解它为什么 重要 的最简单方法是关注它如何用于实现递归。在第一部分中，我们将讨论前者（回答 1. 和 2. 的一半），在第二部分中，我们将讨论后者（回答 3. 和 2. 的另一半）。 （我们将在本文后面回答奖励问题 4！） Y combinator 由 Haskell Curry 设计，他是一位有影响力的逻辑学家，他以将自己的名字借给 一种编程技术 和 一种编程语言 而独树一帜。它也被称为 “不动点 Combinator”（原因我们稍后讨论）和 “悖论 Combinator”（原因我们将在本文的后半部分探讨）。

Lambda Calculus (λ演算)

这篇文章假定你至少熟悉 Lambda Calculus (λ演算)——你不必是专家，但如果它对你来说是全新的，你可能会难以理解正在发生的事情。This 是一个很好的介绍（本文仅使用第 1 节中的材料）。

在阅读本文之前，你应该了解关于 Lambda Calculus 的两件事：

  1. Lambda Calculus 中的 一切 都是一个函数（我也会将这些函数称为 “项”）。当你在 Lambda Calculus 中 “运行” 程序时，你基本上是在一遍又一遍地将函数插入到其他函数中，直到你不能再做为止。这似乎严重限制了 Lambda Calculus 的表达能力，但请考虑到，我们可以通过使用适当的函数来表示不同的数据类型和运算符，从而在 Lambda Calculus 中对它们进行编码（链接的论文展示了如何在 Lambda Calculus 中表示布尔值和自然数，并演示了如何进行算术和一些布尔代数）。Lambda Calculus 是图灵完备的，因此使用这种类型的编码，你可以复制用任何语言编写的任何程序的行为。
  2. 除了变量名之外，Lambda Calculus 中没有名称。你不能将名称分配给函数，也不能按名称调用任何函数。为了便于阅读，我有时会作弊并给函数一个名称，只是为了更容易解释。例如，我可能会写

id=λx.x

然后稍后：

myCoolTerm=λx.xid(x)

请记住，从技术上讲，在真正的 Lambda Calculus 中，你不能写 name=term 或 name(argument)；你必须把一切都写出来。例如，myCoolTerm 只能合法地写成：

λx.x((λx.x)(x))

Y - 不动点 Combinator

函数 f 的不动点 (或 fixpoint) 是当你将 f 应用于它时不会改变的点。换句话说，x 是 f 的不动点，当且仅当

f(x)=x

Y 是一个 不动点 combinator (注意我没有说 the 不动点 combinator——Y combinator 是最古老、最简单的不动点 combinator 之一，但还有很多其他的！)。不动点 combinator 接受一个（单参数）函数并返回该函数的某个不动点（有些函数有多个不动点——例如，考虑一下，幂等函数返回的每个值都是不动点！如果函数 没有 不动点，则 Y(f) 不会终止）。因此我们知道 Y 必须满足：

f(Y(f))=Y(f)

但也意味着：

Y(f)=f(Y(f))

从计算的角度来看，第二个等式表示 Y 的作用是接受一个函数并 将自身嵌套 在对该函数的调用中。

现在是记住 Lambda Calculus 中的一切都是函数的好时机。因此，Y 是一个函数，它接受另一个函数 f 并返回一个不动点，它本身也是一个函数。

乍一看，Y 看起来很容易实现。我们不能简单地说

Y=λf.f(Yf)

吗？好吧，如果我们使用另一种语言，我们可以，但在 Lambda Calculus 中，我们不能按名称引用 Y。请记住，从技术上讲，函数在 Lambda Calculus 中根本没有名称；正式演算只使用 Lambda 和变量。因此，如果我们希望 Y 成为一个有效的术语，我们必须把一切都写出来。让我们用它的显式定义替换函数体中的 Y 出现：

Y=λf.f(Yf)

Y=λf.f(λf.f(Yf)f)

嗯.... 让我们再试一次：

Y=λf.f(λf.f(λf.f(Yf)f)f)

好吧，很明显我们不能显式地写出 Y：这个过程将永远继续下去，并且 Lambda Calculus 中的项不允许是无限大的。

由于我们无法让 Y 在它自己的定义中引用它自己，我们需要它在某种程度上是 自我复制的。Y(f) 必须在运行时生成它自己的副本，然后将该副本包装在另一个 f 中。但现在我们遇到了一个讨厌的先有鸡还是先有蛋的问题：如果不了解 Y(f) 的结构，就不清楚如何复制它，并且在我们弄清楚如何进行复制之前，我们不会知道它的结构！

让我们暂时忘记外部 f，并考虑如何制作最简单的自复制项（称之为 R）。首先要注意的是，我们想要一些可以 reduce 的东西——一个只是坐在那里的 R 总是平凡地等于它自己，但这对我们来说既不有趣也没有用。我们想要一个会改变的项，但以某种方式最终回到了它开始的地方。为了取得任何进展，我们需要对 R 的结构提出 一些 主张（即使最终是错误的）。让我们从最简单的可以 reduce 的结构开始——单个函数应用：

R=MN

让我们看看是否能让它工作。我们需要弄清楚 M 和 N 应该是什么。我们试图通过将 M 应用于 N 来复制 R，因此如果 R 是单个函数应用，则 M 的内部结构可能也应该是单个应用。换句话说，M 应该看起来像这样：

M=λx.((f1x)(f2x))

其中 f1 和 f2 是...一些东西。它们应该是什么？N 应该是什么呢？

我们准备好尝试解决这个问题了。此时，你应该尝试花一些时间 Messing Around，看看你能想出什么；尝试使用不同的 f1、f2 和 N 项，看看结果如何。请记住，Lambda Calculus 中的 一切 都是一个函数——没有其他类型的值！当你弄清楚它（或者你只是准备好继续前进）时，继续阅读。

这个问题的关键是注意到如果我们希望 MN reduce 为自身，则 f1x 必须 等于 M。我们不能将 f1 本身设置为 M；我们将最终得到我们之前看到的无限嵌套，并且我们将永远无法写下 M。我们的另一个选择是将 M 作为参数传入，即 x=M，这意味着 N=M，这意味着 f1 和 f2 只是恒等函数（这意味着我们可以完全省略它们）。将所有这些放在一起，你会得到：

M=N=λx.(xx)

R=λx.(xx)λx.(xx)

这可行！R 只需要一步即可复制（如果你愿意，可以在脑海中完成 - 只需在左侧替换 x 即可）。

我们重新发现了 Omega combinator，即 Ω，它是可以像这样自我复制的最简单的项之一（你会注意到它会永远 reduce 下去！）

回顾我们如何推导出 Omega combinator，我们可以看到自我复制的诀窍是什么。我们通过 Ω 使事情正常工作，因为我们以 参数 的形式传递了 M 的副本，而不是直接将其嵌套在它自己的定义中。这可能只是语义，但它允许我们在 reduce 期间逐步进行嵌套，而不必一次写下所有内容——这意味着我们不会最终得到无限大的项！

是时候把各个部分组合在一起了。让我们调整我们的 Omega combinator，将其变成 Y combinator。

上次，我们基于我们对 Ω 所做的结构假设来构造 M。Ω 和 Yf 之间唯一的不同是 Ω 变成 Ω，我们希望 Y(f) 变成 f(Y(f))。因此，我们将更新 M 的结构 - 它将不是单个函数应用程序，而是 包装在 f() 中的 单个函数应用程序：

M=λx.f(xx)

像以前一样设置 M=N，我们得到：

Y(f)=MN=λx.f(xx)λx.f(xx)

Y=λf.(λx.f(xx))(λx.f(xx))

这可行吗？我们来看看：

Y(f)=λx.f(xx)λx.f(xx)

Y(f)=f(λx.f(xx)λx.f(xx))

是的！它有效。在单个替换步骤中，Y(f) 将自身嵌套在 f 内部。我们在本文开头看到的那个奇怪的结构确实是一个不动点 combinator！

Y - 悖论 Combinator

到目前为止，我们已经了解了 Y combinator 的作用，并且我们 有点 了解了它为什么有用，但也许不是以一种非常令人信服的方式。因此，Y combinator 在不按名称引用自身的情况下进行自我复制......我们为什么要关心？通过禁止自引用或以如此笨拙的风格编写程序，我们得到了什么？这难道不是有点深奥吗（顺便说一句，Y combinator 到底是如何“自相矛盾的”？）我可以给你一个更令人满意的答案，但你必须允许我简要地绕道进入数学史。

Lambda Calculus (λ演算)创建于 20 世纪初，当时数学正围绕 形式主义 的思想重新定位。简而言之，形式主义是一种哲学，它认为数学 “只是” 根据定义明确的规则操纵符号的行为。这可能看起来是同义反复，但事实并非如此 - 它代表着人们对符号和规则本身的关注发生了重大转变，并远离了数学 “关于” 的事物（数字、形状、函数等）。

这种新的形式主义观点导致了 形式系统 的激增。在其最基本的形式中，形式系统是一组可以排列成公式的符号，一组用于操纵符号以生成新公式的规则，以及一组 公理 - 假定为真的公式。你可能已经熟悉了几个形式系统，例如谓词演算、集合论或皮亚诺算术。

形式系统在 20 世纪的数学中占据了突出地位，并且今天仍在创建新的形式系统。构造良好的形式系统可以服务于各种目的。例如：

（有些系统被称为形式系统，有些系统被称为 逻辑 形式系统（或简称形式逻辑），但区分这些系统的标准是模糊的，并且是一些数学家争论的焦点。它们与本文的目的也不相关，因此现在我们将这两个术语视为等效的。）

所有这些都是为了说明 Haskell Curry（可能！）在第一次提出 Lambda Calculus (λ演算)时，将其视为一个形式系统，而不是一种编程语言。

在我们继续之前，还有一些关于 Lambda Calculus 的重要知识需要了解：

  1. 它被创建为 小 的。它有变量、抽象、应用和两条 reduce 规则。就是 这样 - 这就是完整的语言。这种最小化服务于一种审美目标（捕捉计算的 “本质”），但也使得 Lambda Calculus 易于推理（例如，Church-Rosser 定理，它说无论你以何种顺序 reduce 表达式中的项，最终都会得到相同的值。你不会想尝试证明关于更复杂语言的这个事实。）
  2. 它最初由 Church 在 1930 年描述，比 Alan Turing（当时 Church 的博士生）发表关于图灵机的工作早了六年多。当时，人们对计算的本质进行了广泛而持续的研究，但没有物理计算机可言，更不用说编程语言了。与 Church 的系统最接近的类似物是形式逻辑系统 - 毫无疑问，有人想象或假设 Lambda Calculus 本身将被直接用于向计算机发出指令。
  3. 20 世纪计算机科学的一个重要主题是，计算和形式逻辑是同一枚硬币的两面，在一些重要方面（我们稍后会更多地了解这一点。）

也就是说 - Y combinator 从何而来？嗯，Curry 需要它才能在 Lambda Calculus (λ演算)中创建一个 悖论。

在形式逻辑的术语中，悖论是一个没有违反任何规则的证明，但仍然以矛盾结束（即，它同时证明了一个命题及其对立面。）你可能熟悉著名的 Russel 悖论；非正式的版本是这样的：“有一个理发师，他为所有不为自己刮胡子的人刮胡子，并且只为这些人刮胡子。这个理发师会为自己刮胡子吗？”一方面，理发师 必须 为自己刮胡子 - 如果他不刮胡子，他就会符合他为之刮胡子的人的标准，因此他最终还是会为自己刮胡子。另一方面，理发师 不能 为自己刮胡子 - 如果他这样做了，他将不再符合他自己的标准，并且无法将自己作为客户。

证明矛盾通常是逻辑系统的心脏。如果你可以证明一个命题及其对立面都是真的，你通常可以找到一种方法来证明 任何 语句 - 并且一个可以证明任何东西的系统不是很有用（逻辑学家将这种系统称为 微不足道。）你应该只能证明那些实际上是真的东西！

悖论是探测形式系统缺陷和局限性的重要工具。例如，Russel 悖论的发现导致了许多增强的逻辑系统，其中包含各种机制来确保悖论不再发生（有趣的事实：在这些努力中，类型理论的第一个化身！）特别是，由于 Russel 悖论的核心是否定（理发师为 不 为自己刮胡子的人刮胡子），许多逻辑学家希望他们可以通过构建具有修改过的否定概念或根本没有否定概念的系统来避免它。

Curry 的悖论粉碎了这些希望。它是 Russel 悖论的一个变体，它不依赖于否定。Curry 构造了他的悖论，以证明许多不同逻辑的微不足道性 - 其中包括著名的 Lambda Calculus (λ演算)和 Moses Schönfinkel 的 组合逻辑。

组合逻辑是由 Moses Schönfinkel 在 1924 年的一篇论文中发明的（这是他一生中发表的两篇论文之一。）Schönfinkel 的目标是创建一种不包含变量概念的逻辑形式。相反，它使用一组固定的 combinator - 它们是接受其他 combinator 并以各种方式将它们应用于彼此的函数。正如 Lambda Calculus (λ演算)中的一切都是函数一样，组合逻辑中的表达式 仅 由 combinator 组成 - 它一路都是 combinator。当 Haskell Curry 在 1927 年开始研究它时，组合逻辑得到了提升，但 Lambda Calculus (λ演算)总是更受欢迎。直到 60 年代人们重新燃起兴趣，Curry 基本上独自扛起了火炬，独自或与他的学生一起完成了这项工作的大部分。Curry 创建了 Y combinator 以在他的悖论中构造组合逻辑，这就是为什么它被称为 Y combinator 以及它以单个字母命名的原因。在组合逻辑中，Y combinator 的实现方式如下：Y=SSI(S(S(KS)K)(K(SII)))

无论如何，足够的序言 - 让我们研究一下 Curry 的悖论的全部辉煌。

看看这个：

“如果这句话 - 就是我现在说的这句话 - 是真的，那么所有的鸟都是政府间谍。”

事实证明，仅使用这句话，你就可以证明所有的鸟都是政府间谍这一事实 - 或者你希望证明的任何其他事情，包括像 “1 = 1 并且 1 = 0” 这样的矛盾。这个悖论不像 Russel 悖论那么直观，因此我们可能需要更正式地看待它，然后它才能开始变得有意义。

考虑以下语句：

S：如果语句 S 为真，则命题 P 为真。

如前所述，这里的关键是 thay S=>P 通过它自己的前提 S 引用了自身。正如我们之前看到的，我们需要 Y combinator 才能在不允许显式自引用的系统中实现这一点。

Lambda Calculus (λ演算) 中的 Curry 悖论

在本节中，我们将把到目前为止学到的一切结合在一起，以在 Lambda Calculus (λ演算)中实现 Curry 的悖论。这对你来说似乎是荒谬的 - 实现 一个悖论是什么意思？如何将逻辑悖论放入计算系统？

在上一节中，我们了解了 形式系统 的概念，我给出了一些例子。其中一些是逻辑系统，你可以在其中操纵符号以进行逻辑推导，另一些是计算系统，你可以在其中操纵符号以执行计算并得出结果。使用计算系统来证明事物或进行逻辑推导似乎没有任何意义 - 它不是为此而构建的，对吗？

Curry-Howard Correspondence 是 Haskell Curry 和逻辑学家 William Alvin Howard（以及其他一些数学家，在不同时间）以慢动作实现的结果，即这两种 “类型” 的系统实际上，从深刻而重要的意义上说，是相互交织的！换句话说，当我们编写程序时，我们 正在 编写证明 - 它们只是 建设性的 证明。

“建设性证明” 一词得名于 Constructivism (构造主义)，与形式主义一样，Constructivism (构造主义)是一种在 20 世纪初受到一些争论的数学哲学。关于 Constructivism (构造主义)有很多话要说，但与我们相关的是这样一种信念，即证明某一类数学对象存在的唯一方法是构造一个例子并将其呈现出来。特别是，这意味着 Constructivism (构造主义)者拒绝通过矛盾证明，这是一种在 “经典” 数学中使用的技术。通过矛盾证明说 “这种类型的对象必须存在，因为如果它不存在，就会导致矛盾。” 你会注意到该对象本身从未被描述过，即使它已被证明存在；即，我们知道它 “存在”，但我们不知道它是什么样子！对于 Constructivism (构造主义)者来说，这是不允许的。通过矛盾证明是一种重要且广泛使用的技术，并且禁止它使得 - 坦率地说 - 进行数学运算非常困难（David Hilbert 将其比作 “禁止拳击手使用他的拳头。”）出于这个原因，Constructivism (构造主义)从未像形式主义那样完全赶上主流数学家。

为了理解程序代表建设性证明的含义，请考虑值 “hello”。这是一个 String 类型的值，这意味着它是 String 的一个例子，这意味着它是 至少一个 String 类型的值存在的建设性证明。

现在考虑以下（伪代码）函数：

firstChar(myString:String)=myString[0]

它接受一个 String 并返回一个 Char。换句话说，它接受一个 String 存在的建设性证明并返回一个 Char 存在的建设性证明。换句话说，这是一个建设性证明，它说“如果至少存在一个 String 类型的值，则至少存在一个 Char 类型的值”.

这也扩展到高阶函数。例如，这个函数：

firstDigit(firstChar:(String)=>Char,toString:(Number)=>String,num:Number)=firstChar(toString(num))

是一个建设性证明，它说“如果 String 的存在意味着 Char 的存在，并且 Number 的存在意味着 String 的存在，并且至少存在一个 Number，那么至少存在一个 Char”。

对于类型化语言，Curry-Howard Correspondence 意味着类型可以被视为命题，而特定类型的项可以被视为该类型表示的命题的证明。这通常被称为 “命题即类型” 的视角。

（许多商业软件所体现的 “证明” 通常不是很引人注目 - 例如 “如果我们有一个数字列表存在的证明，我们可以证明一个字符串列表存在”，等等。人们可以并且确实使用程序编写完整的、数学上有用的证明，但这些程序通常看起来与专业软件开发人员编写的程序非常不同。）

Curry-Howard Correspondence 的完整陈述和背景比这更技术性，但这是一般的想法，足以让我们开始工作。

现在让我们考虑另一个术语 - 同时为奇数和偶数的数字。我们将这种数字称为 Evil 数字，即我们的数字是 Evil 类型的项。这个项作为至少存在一个 Evil 数字的建设性证明（当然，我们知道这是不正确的！）我们将这个项称为 evil - 并且由于它证明了一些不真实的东西，因此无法直接构造它。但是有没有办法表达它呢？ （剧透：在朴素的 Lambda Calculus (λ演算)中，有一种方法）

我们无法直接创建 evil，但如果该函数有某种方法从其参数中获取 evil，则可以从该函数返回它。直接接受 evil 作为参数没有意义（调用者将如何构造它？）但我们可以接受一个 函数 来返回它。但是 那个 函数应该接受什么？嗯…… 另一个 也返回 evil 的函数！朴素的 Lambda Calculus (λ演算)没有类型，但如果有，我们的新函数的类型（非正式地）将如下所示：

createEvil:createEvil→Evil

要从 createEvil 获取 evil，我们为它提供一个创建 evil 的函数 - 我们唯一的选择是 createEvil 本身。这个函数的非 Lambda Calculus (λ演算) 版本看起来像这样：

createEvil(f)=f(f)

我们这样调用它：

evil=createEvil(createEvil)

（请注意，我们所做的是 表达 一个代表 evil 的术语。如果我们真的尝试运行这个函数，它将永远运行下去。这并不意外 - 悖论和非终止是同一事物的两个方面 “Things are breaking” 现象。）

让我们停下来考虑一下。如果你稍微眯起眼睛，你可以看到这个奇怪的函数类似于 Curry 的悖论。考虑：

这应该让你感到熟悉 - 这正是我们在之前的例子中造成如此多麻烦的结构！让我们完成悖论的其余部分，看看它如何与 createEvil 对齐

逻辑世界 | 程序世界 ---|--- 考虑 S=(S⇒evil) | 考虑 createEvil 首先，我们必须证明 S⇒evil | 首先，我们必须实现 createEvil 假设 S 为真，作为假设。由于 S 为真，因此 S⇒evil 为真，因为 S 直接声明 S⇒evil | createEvil 将 createEvil 作为参数，因此当我们实现 createEvil 时，我们可以假设我们可以使用 createEvil 的实例 - 即，我们对 createEvil⇒evil 有建设性证明 由于我们假设 S 为真并表明 S⇒evil 为真，因此如果 S 为真，则证明 evil 为真 - 即，我们已证明 S⇒evil | 由于我们可以使用 createEvil 的实例，我们可以简单地将其传递给自身以生成 evil 的实例。我们已经实现了 createEvil 并完成了我们对 createEvil⇒evil 的建设性证明 我们已经证明了 S⇒evil，这也意味着我们已经证明了 S。通过组合 S⇒evil 和 S，我们可以推断出 evil 也为真。悖论！！ | createEvil 是 createEvil 和 createEvil⇒evil 的建设性证明。现在我们已经实现了 createEvil，我们可以简单地编写 createEvil(createEvil) 以（理论上）生成不可构造的 evil 的实例。悖论！！

希望现在很清楚 createEvil 是 Curry 悖论的计算体现。我们在这里利用自引用来生成一个 “证明” evil 存在的函数（它也可以证明任何其他值存在，就像 “常规” 版本的 Curry 悖论可以证明任何 P 一样。）然而，由于这个函数永远不会终止，运行它会破坏你的程序，就像证明一个矛盾会破坏你的逻辑系统一样。

现在是最后一击 - 让我们用 Lambda Calculus (λ演算)重写 createEvil。请记住，我们不能直接做 createEvil=createEvil(createEvil)，因为 Lambda Calculus (λ演算)从技术上不允许命名函数。我们需要某种方式在运行时将 createEvil 传递给自身。这就是 Y combinator（最终）进入画面的地方。回想一下：

Y(f)=f(Y(f))

如果我们让 f=λx.(xx)，我们得到：

Y(f)=f(Y(f))

Y(f)=(λx.(xx))Y(f)

Y(f)=Y(f)Y(f)

我们可以看到，如果我们让 createEvil=Yλx.(xx)，我们最终得到 createEvil=createEvilcreateEvil，就像我们想要的那样。因此，createEvil 的最终形式，完全用 Lambda Calculus (λ演算)编写，是：

(λf.(λx.f(xx))(λx.f(xx)))(λx.(xx))

我们已经在 Lambda Calculus (λ演算)中实现了 Curry 悖论是什么意思？这意味着（朴素的）Lambda Calculus (λ演算)作为一个形式系统存在一些非常显着的问题。我们该如何处理？通过添加类型，从而将朴素的 Lambda Calculus (λ演算)升级为简单类型 Lambda Calculus (λ演算)。我们将在第二部分中更多地介绍这个主题！ The Nerve Blog Powered by Ghost Subscribe