8
$\begingroup$

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.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ 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? $\endgroup$
    – cody
    Commented Sep 29, 2015 at 19:26
  • 1
    $\begingroup$ 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? $\endgroup$
    – Damiano Mazza
    Commented Sep 30, 2015 at 20:18
  • $\begingroup$ What @DamianoMazza said. I tried to explain some of this in math.andrej.com/2016/01/04/… $\endgroup$
    – Andrej Bauer
    Commented Mar 13, 2017 at 13:51
  • $\begingroup$ @Andrej Bauer I can't believe you need all that stuff. Not to solve my issue. $\endgroup$
    – Andrea Asperti
    Commented Mar 13, 2017 at 14:16
  • $\begingroup$ Of course not, the relevant bit is just one paragraph in the beginning, explaining what it takes to have an acceptable coding of syntax. $\endgroup$
    – Andrej Bauer
    Commented Mar 19, 2017 at 18:25

2 Answers 2

Reset to default
5
$\begingroup$

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".
Improve this answer
$\endgroup$
4
$\begingroup$

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?

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.