Cubo lambda

Lambda-cube ( λ-cube ) es una clasificación visual de ocho cálculos lambda tipados con asignación de tipo explícita (sistemas de tipo Church ) . El cubo se organiza de acuerdo a las posibles dependencias entre los tipos y términos de este cálculo y forma una estructura natural para el cálculo de construcción . La idea del cubo λ fue propuesta en 1991 por el lógico y matemático holandés Henk Barendregt . Se pueden obtener más generalizaciones del cubo lambda considerando el sistema de tipo puro .

Estructura del cubo λ

En los sistemas de cubos λ, las variables se asignan a uno de dos tipos: o . Todas las expresiones válidas también se ordenan. La afirmación de que una expresión pertenece a un género se construye sobre la afirmación de tipo, es decir, la declaración dice lo siguiente: el elemento tiene un tipo y pertenece al género . La ordenación se usa para variables ordinarias y términos del cálculo λ, la ordenación se usa para variables y expresiones de tipo. Por lo tanto, en los sistemas de cubos λ, los tipos de clasificación y los elementos de clasificación se tratan como intersecantes. Por ejemplo, el tipo de un término se puede escribir como un elemento de un tipo "superior" . Los tipos de cultivares a veces se denominan géneros . $\ ast$ $\Caja$ ${\ estilo de visualización A: B: C}$ $A$ $B$ $C$ $\ ast$ $\Caja$ $\ ast$ $\Caja$ $(\lambda x:\alpha .\,x):(\alpha \to \alpha ):\ast$ $(\alpha \to \alpha ):\ast :\Box$ $\Caja$

La dependencia se entiende como la capacidad de definir y utilizar funciones que asignan elementos de un tipo a otro (o el mismo). Los elementos de un género dependen de los elementos de un género si: $s_{1}$ $s_{2}$

para una expresión válida , que posiblemente contenga una variable , podemos definir una abstracción lambda ; ${\displaystyle F[x]:\tau :s_{1))$ ${\ estilo de visualización x: \ sigma: s_ {2))$ ${\displaystyle (\lambda x:\sigma .\,F[x]):(\sigma \to \tau ):s_{1))$
se debe permitir que la función se aplique a un elemento y el resultado debe ser un elemento de tipo sort , es decir, . $G:(\sigma \to \tau ):s_{1}$ ${\ estilo de visualización Y: \ sigma: s_ {2))$ $\tau$ $s_{1}$ ${\ estilo de visualización (G \, Y): \ tau: s_ {1))$

El vértice base del cubo es el sistema correspondiente al cálculo lambda de tipo simple . Los términos (elementos de género ) dependen de los términos; Los tipos (elementos de clasificación ) no participan en las dependencias. Los tres ejes que emergen del vértice base dan lugar a los siguientes sistemas: $\lambda ^{\rightarrow}$ $\ ast$ $\Caja$

términos según tipos: sistema (cálculo lambda con tipos polimórficos, sistema F ); $\lambda 2$
tipos dependientes de tipos: sistema (cálculo lambda con operadores sobre tipos); $\lambda \subrayado {\omega}$
término tipos dependientes: sistema (cálculo lambda con tipos dependientes ). $\lambda P$

Los sistemas restantes son varias combinaciones de las dependencias enumeradas. El sistema más rico (cálculo lambda polimórfico de orden superior con tipos dependientes) es en realidad un cálculo de construcción . $\lambda p\omega$

Propiedades de los sistemas de cubos λ

Todos los sistemas de cubo lambda tienen la propiedad de normalización fuerte : cualquier término (y tipo) admisible puede reducirse a una sola forma normal después de un número finito de reducciones β .

Soporte en lenguajes de programación

Diferentes lenguajes funcionales admiten un subconjunto diferente de los sistemas de tipos representados en el cubo lambda.

Haskell , ML - λ2 ( sistema F )
De forma limitada, Haskell (en la implementación de GHC desde versiones recientes) admite el uso de "familias de tipos". $\lambda \subrayado {\omega}$
Coq , Agda - ( cálculo de construcción ) $\lambda P\omega$

Enlaces

Henk Barendregt, Lambda Calculi with Types (inglés) , Handbook of Logic in Computer Science, volumen II, Oxford University Press.
Simon Peyton Jones y Erik Meijer, 1997. Henk: un lenguaje intermedio mecanografiado
Lennart Augustsson, 2007. ¡Más simple, más fácil! (Inglés) Descripción de la implementación de sistemas lambda-cube en Haskell.
Lambda Cube en SpbHUG (ruso) con la traducción de Denis Moskvin de la sección sobre cubo lambda del libro Henk Barendregt, Lambda Calculi with Types