El cálculo lambda deductivo considera lo que sucede cuando los términos lambda se consideran expresiones matemáticas. Una interpretación del cálculo lambda sin tipo es como un lenguaje de programación donde la evaluación procede realizando reducciones en una expresión hasta que está en forma normal. En esta interpretación, si la expresión nunca se reduce a la forma normal, el programa nunca termina y el valor no está definido. Considerado como un sistema matemático deductivo , cada reducción no alteraría el valor de la expresión. La expresión sería igual a la reducción de la expresión.
Historia
Alonzo Church inventó el cálculo lambda en la década de 1930, originalmente para proporcionar una base nueva y más simple para las matemáticas. [1] [2] Sin embargo, poco después de inventarlo, se identificaron importantes problemas lógicos con la definición de la abstracción lambda: La paradoja de Kleene-Rosser es una implementación de la paradoja de Richard en el cálculo lambda. [3] Haskell Curry descubrió que el paso clave en esta paradoja podría usarse para implementar la paradoja de Curry más simple . La existencia de estas paradojas significaba que el cálculo lambda no podía ser consistente y completo como sistema deductivo . [4]
Haskell Curry estudió la lógica combinatoria ilativa (deductiva) en 1941. [5] La lógica combinatoria está estrechamente relacionada con el cálculo lambda, y existen las mismas paradojas en cada uno.
Más tarde, el cálculo lambda resucitó como una definición de lenguaje de programación.
Introducción
El cálculo lambda es el modelo y la inspiración para el desarrollo de lenguajes de programación funcionales . Estos lenguajes implementan la abstracción lambda y la usan junto con la aplicación de funciones y tipos.
El uso de abstracciones lambda, que luego se integran en otros sistemas matemáticos y se utilizan como sistema deductivo, conduce a una serie de problemas, como la paradoja de Curry . Los problemas están relacionados con la definición de la abstracción lambda y la definición y uso de funciones como tipo básico en el cálculo lambda . Este artículo describe estos problemas y cómo surgen.
Esta no es una crítica del cálculo lambda puro, y el cálculo lambda como sistema puro no es el tema principal aquí. Los problemas surgen con la interacción del cálculo lambda con otros sistemas matemáticos. Ser consciente de los problemas permite evitarlos en algunos casos.
Terminología
Para esta discusión, la abstracción lambda se agrega como un operador adicional en matemáticas. Los dominios habituales, como booleano y real , estarán disponibles. Se aplicará la igualdad matemática a estos dominios. El propósito es ver qué problemas surgen de esta definición.
La aplicación de la función se representará utilizando la sintaxis de cálculo lambda. Entonces, la multiplicación estará representada por un punto. Además, para algunos ejemplos, se utilizará la expresión let .
La siguiente tabla resume;
Nombre | Notación |
---|---|
Abstracción lambda. | |
Aplicación de la función f a x | |
Multiplicación de a por b | |
Sea x en y | |
Igualdad matemática | |
Igualdad beta reducible |
Interpretación del cálculo lambda como matemáticas
En la interpretación matemática , los términos lambda representan valores. Las reducciones eta y beta son pasos deductivos que no alteran los valores de las expresiones.
Reducción de eta como matemáticas
Un eta-reducto se define por,
En la interpretación matemática,
Tomando f como una variable entonces,
o dejando
Esta definición define para ser la solución de f en la ecuación,
Reducción beta como matemáticas
Un beta reducto es,
y como,
luego,
Esta regla está implícita en la instanciación de variables cuantificadas . Si,
luego es la expresión y con la variable cuantificada x instanciada como z.
entonces,
Como la reducción beta está implícita en la reducción eta, no hay contradicción entre las dos definiciones.
Inconsistencia con el principio de bivalencia
Sea z un booleano ; entonces podemos formar una ecuación sin soluciones,
Para resolver esta ecuación por recursividad, introducimos una nueva función f definida por,
donde n es una variable auxiliar para contener el valor de recursividad. (Lo tomamos que todavía devuelve un booleano incluso si se le da un argumento no booleano). Mediante una reducción de eta, obtenemos,
Y entonces,
Entonces ff no es verdadero ni falso, y como ff es un valor booleano (en cualquier x , f devuelve el valor booleano) entonces vemos que ff no es ni verdadero ni falso; también demuestra que la negación tiene menos sentido cuando se aplica a valores no lógicos.
Igualdad intensiva versus extensional
Otra dificultad para la interpretación del cálculo lambda como sistema deductivo es la representación de valores como términos lambda, que representan funciones. El cálculo lambda sin tipo se implementa realizando reducciones en un término lambda, hasta que el término está en forma normal. La interpretación intensional [6] [7] de la igualdad es que la reducción de un término lambda a la forma normal es el valor del término lambda.
Esta interpretación considera que la identidad de una expresión lambda es su estructura. Dos términos lambda son iguales si son alfa convertibles.
La definición extensional de igualdad de funciones es que dos funciones son iguales si realizan el mismo mapeo;
Una forma de describir esto es que la igualdad extensional describe la igualdad de funciones, mientras que la igualdad intensional describe la igualdad de implementaciones de funciones.
La definición extensional de igualdad no es equivalente a la definición intensional. Esto se puede ver en el siguiente ejemplo. Esta desigualdad se crea al considerar los términos lambda como valores. En el cálculo lambda tipificado, este problema se evita, porque los tipos incorporados pueden agregarse para llevar valores que están en una forma canónica y tienen igualdad tanto extensional como intensional.
Ejemplo
En aritmética , la ley distributiva implica que. Usando la codificación de números de Church, los lados izquierdo y derecho pueden representarse como términos lambda.
Entonces, la ley distributiva dice que las dos funciones,
son iguales, como funciones en los números de la Iglesia. (Aquí nos encontramos con una debilidad técnica del cálculo lambda sin tipo: no hay forma de restringir el dominio de una función a los números de la Iglesia. En el siguiente argumento ignoraremos esta dificultad, pretendiendo que "todas" las expresiones lambda son números de la Iglesia. .) La ley distributiva debe aplicarse si los numerales de la Iglesia proporcionan una implementación satisfactoria de los números.
Los dos términos beta se reducen a expresiones similares. Aún así, no son alfa convertibles, ni siquiera eta convertibles (el último sigue porque ambos términos ya están en forma eta-long). Entonces, de acuerdo con la definición intensional de igualdad, las expresiones no son iguales. Pero si las dos funciones se aplican a los mismos números de la Iglesia, producen el mismo resultado, según la ley distributiva; por tanto, son extensionalmente iguales.
Este es un problema significativo, ya que significa que el valor intensional de un término lambda puede cambiar bajo transformaciones extensionalmente válidas. Una solución a este problema es introducir una regla omega ,
- Si, para todas las expresiones lambda t tenemos, luego .
En nuestra situación, "todas las expresiones lambda" significa "todos los números de la Iglesia", por lo que también es una regla omega en el sentido estándar. Tenga en cuenta que la regla omega implica la regla eta, ya que por una reducción beta en el lado derecho.
Establecer dominio teórico
Las abstracciones lambda son funciones de funciones. Un paso natural es definir un dominio para la abstracción lambda como un conjunto de todas las funciones.
El conjunto de todas las funciones desde un dominio D hasta un rango R viene dado por K en,
Entonces la definición (imaginaria) del conjunto de todas las funciones de funciones viene dada por F en,
Esta definición no se puede formular en una teoría de conjuntos axiomática; y esta ecuación ingenua, incluso si pudiera escribirse en una teoría de conjuntos, no tiene soluciones.
Ahora el cálculo lambda se define por reducciones beta y reducciones eta. Interpretar la reducción como una definición de igualdad da un dominio implícito para el cálculo lambda. Las reglas son
- Cada abstracción lambda tiene un valor.
- La reducción beta de un término lambda tiene el mismo valor.
- La reducción eta de un término lambda tiene el mismo valor.
- Los términos de lambda alfa convertible son iguales.
- [Si la regla omega está presente] los términos lambda "equivalentes a omega" son iguales.
- Si no se puede demostrar que dos términos lambda son iguales por las reglas anteriores, no son iguales.
Si dos términos lambda pueden reducirse a su forma normal, entonces se puede usar el teorema de Church-Rosser para demostrar que son iguales si sus formas normales son alfa convertibles.
Si uno o ambos términos no se normalizan, la indecidibilidad de la equivalencia muestra que, en general, no existe un algoritmo para determinar si dos términos lambda son iguales. En general, esto hace que sea imposible saber cuáles son los distintos elementos del dominio de cálculo lambda.
Ejemplo: sin soluciones → una solución
Por ejemplo, la ecuación puede codificarse con la codificación Church y usar el combinador Y de Curry como,
Y la recursividad es,
- ...
- ... (reducción beta y luego eta)
Cuál es la primera línea y se repetirá indefinidamente. La expresión nunca se reduce a la forma normal. Sin embargo, cada término lambda en la reducción representa el mismo valor. Este valor es distinto de las codificaciones de verdadero o falso . No es parte del dominio booleano pero existe en el dominio de cálculo lambda.
Ejemplo: múltiples soluciones → una solución
Usando la división y los números con signo , el combinador Y se puede usar para definir una expresión que represente la raíz cuadrada de un número entero. La codificación de la Iglesia también puede extenderse más a los números racionales y reales , de modo que se pueda definir una raíz cuadrada real. La tesis de Church-Turing implica que cualquier operador computable (y sus operandos) se puede representar en cálculo lambda.
Usando tal codificación,
Usando la implementación de dividir entonces,
representa dos valores en el dominio de los números con signo, si n no es igual a cero. Sin embargo, es una expresión lambda, por lo que solo tiene un valor en el dominio de cálculo lambda. La reducción beta de este término lambda nunca alcanza la forma normal. Sin embargo, representa un valor, por lo que un solo valor en el dominio de cálculo lambda representa dos valores en el dominio de números con signo.
Ver también
- Cálculo lambda
- Dejemos expresión
- Codificación de la iglesia
Referencias
- ^ Iglesia, A. (1932). "Un conjunto de postulados para la fundación de la lógica". Annals of Mathematics . Serie 2. 33 (2): 346–366. doi : 10.2307 / 1968337 . JSTOR 1968337 .
- ↑ Para obtener una historia completa, consulte " Historia del cálculo Lambda y la lógica combinatoria " deCardone y Hindley(2006).
- ^ Kleene, SC y Rosser, JB (1935). "La inconsistencia de ciertas lógicas formales". Annals of Mathematics . 36 (3): 630–636. doi : 10.2307 / 1968646 . JSTOR 1968646 .
- ^ Curry, Haskell B. (1942). "La inconsistencia de cierta lógica formal". El diario de la lógica simbólica . 7 (3): 115-117. doi : 10.2307 / 2269292 . JSTOR 2269292 .
- ^ Curry, Haskell B. (1941). "La paradoja de Kleene y Rosser" . Transacciones de la American Mathematical Society . 50 : 454–516. doi : 10.1090 / S0002-9947-1941-0005275-6 . JSTOR 1990124 . Señor 0005275 . Consultado el 24 de enero de 2013 .
- ^ Selinger, Peter. "Notas de la conferencia sobre cálculo Lambda (PDF)" (PDF) . pag. 6.
- ^ "Cálculo lambda - intensionalidad" . Stanford. pag. 1.2 Intensionalidad.