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