Universality and quines

Quines, named by Douglas Hofstadter in honor of Willard Van Orman Quine, are self-replicating programs, programs that output their own source code. It’s actually just a consequence of Turing completeness of a programming language that it’s possible to construct a quine. For example, here’s a quine in a sort of classic structure in Python:^[1]

a = ['print "a =", a', 'for s in a: print s']
print "a =", a
for s in a: print s

In this note, I’m going to show how to make a lambda calculus interpreter in lambda calculus (a “universal machine”), how to use it to prove a kind of fixed-point theorem for the lambda calculus, and then how to get a quine from it.

1. The lambda calculus

Alonzo Church came up with a fairly nice and simple calculus that can be used as a basis for both computation and mathematics. In his version, there are three types of symbolic expressions:

• $x$ if $x$ is a symbol (variable), where we presume we have an infinite set of symbols to draw from.
• $(x\mapsto M)$ if $x$ is a symbol and $M$ is a lambda calculus term (abstraction).^[2]
• $\left(MN\right)$ if $M$ and $N$ are lambda calculus terms (application).

This sort of abstractly models the idea of functions and applying functions to values, but with the oddity that everything is a function. The “semantics” are defined by an equivalence relation on lambda calculus terms. The definitions depend quite a lot on the concept of a free variable, which can be inductively defined as such:

• $\mathrm{free}\left(x\right)=\left\{x\right\}$,
• $\mathrm{free}(x\mapsto M)=\mathrm{free}\left(M\right)-\left\{x\right\}$, and
• $\mathrm{free}\left(MN\right)=\mathrm{free}\left(M\right)\cup \mathrm{free}\left(N\right)$.

The $x$ in $x\mapsto M$ is called a bound variable. We also need substitution $M[x\to N]$ that replaces all free instances of $x$ with $N$:

