从Kleene定理构建Quine的函数式视角

Constructing a Quine from Kleene's Second Recursion Theorem

Quine的存在其实是Kleene第二递归定理的直接推论。我一直好奇如何在实践中运用这一构造，于是决定对其进行形式化。形式化过程不仅让定义和证明更清晰，还意外带来了新的洞察。本文基于Untyped Lambda Calculus，展示了如何从函数式编程的视角重新理解Kleene定理，并逐步构建出一个Quine。通过引入Church编码和quasi-quoter等概念，我们能在极简的语言中实现自我指涉。这一过程不仅揭示了计算模型的结构之美，也连接了Gödel不完备定理和Tarski不可定义性等深层逻辑问题。