El poder de los cálculos lambda

Question

Una pregunta sencilla que probablemente exija una respuesta algo compleja... O más bien, un conjunto de preguntas relacionadas.

• ¿Cuáles son las ventajas del cálculo lambda tipificado sobre el cálculo lambda no tipificado en términos de teoría de la prueba?
• En concreto, el Cálculo Lambda original de Church no estaba tipificado y permite funciones de orden arbitrario. ¿Cuáles son las limitaciones con respecto a la construcción de un cálculo de pruebas a partir de él?
• ¿No son los cálculos lambda no tipificados y tipificados sistemas formales de orden superior?
• ¿Cuáles son las razones para utilizar teorías de tipos complejas (por ejemplo, polimórficas/dependientes) en lugar de la teoría de tipos simple en el cálculo lambda? ¿Son más "potentes" en algún sentido; si es así, cómo exactamente?
• ¿Tiene la semántica (interpretación) algo que decir aquí, con respecto a las teorías tipificadas y no tipificadas, especialmente en términos de solidez y completitud?
• El conocido verificador de pruebas Coq que (creo) utiliza un lenguaje de cálculo lambda de tipo complejo de orden superior para representar pruebas en matemáticas constructivas (intuicionistas). He leído que la teoría que lo sustenta (el Cálculo de construcciones ) es esencialmente una extensión del isomorfismo Curry-Howard a la lógica de orden superior. ¿Hay alguna elaboración/aclaración que deba tener en cuenta aquí?

Answer 1

1. ¿Cuáles son las ventajas del cálculo lambda tipificado sobre el cálculo lambda no tipificado en términos de teoría de la prueba? y también
2. En concreto, el Cálculo Lambda original de Church no estaba tipificado y permite funciones de orden arbitrario. ¿Cuáles son las limitaciones con respecto a la construcción de un cálculo de pruebas a partir de él?
   • Simplemente, el cálculo lambda tipificado tiene una teoría de la prueba, y el cálculo lambda no tipificado no la tiene porque carece de un teorema de forma normal.
3. ¿No son los cálculos lambda no tipificados y tipificados sistemas formales de orden superior?
   • Esto es complicado, porque hay dos maneras de ver el orden superior. Son de orden superior cuando se miran los términos, ya que la definición de orden superior es abstracción sobre entidades de orden superior como las funciones, y la abstracción lambda es abstracción. Pero ten en cuenta que, bajo la correspondencia fórmula-como-tipos, las proposiciones en lógica están asociadas con los tipos de los términos lambda, y en, digamos, el cálculo lambda de tipo simple, no hay abstracción sobre nada. Este punto me confundió cuando estudié por primera vez la teoría simple de tipos de Church, porque se trata de un cálculo de orden superior basado en el cálculo lambda de tipo simple, en el que las proposiciones se forman utilizando los términos lambda, en lugar de ser los tipos, como ocurre con la correspondencia fórmula-como-tipos.
4. ¿Cuáles son las razones para utilizar teorías de tipos complejas (por ejemplo, polimórficas/dependientes) en lugar de la teoría de tipos simple en el cálculo lambda? ¿Son más "potentes" en algún sentido; si es así, cómo exactamente?
   • Sí que añaden potencia. Bajo la correspondencia fórmula-como-tipos, el cálculo lambda de tipo simple tiene como lógica coincidente el cálculo proposicional, añadiendo tipos dependientes se añade a su lógica la cuantificación universal y existencial en tipos finitos superiores. Los tipos polimórficos permiten construir tipos que permiten todas las entidades matemáticas habituales (aunque sin la teoría habitual de la demostrabilidad) y tiene una alta consistencia teórica de la prueba: La normalización fuerte del sistema F tiene (sobre una teoría base como RCL0) la misma fuerza que la aritmética de segundo orden de consistencia, aunque carece de un principio de inducción.
5. ¿Tiene la semántica (interpretación) algo que decir aquí, con respecto a las teorías tipificadas y no tipificadas, especialmente en términos de solidez y completitud?
   • Son mucho menos útiles con este tipo de teorías que la teoría de modelos con la lógica clásica, aunque hay buenas aplicaciones de la teoría de categorías a la semántica de la teoría de tipos.
6. El conocido verificador de pruebas Coq, que (creo) utiliza un lenguaje de cálculo lambda de tipo complejo de orden superior para representar pruebas en matemáticas constructivas (intuicionistas). He leído que la teoría que lo sustenta (el Cálculo de Construcciones) es esencialmente una extensión del isomorfismo Curry-Howard a la lógica de orden superior. ¿Hay alguna elaboración/aclaración que deba conocer?
   • Sí, que los tipos polimórficos son complicados, y no conservadores sobre la teoría base. Yo recomendaría empezar a explorar las fórmulas como tipos con la teoría de tipos dependientes de Martin-Löf. Si quieres trabajar con un asistente de pruebas, hay Agda que es un lenguaje de programación funcional cuyo sistema de tipos es la teoría de tipos de Martin-Löf.