En lógica matemática y teoría de tipos , el cubo λ es un marco introducido por Henk Barendregt [1] para investigar las diferentes dimensiones en las que el cálculo de construcciones es una generalización del cálculo λ simplemente tipado . Cada dimensión del cubo corresponde a un nuevo tipo de dependencia entre términos y tipos. Aquí, "dependencia" se refiere a la capacidad de un término o tipo para vincular un término o tipo. Las dimensiones respectivas del cubo λ corresponden a:
- eje y): términos que pueden unir tipos, correspondientes al polimorfismo .
- eje x): tipos que pueden vincular términos, correspondientes a tipos dependientes .
- eje Z (): tipos que pueden vincular tipos, correspondientes a operadores de tipo (vinculantes) .
Las diferentes formas de combinar estas tres dimensiones producen los 8 vértices del cubo, cada uno correspondiente a un tipo diferente de sistema tipificado. El cubo λ se puede generalizar en el concepto de un sistema de tipos puro .
Ejemplos de sistemas
(λ →) Cálculo lambda simplemente mecanografiado
El sistema más simple que se encuentra en el cubo λ es el cálculo lambda simplemente tipado , también llamado λ →. En este sistema, la única forma de construir una abstracción es haciendo que un término dependa de un término , con la regla de escritura
(λ2) Sistema F
En el Sistema F (también llamado λ2 para el "cálculo lambda tipado de segundo orden") [2] hay otro tipo de abstracción, escrito con un, que permite que los términos dependan de los tipos , con la siguiente regla:
Los términos que comienzan con un se denominan polimórficas , ya que se pueden aplicar a diferentes tipos para obtener diferentes funciones, de manera similar a las funciones polimórficas en lenguajes similares a ML . Por ejemplo, la identidad polimórfica
divertido x -> x
de OCaml tiene tipo
' a -> ' a
lo que significa que puede tomar un argumento de cualquier tipo 'a
y devolver un elemento de ese tipo. Este tipo corresponde en λ2 al tipo.
(λ ω ) Sistema F ω
En el sistema FSe introduce una construcción para suministrar tipos que dependen de otros tipos . Esto se denomina constructor de tipos y proporciona una forma de construir "una función con un tipo como valor ". [3] Un ejemplo de este tipo de constructor es, dónde ""informalmente significa" es un tipo ". Esta es una función que toma un parámetro de tipo como argumento y devuelve el tipo de s de valores de tipo . En la programación concreta, esta característica corresponde a la capacidad de definir constructores de tipos dentro del lenguaje, en lugar de considerarlos como primitivos. El constructor de tipos anterior corresponde aproximadamente a la siguiente definición de un árbol con hojas etiquetadas en OCaml:
escriba ' un árbol = | Hoja de ' a | Nodo de ' un árbol * ' un árbol
Este constructor de tipos se puede aplicar a otros tipos para obtener nuevos tipos. Por ejemplo, para obtener tipos de árboles de enteros:
tipo int_tree = int árbol
Sistema Fgeneralmente no se usa solo, pero es útil para aislar la característica independiente de los constructores de tipos. [4]
(λP) Lambda-P
En el sistema λP , también llamado ΛΠ, y estrechamente relacionado con el marco lógico LF , se tienen los llamados tipos dependientes . Estos son tipos que pueden depender de los términos . La regla de introducción crucial del sistema es
dónde representa tipos válidos. El nuevo constructor de tiposcorresponde a través del isomorfismo de Curry-Howard a un cuantificador universal, y el sistema λP en su conjunto corresponde a la lógica de primer orden con implicación como sólo conectivo. Un ejemplo de estos tipos dependientes en la programación concreta es el tipo de vectores en una cierta longitud: la longitud es un término, del cual depende el tipo.
(Fω) Sistema Fω
El sistema Fω combina tanto constructor de System F y los constructores de tipos de System F. Por tanto, el Sistema Fω proporciona términos que dependen de tipos y tipos que dependen de tipos .
(λC) Cálculo de construcciones
En el cálculo de construcciones , denotado como λC en el cubo (λPω es la esquina λC del cubo), [5] : 0:14 estas cuatro características cohabitan, de modo que tanto tipos como términos pueden depender de tipos y términos. El límite claro que existe en λ → entre términos y tipos está algo abolido, ya que todos los tipos excepto el universal ellos mismos son términos con un tipo.
Definicion formal
Como para todos los sistemas basados en el cálculo lambda simplemente tipado, todos los sistemas en el cubo se dan en dos pasos: primero, términos brutos, junto con una noción de reducción β , y luego reglas de tipeo que permiten teclear esos términos.
El conjunto de clases se define como , los géneros se representan con la letra . También hay un conjunto de variables, representadas por las letras . Los términos brutos de los ocho sistemas del cubo vienen dados por la siguiente sintaxis:
y denotando Cuándo no ocurre gratis en .
El entorno, como es habitual en los sistemas tipificados, viene dado por
La noción de reducción β es común a todos los sistemas del cubo. Está escrito y dado por las reglas
Las siguientes reglas de escritura también son comunes a todos los sistemas del cubo:
La correspondencia entre los sistemas y los pares permitido en las reglas es lo siguiente:
λ → | ||||
λP | ||||
λ2 | ||||
λ ω | ||||
λP2 | ||||
λP ω | ||||
λω | ||||
λC |
Cada dirección del cubo corresponde a un par (excluyendo el par compartido por todos los sistemas), y a su vez cada par corresponde a una posibilidad de dependencia entre términos y tipos:
- permite que los términos dependan de los términos.
- permite que los tipos dependan de los términos.
- permite que los términos dependan de los tipos.
- permite que los tipos dependan de los tipos.
Comparación entre los sistemas
λ →
Una derivación típica que se puede obtener es
La potencia de cálculo es bastante débil, corresponde a los polinomios extendidos (polinomios junto con un operador condicional). [6]
λ2
En λ2, tales términos se pueden obtener como
El polimorfismo también permite la construcción de funciones que no fueron construibles en λ →. Más precisamente, las funciones que se pueden definir en el Sistema F son aquellas demostrablemente totales en la aritmética de Peano de segundo orden . [7] En particular, todas las funciones recursivas primitivas son definibles.
λP
En λP, la capacidad de tener tipos dependiendo de los términos significa que uno puede expresar predicados lógicos. Por ejemplo, se puede derivar lo siguiente:
Sin embargo, desde el punto de vista computacional, tener tipos dependientes no mejora la potencia computacional, solo la posibilidad de expresar propiedades de tipo más precisas. [8]
La regla de conversión es muy necesaria cuando se trata de tipos dependientes, ya que permite realizar cálculos sobre los términos del tipo. Por ejemplo, si tiene y , debe aplicar la regla de conversión para obtener para poder escribir .
λω
En λω, el siguiente operador
Desde el punto de vista de la computación, λω es extremadamente fuerte y se ha considerado como una base para los lenguajes de programación. [9]
λC
El cálculo de construcciones tiene tanto la expresividad de predicado de λP como el poder computacional de λω, por lo que es muy poderoso, tanto en el lado lógico como en el computacional. (λPω es la esquina λC del cubo) [5]
Relación con otros sistemas
El sistema Automath es similar a λ2 desde un punto de vista lógico. Los lenguajes similares a ML , desde el punto de vista de la mecanografía, se encuentran en algún lugar entre λ → y λ2, ya que admiten un tipo restringido de tipos polimórficos, es decir, los tipos en forma normal prenex. Sin embargo, debido a que cuentan con algunos operadores de recursividad, su potencia de cálculo es mayor que la de λ2. [8] El sistema Coq se basa en una extensión de λC con una jerarquía lineal de universos, en lugar de solo uno no tipificabley la capacidad de construir tipos inductivos.
Pure Type Systems puede verse como una generalización del cubo, con un conjunto arbitrario de clases, axiomas, productos y reglas de abstracción. Por el contrario, los sistemas del cubo lambda se pueden expresar como sistemas de tipo puro con dos clases, el único axioma y un conjunto de reglas tal que . [1]
A través del isomorfismo de Curry-Howard, existe una correspondencia uno a uno entre los sistemas en el cubo lambda y los sistemas lógicos, [1] a saber:
Sistema del cubo | Sistema lógico |
---|---|
λ → | (Primer orden) Cálculo proposicional |
λ2 | Cálculo proposicional de segundo orden |
λ ω | Cálculo proposicional de orden débilmente superior |
λω | Cálculo proposicional de orden superior |
λP | (Primer orden) Lógica de predicados |
λP2 | Cálculo de predicados de segundo orden |
λP ω | Cálculo de predicados de orden superior débil |
λC | Cálculo de construcciones |
Todas las lógicas son implicativas (es decir, las únicas conectivas son y ), sin embargo se pueden definir otros conectivos como o de forma impredicativa en lógicas de segundo y superior orden. En las lógicas débiles de orden superior, hay variables para predicados de orden superior, pero no se puede realizar una cuantificación de ellas.
Propiedades comunes
Todos los sistemas del cubo disfrutan
- la propiedad Church-Rosser : si y entonces existe tal que y ;
- la propiedad de reducción del sujeto : si y luego ;
- la unicidad de los tipos: si y luego .
Todos estos pueden probarse en sistemas genéricos de tipo puro. [10]
Cualquier término bien tipificado en un sistema del cubo se normaliza fuertemente, [1] aunque esta propiedad no es común a todos los sistemas de tipos puros. Ningún sistema del cubo es Turing completo. [8]
Subtipado
Sin embargo, la subtipificación no está representada en el cubo, aunque sistemas como, conocida como cuantificación acotada de orden superior , que combina subtipificación y polimorfismo son de interés práctico y pueden generalizarse aún más a operadores de tipo acotado . Más ampliaciones depermitir la definición de objetos puramente funcionales ; estos sistemas se desarrollaron generalmente después de la publicación del artículo del cubo lambda. [11]
La idea del cubo se debe al matemático Henk Barendregt (1991). El marco de los sistemas de tipos puros generaliza el cubo lambda en el sentido de que todas las esquinas del cubo, así como muchos otros sistemas, pueden representarse como instancias de este marco general. [12] Este marco es anterior al cubo lambda por un par de años. En su artículo de 1991, Barendregt también define las esquinas del cubo en este marco.
Ver también
- En su Habilitation à diriger les recherches, [13] Olivier Ridoux da una plantilla recortada del cubo lambda y también una representación dual del cubo como un octaedro, donde los 8 vértices son reemplazados por caras, así como una representación dual como un dodecaedro, donde las 12 aristas se reemplazan por caras.
- Teoría del tipo de homotopía
Notas
- ↑ a b c d Barendregt, Henk (1991). "Introducción a los sistemas de tipos generalizados". Revista de programación funcional . 1 (2): 125-154. doi : 10.1017 / s0956796800020025 . hdl : 2066/17240 . ISSN 0956-7968 .
- ^ Nederpelt, Rob; Geuvers, Herman (2014). Teoría de tipos y prueba formal . Prensa de la Universidad de Cambridge. pag. 69. ISBN 9781107036505.
- ^ Nederpelt y Geuvers 2014 , p. 85
- ^ Nederpelt y Geuvers 2014 , p. 100
- ^ a b WikiAudio (22 de enero de 2016) Lambda cube
- ^ Schwichtenberg, Helmut (1975). "Definierbare Funktionen imλ-Kalkül mit Typen". Archiv für Mathematische Logik und Grundlagenforschung (en alemán). 17 (3-4): 113-114. doi : 10.1007 / bf02276799 . ISSN 0933-5846 .
- ^ Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). Pruebas y tipos . Cambridge Tracts en Informática Teórica. 7 . Prensa de la Universidad de Cambridge. ISBN 9780521371810.
- ^ a b c Ridoux, Olivier (1998). Lambda-Prolog de A à Z ... ou presque . [sn] OCLC 494473554 .
- ^ Pierce, Benjamin; Dietzen, Scott; Michaylov, Spiro (1989). Programación en cálculos lambda tipados de orden superior . Departamento de Ciencias de la Computación, Universidad Carnegie Mellon. OCLC 20442222 . CMU-CS-89-111 ERGO-89-075.
- ^ Sørensen, Morten Heine; Urzyczyin, Pawel (2006). "Sistemas de tipo puro y el λ-cubo". Conferencias sobre el isomorfismo de Curry-Howard . Elsevier. págs. 343–359. doi : 10.1016 / s0049-237x (06) 80015-7 . ISBN 9780444520777.
- ^ Pierce, Benjamin (2002). Tipos y lenguajes de programación . Prensa del MIT. págs. 467–490. ISBN 978-0262162098. OCLC 300712077 .
- ^ Pierce 2002 , p. 466
- ^ Ridoux 1998 , p. 70
Otras lecturas
- Peyton Jones, Simon; Meijer, Erik (1997). "Henk: un lenguaje intermedio mecanografiado" (PDF) .
Henk se basa directamente en el cubo lambda , una familia expresiva de cálculos lambda tipificados.
enlaces externos
- Lambda Cube de Barendregt en el contexto de sistemas de tipos puros por Roger Bishop Jones