principiantes - ¿De qué tipo de cálculo lambda sería un ejemplo de Lisp?
lisp para principiantes (3)
Estoy tratando de entender mejor cómo entran en juego los tipos en el cálculo lambda. Es cierto que muchas de las cosas de la teoría de tipos están por encima de mi cabeza. Lisp es un lenguaje de tipo dinámico, ¿correspondería eso aproximadamente al cálculo lambda sin tipo? ¿O hay algún tipo de "cálculo lambda tipificado dinámicamente" que no conozco?
Lisp es un lenguaje de tipo dinámico, ¿correspondería aproximadamente al cálculo lambda sin tipo?
Sí, pero sólo a grandes rasgos. En el cálculo lambda no tipificado "puro", todo se codifica como funciones. (Puede buscar en Google la popular "codificación de la Iglesia" y la menos popular "codificación de Scott".) Lisp tiene datos no funcionales, como átomos y números, por lo que esto contaría como "cálculo lambda sin tipo extendido con constantes".
Otra diferencia importante es en orden de evaluación . Las reglas para reducir los términos de lambda-cálculo son altamente no deterministas. (Hay un teorema, el teorema de Church-Rosser, que dice de manera general que mientras terminen las cosas, el orden de evaluación no importa). En la práctica, los términos lambda se reducen normalmente utilizando la reducción de "orden normal" de extremo a extremo izquierdo, porque si Cualquier estrategia de reducción termina, esa lo hace. Esto es muy diferente de Lisp, que siempre evalúa los argumentos a su forma normal antes de realizar una reducción beta. Este orden de evaluación se llama "llamada por valor".
En resumen, Lisp corresponde a un cálculo lambda de tipo por llamada sin valor extendido con constantes .
John McCarthy presentó LISP en su artículo de abril de 1960 "Funciones recursivas de las expresiones simbólicas y su computación por máquina, Parte I" . El siguiente párrafo es de la página 6:
mi. Funciones y formas. Es habitual en matemáticas, fuera de la lógica matemática, usar la palabra "función" de manera imprecisa y aplicarla a formas como y 2 + x. Como más adelante calcularemos con expresiones para funciones, necesitamos una distinción entre funciones y formas y una notación para expresar esta distinción. Esta distinción y una notación para describirla, de la cual nos desviamos trivialmente, es dada por la Iglesia [3].
...
3. A. CHURCH, The Calculi of Lambda-Conversion (Princeton University Press, Princeton, NJ, 1941).
El artículo de Wikipedia sobre lambda-cálculo tiene una historia de las publicaciones de la Iglesia. El artículo de 1941 al que McCarthy hace referencia parece estar relacionado con el cálculo lambda mecanografiado , en contradicción con la introducción del artículo de Wikipedia.
Se puede entender que la palabra clave lambda en Lisp se refiere al cálculo lambda solo por analogía. Una expresión lambda de Lisp es un tipo de función anónima .
Lisp no es ''un cálculo lambda'', no sé qué es ''un cálculo lambda''.
Si desea identificar los cálculos lambda por sistema de tipo, entonces Lisp es el suyo, por supuesto. La palabra clave ''lambda'' en cualquier palabra antes de Scheme es ciertamente pretenciosa, y después de Scheme también hay espacio para decir que lo es. Solo usando ''func'' hubiera sido más humilde. Lisp es principalmente un procesador de listas, no un ''cálculo lambda''
También escribí un artículo bastante extenso acerca de esto una vez que intenta demostrar por qué A: el término "programación funcional" no tiene sentido y B: por qué el hablar de "un cálculo lambda" en lugar de "un sistema de tipos" es así también:
http://blog.nihilarchitect.net/archives/289/on-functional-programming/
Además, tenga en cuenta que en Lisp, todas las funciones son, en efecto, un solo argumento y solo pueden tener listas como sus argumentos.