A quine in pure lambda calculus

Question

I would like an example of a quine in pure lambda calculus. I was quite surprised that I couldn't find one by googling. The quine page lists quines for many "real" languages, but not for lambda calculus.

Of course, this means defining what I mean by a quine in the lambda calculus, which I do below. (I'm asking for something quite specific.)

In a few places, e.g. Larkin and Stocks (2004), I see the following quoted as a "self-replicating" expression: $(\lambda x.x \; x)\;(\lambda x.x \; x)$. This reduces to itself after a single beta-reduction step, giving it a somehow quine-like feel. However, it's un-quine-like in that it doesn't terminate: further beta-reductions will keep producing the same expression, so it will never reduce to normal form. To me a quine is a program that terminates and outputs itself, and so I would like a lambda expression with that property.

Of course, any expression that contains no redexes is already in normal form, and will therefore terminate and output itself. But that's too trivial. So I propose the following definition in the hope that it will admit a non-trivial solution:

definition (tentative): A quine in lambda calculus is an expression of the form $$(\lambda x . A)$$ (where $A$ stands for some specific lambda calculus expression) such that $((\lambda x . A)\,\, y)$ becomes $(\lambda x . A)$, or something equivalent to it under changes of variable names, when reduced to normal form, for any input $y$.

Given that the lambda calculus is as Turing equivalent as any other language, it seems as if this should be possible, but my lambda calculus is rusty, so I can't think of an example.

Reference

James Larkin and Phil Stocks. (2004) "Self-replicating expressions in the Lambda Calculus" Conferences in Research and Practice in Information Technology, 26 (1), 167-173. http://epublications.bond.edu.au/infotech_pubs/158

Answer 1

You want a term $Q$ such that $\forall M \in \Lambda$:

$$QM \rhd_\beta Q$$

I will specify no further restrictions on $Q$ (e.g. regarding its form and whether it is normalising) and I will show you that it definitely must be non-normalising.

1. Assume $Q$ is in normal form. Choose $M \equiv x$ (we can do so because the theorem needs to hold for all $M$). Then there are three cases.

   • $Q$ is some atom $a$. Then $QM \equiv ax$. This is not reducible to $a$.
   • $Q$ is some application $(RS)$. Then $QM \equiv (RS)x$. $(RS)$ is a normal form by hypothesis, so $(RS)x$ is also in normal form and not reducible to $(RS)$.
   • $Q$ is some abstraction $(\lambda x.A)$ (if $x$ is supposed to be free in $A$, then for simplicity we can just choose $M$ equivalent to whatever variable $\lambda$ abstracts over). Then $QM \equiv (\lambda x.A)x \rhd_\beta A[x/x] \equiv A$. Since $(\lambda x.A)$ is in normal form, so is $A$. Consequently we cannot reduce $A$ to $(\lambda x.A)$.

   So if such a $Q$ exists, it cannot be in normal form.

2. For completeness, suppose $Q$ has a normal form, but is not in normal form (perhaps it is weakly normalising), i.e. $\exists N \in \beta\text{-nf}$ with $N \not\equiv Q$ such that $\forall M \in \Lambda$: $$QM \rhd_\beta Q \rhd_\beta N$$

   Then with $M \equiv x$ there must also be exist a reduction sequence $Qx \rhd_\beta Nx \rhd_\beta N$, because:

   • $Qx \rhd_\beta Nx$ is possible by the fact that $Q \rhd_\beta N$.
   • $Nx$ must normalise since $N$ is a $\beta$-nf and $x$ is just an atom.
   • If $Nx$ were to normalise to anything other than $N$, then $Qx$ has two $\beta$-nfs, which is not possible by a corollary to the Church-Rosser theorem. (The Church-Rosser theorem essentially states that reductions are confluent, as you probably already know.)

   But note that $Nx \rhd_\beta N$ is not possible by argument (1) above, so our assumption that $Q$ has a normal form is not tenable.

3. If we permit such a $Q$, then, we are certain that it must be non-normalising. In that case we can simply use a combinator that eliminates any argument it receives. Denis's suggestion works just fine: $$Q \equiv (\lambda z.(λx.λz.(x x)) (λx.λz.(x x)))$$ Then in only two $\beta$-reductions: \begin{align} QM &\equiv (\lambda z.(λx.λz.(x x)) (λx.λz.(x x))) M \\ & \rhd_{1\beta} (λx.λz.(x x)) (λx.λz.(x x)) \\ & \rhd_{1\beta} (λz.((λx.λz.(x x))(λx.λz.(x x))) \\ & \equiv Q \end{align}

This result is not very surprising, since you are essentially asking for a term that eliminates any argument it receives, and this is something I often see mentioned as a direct application of the fixed-point theorem.

Answer 2

One one hand this is impossible, because a quine is supposed to output its own code, and the pure lambda calculus has no means for performing output.

On the other hand, if you assume that the resulting term is the output, then every normal form is a quine.

For example, lambda term $(\lambda x. x)$ is already a normal form, then assuming that its output is the resulting normal form, the output is $(\lambda x. x)$. Thus $(\lambda x. x)$ is a quine.

Answer 3

Here is a proposition:

We choose $A$ to be a fixpoint of the function $f=\lambda t. (\lambda z.t)$.

This can be done by using the fixpoint combinator $Y=\lambda g.((\lambda x.g\ (x\ x))\ (\lambda x.g\ (x\ x)))$, and setting $A=Y f=(\lambda x.\lambda z.(x\ x))\ (\lambda x.\lambda z.(x\ x)) $.

Now we show that $A$ is a quine. Indeed $A$ reduces to $\lambda z.A$, so it means that for any $y$, $(\lambda z.A)y \to_\beta A \to_\beta (\lambda z.A)$.