Cálculo lambda tipificado - Typed lambda calculus

Un cálculo lambda con tipo es un formalismo con tipo que utiliza el símbolo lambda ( ) para denotar la abstracción de funciones anónimas. 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 es un caso especial con un solo tipo. ${\ Displaystyle \ lambda}$

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, 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 capacidad de escribir normalmente captura las 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 clases de categorías ; por ejemplo, el cálculo lambda simplemente tipado es el lenguaje de las categorías cerradas cartesianas (CCC).

Tipos de cálculos lambda tipificados

Se han estudiado varios cálculos lambda tipificados. El cálculo lambda simplemente tipado tiene solo un constructor de tipo , la flecha , y sus únicos tipos son los tipos básicos y los tipos de función . El sistema T amplía el cálculo lambda simplemente tipado con un tipo de números naturales y recursividad primitiva de orden superior; en este sistema, todas las funciones probablemente 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 probables totales en la lógica de segundo orden . Los cálculos lambda con tipos dependientes son la base de la teoría intuicionista de tipos , 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, System F, LF y el cálculo de construcciones). ${\ Displaystyle \ to}$ ${\ Displaystyle \ sigma \ to \ tau}$

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 . Con tipo lambda cálculos con los subtipos son el cálculo lambda simplemente mecanografiado con tipos conjuntivas y System F _<: . ${\ Displaystyle A}$${\ Displaystyle B}$${\ Displaystyle A}$${\ Displaystyle B}$

Todos los sistemas mencionados hasta ahora, con la excepción del cálculo lambda sin tipo, se normalizan fuertemente : todos los cálculos terminan. Por lo tanto, no pueden describir todas las funciones computables de Turing . Como otra consecuencia, son coherentes 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 de tipo 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 tipo puro más simple, un formalismo que generaliza el cubo Lambda. Los sistemas con combinadores de recursividad explícitos, como el " Lenguaje de programación para funciones computables " (PCF) de Plotkin , no se normalizan, pero no están destinados a ser interpretados como una lógica. De hecho, PCF es un lenguaje de programación funcional prototípico y tipificado, en el que los tipos se utilizan para garantizar que los programas se comporten bien, pero no necesariamente que terminen.

Aplicaciones a lenguajes de programación

En la 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 tipadas.

Ver también

• Cálculo Kappa: un análogo del cálculo lambda tipificado que excluye funciones de orden superior

Notas

Otras lecturas

• Barendregt, Henk (1992). "Cálculos lambda con tipos" . En Abramsky, S. (ed.). Antecedentes: Estructuras Computacionales . Manual de Lógica en Informática. 2 . Prensa de la Universidad de Oxford. págs. 117-309. ISBN   9780198537618 .