¿Qué funciones pueden calcular las expresiones de cálculo del combinador?

Una expresión combinatoria (digamos en la base SK) puede considerarse como una función que asigna expresiones de cálculo combinador a expresiones de cálculo combinador. Es decir, se puede pensar en una expresión como una función X : L → L , donde L es el conjunto de todas las expresiones de combinador sintácticamente válidas en la base SK. Este mapeo se realiza aplicando la entrada a la expresión y luego reduciendo a la forma normal para obtener la salida.$X$$X:L \to L$$L$

Dado que la base SK se completa Turing, uno podría pensar ingenuamente que existe una expresión SK que implementa cualquier función computable desde L a L . Sin embargo, esto claramente no es el caso, ya que el resultado de la reducción siempre estará en forma normal. Esto significa que no hay forma de que una expresión tenga una salida que no esté en forma normal.$X$$L$$L$

Entonces, en cambio, podría pensar en las expresiones de cálculo SK como mapeo de a L ' , donde L ' es el conjunto de expresiones de SK en forma normal. ¿Es el caso de que, para cualquier mapa computable f : L ' → L ' , hay una expresión SK X que implementa este mapa? ¿O hay más restricciones en el conjunto de funciones que pueden ser calculadas por las expresiones de cálculo del combinador de esta manera?$L'$$L'$$L'$$f:L'\to L'$$X$

Para que la pelota ruede, y con la esperanza de que otras personas den respuestas más profundas y detalladas sobre la estructura de las funciones definibles L ′ → L ′ , permítanme citar el Corolario 20.3.3 del Cálculo Lambda de Barendregts , su sintaxis y Semántica (también conocida como "la biblia").$\lambda$$L'\to L'$

Corolario 20.3.3: La función , definida por δ ( M , N ) = { T r u e  si  M = β η N F a l s e de lo  contrario no se puede definir en el tipo λ - cálculo, es decir, no existe un término D tal que D M N = β η δ ( M , N $\delta:L'^2\to L'$

$$\delta(M, N) = \cases{\mathrm{True}\mbox{ if }M=_{\beta\eta}N\\ \mathrm{False}\mbox{ otherwise}}$$ $\lambda$$D$ $$D\ M\ N =_{\beta\eta} \delta(M,N)$$ para todo .$M,N\in L'$

La prueba involucra consideraciones sobre los árboles Böhm que dan una caracterización bastante fuerte de las posibles "acciones" de términos lambda arbitrarios en formas normales. En particular, para cualquier término cerrado no constante , on puede encontrar n ∈ N y P 1 , ... , P n tal que F x P 1 ... P n = β η x Q 1 ... Q $F$$n\in\mathbb{N}$$P_1,\ldots,P_n$

$$F\ x\ P_1\ldots P_n =_{\beta\eta} x\ Q_1\ldots Q_k$$

$k$$Q_1,\ldots,Q_k$$D$$\delta$$D$ no puede existir.