June 15, 2026. A panoply of self-reference, from quines to antiquines to safe recursion.

Introduction

A cool fact is that certain programs are self-replicating: run them, and they output themselves. Such programs are called quines, after the philosopher and logician Willard Van Orman Quine. They are often quite elaborate. Consider for instance this very clever example in Python 3 (to be saved as exceptionQuine.py):

    File "exceptionQuine.py", line 1
        File "exceptionQuine.py", line 1
        ^
IndentationError: unexpected indent

Running the program, it trips up on the first line and produces the second two lines as error output. It’s a pun, hinging on the syntax of error printouts. Purists might consider this cheating, but quines are not so easily eliminated; they are puns that run surprisingly deep.

Diagon Alley

As it turns out, quines exist in any Turing-complete language for profound mathematical reasons. Consider a language $\mathcal{L}$ with some syntax rules for building valid programs. Each program $x \in \mathcal{L}$ is associated with a unique Gödel number, $\ulcorner x \urcorner \in \mathbb{N}$, via a cute procedure involving primes. Define the $\text{eval}: \mathbb{N} \to \mathcal{L}$ function as executing the program associated with Gödel number $n$ and outputting some result in $\mathcal{L}$. Then a quine $q$ is a “fixed point”

\[q = \text{eval}(\ulcorner q \urcorner).\]

The existence of such a fixed point follows from Kurt Gödel’s famous diagonal lemma. Although this is the right intuition, technically, the diagonal lemma is for predicates which are true or false, and it’s more correct to translate into the language of computable functions using Kleene’s second recursion theorem. Instead of a predicate, we have that for any partial recursive $Q: \mathbb{N}\times\mathbb{N}\to \mathbb{N}$, there is partial recursive function $p$ such that

\[p = \lambda y. Q(\ulcorner p \urcorner, y)\]

where the RHS is fancy notation for the function left over when we saturate the first argument. A quine is just the case where $Q(x, y) = x$, i.e. we project onto the first argument and ignore $y$ altogether, giving a partial recursive function $q$ such that

\[q(y) = \ulcorner q \urcorner.\]

In words, it always outputs its own index.

Antiquines

The existence of quines is tied up with fixed points and self-reference. In this case, the self-reference is harmless (not to mention entertaining) but it is closely allied with a more sinister form of self-reference I call the antiquine. Instead of returning the object itself, either by evaluation or projection, it somehow changes the returned object, yielding a type of “anti”-self-reference. To illustrate concretely, instead of $\text{eval}$, we can look $\text{prov}(n)$, a predicate which states that a formula with a given Gödel number $n$ is provable in some formal system (such as Peano arithmetic $\mathsf{PA}$). The equivalent of a quine is

\[q \leftrightarrow \text{prov}(\ulcorner q \urcorner),\]

which asserts its own provability. We’ll return to these below. The antiquine is

\[a \leftrightarrow \neg\text{prov}(\ulcorner a \urcorner),\]

which asserts its unprovability. If $a$ is false, then the system can prove $a$, i.e. it is unsound. If $a$ is true, then there is a statement which is true but not provable, i.e. the system is incomplete. Gödel proved the diagonal lemma in order to reach this famous conclusion!

Exercises. Solve the following using antiquines. (a) Show that the halting predicate $\text{halt}$ is undecidable, i.e. we cannot determine if an arbitrary program halts. (b) Extend this to show that any non-trivial (i.e. non-constant) semantic property is undecidable. (c) Instead of provability, apply the argument to the predicate $\text{true}(n)$ which evaluates the truth of the formula with a given Gödel number $n$.

Löb’s surprise

A logical quine is equivalent to its own provability:

\[q \leftrightarrow \text{prov}(\ulcorner q \urcorner).\]

If $q$ is true, it is provable, so it does not witness incompleteness; if it is provable, it is true, so it does not witness unsoundness. They haven’t seen anything, honest! Such a formula seems useless, and in particular, it could be true or false. Remarkably, this is not the case: Martin Löb proved in 1955 that the fixed point $q$ is always true. More generally, if you can prove that

\[\text{prov}(\ulcorner x \urcorner) \to x\]

then you can prove $x$ itself. The argument goes roughly as follows:

• Use the diagonal lemma to construct a sentence $L$ saying “If $L$ is provable, $x$ follows”.
• If our formal system is sound and $L$ is provable, it is true.
• In that case, since $L$ is provable, then $x$ follows.
• But this demonstrates, by assumption, if $L$ is provable $x$ follows!
• Thus $L$ is proven, and $x$ follows. We have proven $x$!

Going back to programs instead of proofs, what does this tell us? Löb becomes something like

\[(\text{eval}(\ulcorner x \urcorner) \to x) \to x,\]

where we interpret $\to$ as “produces”. Thus, if evaluating a program outputs a program, we can collapse the produced value into the program. This sounds arcane, but it is just the notion of recursion, and Löb’s theorem tells us that recursion works.

Safe recursion

We have been a little loose with our interpretation, and it is time to pay the piper. If we really want to think of programs in terms of logic, we need to invoke something called the Curry-Howard isomorphism, which asserts that proofs are programs and formulas are their types. We cannot evaluate a type, so the naive recursion I sketched above fails. We need to interpret eval in a subtly different way. We replace $\text{eval}(\ulcorner \cdot \urcorner)$ with the modality $\triangleright$, pronounced “later”, with the interpretation that

\[\triangleright x = \text{a value of type $x$ obtained after a unit of computation}.\]

This is comparable to $\text{eval}(\ulcorner x \urcorner)$ since it bakes in the idea of a computational pass. Löb’s theorem, in this new language, is then

\[\text{löb}: (\triangleright x \to x) \to x,\]

which states that if I can turn a later value into a current value, I can produce a value now. This tells us that a special sort of self-referential process is possible called guarded recursion; this prevents runaway self-reference by enforcing that a unit of computation is performed per step, so the recursion is productive, i.e. it produces something. In fact, we can view $\text{löb}$ as a fixed-point combinator, akin to the Y-combinator familiar from (unrestricted) recursion:

\[Y = \lambda f. (\lambda x. f (x\, x))(\lambda x. f (x\, x)), \quad Y f = f (Y f).\]

The Y-combinator applies a function to the Y of itself; this can easily lead to runaway empty self-reference, while $\text{löb}$ instead gives

\[\text{löb} f = f (\text{next}(\text{löb} f))\]

with $\text{next}$ advancing computational time, forcing progress in the recursive stream. So, far from being a puzzling factoid about formal systems, Löb is a beautiful structural fix ensuring the (productive) safety of self-referential definitions. It guards against the coming of the antiquine, and is used in type-theoretic languages like Agda, Coq and Idris.

Conclusion

So, we’ve covered, in a brief and hopefully entertaining way, some different notions of self-reference arising from fixed point constructions of the diagonal lemma and Kleene’s recursion theorem. This includes self-replicating objects called quines, anti-self-replicating objects I’ve baptised antiquines (more conventionally called “liars” after the Liar Paradox), and finally a curious property of self-replication called Löb’s theorem, which points the way not only to recursive fixed points, but a structural method of safeguarding them from unproductive proliferation. I for one welcome more Löb security.