I would like an example of a quine in pure lambda calculus. I was quite surprise
ID: 654433 • Letter: I
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: (?x.xx)(?x.xx). 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
(?x.A)
(where A stands for some specific lambda calculus expression) such that ((?x.A)y) becomes (?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
Explanation / Answer
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 (?x.x) is already a normal form, then assuming that its output is the resulting normal form, the output is (?x.x). Thus (?x.x) is a quine.