Existe abundante información sobre cómo codificar la aritmética a partir del cálculo lambda. El artículo de wikipedia sobre Codificación eclesiástica parece completa para mi ojo inexperto. Mi pregunta es "¿y en la otra dirección?". ¿Cuál es una buena manera de codificar el cálculo lambda en aritmética real o entera ordinaria (o incluso matricial)? Parece que una aplicación de Numeración de Godel lo haría, pero no he podido encontrar ningún escrito sobre la numeración de Godel para el cálculo lambda específicamente. También parece plausible codificar el cálculo lambda en aritmética de alguna forma más eficiente que la numeración de Godel; ¿quizás alguien lo haya hecho? Yo me conformaría con el Cálculo SKI o algún otro lenguaje Turing-completo que sea más fácil de codificar que el cálculo lambda.
Respuestas
¿Demasiados anuncios?
No es una cuestión en la que la gente se preocupe mucho por la eficiencia. Cuando uno contempla aplicación de el cálculo lambda en la práctica, el modelo objetivo no suele ser uno de aritmética sobre un único entero enorme a la vez, sino un modelo más realista como una RAM con tamaño de palabra acotado. Y entonces estarías pensando en términos de punteros y estructuras de datos enlazadas (o quizás incluso secuencias de bytes) en lugar de aritmetización.
Por otro lado, por consideraciones puramente teóricas, los números de Gödel hacen el trabajo lo suficientemente bien como para que un esquema mejorado no sea realmente una cuestión publicable.
Sin embargo, para fines "recreativos", lo que harías es empezar seleccionando alguna función de emparejamiento $f:\mathbb N\times\mathbb N\hookrightarrow\mathbb N$ . Hay varias opciones que logran diferentes equilibrios entre la eficacia de la representación y lo engorrosos que son de codificar y descodificar.
Una vez que lo tengas, un plan podría ser representar términos lambda con Índices de Bruijn :
$$ \begin{align} [\![ M N ]\!] &= 3 f( [\![ M ]\!], [\![ N ]\!] ) \\ [\![ \lambda . M ]\!] &= 1+3 [\![ M ]\!] \\ [\![ v^n ]\!] &= 2 + 3n \end{align} $$ (recuérdese que con los índices de Bruin, la variable en un enlazador lambda es implícita, y un incidencia de una variable se representa como el número de otros ligantes anidados entre el ligante y la ocurrencia ligada de la variable. Aquí estoy mostrando que como $v^n$ que significa "la variable vinculada $n$ niveles por encima de aquí" -- algunas fuentes, como el artículo de Wikipedia, sólo utilizan el número $n$ como sintaxis para la aparición de una variable).
La notación De Bruijn es conveniente para manipular términos lambda, porque se abstrae de $\alpha$ -pero si prefieres representar los términos lambda de forma más parecida a como se ven escritos, puedes hacer lo siguiente $$ \begin{align} [\![ M N ]\!] &= 3 f( [\![ M ]\!], [\![ N ]\!] ) \\ [\![ \lambda x_n . M ]\!] &= 1+3 f( n, [\![ M ]\!] ) \\ [\![ x_n ]\!] &= 2 + 3n \end{align} $$
Alternativamente, se podría representar un cálculo combinatorio como $\mathbf{SKI}$ como usted propone: $$ \begin{align} [\![ \mathbf I ]\!] &= 0 \\ [\![ \mathbf K ]\!] &= 1 \\ [\![ \mathbf S ]\!] &= 2 \\ [\![ M N ]\!] &= 3 + f( [\![ M ]\!], [\![ N ]\!] ) \end{align} $$
Las posibilidades son prácticamente infinitas. Y tenga en cuenta que todo esto tiene tanto sentido para representar a fórmulas lógicas como en el caso de los términos lambda. La prevalencia de las factorizaciones primos en la literatura sobre aritmetización incluso en entornos lógicos es en gran medida sólo una cuestión de inercia y el legado del trabajo original de Gödel. Desde un punto de vista técnico, una codificación más estructurada como las anteriores funcionaría igual de bien.
Un punto a favor de utilizar una codificación basada en secuencias de símbolos (como los números trandicionales de Gödel) en lugar de uno basado en estructuras de árbol (como arriba) es que -supuestamente- facilita convencer a un lector no iniciado de que lo que ocurre en la aritmética es, en efecto, exactamente lo mismo que se puede hacer mecánicamente con símbolos en papel. Sin embargo, eso depende de los antecedentes del supuesto lector. Por ejemplo, si escribimos para un público especializado en ciencias de la computación, lo más probable es que les resulte más natural pasar directamente a los árboles.
