[Solved]: A quine in pure lambda calculus

ignougroup
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 betatext{-nf}$ with $N notequiv 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_{1beta} (λx.λz.(x x)) (λx.λz.(x x)) & rhd_{1beta} (λ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