Un cálculo lambda escrito es un formalismo escrito que utiliza el símbolo lambda ( ) para denotar la abstracción de una función anónima. En este contexto, los tipos suelen ser objetos de naturaleza sintáctica que se asignan a términos lambda; la naturaleza exacta de un tipo depende del cálculo considerado (ver tipos a continuación). Desde cierto punto de vista, los cálculos lambda tipificados pueden verse como refinamientos del cálculo lambda no tipificado , pero desde otro punto de vista, también pueden considerarse la teoría más fundamental y el cálculo lambda no tipificado un caso especial con un solo tipo.
Los cálculos lambda tipificados son lenguajes de programación fundamentales y son la base de los lenguajes de programación funcionales tipificados como ML y Haskell y, más indirectamente, de los lenguajes de programación imperativos tipificados . Los cálculos lambda tipificados juegan un papel importante en el diseño de sistemas de tipos para lenguajes de programación; aquí, la tipificación generalmente captura propiedades deseables del programa (por ejemplo, el programa no causará una violación de acceso a la memoria).
Los cálculos lambda tipificados están estrechamente relacionados con la lógica matemática y la teoría de la prueba a través del isomorfismo de Curry-Howard y pueden considerarse como el lenguaje interno de ciertas clases de categorías . Por ejemplo, el cálculo lambda escrito simplemente es el lenguaje de las categorías cerradas cartesianas (CCC) [1]
Se han estudiado varios cálculos lambda tipificados. El cálculo lambda de tipo simple tiene sólo un constructor de tipo , la flecha , y sus únicos tipos son tipos básicos y tipos de funciones . El Sistema T amplía el cálculo lambda de tipo simple con un tipo de números naturales y recursividad primitiva de orden superior; en este sistema todas las funciones demostrablemente recursivas en la aritmética de Peano son definibles. El sistema F permite el polimorfismo mediante el uso de cuantificación universal sobre todos los tipos; desde una perspectiva lógica, puede describir todas las funciones que son demostrablemente totales en lógica de segundo orden . Los cálculos lambda con tipos dependientes son la base de la teoría de tipos intuicionista , el cálculo de construcciones y el marco lógico (LF), un cálculo lambda puro con tipos dependientes. Basado en el trabajo de Berardi sobre sistemas de tipos puros , Henk Barendregt propuso el cubo Lambda para sistematizar las relaciones de los cálculos lambda tipificados puros (incluido el cálculo lambda simplemente tipificado, el Sistema F, LF y el cálculo de construcciones). [ cita necesaria ]
Algunos cálculos lambda tipificados introducen una noción de subtipo , es decir, si es un subtipo de , entonces todos los términos de tipo también tienen tipo . Los cálculos lambda tipificados con subtipificación son cálculos lambda tipificados simplemente con tipos conjuntivos y Sistema F <: .
Todos los sistemas mencionados hasta ahora, con excepción del cálculo lambda sin tipo, son fuertemente normalizadores : todos los cálculos terminan. Por lo tanto, no pueden describir todas las funciones computables por Turing . [2] Como otra consecuencia, son consistentes como lógica, es decir, hay tipos deshabitados. Sin embargo, existen cálculos lambda tipificados que no se normalizan fuertemente. Por ejemplo, el cálculo lambda tipado de forma dependiente con un tipo de todos los tipos (Tipo: Tipo) no se normaliza debido a la paradoja de Girard . Este sistema es también el sistema de tipos puros más simple, un formalismo que generaliza el cubo Lambda. Los sistemas con combinadores recursivos explícitos, como el " lenguaje de programación para funciones computables " (PCF) de Plotkin , no son normalizadores, pero no deben interpretarse como una lógica. De hecho, PCF es un lenguaje de programación funcional tipificado prototípico, donde los tipos se utilizan para garantizar que los programas se comporten bien, pero no necesariamente que estén finalizando.
En programación de computadoras , las rutinas (funciones, procedimientos, métodos) de los lenguajes de programación fuertemente tipados se corresponden estrechamente con las expresiones lambda tipificadas.
