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.