Constructing a Quine from Kleene's Second Recursion Theorem

The construction recasts Kleene’s Second Recursion Theorem as a general method for making a term refer to its own syntax. In a language with quoted syntax trees and a quasi-quoter that turns a quotation into a quotation of that quotation, any function P from syntax to some result type has a fixed point: a term t satisfying P applied to the quotation of t equals t. The proof builds an auxiliary function that feeds P a representation of its own application. Choosing P as the identity produces a quine; choosing functions that measure or print syntax produces programs that output their own size or source code. The same pattern gives the diagonal lemma used in Gödel’s incompleteness argument and shows why a suitable truth predicate would yield a contradiction. This formulation does not require the language to be Turing complete.

The construction is then implemented in the untyped lambda calculus, whose small syntax consists only of variables, applications, and abstractions. Church encodings represent these syntax trees, with de Bruijn indices identifying bound variables. A recursively defined quasi-quoter rebuilds each syntax node as quoted lambda-calculus code; together with a similar mechanism for Church numerals, it supplies the ingredients for the fixed-point proof. The definitions and reasoning are formalized in Rocq, producing an explicit, very large quine in de Bruijn notation. The central point is that formalizing the result clarifies how self-reference works: rather than treating every program as an encoded number, the construction uses the structure of syntax directly and reveals links between computability, programming, and logic.