Constructing a Quine from Kleene's Second Recursion Theorem

Table of contents Introduction Kleene, Classical Perspective Models of Computation Kleene, Functional Programming Perspective Some Logical Digressions Building a Quine in Untyped Lambda Calculus Putting It All Together References Introduction It is a well-known fact that the existence of Quines are a consequence of Kleene’s 2nd recursion theorem. I was curious about how easy or difficult it was to use this construction in practice, so I decided to try to formalize it. One of the virtues of formalization is that it naturally motivates the mathematician to structure their definitions and proofs in a clearer and more concise fashion. The pain of a clunky definition or ill-structured argument is actually felt, and so the goals of expedient proofs and well-structured proofs often align. Far from being a mechanical chore, the act of formalization can actually be a source of insight and creativity (incidentally, this is why I think the popular view of formal verification as a mere exercise in transcription misses the mark). With this in mind, I hoped that I could find or develop a clean formalization that could shed some light on a theorem that I was only familiar with on rather hand-wavy terms. During my search, I was fortunate enough to uncover this excellent preprint that laid out how to perform this construction in the untyped lambda calculus. For the remainder of this post I will sketch out the proof from this preprint and offer some motivation for why we might chose to present the theorem this way. Kleene, Classical Perspective The usual presentation of the recursion theorem assumes we are working with an effective numbering of the partial recursive functions $\lbrace \varphi_i \rbrace_{i \in \mathbb{N}}$. We can then state the result as follows: Theorem (Kleene’s second recursion theorem, classical computability theoretic version) Let $\psi$ be an $n+1$-ary partial recursive function. Then there is an index $e$ such that \[\psi(e,\bar{x}) \simeq \varphi_e(\bar{x})\] Quines fall out as a corollary when we take $\psi$ to be the identity, giving us \[e = \psi(e) \simeq \varphi_e()\] If we squint we can imagine this to be a Quine. Intuitively, the index $e$ is a representation of the function $\varphi_e$, and thus $\varphi_e$ is a program that on no inputs outputs $e$, its own “source code”. Models of Computation Traditional presentations of computability theory tend to adopt a reductionist attitude where all discrete structures (pairs, lists, syntactic objects, etc.) are just natural numbers. This necessitates many tedious encodings whose details the presenter would prefer to not mention, and thus we get a lot of hand-waving. This sort of presentation is understandable to an extent. If you are only interested in arriving at deep/advanced results, it makes sense that you would not want to waste too much time with the low-level details when, after all, “all these models of computation are equivalent” anyway. However, this sort of approach runs the risk of engendering a sort of nihilism with respect to formal systems. All systems are equally arbitrary, ugly, etc. so why bother even studying them in detail? There is a subfield that takes matters of structure in formal systems more seriously: Proof theory. One of the big takeaways I received from proof theory is that there can be significant content found in the way we structure our formal systems. So, returning to computability theory, it is appropriate that our search for a model that takes structure seriously, we arrive at the most proof-theoretic model of computation, the lambda calculus. Kleene, Functional Programming Perspective Even though we will ultimately work in the untyped lambda calculus, it is helpful to consider a typed presentation of the recursion theorem. We will see that using explicitly types draws connections to other results, but the argument still applies to the untyped case, where the types fall away as “moral types” (for instance, we can still speak of functions $\mathbb{N} \rightarrow \mathbb{N}$ in untyped lambda calculus even though the types aren’t really there). We will suppose we are working in a functional language $L$ that is capable of self-reflection. In particular: It has a type $\mathsf{AST}$ of syntax trees that represent $L$-expressions: If $t$ is a term then we will take $\lceil t \rceil : \mathsf{AST}$ to denote its quotation. The constructor for function application will be given by the infix $\cdot$ and so the following equation is valid: $ \lceil t_1 t_2\rceil = \lceil t_1 \rceil \cdot \lceil t_2 \rceil $ It has a quasi-quoter that is capable of internally performing quotations when the expression is itself a quote. Specifically, there is a term $\mathsf{q} : \mathsf{AST} \rightarrow \mathsf{AST}$ such that for any term $t$ we have that $\mathsf{q} \lceil t \rceil = \lceil \lceil t \rceil \rceil$. In other words, $\mathsf{q}$ is a function that turns single-quoted expressions into double-quoted expressions. With those assumptions, Kleene’s theorem can be stated as follows: Theorem (Kleene’s second recursion theorem, functional version) Let $T$ be a type and $P : \mathsf{AST} \rightarrow T$. Then there is a term $t : T$ such that $P \lceil t \rceil = t$.

Proof.