¿Cómo establecer la idoneidad de una codificación del cálculo lambda en sí misma?

8

M M EMMME

EM=βM.

Hay una variedad de codificaciones como la de Kleene que usa números naturales y la codificación moderna más eficiente es una sintaxis de orden superior de Mogensen. Otra posible codificación (trivial) es la función de identidad, luego el intérprete es nuevamente la función de identidad.

¿Existe alguna noción razonable de una "codificación adecuada" que prohíba las codificaciones triviales?

Esta pregunta surgió al considerar el problema de detención aplicado al cálculo lambda en lugar de a las máquinas de Turing: si se indica en términos de codificación trivial, entonces se mantiene por la razón trivial de que esencialmente no hay nada que podamos hacer con un término lambda citado.

Dicho de otra manera: ¿Cuál es el conjunto de funciones que deberíamos esperar poder calcular en términos lambda citados?

Puedo enumerar algunos como: contar la profundidad del término, tomar subterms, decir si el nodo raíz de un término es una lambda o una aplicación, ... pero dudaría en definir una "codificación adecuada" simplemente enumerando una variedad de funciones eso me vino a la mente.

Brennan.Tobias
fuente
1
Elija una "codificación adecuada" concreta (por ejemplo, la que da Kleene). Supongamos que una codificación es adecuada si hay un -term tomando un codificados en término a la codificación Kleene. Esto es un poco tonto, pero ¿funcionaría para tus propósitos? λ ι ι ( M )ιλιι(M)
cody
1
Creo que en realidad enumeró las operaciones clave: decir el tipo de término (variable, abstracción, aplicación) y, cuando corresponda, tomar subterms. El único punto delicado es la unión de lambdas, pero puede hacerlo utilizando la notación de Bruijn. Cualquier otra operación razonable (por ejemplo, contar la profundidad) se deduce de estos, porque puede deconstruir completamente un término. ¿Estarías de acuerdo?
Damiano Mazza
Lo que dijo @DamianoMazza. Traté de explicar algo de esto en math.andrej.com/2016/01/04/…
Andrej Bauer
@Andrej Bauer No puedo creer que necesites todas esas cosas. No para resolver mi problema.
Andrea Asperti
Por supuesto que no, el bit relevante es solo un párrafo al principio, explicando lo que se necesita para tener una codificación de sintaxis aceptable.
Andrej Bauer

Respuestas:

5

Como señalaron otros, la definición obvia de una codificación "adecuada" es que es equitranslatable con cualquier estándar. Por lo tanto, la cuestión es caracterizar tales codificaciones en términos de propiedades más elementales.

( Nota histórica . Smullyan estudió esta pregunta en el contexto de la lógica combinatoria. Cuando era estudiante, Henk Barendregt me sugirió las conjeturas de Smullyan como un problema de investigación, lo que condujo a mi primera publicación científica).

http://drops.dagstuhl.de/opus/volltexte/2011/3249/

Para resumir, dado un mapa , consideramos si existen combinadores que satisfagan ciertas propiedades. Los más significativos son:¯:ΛΛ

  • AM¯N¯=MN¯
  • BM¯=M¯¯
  • PiM0M1¯=Mi¯,i{0,1}
  • ZbM¯={λxy.xMb{I,K,S}λxy.yotherwise
  • ΔM¯N¯={λxy.xMNλxy.yotherwise
  • UM¯=M¯s , donde es una codificación estándar¯s
  • U1M¯s=M¯

Es fácil ver que cualquier codificación adecuada tiene estas propiedades. El principal resultado del trabajo (Corolario 14) es que, para una codificación adecuada, uno de los siguientes es suficiente:

  • A+Δ ;
  • U1+Δ ;
  • U1+Pi+Zb ;
  • ¯ Pi+Zb+ "el rango de está contenido en un conjunto recursivamente enumerable y hay un combinador que decide si un elemento dado de este conjunto está en el rango o no".¯
Andrew Polonsky
fuente
4

Esta no es una respuesta. Es una elaboración de la pregunta, que me parece interesante y quizás debería merecer más atención de la que realmente recibió.

En primer lugar, permítanme decir que hay una condición importante en la definición de Barendregt que Brennan ha omitido, a saber, que debe estar en forma normal , que inmediatamente descarta la función de identidad como una codificación adecuada.M

Ahora, la pregunta puede formularse con mayor precisión siguiendo la sugerencia de Cody.

Dadas dos codificaciones, ¿son recursivamente isomorfas? En otras palabras, suponga que tiene dos codificaciones tales que

F

𝖤1M1=βMand𝖤2M2=βM
¿existe un término lambda tal que para cualquier términoFM

E2(FM1)=βM
y viceversa?

Si la respuesta no es, ¿cuáles son los requisitos abstractos "mínimos" que deben agregarse para asegurarlo?

Andrea Asperti
fuente