Kleene 第二递归定理是可计算理论中的一个基础结果，它允许构建自我指涉的程序。在其经典形式中，该定理指出对于任何偏递归函数 $\psi$，存在一个索引 $e$，使得函数 $\varphi_e$ 的行为表现为 $\psi(e, \bar{x})$。Quine 是该定理的一个特定推论：通过将 $\psi$ 设置为恒等函数，可以找到一个代表程序的索引 $e$，该程序在执行时会输出其自身的源代码。虽然这通常在抽象层面被讨论，但形式化这一构建过程为理解计算底层逻辑如何结构性地支持自我指涉提供了一条更清晰的路径。
这张图片展示了 Kleene 第二递归定理的核心数学属性，即找到一个函数索引 $e$，使得 $\varphi_e$ 表现为所需的属性。
这一特定符号直接支持了文章关于 Quine 是通过寻找不动点而成为该定理推论的解释。
为了从抽象理论转向具体实现，可以采用函数式编程的视角。在这种模型中，假设语言 $L$ 拥有用于语法树的类型 $\mathsf{AST}$，以及一个可以在内部执行引用的准引用器 $\mathsf{q}$。在这些假设下，该定理可以表述为：对于任何类型 $T$ 和任何属性 $P : \mathsf{AST} \rightarrow T$，存在一个项 $t : T$，使得 $P \lceil t \rceil = t$。证明过程涉及构建一个捕捉属性 $P$ 的项 $d$，然后找到不动点 $t := d \lceil d \rceil$。这种方法表明，该定理不仅关乎 Quine，还关乎为任何语法属性寻找不动点，例如输出自身大小或自身美化打印源代码的程序。
在无类型 lambda 演算中实现这一点需要使用 Church 编码来表示语言自身的语法。由于无类型 lambda 演算具有足够的表达能力来处理树状数据，因此可以定义一种 AST 表示，其中变量、应用和 lambda 抽象本身被编码为 lambda 抽象。最复杂的组件是准引用器，它必须定义为对 AST 树结构的 fold 操作。通过将这些方程转换为 Church 编码，可以在 de Bruijn 表示法中构建一个 Quine。这种形式化凸显了一个显著的权衡：虽然无类型 lambda 演算通过移除类型约束简化了证明，但它需要对 AST 和引用机制进行严谨的手动构建，才能达到与高层函数式语言相同的效果。