Secuenciación o paso de continuación en cálculo lambda puro

Question

Estoy tratando de resolver el siguiente ejercicio dado aquí.

Considere la siguiente representación numérica.¿Cómo definir la suma?

|0| = λx.x
|1| = λx.λx.x
 ...
|n + 1| = λx.|n|

Los operadores sucesores y predecesores son fáciles de definir:

Succ n = λx.n
Pred n = n (λx.x)

Una solución "obvia" para definir la suma es utilizar la operación sucesora más la prueba de cero junto con el combinador de punto fijo, algo así como (YF) para F indicado a continuación (el operador si y los booleanos se definen como de costumbre):

F = λf.(λm n. if (Is0 m) n (Succ (f (Pred m) n))

Pero definiendo Is0 parece no trivial.El problema es que un número |norte| consume N+1 argumentos y N argumentos simplemente los borra.Por lo tanto, si aplico dicha función, parece razonable detener su aplicación cuando quede claro que el número, p.e.No es una identidad.Supongo que es una especie de continuación, pero no puedo imaginar cómo modelarlo en el cálculo lambda puro.¿Quizás alguien conozca algún consejo que pueda ayudar?

Un operador de secuenciación también puede ayudar a definir la suma.Si una aplicación de un número |metro| se retrasa hasta un numeral |norte| es aplicado a todo sus argumentos, el resultado será exactamente un numeral |n+m|.¿Quizás exista una variante de dicho combinador de secuenciación en el cálculo lambda puro?

La respuesta proporcionada por el autor del ejercicio utiliza una operación no pura (es decir, EsProcedimiento que comprueba si su argumento es una función).

ACTUALIZACIÓN: No es difícil hacer un CPS en cálculo lambda (los detalles para CBV se pueden encontrar aquí).Parece que eso no es suficiente para resolver el problema.

UPD:Si tenemos alguna versión de evaluación de cotización funciones para el cálculo lambda puro, entonces debe haber una función $eq$, que reconoce si las expresiones lambda citadas son sintácticamente iguales y podemos construir Is0 usando $eq$.Pero lo dudo $eq$ es definible.La razón es el "lema de genericidad" (libro de Barendregt, lema 14.3.24).Si pudiéramos probar la igualdad en los términos lambda citados, entonces ($eq$ (Cita $\Omega$) (Cita $\lambda x.x$)) volvería $falso$, y la genericidad implica que ($eq$ (Cita $\lambda x.x$) (Cita $\lambda x.x$)) también regresaría $falso$.¿Eso contradice la posibilidad de construir Cita en el cálculo lambda puro?

Answer 1

No creo que encuentres lo que buscas en el cálculo lambda puro.La clave es esta declaración que hiciste:

Un operador de secuenciación también puede ayudar a definir la suma.Si una aplicación de un número | M | se retrasa hasta un número | n | se aplica a todos sus argumentos, ...

Bueno, se supone que los modelos del cálculo lambda son como:

$$U \cong U^U$$

Y el punto de este es que cada valor semántico $u \en U$ puede aplicarse a algo.Por lo tanto, no tiene sentido hablar de que algo se "aplique a todos sus argumentos". No hay ningún valor que no se pueda aplicar a más argumentos en el cálculo de lambda puro.

No conozco un modelo/argumento de que esta representación de los naturales haga imposible su implementación. IsZero, aunque si lo pensamos un poco, parece poco probable.Sin embargo, para que sea posible en el cálculo lambda puro, tendrá que tener sentido semánticamente y no basarse en nociones que sean sólo sintácticas.

Editar:He aquí un esbozo de un argumento.una definición de $\mathsf{EsCero}$ eventualmente debe reducirse como:

$$\mathsf{IsZero}\ n ightsquigarrow^* n \overrightarrow v$$

La razón es que aplicar a una cierta cantidad de valores es el único mecanismo en el cálculo lambda para distinguir realmente entre números.Debe darse el caso de que: $$0 \overrightarrow v = \mathsf{true} \\ \mathsf{s}n \overrightarrow v = \mathsf{false}$$ Sin embargo, por cada $\overrightarrowv$ es el caso que: $$ || OverrieTarrow v | + k | overrleinRarrow v = | k | $$ (dónde $|\overrightarrowv|$ es la longitud de $\overrightarrowv$).Pero sólo $ | 1 | = Mathsf {false} $ (si esa es la convención elegida).En inglés, no hay límite en el número de términos necesarios para obtener un valor booleano aplicando un número.Entonces no puede haber una $\overrightarrowv$ que satisface las ecuaciones para todos los números, y por lo tanto $\mathsf{EsCero}$ no se puede definir.

Answer 2

La forma más sencilla de definir la adición en lambda-cálculo es tratar los números como si fueran listas vinculadas y catenar las listas.Para hacer este derecho, es necesario usar variables adicionales para reemplazar las variables externas de cada número, por lo que la expresión resultante para el segundo número puede ser sustituida por la variable interna de la expresión resultante para el primer número.Esto produce la siguiente expresión para la adición:

  λw.λx.λy.λz.w y (x y z)