Como declarar a adequação de uma codificação do cálculo lambda em si?

No artigo Discriminando termos lambda codificados - Henk Barendregt, um codificador de um termo lambda M é um termo tal que M (e suas partes) podem ser reconstruídas a partir dele de maneira definível por lambda. Essencialmente, precisamos ser capazes de escrever um auto-intérprete \ mathsf E :$\ulcorner M \urcorner$$M$$M$$\mathsf E$

Há uma variedade de codificações como a de Kleene, que usa números naturais e a codificação moderna mais eficiente é uma sintaxe de ordem superior de Mogensen. Outra codificação possível (trivial) é a função de identidade, então o intérprete é novamente a função de identidade.

Existe alguma noção razoável de uma "codificação adequada" que proíba as codificações triviais?

Essa pergunta surgiu ao considerar o problema de parada aplicado ao cálculo lambda em vez de máquinas de Turing: se declarado em termos de codificação trivial, é válido pelo motivo trivial de que não há essencialmente nada que possamos fazer com um termo lambda citado.

Em outras palavras: Qual é o conjunto de funções que deveríamos esperar poder computar nos termos lambda citados?

Posso listar algumas coisas como: contar a profundidade do termo, obter subtermos, dizer se o nó raiz de um termo é um lambda ou aplicativo, ... mas hesitaria em definir uma "codificação adequada" apenas listando várias funções isso veio à mente.

Como apontado por outros, a definição óbvia de uma codificação "adequada" é que ela é equitranslutável a qualquer codificação padrão. A questão é, portanto, caracterizar essas codificações em termos de propriedades mais elementares.

( Nota histórica . Smullyan estudou essa questão no contexto da lógica combinatória. Quando eu era estudante, Henk Barendregt sugeriu as conjecturas de Smullyan para mim como um problema de pesquisa - o que levou à minha primeira publicação científica.)

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

Para resumir, dado um mapa , consideramos se existem combinadores que satisfazem determinadas propriedades. Os mais significativos são:$\code{\cdot} : \Lambda \to \Lambda$

• $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$ , onde é uma codificação padrão$\code{\cdot}^s$
• $U^{-1}\, \code{M}^s = \code{M}$

É fácil ver que qualquer codificação adequada possui essas propriedades. O principal resultado do artigo (Corolário 14) é que, para uma codificação adequada, basta um dos seguintes:

• $A + \Delta$ ;
• $U^{-1} + \Delta$ ;
• $U^{-1} + P_i + Z_b$ ;
• $P_i + Z_b +$ "o intervalo de está contido em um conjunto recursivamente enumerável e existe um combinador que decide se um determinado elemento desse conjunto está ou não no intervalo".$\code{\cdot}$

Esta não é uma resposta. É uma elaboração da pergunta, que me parece interessante e talvez deva merecer mais atenção do que realmente recebeu.

Antes de mais, deixe-me dizer que existe uma condição importante na definição de Barendregt que foi omitida por Brennan, a saber, o fato de o estar na forma normal , que exclui imediatamente a função de identidade como uma codificação adequada.$\lceil M \rceil$

Agora, a questão pode ser formulada com mais precisão, seguindo a sugestão de Cody.

Dadas duas codificações, elas são recursivamente isomórficas? Em outras palavras, suponha que haja duas codificações, de modo que

Se a resposta não for, quais são os requisitos abstratos "mínimos" que devem ser adicionados para garantir isso?