[Solved]: A quine in pure lambda calculus

Problem Detail: 

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

Asked By : Nathaniel

Answered By : Roy O.

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/21367