通往哥德尔机的实现：关于自省系统的一课

作者：Bas R. Steunebrink and Jürgen Schmidhuber

来自：Pei Wang (Ed.) & Ben Goertzel (Ed.), Theoretical Foundations of Artificial General Intelligence, 第十章

摘要

近期，人们对自省系统 (self-reflective system) 的兴趣在人工广义智能 (Artificial General Intelligence; AGI) 的语境下复苏了。一个 AGI 系统应该有足够的智能来对其自身的代码进行推理，并且在它认为合适的地方修改代码，从而改进最初由人类程序员写的代码。一个相关的例子是哥德尔机 (Gödel Machine)，它利用一个证明搜索器 (proof searcher)---平行于它通常的解题任务---来寻找对自身的重写，并且它自己可以证明这种重写是有利的。显然，要在 AGI 系统中实现这种层次的自省会有许多技术挑战，但这些挑战中有许多并没有被广泛了解或领会。本文中我们回到自省的理论基础，并检视真的要实现一个自省 AGI 系统 (以及哥德尔机) 时面临的问题 (通常很微妙)。

引言

一个人工广义智能 (AGI) 系统很可能会需要自省的能力；也就是说，在系统运行的过程中检视和推断自身的代码并对其进行综合修改。这是因为人类程序员不像有能力写出完全预先决定好的、不需要调节的程序来满足广义智能的要求。当然，自我修改可以有多种形式，从简单地通过机器学习技术调节几个参数，到对自身正在运行的代码有完全的读写权限的系统。本文中我们考虑迈向第二种极端---方法是构建一个编程语言以及一个允许对内部构造以安全和容易理解的方式进行完全省察和操纵的解释器---在技术上意味着什么。

能够省察和操纵自身代码不新鲜；事实上，在早期计算机内存很有限且昂贵的时候这是标准做法。但是，近些时间，不再鼓励使用自我修改的程序了，因为人类程序员很难掌控自我修改的所有后果 (特别是在大的时间跨度下)，使得这么做倾向于引入错误。结果就是，很多现代 (高级) 语言严格限制对内部构造 (比如调用栈) 的存取，或者干脆禁止。但是有两个原因让我们不应该永远禁止自我修改的程序。第一，仍然有可能发明一种允许写出安全且容易理解的自我修改程序的语言。第二，如今自动推理系统越来越成熟，考察让机器——而不是人类程序员——基于对其自身代码的自动推理去做所有自我修改，是有价值的。

做为上面第二个动机的实体化的一个例子，我们考虑哥德尔机，这样我们对自省的技术讨论会有的放矢一些。完全的自指哥德尔机是一个在某种意义上理论最优的通用人工智能。它可以与某些一开始未知、部分可观测的环境发生相互作用，来解决任何用户定义的计算任务，方法是让累积的未来效用的期望最大化。初始的算法不是硬植入的；它可以完全重写自身而没有除了可计算性之外任何实质上的限制，前提是初始算法要包含一个证明搜索器，这个搜索器能先证明重写是有用的，依据是考虑了有限计算资源的形式化效用函数。可以证明这种途径的自我修改对于初始效用函数 (比如强化学习的奖励函数) 来说是全局最优的，与此对比的是哥德尔关于可证明性的周知的基本限制。

下一节我们给出哥德尔机概念的描述，这提供了之后讨论自省系统的语境。上面已经指出，哥德尔机的实现要求系统能够对当前正在运行的程序作出任意修改。但这是什么意思？什么是一个修改，修改有多大的任意性，以及一个运行的程序长什么样？我们会看到这些都不是平凡问题，涉及到一些微妙而重要的问题。本文提供这些问题的综述以及克服办法。

哥德尔机的概念

可以把哥德尔机堪称由两部分组成的程序。第一部分我们称为求解器，可以是任何解决问题的程序。为了讲述的清晰，我们假定求解器是个与外部环境交互的强化学习 (RL) 程序。这让我们方便决定效用 (使用 RL 的奖励函数)，这在后面是个重要话题。但一般来说，对求解器没有限制。第二部分我们称为搜索器，是一个以可证明的最优方式改进整个哥德尔机的程序。搜索器是本节的主要话题。

