cálculo lambda tipado

En matemáticas e informática , un cálculo lambda tipado es un formalismo tipado que utiliza el símbolo lambda (${\displaystyle \lambda }$) para denotar la abstracción de 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 (véase tipos más adelante). Desde cierto punto de vista, los cálculos lambda tipados pueden verse como refinamientos del cálculo lambda no tipado , pero desde otro punto de vista, también pueden considerarse la teoría más fundamental y el cálculo lambda no tipado un caso especial con un solo tipo. ^{[ 1 ]}

Los cálculos lambda tipados son fundamentales para los lenguajes de programación y constituyen la base de lenguajes de programación funcional tipados como ML y Haskell , y, de forma más indirecta, de lenguajes de programación imperativos tipados . Los cálculos lambda tipados desempeñan un papel importante en el diseño de sistemas de tipos para lenguajes de programación; en este caso, la tipabilidad suele reflejar propiedades deseables del programa (por ejemplo, que el programa no provoque una violación de acceso a la memoria).

Los cálculos lambda tipados están estrechamente relacionados con la lógica matemática y la teoría de la demostración 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 tipado simple es el lenguaje de las categorías cartesianas cerradas (CCC). ^{[ 2 ]}

Se han estudiado varios cálculos lambda tipados. El cálculo lambda tipado simple tiene solo un constructor de tipos , la flecha${\displaystyle \to }$y sus únicos tipos son los tipos básicos y los tipos de función.${\displaystyle \sigma \to \tau }$El sistema T extiende el cálculo lambda simplemente tipado con un tipo de números naturales y recursión primitiva de orden superior ; en este sistema, todas las funciones demostrablemente computables en la aritmética de Peano son definibles. El sistema F permite el polimorfismo mediante la 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. Basándose 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 puramente tipados (incluidos el cálculo lambda simplemente tipado, el sistema F, el LF y el cálculo de construcciones). ^{[ 3 ]}

Algunos cálculos lambda tipados introducen una noción de subtipado , es decir, si${\displaystyle A}$es un subtipo de${\displaystyle B}$, entonces todos los términos de tipo${\displaystyle A}$también tienen tipo${\displaystyle B}$. Los cálculos lambda tipados con subtipado son el cálculo lambda simplemente tipado con tipos conjuntivos y el sistema F _<: .

Todos los sistemas mencionados hasta ahora, con la excepción del cálculo lambda sin tipado, son fuertemente normalizadores : todos los cálculos terminan. Por lo tanto, no pueden describir todas las funciones computables por Turing . ^{[ 4 ]} Como otra consecuencia, son consistentes como lógica, es decir, hay tipos no habitados. Sin embargo, existen cálculos lambda tipados que no son fuertemente normalizadores. Por ejemplo, el cálculo lambda con tipado dependiente con un tipo de todos los tipos (Tipo  : Tipo) no es normalizador 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 de recursión explícitos, como el " Lenguaje de programación para funciones computables " (PCF) de Plotkin , no son normalizadores, pero no están pensados ​​para ser interpretados como una lógica. De hecho, PCF es un lenguaje de programación funcional tipado prototípico, donde los tipos se utilizan para asegurar que los programas se comporten bien, pero no necesariamente que terminen.

En programación informática , las rutinas (funciones, procedimientos, métodos) de los lenguajes de programación fuertemente tipados se corresponden estrechamente con las expresiones lambda tipadas. ^{[ 5 ]}

• Cálculo kappa : un análogo del cálculo lambda tipado que excluye funciones de orden superior.

• Barendregt, Henk (1992). «Cálculos lambda con tipos» . En Abramsky, S. (ed.). Antecedentes: Estructuras computacionales . Manual de lógica en informática. Vol.  2. Oxford University Press. pp. 117–309 . ISBN  9780198537618.
• Brandl, Helmut (2022). Cálculo de construcciones / Cálculo lambda tipado