¿Alguien puede explicar brevemente (si es posible!) O referirme a una referencia, resumiendo las diferencias entre el cálculo lambda sin tipo y los cálculos lambda con tipo más comunes?
Estoy buscando particularmente declaraciones de su poder expresivo, equivalencias a sistemas lógicos / aritméticos o métodos de cálculo, y analogías con lenguajes de programación, si corresponde.
Si bien tengo la intención de leer, algo así como una tabla de referencia que describe los cálculos y sus equivalencias / diferencias / lugar en la jerarquía sería una ENORME referencia para ayudarme a resolverlos.
No digo que lo siguiente sea correcto, solo trato de esbozar algunas de las impresiones que tengo que ver si al menos sirven como punto de partida (¡o algo para corregir!)
Cálculo lambda sin tipo - ec. a la lógica de primer orden: no se puede hacer X
Simplemente tecleó cálculo lambda - eq a ... lógica, relacionada con Lisp?
Calc lambda 'polimórfica', etc.
Cálculo de construcciones: ¿lógica intuicionista?
Lógica combinatoria - comparable a ??? cálculo lambda mecanografiado, relacionado con el tipo de lenguajes APL / J
Si esto se vincula con el cubo lambda y sus tres ejes, mejor.
Si bien estoy familiarizado con los conceptos básicos del cálculo lambda y la programación con lenguajes funcionales, nunca he entendido ni hecho conexiones significativas con los sistemas de tipos involucrados y los diferentes sabores de los cálculos lambda (¿y quizás pi?).
Cuando intento investigar esto, no puedo evitar encontrarme desviado, abriendo muchas pestañas del navegador y bifurcando en tantas direcciones que nunca entro en ninguna de ellas con tanta profundidad.
No estoy seguro de si lo que estoy pidiendo es razonable, pero espero que al menos haya pintado lo suficiente como para sugerir alguna lectura que pueda explicar lo que estoy buscando.
fuente
lo.logic
se ha agregado una etiqueta. probablemente una pregunta tonta, pero ¿qué significa eso exactamente?Respuestas:
Tu mesa está un poco confundida; Aquí hay uno mejor.
La dependencia de tipo es más general que la cuantificación de primer orden, ya que convierte las pruebas en objetos que puede cuantificar. Existen cálculos Lambda que corresponden al FOL intuicionista ordinario, pero no se usan lo suficiente como para tener un nombre especial: las personas tienden a ir directamente a los tipos dependientes.
También puede relacionar la forma sintáctica de un cálculo con los sistemas lógicos.
fuente
nat
U
lambda : U -> (U -> U)
gamma : (U -> U) -> U
Referencias
Dana S. Scott: " Cálculo de Lambda: algunos modelos, cierta filosofía ", Estudios en lógica y fundamentos de las matemáticas, Volumen 101, 1980, páginas 223-265, Simposio de Kleene
Hendrik Pieter Barendregt: " El cálculo lambda: su sintaxis y semántica ", Elsevier, 1984.
fuente
Se puede encontrar una discusión bastante exhaustiva de estas cosas en este libro: Conferencias sobre el isomorfismo de Curry-Howard . Esto se basa en la versión anterior disponible gratuitamente: Conferencias sobre el isomorfismo de Curry-Howard .
fuente