• $y[x\to N]=\{\begin{array}{cc}N& \text{if}x=y\\ y& \text{otherwise}\end{array}$
• $(y\mapsto M)[x\to N]=\{\begin{array}{cc}(y\mapsto M)& \text{if}x=y\\ (y\mapsto M[x\to N\left]\right)& \text{otherwise}\end{array}$ where $y\notin \mathrm{free}\left(N\right)$
• $\left(M_1{M}_2\right)[x\to N]=\left(M_1\right[x\to N\left]M_2\right[x\to N\left]\right)$.

This is a partial function because of the constraint in the second rule, but up to the following equivalence relations one may think of it as being a function.

$\alpha$-renaming:

If $(x\mapsto M)$ is a lambda term and $y\notin \mathrm{free}\left(M\right)$, $(x\mapsto M)\equiv (y\mapsto M[x\to y\left]\right)$.

$\beta$-reduction:

If $\left(\right(x\mapsto M\left)N\right)$ is a lambda term, then $\left(\right(x\mapsto M\left)N\right)\equiv M[x\to N]$.

$\eta$-conversion:

If $x\notin \mathrm{free}\left(M\right)$, then $M\equiv (x\mapsto (Mx\left)\right)$.

There’s not really a sense in which a lambda calculus term is evaluated per se, but there are various normal forms one could try to put a particular lambda calculus term in (as functional programming languages do). But, reduction strategies have divergent terms, which are lambda calculus terms that do not stabilize while applying the reduction strategy. For example, $\Omega =\left(\right(x\mapsto \left(xx\right)\left)\right(x\mapsto \left(xx\right)\left)\right)$ is generally divergent.

As a shorthand, we will take application to be left-associative, meaning $\left(LMN\right)$ is $\left(\right(LM\left)N\right)$, and abstraction to be right-associative, meaning $(x\mapsto y\mapsto M)$ is $(x\mapsto (y\mapsto M\left)\right)$. One usually thinks of $(x\mapsto y\mapsto M)$ as being a two-argument function.^[3] We will also sometimes not write outermost parentheses, and we will use the rule that $x\mapsto MN$ means $(x\mapsto (MN\left)\right)$.

1.1. de Bruijn indexes

Symbolic variables are an annoying complexity for lambda calculus because of all the issues with free variables in $\alpha$-renaming and substitution. One way around this is to use the natural numbers $N=\{0,1,2,\dots \}$ for variables, where the number represents how many abstractions out that variable is bound from.

Lambda calculus terms when using de Bruijn indexes are

• $n$ if $n\in N$ (variable),
• $\left(\lambda M\right)$ if $M$ is a term (abstraction), and
• $\left(MN\right)$ if $M$ and $N$ are terms (application).

Then, the equivalence relation no longer needs $\alpha$-renaming. Substitution is

• $m[n\to N]=\{\begin{array}{cc}N& \text{if}m=n\\ m& \text{otherwise}\end{array}$
• $\left(\lambda M\right)[n\to N]=\left(\lambda M\right[n+1\to N_{+}\left]\right)$
• $\left(M_1{M}_2\right)[n\to N]=\left(M_1\right[n\to N\left]M_2\right[n\to N\left]\right)$.

The $N_{+}$ denotes incrementing each unbound variable appearing in $N$ (this can be thought of as the simultaneous application of the substitutions $[n\to n+1]$ for all $n\in N$).

The equivalence relation is generated by two rules.

$\beta$-reduction:

$\left(\right(\lambda M\left)N\right)\equiv M[0\to N_{+}]$.

$\eta$-conversion:

$M\equiv \left(\lambda \right(M_{+}0\left)\right)$.

For lambda calculus terms with no free variables, it is a purely mechanical process going back and forth between de Bruijn indexes. One way to start is to $\alpha$-rename all the bound variables so that they come from some alphabet $x_0,x_1,x_2,\dots$ so that each nested abstraction uses the next variable in the list, and then the index is $d-i$ where $i$ is from $x_i$ and $d$ is the abstraction depth. Terms with free variables can be dealt with by imagining a that those variables have been bound in some specified order.

I sort of like the following variation of de Bruijn indexes, where variables are written in unary rather than from the infinite alphabet $N$.

• $z$ is a term (representing zero in $N$).
• $SM$ is a term if $M$ is a term (the successor, representing $n+1$ in $N$ but extended to all terms).
• $\left(\lambda M\right)$ is a term if $M$ is a term.
• $\left(MN\right)$ is a term if $M$ and $N$ are terms.

The substitution rules $M[n\to N]$ with $n\in N$ are

• $z[n\to N]=\{\begin{array}{cc}N& \text{if}n=0\\ z& \text{otherwise}\end{array}$
• $\left(SM\right)[0\to N]=SM$
• $\left(SM\right)[n+1\to N]=SM[n\to N]$ (Errata: ^[4])
• $\left(\lambda M\right)[n\to N]=\left(\lambda M\right[n+1\to SN\left]\right)$
• $\left(M_1{M}_2\right)[n\to N]=\left(M_1\right[n\to N\left]M_2\right[n\to N\left]\right)$.

Then, while $\beta$-reduction is the same, $\eta$-conversion is simply $M\equiv \left(\lambda \right(SMz\left)\right)$. However, this is at the cost of needing an $S$-reduction rule, the details of which I’ll spare you because they’re easy to figure out if you need them.

2. Algebraic data types

Pretty much every data type that you want can be represented as some expression of products and disjoint unions of basic data types, possibly with some recursion. For example, if $\top$ represents a singleton type, the the type $LL\left(X\right)$ for a linked list of things of type $X$ is recursively defined by $LL\left(X\right)=\top \bigsqcup (X\times LL(X\left)\right)$. These sorts of algebraic expressions to represent types are ADTs (algebraic data types).

In lambda calculus, a value $(x,y)$ of a product type $X\times Y$ can be represented by the expression $f\mapsto fxy$, where the projector functions are ${\pi }_X=p\mapsto p(x\mapsto y\mapsto x)$ and ${\pi }_Y=p\mapsto p(x\mapsto y\mapsto y)$. The constructor function is $x\mapsto y\mapsto f\mapsto fxy$. The idea is that a value is something that provides its component values to some supplied function.

A disjoint union $X\bigsqcup Y$, on the other hand, is described by its inclusion functions: ${\iota }_X=x\mapsto (f\mapsto g\mapsto fx)$ and ${\iota }_Y=y\mapsto (f\mapsto g\mapsto gy)$, which is a sort of dual to the projectors for the product type. The idea here is that a value is something that selects a function to handle which of the types the value is from.

A famous disjoint union is the two-valued boolean algebra, of two singleton types. In an optimized representation that doesn’t use the values from the singleton types,

$$\begin{array}{cccc}T& =x\mapsto y\mapsto x& F& =x\mapsto y\mapsto y\end{array}$$ so if $b$ is a boolean, an if statement looks like $\left(bxy\right)=\{\begin{array}{cc}x& \text{if}b=T\\ y& \text{if}b=F\end{array}$.^[5]

In the case of products and disjoint unions of more than two types, there is an obvious optimization that one can apply. For example, for $X\times Y\times Z$ we can use $x\mapsto y\mapsto z\mapsto pxyz$ as a constructor.

2.1. Representing lambda calculus terms

The point of introducing ADTs is that we can use them to represent lambda calculus terms within the lambda calculus itself. While it is true that technically a lambda calculus term is a string, we will be representing it in a tree form. In particular, we will represent the variation on lambda calculus terms from the end of the de Bruijn indexes section.

Let $L$ denote the type for a lambda calculus term, for which we give the following recursive ADT description

$$L=\top \bigsqcup L\bigsqcup L\bigsqcup (L\times L)$$ where the four terms correspond to $z$, successor, abstraction, and application. In particular, we’ll use these constructors:

• $zero=z\mapsto s\mapsto l\mapsto a\mapsto z$
• $\mathrm{succ}\left(e\right)=z\mapsto s\mapsto l\mapsto a\mapsto se$
• $\mathrm{abs}\left(m\right)=z\mapsto s\mapsto l\mapsto a\mapsto lm$
• $\mathrm{apply}(m,n)=z\mapsto s\mapsto l\mapsto a\mapsto amn$

As an example, the expression for $T$ can be expressed in this type as $\mathrm{abs}\left(\mathrm{abs}\right(\mathrm{succ}\left(zero\right)\left)\right)$.

If we have an expression $p$ from $L$, we can decompose it and convert it into a lambda calculus term. Write $I\left(p\right)$ for the corresponding term, the $I$ being for “interpretation.” This $I$ is a function outside the lambda calculus, but we will show the lambda calculus is powerful enough to implement it.

3. An interpreter

In this section we’ll derive a term $u$ such that when $p$ is an expression representing a lambda calculus term from the type $L$, then $up\equiv I\left(p\right)$. This interpreter is the lambda calculus equivalent of a universal machine, because it can take descriptions of lambda terms and convert them into actual lambda terms, compared to descriptions of Turing machines being run as actual Turing machines.

At a high level, the term looks like the following, in a pseudo-Haskell notation. We make the decision that free variables in $p$ evaluate to a diverging term. The env variable is a linked list of lambda calculus terms (actual terms, not representations of them).

u p := eval p empty
eval p env := case p of
    zero -> head env
    succ(e) -> eval e (tail env)
    abs(m) -> (x |-> eval m (push x env))
    app(m1, m2) -> (eval m1 env) (eval m2 env)
empty := nil |-> cons |-> nil
push x list := nil |-> cons |-> cons x list
head list := list fail (x |-> sublist |-> x)
tail list := list empty (x |-> sublist |-> sublist)
fail := fail

The way this works is that the eval function keeps track of an environment of all the substitutions from $\beta$-reduction. The interpretation of $\mathrm{abs}\left(m\right)$ is as an actual lambda abstraction that pushes the value of the bound x to the zeroth entry of the environment list. Furthermore, empty is the empty linked list, push is the constructor, and head and tail are convenience destructors, where head fails in the case the environment is an empty list.

I’m afraid I’m going to be lazy and not explicitly prove that $up\equiv I\left(p\right)$, but it is a matter of checking the equivalence relations (and the substitution rule). Note that we do not care about evaluation strategies because the point is just that $up$ is a lambda term in the right equivalence class.

Now, how do we deal with recursion when the lambda calculus does not seem to provide it? The $Y$ combinator is a way to let a term refer to itself, and its defining relation is that $Yf\equiv f\left(Yf\right)$. Thus, if a function needs to refer to itself, like in the factorial function

factorial n := if n <= 1
    then 1
    else n * factorial (n - 1)

we can transform it like so

factorial' fact n := if n <= 1
    then 1
    else n * fact (n - 1)
factorial := Y factorial'

where none of the definitions are self-referential. The trick is that

factorial n = Y factorial' n
            = factorial' (Y factorial') n
            = factorial' factorial n

where the equality signs actually mean equivalence, and hence factorial’ is able to refer to something that is equivalent to the factorial expression itself. This $Y$ combinator can actually be given as a lambda calculus term: $$Y=f\mapsto (x\mapsto f(xx\left)\right)(x\mapsto f(xx\left)\right)$$ The defining relation is not too difficult to check.

Let’s look at the fail function, which we could define as

fail := Y fail'
fail' f := f

hence fail is $Y(x\mapsto x)\equiv (x\mapsto (xx\left)\right)(x\mapsto (xx\left)\right)=\Omega$, the divergent term from before.

Let’s rewrite the definition for u to be non-self-referential, while also substituting in some of the definitions for linked lists.

u p := (Y eval') p (n |-> c |-> n)
eval' eval p env := case p of
  zero -> env omega (x |-> t |-> x)
  succ(e) -> eval e (env env (x |-> t |-> t))
  abs(m) -> (x |-> eval m (n |-> c |-> c x env))
  app(m1, m2) -> (eval m1 env) (eval m2 env)
omega := (x |-> x x) (x |-> x x)
Y f = (x |-> f (x x)) (x |-> f (x x))

For succ(e), there is a trick that if env is empty then by passing env as the first argument the expression is equivalent to the empty list in that case.

Now, to write this in an impenetrable way as a single lambda term:

u := expr |->
  ((f |-> (x |-> f (x x)) (x |-> f (x x)))
    (eval |-> p |-> env |->
     p (env ((x |-> x x) (x |-> x x)) (x |-> t |-> x))
       (e |-> eval e (env env (x |-> t |-> t)))
       (m |-> x |-> eval m (n |-> c |-> c x env))
       (m1 |-> m2 |-> (eval m1 env) (eval m2 env)))
  ) expr (n |-> c |-> n)

Or, if that was too clear, using de Bruijn indexes:

$$u=\lambda \left(\right(\lambda \left(\lambda 1\right(00\left)\right)\left(\lambda 1\right(00\left)\right)\left)\right(\lambda \lambda \lambda 1\left(0\right(\left(\lambda 00\right)\left(\lambda 00\right)\left)\right(\lambda \lambda 1\left)\right)\left(\lambda 30\right(11\left(\lambda \lambda 0\right)\left)\right)\left(\lambda \lambda 41\right(\lambda \lambda 024\left)\right)\left(\lambda \lambda \right(412\left)\right(402\left)\right)\left)\right)0\left(\lambda \lambda 1\right)$$ The point of this last exercise was just to make it obvious that $u$ can be represented as an expression $U$. If everything worked out, then in fact $uU\equiv u$.

If we do not care about the behavior for free variables, we could shorten this term by replacing $\Omega$ with something random, like $0$ for instance, which would have the effect of making free variables evaluate to the empty list.

It’s also possible to write a universal interpreter that enforces a particular reduction strategy, for example the Krivine machine^[6], with a short implementation by Scott Kovach.

4. A fixed-point theorem

Consider a lambda term $f$ with the property that for every lambda expression $p$ from $L$, $fp$ is equivalent to something in $L$. That is, $f$ can be thought of as an actual function $L\to L$. We will show that then $f$ has a fixed point with respect to $u$, namely that there is some expression $q$ from $L$ such that $u\left(fq\right)\equiv uq$. (The argument is adapted from the one presented here.^[7])

A key operator in the construction of $q$ is $\mathrm{quote}:L\to L$ which takes a lambda expression and produces a lambda expression that when evaluated is a term that is equivalent to that expression. It’s much less complicated to say in symbols: $u\mathrm{quote}\left(p\right)\equiv p$. We can (tediously) define this operator inductively.^[8]

• $\mathrm{quote}\left(zero\right)=\mathrm{abs}\left(\mathrm{abs}\right(\mathrm{abs}\left(\mathrm{abs}\right(\mathrm{succ}\left(\mathrm{succ}\right(\mathrm{succ}\left(zero\right)\left)\right)\left)\right)\left)\right)$
• $\mathrm{quote}\left(\mathrm{succ}\right(e\left)\right)=\mathrm{abs}\left(\mathrm{abs}\right(\mathrm{abs}\left(\mathrm{abs}\right(\mathrm{apply}\left(\mathrm{succ}\right(\mathrm{succ}\left(zero\right)),\mathrm{quote}(e\left)\right)\left)\right)\left)\right)$
• $\mathrm{quote}\left(\mathrm{abs}\right(m\left)\right)=\mathrm{abs}\left(\mathrm{abs}\right(\mathrm{abs}\left(\mathrm{abs}\right(\mathrm{apply}\left(\mathrm{succ}\right(zero),\mathrm{quote}(m\left)\right)\left)\right)\left)\right)$
• $\mathrm{quote}\left(\mathrm{apply}\right(m,n\left)\right)=\mathrm{abs}\left(\mathrm{abs}\right(\mathrm{abs}\left(\mathrm{abs}\right(\mathrm{apply}\left(\mathrm{apply}\right(zero,\mathrm{quote}\left(m\right)),\mathrm{quote}(n\left)\right)\left)\right)\left)\right)$

Hopefully it’s clear how to write down a lambda term that actually implements $\mathrm{quote}$, but it’s similar to the way the case expression in $u$ was implemented.

Let $s:L\to L$ be defined by $sp=\mathrm{apply}(p,\mathrm{quote}(p\left)\right)$, which creates an expression that represents supplying the representation of a lambda term to itself as an argument.

Let $m$ be the expression for $p\mapsto u\left(f\right(sp\left)\right)$, and let $q=sm$.

$$u\left(fq\right)\equiv u\left(f\right(sm\left)\right)\equiv (p\mapsto u(f\left(sp\right)\left)\right)m\equiv \left(um\right)m\equiv u\mathrm{apply}(m,\mathrm{quote}(m\left)\right)\equiv u\left(sm\right)\equiv uq.$$ Hence, $q$ is indeed a fixed point of $f$ with respect to $u$.

5. Quines

A quine is an expression $q$ in $L$ such that $uq\equiv q$.

Quines are the result of applying this fixed-point theorem to the $\mathrm{quote}$ operator. By that theorem, there is some $q$ in $L$ such that $u\mathrm{quote}\left(q\right)\equiv uq$, but since $u\mathrm{quote}\left(q\right)\equiv q$, we have obtained a quine.

What does this quine look like? We had that $m$ was the expression for $p\mapsto u\mathrm{quote}\left(\mathrm{apply}\right(p,\mathrm{quote}\left(p\right))$, but this simplifies to $p\mapsto \mathrm{apply}(p,\mathrm{quote}(p\left)\right)$, so we may let $m=\mathrm{abs}\left(\mathrm{apply}\right(\mathrm{apply}(A,zero),\mathrm{apply}(Q,zero)\left)\right)$, where $A$ is the lambda expression for $\mathrm{apply}$ and $Q$ is a lambda expression for $\mathrm{quote}$. Then, $q$ is $\mathrm{apply}(m,\mathrm{quote}(m\left)\right)$, which expanded a bit is

$$q=\mathrm{apply}\left(\mathrm{abs}\right(\mathrm{apply}\left(\mathrm{apply}\right(A,zero),\mathrm{apply}(Q,zero\left)\right)),\mathrm{quote}(\mathrm{abs}\left(\mathrm{apply}\right(\mathrm{apply}(A,zero),\mathrm{apply}(Q,zero)\left)\right)\left)\right)$$ It doesn’t seem like it would be too illuminating to expand this out anymore, but it is interesting that $u$ was eliminated so easily, suggesting the fixed-point theorem was tremendously overpowered for the purpose of deriving a quine.

Anyway, notice that the way $q$ works is that there is a code part and a data part, and that $Q$ is sort of like a print function. There’s sort of a parallel between the structure of $q$ and the Python program from the beginning.

6. In set theory

As I understand it, one of the ways to study ZFC set theory is by model theory, where a model is a set $M$ along with a relation $\left(\in \right)\subset M\times M$ that satisfies all of the axioms. Propositions of first-order logic can themselves be represented as sets (like how lambda terms can be represented in $L$ as lambda calculus terms), and there is a truth term that evaluates the truth of a particular proposition against a particular model.

Unfortunately there is no way to prove in ZFC that there is a model of ZFC (that’s Gödel’s second incompleteness theorem).

As an application of the idea in the fixed-point theorem, let’s show that there’s no absolute notion of Truth in ZFC. If you want, that there’s no truth term $\tau \left(p\right)$ that evaluates whether or not $p$ is a true proposition in the current model.

The idea is that we can use proposition-level functions defined on set representations of propositions. If $f:P\to P$ is a proposition-level function on the set of propositions $P$ (i.e., $\forall x\in P_1,\exists !y,y\in P_1\wedge f(x,y)$, where we will write $f\left(x\right)$ for this $y$ and leave it up to the reader to transform the first-order statement appropriately), then we can show that there is some statement $q\in P$ such that $\tau \left(f\right(q\left)\right)\iff \tau \left(q\right)$. Let $P_1$ be the set of set representations of propositions with one free variable (predicates). We can define proposition-level function $s:P_1\to P$ that feeds a predicate the representation of the predicate. Then, we can define a predicate $F\left(p\right)=\tau \left(f\right(s\left(p\right)\left)\right)$ and thus a proposition $q=s\left(F\right)\in P$, the required fixed point.

But, what if $f$ is the function $p\mapsto \neg p$ that negates a proposition? Then we have a proposition $q$ such that $\tau \left(\neg q\right)\iff \tau \left(q\right)$, so $\tau$ can’t possibly be a truth term in actuality. My intuition for what is going wrong is that $\tau$ seems like it would need to have an environment to keep track of all of the bound variables, but ZFC prevents you from having sets with arbitrary elements: you always have to specify a domain. Well, the domain would be the model, but you don’t have a way to gain direct access to the current model from within the model. If you did, you’d have Russell’s paradox.

A kind of fun modification to this is to say “well, ok, fine, there’s no $\tau \left(p\right)$ predicate, but we can still have have a universal truth predicate $T\left(p\right)=\forall M,\mathrm{model}\left(M\right)\Rightarrow \tau (p,M)$ that checks the truth across all models, since you can write down a predicate to check whether a set is a model of set theory, so what happens now?”^[9] Here’s what happens: the kind of argument above gives us a proposition $q$ such that $T\left(q\right)\iff T\left(\neg q\right)$. Gödel’s completeness theorem says that $T\left(p\right)$ is equivalent to $p$ being provable, and so $q$ being provable is equivalent to $\neg q$ being provable. So, if the theory is consistent, neither $q$ nor $\neg q$ are provable (the law of the excluded middle does not apply to provability). The theory is incomplete!