# A quine in pure lambda calculus

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

• Not an answer to my question, but for my own future reference (and for future visitors) it will be useful to have a link to wiki.haskell.org/Combinatory_logic , in which someone has much deeper thoughts about quines than I did. – Nathaniel May 15 '16 at 10:04
• Note that a quine needs to produce its own source code. Producing the function it represents is not sufficient. – PyRulez Dec 14 '18 at 20:49
• @PyRulez what is the source code for a lambda expression? If it's a sequence of characters then it's impossible for a lambda expression to output it, and consequently we can define the word "quine" to mean something slightly different for lambda expressions without fear of ambiguity. On the other hand, if you think of the source code as being the lambda expesssion itself then "the source code" and "the function it represents" are the same thing. So I think I'm ok here. – Nathaniel Dec 15 '18 at 2:42
• there is a church encoding for strings. A lambda calculus quine should output the church encoding of the string of characters representing it. – PyRulez Dec 15 '18 at 4:20
• Sure, that is not hard to do, if you define it that way. This question was about a different thing. – Nathaniel Dec 15 '18 at 9:04

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.

• If I could accept Denis' answer as well then I would, but (after I'd learned a bit more and was able to fully understand it) it was this answer that really convinced me that this "quine combinator" cannot be implemented by a lambda expression in normal form. – Nathaniel May 15 '16 at 5:43

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.

• That's an interesting point. In the question I tried to give a definition of what might count as a non-trivial quine in lambda calculus: a function that, when applied to any input, beta-reduces to itself (up to variable name substitutions). It might be that this is impossible, but it's not obvious, at least to me. – Nathaniel Feb 6 '14 at 10:58

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)$.

• This is pretty neat, and answers the question as I asked it, so I feel bad for not accepting it --- but unfortunately I made a slight mistake in specifying what I want. I actually want $(\lambda z.A)\;y$ to become $(\lambda z.A)$ when reduced to normal form, not just after a beta reduction step. (See the updated question for why.) This means that $A$ can't contain any redexes, because if it does then the reduction will not terminate. – Nathaniel Feb 7 '14 at 5:03
• Ah in this case i'm pretty sure it is impossible, because of the following intuition (not a proof but almost): you want $y$ to play no role since it has to work for every $y$, so $y$ should not be free in $A$. Then $(\lambda z.A)y$ just reduces to $A$. Now you want $A$ to reduce to $\lambda z.A$. This last expression cannot be a normal form, since the $A$ inside can again be reduced... – Denis Feb 7 '14 at 13:28
• This behaviour is not very surprising, because thince the "printing" of $\lambda-calculus$ are again instructions, a quine printing its own code is always executable. What you are asking is similar to asking for a quine such that if you execute the output, it prints nothing (which is impossible by definition). – Denis Feb 7 '14 at 13:32
• Ahh, you're right of course. I should have seen that. I'm not sure whether to accept your answer or edit the question to ask for a better definition. I'll give it a bit of thought. (It still seems to me that it should be possible to give a non-trivial definition where you're asking for something that will terminate, but I'm not sure how.) – Nathaniel Feb 9 '14 at 5:42
• Though having said that, is it really true that $z$ (I assume you mean $z$) has to not be free in $A$? E.g. $A$ could be something along the lines of if z==p then return q, otherwise return q. (Pseudocode because I'm not sure if it's even possible to define the equality operator for arbitrary expressions in lambda calculus, but I think you see what I mean.) – Nathaniel Feb 9 '14 at 5:55