哥德尔机的搜索器有一个计算这机器累积未来效用的期望值的函数。这个效用函数被用来构造目标定理；也就是说，哥德尔机会进行自我修改，仅当可证明这么做有用时。下面会看到，目标定理准确指定了何时重写是有用的。

基本来说，决定累积未来效用期望值的函数 (记为 \(u\)) 是所有未来时间点的奖励之和。这里时间点不是指时钟滴答，而是对基本指令的执行。事实上，每个指令要花时间来执行，所以如果我们能找到办法来明确表示未来将要执行的指令，我们自动有了开向未来时间的窗口。对于这种表示，一个明显的选择是延续 (continuation)，一个在基于 \(\lambda\)-运算的程序语言里被研究得很好的概念。直观地讲，一个延续可以被看成调用栈的反面；不是给出“我们来自哪里”，一个延续显式给出的是“下面将发生什么”。注意到除了最简单的情况之外，一个延续只会被部分展开。比如，假设当前的延续是 { A(); if B() then C() else D() } ; 这个延续指出下一件要做的事情是展开 A 并执行其内容，然后执行条件语句，这意味着 B 会先被展开，然后根据其结果，C 或 D 之一被展开。在 B 执行之前是不清楚 C 或 D 要不要执行的；所以在知道 B 的结果之前展开它们没有意义。

