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.
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”.
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.
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.
Take $d : \mathsf{AST} \rightarrow T := \lambda e. P (e \cdot \mathsf{q} \hspace{2pt} e)$. Then our fixpoint expression is $t := d \lceil d \rceil$:
\[\begin{aligned} t &= d \lceil d \rceil \\ &= (\lambda e. P (e \cdot \mathsf{q} \hspace{2pt} e)) \lceil d \rceil \\ &= P (\lceil d \rceil \cdot \mathsf{q} \lceil d \rceil) \\ &= P (\lceil d \rceil \cdot \lceil \lceil d \rceil \rceil) \\ &= P \lceil d \lceil d \rceil \rceil \\ &= P \lceil t \rceil. \end{aligned}\]As before, we get Quines when we take $P$ to be the identity, but we see that the theorem can be more broadly applied to find fixed-points for any sort of “syntactic” property of a program. For example, taking $P := \mathsf{size} : \mathsf{AST} \rightarrow \mathbb{N}$ produces a program that outputs its own size, and letting $P := \mathsf{pretty}\text{_}\mathsf{print}: \mathsf{AST} \rightarrow \mathsf{string}$ yields the more familiar form of a Quine as a program printing out its own source code in a text format.
Even though the recursion theorem is often presented in the context of the partial recursive functions, it should be noted that our proof does not assume $L$ is Turing complete. Indeed, we find important connections to other areas of logic when we consider Kleene in the context of a particular class of total languages: the term languages of arithmetic systems.
Imagine we are working in some sort of higher-order arithmetic with a type of propositions $\mathsf{Prop}$. This could be a proof assistant like Rocq itself, for example. If we take $T = \mathsf{Prop}$ we have ourselves a very functional presentation of the diagonal lemma, the key ingredient to both Gödel’s first incompleteness theorem and Tarski’s undefinability theorem. Here’s how those two appear in this setting:
-
Gödel: Take $\mathsf{Prov} : \mathsf{AST} \rightarrow \mathsf{Prop}$ to be our provability predicate. If we set $P := \neg \circ \mathsf{Prov}$ then the recursion theorem gives us some $\phi$ such that
\[\phi = \neg \mathsf{Prov} \lceil \phi \rceil\]This $\phi$ is the Gödel sentence.
-
Tarski: Suppose $\mathsf{Tr} : \mathsf{AST} \rightarrow \mathsf{Prop}$ is a truth predicate, meaning that the truth scheme \(\mathsf{Tr}\lceil \phi \rceil \iff \phi\) holds for all $\phi$.
Take $P := \neg \circ \mathsf{Tr}$. Then there is some $\phi$ with
\[\phi = \neg \mathsf{Tr}\lceil \phi \rceil \iff \neg \phi\]
We have seen from the proof outlined above that lambda calculi lead to a fairly clean and concise proof outline. What makes the untyped lambda calculus particularly attractive is that the language is very simple with few features, while also being expressive enough to do non-trivial programming tasks in it. For a task such as this where we need to implement the language inside itself, this combination of qualities is essential.
The first thing we need to implement the proof above is an AST representation of the language itself. Fortunately, the untyped lambda calculus can easily handle such treelike data with Church encodings.
The untyped lambda calculus consists of variables, applications, and lambda abstractions:
\[\Lambda ::= v | \Lambda \Lambda | \lambda v. \Lambda\]These three constructors show up in the encoding as three lambda abstractions $\lambda v a l. \cdots$, where the body of the term is built up from $v, a, l$ in a fashion that directly mirrors the structure of the term. For example, if we wish to quote the term $\lambda x y. y x$ we get this:
\[\lceil \lambda x y. y x \rceil = \lambda v a l. l (l (a (v \underline{0}) (v \underline{1})))\]($\underline{0}$ and $\underline{1}$ are the Church numerals of the variables’ de Bruijn indices).
The last thing we need is a quasi-quoter. This is definitely the hairiest part but it not too bad once you have the details figured out.
If we were to write out the equations for a quasi-quoter in colloquial FP, it might look something like this:
\[\begin{aligned} \mathsf{q}(\mathsf{Var} \hspace{2pt} i) &= \mathsf{App} (\mathsf{Constr} \hspace{2pt} \texttt{"Var"}) (\mathsf{Num} \hspace{2pt} i)\\ \mathsf{q}(\mathsf{App} \hspace{2pt} e_1 \hspace{2pt} e_2) &= \mathsf{App}(\mathsf{App}(\mathsf{Constr} \hspace{2pt} \texttt{"App"}) (\mathsf{q} \hspace{2pt} e_1)) (\mathsf{q} \hspace{2pt} e_2)\\ \mathsf{q}(\mathsf{Lam} \hspace{2pt} e) &= \mathsf{App} (\mathsf{Constr} \hspace{2pt} \texttt{"Lam"}) (\mathsf{q} \hspace{2pt} e) \end{aligned}\]Translated back into our Church encoding:
\[\begin{aligned} \mathsf{q}(v \hspace{2pt} \underline{i}) &= a (v \hspace{2pt} \underline{2}) (\mathsf{qn} \hspace{2pt} \underline{i})\\ \mathsf{q}(a \hspace{2pt} e_1 \hspace{2pt} e_2) &= a (a (v \hspace{2pt} \underline{1}) (\mathsf{q} \hspace{2pt} e_1)) (\mathsf{q} \hspace{2pt} e_2)\\ \mathsf{q}(l \hspace{2pt} e) &= a (v \hspace{2pt} \underline{0}) (\mathsf{q} \hspace{2pt} e) \end{aligned}\]where $\mathsf{qn}$ is a quasi-quoter for Church numerals (derived similarly). Note the correspondence between $v, a, l$ and $v \hspace{2pt} \underline{2}, v \hspace{2pt} \underline{1}, v \hspace{2pt} \underline{0}$ is determined by our Church encoding convention $\lambda v a l. \cdots$.
These three equations describe a fold over the tree structure of the ASTs. Since Church encodings naturally handle folds, we can easily turn those equations into a single term.
These constructions were carried out and reasoned about in Rocq, which you can see here.
The resulting Quine is shown below in de Bruijn notation:
((λ((λ0) (((λ(λ(λ(λ(λ((1 (((4 2) 1) 0)) (((3 2) 1) 0))))))) 0) ((λ(λ(λ(λ(0 (0 (0 (((((λ(λ(λ(λ(((3 ((((λ(λ(λ(λ((2 (3 (λ(λ(1 (1 0)))))) (((((λ(λ(λ(λ(1 (1 (((((λ(λ(λ(λ((0 (2 (3 (λ(λ(1 0)))))) (3 (λ(λ0)))))))) 3) 2) 1) 0))))))) 3) 2) 1) 0)))))) 2) 1) 0)) ((((λ(λ(λ(λ(2 ((2 (3 (λ(λ(1 0))))) 0)))))) 2) 1) 0)) ((((λ(λ(λ(1 (2 (λ(λ0))))))) 2) 1) 0)))))) 3) 2) 1) 0)))))))) 0)))) (λ(λ(λ(0 ((1 (0 (2 (λ(λ0))))) ((1 ((1 (0 (0 (0 (0 (0 ((1 ((1 (2 (λ(λ(1 0))))) ((1 ((1 ((1 (2 (λ(λ(1 (1 (1 (1 0)))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))) ((1 ((1 ((1 (2 (λ(λ(1 (1 (1 0))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0))))))))))) (2 (λ(λ0))))) ((1 (0 (0 (0 (0 ((1 (2 (λ(λ0)))) ((1 (2 (λ(λ0)))) ((1 (2 (λ(λ0)))) ((1 ((1 ((1 ((1 (0 (0 (0 (0 ((1 ((1 ((1 (2 (λ(λ(1 (1 (1 0))))))) ((1 ((1 ((1 (0 (0 (0 (0 ((1 ((1 (2 (λ(λ(1 (1 0)))))) ((1 (2 (λ(λ(1 (1 (1 0))))))) (0 (0 ((1 (2 (λ(λ(1 0))))) ((1 (2 (λ(λ(1 0))))) (2 (λ(λ0)))))))))) ((1 ((1 ((1 ((1 (0 (0 (0 (0 ((1 (2 (λ(λ(1 0))))) ((1 (2 (λ(λ(1 0))))) ((1 ((1 ((1 ((1 (0 (0 (0 (0 ((1 ((1 (2 (λ(λ0)))) ((1 (2 (λ(λ(1 (1 0)))))) ((1 (2 (λ(λ(1 (1 (1 0))))))) (0 (0 ((1 (2 (λ(λ(1 0))))) (2 (λ(λ0)))))))))) ((1 (2 (λ(λ(1 (1 (1 0))))))) (0 (0 (2 (λ(λ0)))))))))))) (2 (λ(λ(1 (1 (1 0)))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0))))))))))) (2 (λ(λ(1 (1 (1 0)))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))) ((1 ((1 ((1 (0 (0 (0 (0 ((1 (2 (λ(λ(1 (1 0)))))) ((1 ((1 (2 (λ(λ(1 (1 0)))))) ((1 (2 (λ(λ(1 (1 (1 0))))))) (0 (0 ((1 (2 (λ(λ(1 0))))) (2 (λ(λ0))))))))) (2 (λ(λ0)))))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))) ((1 ((1 ((1 (0 (0 (0 ((1 (2 (λ(λ(1 0))))) ((1 (2 (λ(λ(1 (1 0)))))) (0 (0 (2 (λ(λ0))))))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))))))) (2 (λ(λ(1 (1 (1 0)))))))) (2 (λ(λ(1 (1 0))))))) (2 (λ(λ(1 0)))))) (2 (λ(λ0)))))))))))) (2 (λ(λ0)))))))))))