How to state the adequacy of an encoding of lambda calculus in itself? In the paper Discriminating coded lambda terms - Henk Barendregt a coding $\ulcorner M \urcorner$ of a lambda term $M$ is a term such that $M$ (and its parts) can be reconstructed from it in a lambda-definable way. Essentially we need to be able to write a self-interpreter $\mathsf E$:

$$\mathsf E \ulcorner M \urcorner =_\beta M.$$

There are a variety of encodings like Kleene's which uses natural numbers and the most efficient modern encoding is a higher-order syntax by Mogensen. Another possible (trivial) encoding is the identity function, then the interpreter is again the identity function.


  Is there any reasonable notion of an "adequate encoding" that outlaws trivial encodings?


This question came up when considering the halting problem applied to lambda calculus rather than Turing machines: If stated in terms of the trivial encoding then it holds for the trivial reason that there is essentially nothing we can do with a quoted lambda term.

Put differently: What is the set of functions that we should expect to be able to compute on quoted lambda terms?

I can list a few like: counting the depth of the term, taking subterms, telling if the root node of a term is a lambda or application, ... but I would hesitate to define an "adequate encoding" by just listing assorted functions that came to mind.
As pointed out by others, the obvious definition of an "adequate" coding is that it is equitranslatable with any standard one.  The question is therefore to characterize such codings in terms of more elementary properties.

(Historical note.  Smullyan studied this question in the context of combinatory logic.  When I was a student, Henk Barendregt suggested Smullyan's conjectures to me as a research problem -- which led to my first scientific publication.)  See

http://drops.dagstuhl.de/opus/volltexte/2011/3249/
$\newcommand{\code}[1]{\overline{#1}}$

To summarize, given a map $\code{\cdot} : \Lambda \to \Lambda$, we consider whether there exist combinators satisfying certain properties.  The most significant ones are:


$A\, \code{M}\, \code{N} = \code{MN}$
$B\, \code{M} = \code{\code{M}}$
$P_i\, \code{M_0 M_1} = \code{M_i},\quad i \in \{0,1\}$
$Z_b\, \code{M} = \begin{cases} \lambda x y.x &amp;M \equiv b \in \{I,K,S\}\\
\lambda xy.y &amp;otherwise
\end{cases}$
$\Delta\, \code{M}\, \code{N} = \begin{cases}
\lambda x y. x &amp;M \equiv N\\
\lambda x y.y &amp;otherwise
\end{cases}$
$U\, \code{M} = \code{M}^s$, where $\code{\cdot}^s$ is some standard coding
$U^{-1}\, \code{M}^s = \code{M}$


It is easy to see that any adequate coding has these properties.  The main result of the paper (Corollary 14) is that, for an adequate coding, one of the following suffices:


$A + \Delta$;
$U^{-1} + \Delta$;
$U^{-1} + P_i + Z_b$;
$P_i + Z_b + $ "the range of $\code{\cdot}$ is contained in a recursively enumerable set and there is a combinator that decides whether a given element of this set is in the range or not".