¿Qué tipo de cálculo lambda sería Lisp vagamente ser un ejemplo de?

Question

Estoy tratando de obtener un mejor agarre sobre cómo tipos entran en juego en el cálculo lambda. Es cierto que muchas de las cosas tipo teoría es sobre mi cabeza. Lisp es un lenguaje de tipos dinámicos, habría que corresponden aproximadamente a cálculo lambda sin tipo? ¿O hay algún tipo de "cálculo lambda de tipos dinámicos" que soy consciente de?

Answer 1

Lisp es un lenguaje de tipos dinámicos, tendría que corresponden aproximadamente al cálculo lambda sin tipo?

Sí, pero sólo aproximadamente. En el cálculo lambda sin tipo "puro", todo está codificado como funciones. (Puede google para el popular "Iglesia de codificación" y los menos populares "codificación de Scott".) Lisp tiene datos no funcionales, como los átomos y los números y tal, así que esto contaría como "cálculo lambda sin tipo ampliado con constantes."

Otra diferencia importante es en orden de evaluación . Reglas para la reducción de términos lambda-cálculo son altamente determinista. (Hay un teorema, el teorema de Church-Rosser, que dice vagamente que mientras las cosas terminan, orden de evaluación no importa.) En términos lambda práctica se reduce típicamente el uso de más a la izquierda-más externa también conocido como reducción de "orden normal" porque si ningún termina de estrategia de lucha, que lo hace. Esto es muy diferente de Lisp que siempre evalúa argumentos de forma normal antes de hacer una beta-reducción. Esta orden de evaluación se llama "llamada por valor."

En resumen, Lisp corresponde a una, llamada por valor cálculo lambda sin tipo extendido con constantes .

Answer 2

John McCarthy introdujo en LISP su abril de 1960 de papel "funciones recursivas de expresiones simbólicas y su cálculo a través de la máquina, Parte I ". El párrafo siguiente es de la página 6:

e. Funciones y formas. Es habitual en matemáticas - fuera de la lógica matemática - usar la palabra “función” de forma imprecisa y aplicarlo a las formas tal como y ² + x. Debido a que vamos a calcular posteriormente con expresiones de funciones, necesitamos una distinción entre funciones y formas y una notación para Express- ing esta distinción. Esta distinción y una notación para describir, desde el cual nos desviamos trivialmente, viene dada por la Iglesia [3]. ...
3. A. IGLESIA, los cálculos de Lambda-Conversión (Universidad de Princeton Press, Princeton, N. J., 1941).

El href="http://en.wikipedia.org/wiki/Lambda_calculus" rel="nofollow noreferrer"> artículo de Wikipedia sobre tiene una historia de las publicaciones de la Iglesia. En el documento se hace referencia 1941 por McCarthy parece ser acerca de la mecanografiada cálculo lambda, en contradicción con la introducción del artículo de Wikipedia.

La palabra clave lambda en Lisp puede ser entendido para referirse a la lambda-cálculo sólo a través de analogía. expresión lambda A Lisp es un tipo de función anónimo.

Answer 3

Lisp no es 'un cálculo lambda', yo no sé qué 'un cálculo lambda' está.

Si desea identificar lambda cálculos por ahí sistema de tipos a continuación, Lisp es su propia, por supuesto. El 'lambda' palabra clave en cualquier Lisp antes Esquema duda es pretenciosa, y después de esquema que hay espacio también para decir que es. Simplemente usando 'func' habría sido más humilde. Lisp es un procesador de lista sobre todo, no un 'cálculo lambda'

También escribió una bastante extenso artículo sobre esto una vez que los intentos para demostrar por qué R: 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 tipo' es también lo :

http://blog.nihilarchitect.net/archives/289/ en-funcional de programación /

Además, tenga en cuenta que en Lisp, todas las funciones están en vigor solo argumento y sólo puede ser Have listas como sus argumentos.