下面我们用一致的下标来表示一个元素在何处被编码。\(u\) 是二元函数，\(u_{\bar{s}}(s, c)\)，代表的是在 \(s\) 状态下运行延续 \(c\) 的累计未来效用期望。这里 \(\bar{s}\) 是评估态 (evaluating state; \(u\) 编码的地方)，而 \(s\) 是被评估的态 (evaluated state)。考虑 \(u\) 的具体定义就清楚为什么作出这种区分了 \begin{equation} \begin{split} u_{\bar{s}}(s,c) &= \mathbb{E}_{\mu_s,M_s}\left[u'\right],\ \text{其中} \\ u'(env) &= r_{\bar{s}}(s, env) + \mathbb{E}_{\kappa_c,K_c}\left[u_{\bar{s}} | env\right] \end{split} \label{eq_usbar} \end{equation} 如下标标出的，外部环境的表示 \(M\) 在 \(s\) 内编码，因为哥德尔机的所有知识必须被 \(s\) 编码。为了清楚，让 \(M\) 是一个位串组成的集合，每个组成哥德尔机容许的可能环境的一个表示。\(\mu\) 是从 \(M\) 到概率的映射，也在 \(s\) 内编码。\(c\) 不止是编码将来会被执行的指令的 (部分展开的) 表示，而且编码了集合 \(K\)，\(K\) 是状态-延续对的集合，代表执行 \(c\) 的第一个指令后所有可能的下一步的状态和延续； \(c\) 还编码了从 \(K\) 到概率的映射 \(\kappa\)。所以 \(\mu\) 和 \(\kappa\) 分别是样本空间 \(M\) 和 \(K\) 上的 (离散) 概率分布。\(r_{\bar{s}}(s, env)\) 决定在环境 \(env\) 里状态 \(s\) 是否是有利的。比如，在求解器 (是 \(s\) 的一部分) 是个 RL 程序的情况，\(r_{\bar{s}}(s, env)\) 仅当在 \(s\) 代表刚刚执行一个接收输入的指令后的状态时才不是 0。最后，\(\mathbb{E}_{\kappa_c,K_c}\left[u_{\bar{s}} | env\right]\) 对 \(u\) 递归，相应的态和延续来自执行延续 \(c\) 里的下一条指令。

关键的一点是要注意到 \(u\) 和 \(r\) 是来自评估态 \(\bar{s}\)，而不是被评估态 \(s\)。后一种做法会破坏哥德尔机的全局最优性，因为那样的话它将能以任何方式 (包括有害的方式) 重写其效用函数。因此，起初的、未被改动的效用函数 \(\bar{s}\) 应该被先用来证明重写是有用的。与此对照，\(\mu\) 和 \(M\) 是来自 \(s\)，因为对于任何有点意思的哥德尔机，\(c\) 会同时限制影响外部环境的指令 (比如输出给行动器)，以及据此更新外部环境 (在 \(s\) 内编码) 的内部模型的指令。类似地，\(\kappa\) 和 \(K\) 取自 \(c\)，因为每次执行指令后延续必定变化，导致 \(\kappa\) 和 \(K\) 的更新。

还要注意到 \(u\) 这个函数是递归的。方程 \eqref{eq_usbar} 中，一个哥德尔机的生命在延续样本 \(K_c\) 为空时中止。在那个情况，\(\mathbb{E}_{\kappa_c,K_c}\left[u_{\bar{s}} | env\right]\) 是零而对 \(u\) 的递归停止。在最常见的情形，指令是决定论性的，比如 \(K_c=\left\{(s',c')\right\}\)。这时 \eqref{eq_usbar} 简化为 \(u_{\bar{s}}(s,c) = \mathbb{E}_{\mu_s,M_s}\left[r_{\bar{s}}(s,\cdot)\right] + u_{\bar{s}}(s',c')\)。于是对于决定论性的状态转换，累积未来效用的期望值约简到对后续状态预期奖励的求和。但是比如在 RL 的设定下，即便那些期望收益一般也都是零，因为多数指令不涉及从环境中接收信息 (而这在 RL 中一般是奖励的来源)。

我们现在可以介绍目标定理 (target theorem) 了；它是基于效用函数 \(u\) 的。让 \(s\) 表示在某个时间 \(t\) 之前的一个预期未来状态。进一步，让 \(c^\ast = \left\{wait\_until(t); switchprog()\right\}\) 表示一直等待直到时间 \(t\) 的延续 (比如，通过不断调用一个基本时钟函数直到返回的时间大于或等于 \(t\))，之后执行 \(switchprog\)，而这个程序会检查并修改 \(s\) 的任何部分。现在 \(u_{\bar{s}}(s,c^\ast)\) 告诉我们在时刻 \(t\) 在 \(s\) 态上执行 \(switchprog\) 的期望累积未来效用是什么。如果这个效用大于不转换 (switch) 的预期累积未来效用，则这个哥德尔机必须在 \(t\) 时刻执行转换。这样，搜索器的目的是要找到一个状态 \(s\)，一个时刻 \(t\)，以及一个不接收自变量 (nullary) 的子程序 \(switchprog\)，使得 \(\mathfrak{tt}_{\bar{s}}(s, t, switchprog)\) 成立，这里： \begin{equation} \mathfrak{tt}_\bar{s}(s, t, switchprog) = \left[ u_\bar{s}(s, \left\{wait\_until_s(t); switchprog()\right\}) {>} u_\bar{s}(s, \left\{scheduler_s()\right\})\right] \end{equation} 这里 \(scheduler\) 是让哥德尔机的求解器和搜索器交织起来的子程序。因此 \(\left\{scheduler_s()\right\}\) 表示从 \(s\) 态出发“照常继续”的延续 (包括搜索新的 \(switchprog\))。注意，由于 \(switchprog\) 可能会重写调度器，它必须在其最后一条指令启动一个新的调度器 (如果有必要)，或者简单地启动旧调度器 (如果没有被改变的话)。

有两种方法可被用来从这个目标定理找到可被证明有用的自我修改：(1) 生成候选 \(switchprog\) (比如，一个执行优化技术 (也被前沿的编译器使用) 的程序)，生成一个转换时间 \(t\)——\(t\) 不早于评估运行 \(switchprog\) 的效用所需要的时间，以及为当前状态 \(s\) 生成一个拷贝 \(\bar{s}\)；然后在 \(s\) 上运行由 \(\mathfrak{tt}\) 指定的两个延续 (这是安全的，因为 \(s\) 相当于一个沙盒)，直到可以确认那个不等式是否成立，或者直到时间超过 \(t\)；如果不等式不成立或者超时，那么生成一个新的 \(switchprog\) 然后重来；否则，把当前状态与 \(s\) 交换，等待直到时间 \(t\) 然后执行 \(switchprog\)。(2) 从一个公理系统出发生成定理 (或者产生可以计算定理的程序)，测试它们与 \(\mathfrak{tt}\) 的等价性。第一种方法可被视为自顶向下证明 \(\mathfrak{tt}\) 的方法，而第二种是从下往上的。混合的方法也是可能的，所以这种对目标定理的描述允许一系列可能的哥德尔机实现。

为了让哥德尔机就算在第一次自我改写之前就是渐进最优的，可以把它初始化为 Hutter 的 Hsearch 算法，一种对所有良好定义问题的非自指但渐进最快的算法，其中使用了硬植入的蛮力证明搜索器并忽略了证明搜索的成本。给定这样的问题，哥德尔机可能会决定把 Hsearch 替换为更快的方法从而减小恒定开销，但就算不能减小，其性能也不会比渐进最优差。

解释了一个需要自省的系统的例子，下面我们继续解释获得自省的技术方面。

自省系统的理论基础

八十年代中期有股自省解释器的风潮，带来了一个著名的词语，“自省塔”。想象一个迷雾缭绕的沼泽，一个矗立着的顶端隐没于灰暗天空的高塔——纯粹的 Rackham 风格！(...) 说起来，谁没有梦想过发明 (或至少可获得) 一种语言，在里面任何东西都可以被重定义，我们的想象可以信马由缰，可以获得完全的编程自由任意玩耍而没有束缚和阻碍？

来自 Queinnec, LISP in small pieces

Queinnec 这样诗意描绘的自省塔是对进行自省 (这里理解为检查和修改自身的正在运行的代码) 时发生的事情的图像化。运行在第 \(n\) 层的程序是运行在第 \(n-1\) 层的求值器的效果。当一个第 \(n\) 层的程序执行一次自省指令时，这意味着它可以访问运行在 \(n-1\) 层的程序的状态。但第 \(n\) 层的程序也能启动求值器，这导致一个程序在 \(n+1\) 层运行。如果一个取值器计算一个正在计算一个...取值器的值，我们得到“矗立着的顶端隐没于灰暗天空的高塔”的图景。如果一个程序正在自省一个正在自省一个正在自省一个...自省程序，我们得到“塔底迷雾缭绕”的图景。如果我们踏上塔的底层会发生什么？在自省塔的原始版本中，没有底层，因为往两个方向都是无限的。当然，现实中这样的无限性必须被放宽，但要点是，问题具体何时何地以及如何浮现，是个极有意思的话题，而这是本节要讲的。

根据 Queinnec，自省式解释器必须允许两件事。第一：

自省式解释器应该支持自我检视，所以它们必须为程序员提供在任何时间提取计算复杂性的方法。通过“计算性上下文”，我们指的是词法环境和延续。

来自 Queinnec, LISP in small pieces

自省式解释器必须提供修改自身的方法 (真的很刺激，毫无疑问)，...，实现解释器的那些函数可以获取被解释的那些函数。

来自 Queinnec, LISP in small pieces

本节我们来看针对自省的这两个要求在技术上意味着什么，以及在何种程度上它们在理论和实践中是可实现的。

\(\lambda\)-运算基础

现在我们来关注计算上下文的表达；也就是，词法环境加延续。为了阐释这些，最明显和研究得最好的方法是 \(\lambda\)-运算，一种很简单的 (理论的) 编程语言。\(\lambda\)-运算里表达式的写法跟通常的数学写法有些不同；比如，函数作用的括号写在外面，即用 \((f\ x)\) 表示 \(f(x)\)。\((f\ x)\) 里的括号是语法的一部分，总是表达函数的作用，不能随便乱用。函数通过 lambda abstraction 构造出来；比如，恒等函数写作 \(\lambda x.x\)。也就是说，先写 \(\lambda\) 这个符号，然后一个变量，然后一个点，最后一个表达式作为函数体。变量可被用来命名表达式；比如，把恒等函数应用到 \(y\) 上可以写为 “\(g(y)\) where \(g(x)=x\)”，在\(\lambda\)-运算中写为 \((\lambda g . (g\ y)\ \lambda x . x)\)。_{[译者注: 这里应该这么理解：\(\lambda g.(g\ y)\) 定义了一个函数，其操作是把自变量作用到 \(y\) 上；然后再把这个定义出的函数作用到恒等函数 \(\lambda x.x\) 上。]}

形式上，基本 \(\lambda\)-运算的语法 \(\Lambda_1\) 是通过下面的递归语法定义的 \begin{equation} \Lambda_1 ::= \nu\ |\ \lambda\nu . \Lambda_1\ |\ (\Lambda_1\ \Lambda_1) \end{equation} 它简明地表达了 (1) 如果 \(x\) 是变量，则 \(x\) 是表达式，(2) 如果 \(x\) 是变量而 \(M\) 是表达式，则 \(\lambda x . M\) 是表达式 (lambda abstraction)，以及 (3) 如果 \(M\) 和 \(N\) 是表达式，则 \((M\ N)\) 是表达式 (应用)。

对于纯粹的 \(\lambda\)-运算，唯一能进行的类似于求值的“操作”是 \(\beta\)-约化。\(\beta\)-约化可被应用到一个 \(\Lambda_1\) (子) 表达式上，如果那个 (子) 表达式在操作符的位置是个 lambda abstraction。形式上 \begin{equation} (\lambda x . M\ N)\qquad \overset{\beta}{\Longrightarrow} \qquad M[x\leftarrow N] \end{equation} 所以提供表达式 \(N\) 给 lambda abstraction \(\lambda x . M\) 得到的“值”是把 \(M\) 里所有出现的 \(x\) 替换为 \(N\)。当然，考虑到嵌套的 lambda abstraction 如果使用相同的变量名称的话会带来各种问题，但这里我们就不管了，而假定所有变量名都是唯一的。

在这里你可能会好奇如何对任何一个 \(\Lambda_1\) 表达式求值。比如，一个变量应该被取值为其值，但我们如何处理好由 lambda abstraction 引入的那些绑定？为此我们需要引入一个词法环境，包含作用域内所有变量的绑定。词法环境通常用 \(\rho\) 表示，在这里表达为一个函数，接收一个变量，返回其绑定的值。于是我们可以把我们的第一个取值器 \(\mathcal{E}_1\) 定义为一个接收一个表达式和词法环境而返回表达式的值的函数。原则上这个取值器可以用任何形式规定，但如果我们用 \(\lambda\)-运算来描述它，我们可以容易地朝着无穷自省塔的方向构造，因为这样的话计算上下文和求值器以及表达式拥有相同的格式。

\(\Lambda_1\) 包含三种语法类别，而 \(\mathcal{E}_1\) 把它们用双重方括号分开。再次强调，我们不要混淆定义语言与被定义的语言。在这里为了展示自省塔的运行，它们都是 \(\lambda\)-运算，但我们不应该混淆塔的不同层！所以在下面的定义中，如果在双重方括号之间的 \(\Lambda_1\) 表达式是第 \(n\) 层，则等号右边是第 \(n-1\) 层的 \(\Lambda_1\) 表达式。\(\mathcal{E}_1\) 如下定义 \(\newcommand\dsbl{[\![} \newcommand\dsbr{]\!]}\) \begin{equation} \mathcal{E}_1\dsbl x\dsbr = \lambda \rho . (\rho\; x) \end{equation} \begin{equation} \mathcal{E}_1\dsbl \lambda x . M\dsbr = \lambda \rho . \lambda \varepsilon . (\mathcal{E}_1\dsbl M\dsbr\;\rho[x\leftarrow\varepsilon]) \end{equation} \begin{equation} \mathcal{E}_1\dsbl(M\;N)\dsbr = \lambda \rho . ((\mathcal{E}_1\dsbl M\dsbr \;\rho)\; (\mathcal{E}_1\dsbl N\dsbr\;\rho)) \end{equation} 注意到所有右边的表达式都是需要一个词法环境 \(\rho\) 的 lambda abstraction，词法环境被用来查询变量的值。要开始对一个表达式取值，可以提供一个空的环境。按照第一种情况，一个变量 \(x\) 的值是其在 \(\rho\) 内的绑定。按照第二种情况，一个 lambda abstraction 的值本身也是个表达式，需要一个值 \(\varepsilon\) 作为输入；当接收到输入后，\(M\) 在扩展了从 \(x\) 到 \(\varepsilon\) 的绑定后的 \(\rho\) 内取值。按照第三种情况，一个函数作用的值是操作符 \(M\) 作用到 \(N\) 上的值，假定 \(M\) 的值的确是个函数。操作符和操作数在同一个词法环境中取值。

为了记号方便，我们将把嵌套应用和 lambda abstraction 简写。于是 \(((f\;x)\ y)\) 可写为 \((f\;x\;y)\)，而 \(\lambda x.\lambda y.M\) 可写为 \(\lambda xy . M\)。

我们已经引入了显式的词法环境，但对于完整的计算上下文而言，我们还需要延续的表示。为了那个目的，我们把取值器 \(\mathcal{E}_1\) 按照延续传递风格 (continuation-passing style; CPS) 重写。这意味着一个延续，作为一个函数 (历史上记为 \(\kappa\))，当需要进一步取值时会被扩展，或者当已经取值时可以被启动。这样，\(\kappa\) 永远表达的时未来的计算——尽管，如前面描述的，通常只是 (把延续) 部分地展开。新的取值器 \(\newcommand{\EO}{\mathcal{E}_1}\) \(\EO'\) 显式地在完全的计算上下文里工作，把词法环境 \(\rho\) 和延续 \(\kappa\) 作为自变量。形式地 \begin{equation} \mathcal{E}_1'\dsbl x\dsbr = \lambda \rho\kappa . (\kappa\;(\rho\; x)) \end{equation} \begin{equation} \mathcal{E}_1'\dsbl \lambda x . M\dsbr = \lambda \rho\kappa . (\kappa\; \lambda \varepsilon\kappa' . (\mathcal{E}_1'\dsbl M\dsbr\;\rho[x\leftarrow\varepsilon]\;\kappa')) \label{eq_EOm} \end{equation} \begin{equation} \mathcal{E}_1'\dsbl(M\;N)\dsbr = \lambda \rho\kappa . (\mathcal{E}_1'\dsbl M\dsbr \;\rho\; \lambda f . (\mathcal{E}_1'\dsbl N\dsbr\;\rho\;\lambda x . (f\; x\; \kappa))) \end{equation} 在第一个和第二个情形，延续被立即调用，这意味着未来的计算被约简了。在这情况是恰当的，因为没有别的需要被取值的东西。但是，在第三种情况，有两件事要做：操作符和操作数要被取值。换句话说，当取得操作符 (\(M\)) 的值时，对操作数 (\(N\)) 的取值是一个要在未来进行的计算。于是，代表了未来的延续，必须被扩展。这个事实精确地体现在为操作符 \(\EO'\dsbl M\dsbr\) 的取值器提供一个新的、扩展了原先提供的 \(\kappa\) 的延续：它是一个函数，等待操作符的值 \(f\)。只要收到了 \(f\) 的值，这个扩展的延续就会调用 \(\EO'\dsbl N\dsbr\) 的取值器，但再次使用新的延续 \(\lambda x . (f\;x\;\kappa)\)。这是因为，当操作数 \(N\) 被取值时，仍然有未来需要进行的计算；也就是，实际调用操作符的值 \(f\) 并作用到操作数的值 \(x\) 上。在这个调用发生之时，未来的计算与在给 \(M\) 和 \(N\) 取值之前的未来一模一样；因此，那个时刻的延续 \(\kappa\) 必须被传递到函数调用上。其实，从\eqref{eq_EOm} 我们可以看到要用这个延续做什么：一个 lambda abstraction 被取值，得到一个二元函数，这里 \(\varepsilon\) 是操作数的值，而 \(\kappa'\) 是当这个函数真正被调用时的延续。这也是需要被提供给函数体 (\(\EO'\dsbl M\dsbr\)) 的取值器的延续。

常数，条件，副作用，引用

嵌套的元循环评估器

可自我修改性的回归必须在某个地方停止_{除非我们考虑能够改变自身硬件的系统。但即便如此仍然 (很可能) 会有关于硬件可修改性的物理限制。}。

功能性自省系统

考虑到上面最后一句话的逻辑推论，我们现在来研究，如果在负责实现解释器的那些函数所在的地方就停止自我修改回归，会有什么后果。如果解释器解释的是图灵完备的指令集，那么，在任何地点检查和修改词法环境和延续的能力，就足以达到功能性的完全自省控制。

Queinnec 之所以提到用于实现解释器的那些函数的可修改性，很可能不是处于功能性的原因，而是处于时间和效率的考虑。我们已经看到，“获得计算上下文”的能力足以实现功能性自省，但不足以让程序提高其自身解释器的运行速度 (如果它知道怎么做的话)。本节我们为自省系统引入一个新的解释器，采用的是中间道路。用于实现解释器的那些函数是基元函数 (即黑盒子)；但是，它们 (1) 数量很少，(2) 很小，以及 (3) 执行速度快。_{这最后一点当然依赖于具体的实现，但既然它们小，它们可以被高效实现。在我们的没太优化的 C++ 参考实现中，取值器的一个基元步骤在 2009 年的普通配置电脑上花费大约 20 纳秒。由于自省在每个这样的步骤后都可能，每秒有五千万次机会来中断取值，抓取计算上下文，以及检查并修改它。} 我们要证明被这个解释器运行的程序可以以一种足够强大的方式检查并修改自身 (包括速度提升) 并成为自省的。

首先我们需要一个编程语言。这里我们用一种甚至比经典的 \(\lambda\)-运算更简单的语法，由下面的递归语法定义 \begin{equation} \Lambda_3 ::= c\ |\ n\ |\ (\Lambda_3\;\Lambda_3) \end{equation} 这里 \(c\) 是一些常数 (布尔值以及基元函数的符号)，而 \(n\) 是一些数。没有特殊形式 (比如 Scheme 里的 quote，lambda，set!，if 之类)，只有函数作用，而所有函数都是一元的。基本的二元函数像 \(((+\ 1)\ 2)\) 这样启动。在内部，唯一的复合结构是对，_{尽管我们的参考实现也支持矢量 (固定长度的数组)。} 而一个函数作用 \((f\ x)\) 简单地表示为一个对 \(f:x\)。一个数字的实例占据的空间跟一个对占据的一样 (比如 64 位)；常数不占空间。

为了表达内部的东西，我们大量使用记号 \(a:d\)，意思是头为 \(a\) 尾为 \(d\) 的一个对。冒号从右往左结合，所以 \(a:ad:dd\) 与 \((a:(ad:dd))\) 相同。\(\bot\) 是个常数，代表错误或未定义值；比如，整数除以 0 的结果是 \(\bot\) (程序永远不会因为错误而停止)。空列表 (Scheme 里的 \('()\)) 用常数 \(\varnothing\) 表示。

为了查找保存在存储空间 \(\sigma\) 的 \(p\) 位置的值，我们对于数字使用记号 \(\sigma[p\rightarrow n]\)，而对于对使用 \(\sigma[p\rightarrow a:d]\)。存储分配记为 \(\sigma[q\overset{\ast}\leftarrow n]\) 和 \(\sigma[q\overset{\ast}\leftarrow a:d]\)，这里 \(q\) 是一个新位置，在那里可以找到被分配空间的数字或对。\(\mathbb{N}_\sigma\) 用来标记存有数字的那些位置；所有别的位置存储对。常数的集合记为 \(\mathbb{P}\)。遇到不清楚的地方时，读者可以在附录里看到关于记号和存储的更多细节。

本节要定义的解释器的关键是，不仅程序以对的方式存储，词法环境和延续也是。既然程序可以对对执行构建 (cons)，检查 (car, cdr)_{在 Scheme 和 \(\Lambda_3\) 里，car 和 cdr 是基元一元函数，分别返回一个对的头和尾。}，以及修改 (set-car!, set-cdr!) 操作，它们也可以用相同的函数构建，检查，以及修改词法环境和延续，只要能获取它们。下面展示的解释器就可以。

讨论

\(\Lambda_3\) 是可以为自省哥德尔机编程的语言吗？它当然可以作为这样的语言的核心。极致的简单和小巧 (因此容易推理)，同时允许完全的功能性自省。还应注意到我们没有剩下什么没有详细规定的东西；程序、函数，以及数字的表达结构和存储方式都是精确知道的。即便每个基本函数的内存分配的次数都是事先知道且可预测的。这对于哥德尔机这样的自我推理系统而言是重要的信息。在那种意义上 \(\Lambda_3\) 的求值器解决了所有我们在研究基于纯粹 \(\lambda\)-运算的元循环求值器塔时发现那些的自省所牵涉的问题。

我们正在用类似于 \(\Lambda_3\) 的语言来实现一个哥德尔机。我们引入的最重要的扩展是，与其维护单个延续，我们保留了一个延续栈，就像顶部隐没于灰暗天空的自省塔——除了这次是有坚实基础而没有那些迷雾沼泽之外！尽管由于版面限制我们讲不了细节，这个构造允许用容易而高效的方法进行交缠式的运算 (包含关键部分)，而这是哥德尔机的调度器的规格所需要的。

附录：本文用到的符号