Este artículo sugiere que hay combinadores (que representan cálculos simbólicos) que no pueden ser representados por el cálculo Lambda (si entiendo las cosas correctamente):
Hay varias cosas que uno puede querer hacer en la práctica y que no se pueden expresar directamente en el cálculo lambda.
El cálculo SF es un ejemplo. Su poder expresivo no es noticia; La parte interesante del documento (no se muestra en las diapositivas) es la teoría de la categoría detrás de él. El cálculo SF es análogo a una implementación de lisp donde permite que las funciones inspeccionen la representación de su argumento, por lo que puede escribir cosas como (print (lambda (x) (+ x 2)))⟹ "(lambda (x) (+ x 2))".
Otro ejemplo importante es el paralelo o de Plotkin . Intuitivamente hablando, hay un resultado general que establece que el cálculo lambda es secuencial: una función que toma dos argumentos debe elegir uno para evaluar primero. Es imposible escribir un término lambda ortal que ( or⊤ ⊥) ⟹ ⊤, ( or⊥ ⊤) ⟹ ⊤ y or⊥ ⊥ ⟹ ⊥ (donde ⊥ es un término que no termina y ⊤ es un término que termina). Esto se conoce como "paralelo o" porque una implementación paralela podría hacer un paso de cada reducción y detenerse cada vez que uno de los argumentos termina.
Otra cosa que no puedes hacer en el cálculo lambda es la entrada / salida. Tendría que agregarle primitivas adicionales.
Por supuesto, todos estos ejemplos se pueden representar en el cálculo lambda agregando un nivel de indirección, que representa esencialmente los términos lambda como datos. Pero luego el modelo se vuelve menos interesante: se pierde la relación entre las funciones en el lenguaje modelado y las abstracciones lambda.
La respuesta a su pregunta depende de cómo defina "cálculos" y "representados". El hilo en LtU que sclv mencionó , por otro lado, consiste principalmente en personas que hablan entre sí debido a definiciones desalineadas de varios términos.
La distinción ciertamente no es la potencia computacional: cada sistema considerado es equivalente a Turing. El problema es que la mera equivalencia de Turing realmente no dice nada sobre la estructura o la semántica de una expresión. Para el caso, en modelos de computación extremadamente minimalistas que requieren codificaciones complejas o estados iniciales no triviales, incluso puede no estar claro si un sistema es capaz de computación universal, o si una interpretación del sistema está creando una ilusión de universalidad. . Por ejemplo, vea esta discusión de la lista de correo con respecto a una máquina de Turing de 2 estados y 3 símbolos, particularmente las preocupaciones planteadas por Vaughan Pratt.
En cualquier caso, la distinción que se hace es entre algo como:
La equivalencia de Turing solo implica que un sistema cumple con el tercer criterio para cualquier función computable, mientras que con frecuencia es el primer criterio que nos interesa, ya sea en un sistema formal de lógica o en un lenguaje de programación (en la medida en que realmente difieran).
Esa es una descripción muy informal, pero la idea esencial puede concretarse con mayor precisión. En el hilo de LtU mencionado anteriormente se pueden encontrar un par de referencias al trabajo existente en líneas similares.
Tanto la lógica combinatoria de Schönfinkel como el cálculo λ de Church fueron concebidos inicialmente como abstracciones destiladas de razonamiento lógico, y como tal, su estructura se mapea muy claramente en el razonamiento lógico y viceversa. También conllevan una suposición de extensionalidad , como la descrita por la regla de reducción de eta:, λx. f xdonde xno ocurre en f, es equivalente a solo fsolo.
En la práctica, una noción muy estricta de extensionalidad puede ser demasiado limitante, mientras que la intensionalidad desenfrenada hace que el razonamiento local sobre las subexpresiones sea difícil o imposible.
El cálculo SF es un cálculo combinador modificado que proporciona, como operación primitiva, una forma limitada de análisis intensional: la capacidad de deconstruir expresiones parcialmente aplicadas, pero no valores primitivos o expresiones no normalizadas. Esto sucede para mapearse muy bien en ideas como la coincidencia de patrones como se encuentra en lenguajes de programación de estilo ML o macros como se encuentra en Lisps, pero no puede describirse en cálculo SK o λ sin, efectivamente, implementar un intérprete para evaluar términos "intensionales".
Entonces, en resumen: el cálculo de SF no puede representarse directamente en cálculo de λ en el sentido de que la mejor representación posible probablemente implica la implementación de un intérprete de cálculo de SF, y la razón de esto es una diferencia semántica fundamental: las expresiones tienen un carácter interno estructura, o se definen únicamente por su comportamiento externo?
El cálculo SF de Barry Jay puede analizar la estructura de términos a los que se aplica, que no es funcional. El cálculo Lambda y la lógica combinatoria tradicional son puramente funcionales, por lo que no pueden hacer esto.
Hay muchas extensiones del cálculo lambda que hacen cosas que violan la pureza, la mayoría de las cuales requieren corregir la estrategia de reescritura en algún grado, como agregar estados, controles (por ejemplo, a través de continuaciones) o variables lógicas.
fuente