<p>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.</p>

<p>(<em>Historical note</em>.  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</p>

<p><a href="http://drops.dagstuhl.de/opus/volltexte/2011/3249/" rel="noreferrer">http://drops.dagstuhl.de/opus/volltexte/2011/3249/</a>
$\newcommand{\code}[1]{\overline{#1}}$</p>

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

<ul>
<li>$A\, \code{M}\, \code{N} = \code{MN}$</li>
<li>$B\, \code{M} = \code{\code{M}}$</li>
<li>$P_i\, \code{M_0 M_1} = \code{M_i},\quad i \in \{0,1\}$</li>
<li>$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}$</li>
<li>$\Delta\, \code{M}\, \code{N} = \begin{cases}
\lambda x y. x &amp;M \equiv N\\
\lambda x y.y &amp;otherwise
\end{cases}$</li>
<li>$U\, \code{M} = \code{M}^s$, where $\code{\cdot}^s$ is some standard coding</li>
<li>$U^{-1}\, \code{M}^s = \code{M}$</li>
</ul>

<p>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:</p>

<ul>
<li>$A + \Delta$;</li>
<li>$U^{-1} + \Delta$;</li>
<li>$U^{-1} + P_i + Z_b$;</li>
<li>$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".</li>
</ul>

CC BY-SA 3.0
2017-03-18T14:21:32.257Z
2017-03-18T14:21:32.257Z
Andrew Polonsky
<p>This is not an answer. It is an elaboration of the question, that looks interesting to me and maybe should deserve more attention than it actually received.</p>

<p>First of all, let me say that there is an important condition in Barendregt's definition that has been omitted by Brennan, namely the fact that $\lceil M \rceil$ must be in <em>normal</em> <em>form</em>, that immediately rules out the identity function as an adequate encoding. </p>

<p>Now, the question can be more precisely formulated following Cody's suggestion.</p>

<p>Given two encodings, are they recursively isomorphic?
In other words, suppose to have two encodings such that</p>

<p>$$_1 \lceil M \rceil_1 =_\beta M  \hspace{1cm} and \hspace{1cm}_2 \lceil M \rceil_2 =_\beta M$$ 
does it exists a lambda term $F$ such that for any term $M$ </p>

<p>$$E_2 (F \lceil M \rceil_1) =_\beta M$$
and vice-versa?</p>

<p>If the answer is not, what are the "minimal" abstract requirements that must be added to ensure it?</p>

CC BY-SA 3.0
2017-03-13T10:07:32.800Z
2017-03-13T10:07:32.800Z
Andrea Asperti
<p>In the paper <strong>Discriminating coded lambda terms - Henk Barendregt</strong> a <em>coding</em> $\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$:</p>

<p>$$\mathsf E \ulcorner M \urcorner =_\beta M.$$</p>

<p>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.</p>

<blockquote>
  <p>Is there any reasonable notion of an "adequate encoding" that outlaws trivial encodings?</p>
</blockquote>

<p>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.</p>

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

<p>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.</p>

CC BY-SA 3.0
2015-09-29T19:26:14.197Z
Pick a given concrete "adequate encoding" (say, the one given by Kleene). Say that an encoding $\iota$ is adequate if there is a $\lambda$-term taking a $\iota$-encoded term $\iota(M)$ to the Kleene encoding. This is a bit silly, but would this work for your purposes?
cody
CC BY-SA 3.0
2015-09-30T20:18:41.007Z
I think you actually listed the key operations: telling the kind of term (variable, abstraction, application) and, where appropriate, taking subterms.  The only delicate point is representing the binding of lambdas, but you can do that using de Bruijn notation.  Any other reasonable operation (for instance, counting the depth) follows from these, because you are able to completely deconstruct a term.  Would you agree?
Damiano Mazza
CC BY-SA 3.0
2017-03-13T13:51:22.380Z
What @DamianoMazza said. I tried to explain some of this in http://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/
Andrej Bauer
CC BY-SA 3.0
2017-03-13T14:16:42.480Z
@Andrej Bauer I can't believe you need all that stuff. Not to solve my issue.
Andrea Asperti
CC BY-SA 3.0
2017-03-19T18:25:00.250Z
Of course not, the relevant bit is just one paragraph in the beginning, explaining what it takes to have an acceptable coding of syntax.
Andrej Bauer
<lambda-calculus><encoding>
How to state the adequacy of an encoding of lambda calculus in itself?
Brennan.Tobias
# How to state the adequacy of an encoding of lambda calculus in itself?

(Asked by: username_0 on 2015-09-29)

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.

**Tags:** lambda-calculus, encoding
> **Comments:**
> **username_1**: Pick a given concrete "adequate encoding" (say, the one given by Kleene). Say that an encoding $\iota$ is adequate if there is a $\lambda$-term taking a $\iota$-encoded term $\iota(M)$ to the Kleene encoding. This is a bit silly, but would this work for your purposes?  
> **username_2**: I think you actually listed the key operations: telling the kind of term (variable, abstraction, application) and, where appropriate, taking subterms.  The only delicate point is representing the binding of lambdas, but you can do that using de Bruijn notation.  Any other reasonable operation (for instance, counting the depth) follows from these, because you are able to completely deconstruct a term.  Would you agree?  
> **username_3**: What @DamianoMazza said. I tried to explain some of this in http://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/  
> **username_4**: @Andrej Bauer I can't believe you need all that stuff. Not to solve my issue.  
> **username_3**: Of course not, the relevant bit is just one paragraph in the beginning, explaining what it takes to have an acceptable coding of syntax.  

---

## 2 answers

### Answer by username_5 on 2017-03-18. Score: 5

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 &M \equiv b \in \{I,K,S\}\\
  \lambda xy.y &otherwise
  \end{cases}$
* $\Delta\, \code{M}\, \code{N} = \begin{cases}
  \lambda x y. x &M \equiv N\\
  \lambda x y.y &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".


---

### Answer by username_4 on 2017-03-13. Score: 4

This is not an answer. It is an elaboration of the question, that looks interesting to me and maybe should deserve more attention than it actually received.

First of all, let me say that there is an important condition in Barendregt's definition that has been omitted by Brennan, namely the fact that $\lceil M \rceil$ must be in *normal* *form*, that immediately rules out the identity function as an adequate encoding.

Now, the question can be more precisely formulated following Cody's suggestion.

Given two encodings, are they recursively isomorphic?
In other words, suppose to have two encodings such that

$$\_1 \lceil M \rceil\_1 =\_\beta M \hspace{1cm} and \hspace{1cm}\_2 \lceil M \rceil\_2 =\_\beta M$$
does it exists a lambda term $F$ such that for any term $M$

$$E\_2 (F \lceil M \rceil\_1) =\_\beta M$$
and vice-versa?

If the answer is not, what are the "minimal" abstract requirements that must be added to ensure it?


---

