Cubo lambda

El cubo lambda. La dirección de cada flecha es la dirección de inclusión.

En lógica matemática y teoría de tipos , el λ-cubo (también escrito cubo lambda ) 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 de tipos simples . 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 x ( ): tipos que pueden vincular términos, correspondientes a tipos dependientes . ${\displaystyle \rightarrow }$
• Eje y ( ): términos que pueden unir tipos, correspondientes al polimorfismo . ${\displaystyle \uparrow }$
• Eje z ( ): tipos que pueden vincular tipos, correspondientes a operadores de tipo (de vinculación) . ${\displaystyle \nearrow }$

Las diferentes formas de combinar estas tres dimensiones dan como resultado los 8 vértices del cubo, cada uno de los cuales corresponde a un tipo diferente de sistema tipificado. El λ-cubo se puede generalizar al concepto de un sistema de tipos puros .

Ejemplos de sistemas

(λ→) Cálculo lambda de tipos simples

El sistema más simple que se encuentra en el λ-cubo es el cálculo lambda de tipos simples , también llamado λ→. En este sistema, la única forma de construir una abstracción es haciendo que un término dependa de otro término , con la regla de tipificación :

${\displaystyle {\frac {\Gamma ,x:\sigma \;\vdash \;t:\tau }{\Gamma \;\vdash \;\lambda x.t:\sigma \to \tau }}}$

(λ2) Sistema F

En el Sistema F (también llamado λ2 por el "cálculo lambda tipado de segundo orden") ^[2] hay otro tipo de abstracción, escrita con , que permite que los términos dependan de tipos , con la siguiente regla: ${\displaystyle \Lambda }$

${\displaystyle {\frac {\Gamma \;\vdash \;t:\sigma }{\Gamma \;\vdash \;\Lambda \alpha .t:\Pi \alpha .\sigma }}\;{\text{ if }}\alpha {\text{ does not occur free in }}\Gamma }$

Los términos que comienzan con a se denominan polimórficos , ya que se pueden aplicar a diferentes tipos para obtener diferentes funciones, de manera similar a las funciones polimórficas en lenguajes tipo ML . Por ejemplo, la identidad polimórfica ${\displaystyle \Lambda }$

diversión  x  ->  x

de OCaml tiene tipo

' un  ->  ' un

lo que significa que puede tomar un argumento de cualquier tipo 'ay devolver un elemento de ese tipo. Este tipo corresponde en λ2 al tipo . ${\displaystyle \Pi \alpha .\alpha \to \alpha }$

(λω) Sistema Fω

En el Sistema F se introduce una construcción para suministrar tipos que dependen de otros tipos . Esto se llama constructor de tipos y proporciona una forma de construir "una función con un tipo como valor ". ^[3] Un ejemplo de un constructor de tipos de este tipo es el tipo de árboles binarios con hojas etiquetadas por datos de un tipo dado : , donde " " significa informalmente " 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 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: ${\displaystyle {\underline {\omega }}}$ ${\displaystyle A}$ ${\displaystyle {\mathsf {TREE}}:=\lambda A:*.\Pi B.(A\to B)\to (B\to B\to B)\to B}$ ${\displaystyle A:*}$ ${\displaystyle A}$ ${\displaystyle A}$ ${\displaystyle {\mathsf {TREE}}}$ ${\displaystyle A}$

tipo  ' un  árbol  =  |  Hoja  de  ' un  |  Nodo  de  ' un  árbol  *  ' un  árbol

Este constructor de tipos se puede aplicar a otros tipos para obtener nuevos tipos. Por ejemplo, para obtener el tipo de árboles de números enteros:

tipo  int_tree  =  int  árbol

El sistema F generalmente no se utiliza por sí solo, pero es útil para aislar la característica independiente de los constructores de tipos. ^[4] ${\displaystyle {\underline {\omega }}}$

(λP) Lambda-P

En el sistema λP , también llamado ΛΠ, y estrechamente relacionado con el Marco Lógico LF , existen los llamados tipos dependientes . Estos son tipos a los que se les permite depender de términos . La regla de introducción crucial del sistema es

${\displaystyle {\frac {\Gamma ,x:A\;\vdash \;B:*}{\Gamma \;\vdash \;(\Pi x:A.B):*}}}$

donde representa tipos válidos. El nuevo constructor de tipos corresponde, 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 solo conectivo. Un ejemplo de estos tipos dependientes en la programación concreta es el tipo de vectores de una cierta longitud: la longitud es un término, del cual depende el tipo. ${\displaystyle *}$ ${\displaystyle \Pi }$

(λω) Sistema Fω

El sistema Fω combina tanto el constructor del sistema F como los constructores de tipos del sistema F. Por lo tanto, el sistema Fω proporciona tanto términos que dependen de tipos como tipos que dependen de tipos . ${\displaystyle \Lambda }$ ${\displaystyle {\underline {\omega }}}$

(λC) Cálculo de construcciones

En el cálculo de construcciones , denotado como λC en el cubo o como λPω, ^{[1] : 130} estas cuatro características cohabitan, de modo que tanto los tipos como los términos pueden depender de tipos y términos. La clara frontera que existe en λ→ entre términos y tipos se elimina en cierta medida, ya que todos los tipos excepto el universal son en sí mismos términos con un tipo. ${\displaystyle \square }$

Definición formal

Como ocurre con todos los sistemas basados ​​en el cálculo lambda de tipos simples, todos los sistemas del cubo se proporcionan en dos pasos: primero, los términos sin procesar, junto con una noción de β-reducción , y luego las reglas de tipificación que permiten tipificar esos términos.

El conjunto de tipos se define como , los tipos se representan con la letra . También existe un conjunto de variables, representadas por las letras . Los términos en bruto de los ocho sistemas del cubo se dan mediante la siguiente sintaxis: ${\displaystyle S:=\{*,\square \}}$ ${\displaystyle s}$ ${\displaystyle V}$ ${\displaystyle x,y,\dots }$

${\displaystyle A:=x\mid s\mid A~A\mid \lambda x:A.A\mid \Pi x:A.A}$

y denotando cuando no ocurre libre en . ${\displaystyle A\to B}$ ${\displaystyle \Pi x:A.B}$ ${\displaystyle x}$ ${\displaystyle B}$

Los entornos, como es habitual en los sistemas tipificados, vienen dados por ${\displaystyle \Gamma :=\emptyset \mid \Gamma ,x:A}$

La noción de β-reducción es común a todos los sistemas del cubo. Se escribe y se da mediante las reglas. Su clausura reflexiva y transitiva se escribe . ${\displaystyle \to _{\beta }}$ $${\displaystyle {\frac {}{(\lambda x:A.B)~C\to _{\beta }B[C/x]}}}$$ $${\displaystyle {\frac {B\to _{\beta }B'}{\lambda x:A.B\to _{\beta }\lambda x:A.B'}}}$$ $${\displaystyle {\frac {A\to _{\beta }A'}{\lambda x:A.B\to _{\beta }\lambda x:A'.B}}}$$ $${\displaystyle {\frac {B\to _{\beta }B'}{\Pi x:A.B\to _{\beta }\Pi x:A.B'}}}$$ $${\displaystyle {\frac {A\to _{\beta }A'}{\Pi x:A.B\to _{\beta }\Pi x:A'.B}}}$$ ${\displaystyle =_{\beta }}$

Las siguientes reglas de escritura también son comunes a todos los sistemas del cubo: $${\displaystyle {\frac {}{\vdash *:\square }}\quad {\text{(Axiom)}}}$$ $${\displaystyle {\frac {\Gamma \vdash A:s\quad x{\text{ does not occur in }}\Gamma }{\Gamma ,x:A\vdash x:A}}\quad {\text{(Start)}}}$$ $${\displaystyle {\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s}{\Gamma ,x:C\vdash A:B}}\quad {\text{(Weakening)}}}$$ $${\displaystyle {\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash D:A}{\Gamma \vdash CD:B[D/x]}}\quad {\text{(Application)}}}$$ $${\displaystyle {\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(Conversion)}}}$$

La diferencia entre los sistemas está en los pares de tipos que se permiten en las siguientes dos reglas de tipificación: ${\textstyle (s_{1},s_{2})}$ $${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \Pi x:A.B:s_{2}}}\quad {\text{(Product)}}}$$ ${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash C:B\quad \Gamma ,x:A\vdash B:s_{2}}{\Gamma \vdash \lambda x:A.C:\Pi x:A.B}}\quad {\text{(Abstraction)}}}$

La correspondencia entre los sistemas y los pares permitidos en las reglas es la siguiente: ${\textstyle (s_{1},s_{2})}$

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: ${\textstyle (*,*)}$

• ${\textstyle (*,*)}$permite que los términos dependan de los términos.
• ${\textstyle (*,\square )}$permite que los tipos dependan de los términos.
• ${\textstyle (\square ,*)}$permite que los términos dependan de los tipos.
• ${\textstyle (\square ,\square )}$permite que los tipos dependan de tipos.

Comparación entre los sistemas

λ→

Una derivación típica que se puede obtener es o con el atajo de flecha que se asemeja mucho a la identidad (de tipo ) del λ→ habitual. Tenga en cuenta que todos los tipos utilizados deben aparecer en el contexto, porque la única derivación que se puede realizar en un contexto vacío es . $${\displaystyle \alpha :*\vdash \lambda x:\alpha .x:\Pi x:\alpha .\alpha }$$ $${\displaystyle \alpha :*\vdash \lambda x:\alpha .x:\alpha \to \alpha }$$ ${\textstyle \alpha }$ ${\textstyle \vdash *:\square }$

La potencia de cálculo es bastante débil, corresponde a los polinomios extendidos (polinomios junto con un operador condicional). ^[5]

λ2

En λ2, se pueden obtener términos como con . Si se lee como una cuantificación universal, a través del isomorfismo de Curry-Howard, esto puede verse como una prueba del principio de explosión. En general, λ2 agrega la posibilidad de tener tipos impredicativos como , es decir, términos que cuantifican sobre todos los tipos, incluidos ellos mismos. El polimorfismo también permite la construcción de funciones que no eran construibles en λ→. Más precisamente, las funciones definibles en λ2 son aquellas demostrablemente totales en la aritmética de Peano de segundo orden . ^[6] En particular, todas las funciones recursivas primitivas son definibles. $${\displaystyle \vdash (\lambda \beta :*.\lambda x:\bot .x\beta ):\Pi \beta :*.\bot \to \beta }$$ ${\textstyle \bot =\Pi \alpha :*.\alpha }$ ${\textstyle \Pi }$ ${\textstyle \bot }$

lambda

En λP, la capacidad de tener tipos que dependen de términos significa que se pueden expresar predicados lógicos. Por ejemplo, el siguiente es derivable: lo que corresponde, a través del isomorfismo de Curry-Howard, a una prueba de . 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. ^[7] $${\displaystyle {\begin{array}{l}\alpha :*,a_{0}:\alpha ,p:\alpha \to *,q:*\vdash \\\quad \lambda z:(\Pi x:\alpha .px\to q).\\\quad \lambda y:(\Pi x:\alpha .px).\\\quad (za_{0})(ya_{0}):(\Pi x:\alpha .px\to q)\to (\Pi x:\alpha .px)\to q\end{array}}}$$ ${\displaystyle (\forall x:A,Px\to Q)\to (\forall x:A,Px)\to Q}$

La regla de conversión es muy necesaria cuando se trabaja con tipos dependientes, porque permite realizar cálculos sobre los términos del tipo. Por ejemplo, si se tiene y , se debe aplicar la regla de conversión ^[a] para obtener y poder escribir . ${\displaystyle \Gamma \vdash A:P((\lambda x.x)y)}$ ${\displaystyle \Gamma \vdash B:\Pi x:P(y).C}$ ${\displaystyle \Gamma \vdash A:P(y)}$ ${\displaystyle \Gamma \vdash BA:C}$

λω

En λω, el siguiente operador es definible, es decir . La derivación se puede obtener ya en λ2, sin embargo, el polimorfismo solo se puede definir si la regla también está presente. $${\displaystyle AND:=\lambda \alpha :*.\lambda \beta :*.\Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma }$$ ${\displaystyle \vdash AND:*\to *\to *}$ $${\displaystyle \alpha :*,\beta :*\vdash \Pi \gamma :*.(\alpha \to \beta \to \gamma )\to \gamma :*}$$ ${\textstyle AND}$ ${\textstyle (\square ,*)}$

Desde un punto de vista computacional, λω es extremadamente fuerte y ha sido considerado como base para lenguajes de programación. ^[10]

lambda

El cálculo de construcciones tiene tanto la expresividad predicativa de λP como el poder computacional de λω, de ahí que λC también se llame λPω, ^{[1] : 130} por lo que es muy potente, tanto en el lado lógico como en el lado computacional.

Relación con otros sistemas

El sistema Automath es similar a λ2 desde un punto de vista lógico. Los lenguajes tipo ML , desde un punto de vista de tipificación, se encuentran en algún punto 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 presentan algunos operadores de recursión, su poder de cálculo es mayor que el de λ2. ^[7] El sistema Coq se basa en una extensión de λC con una jerarquía lineal de universos, en lugar de solo uno no tipificable , y la capacidad de construir tipos inductivos. ${\textstyle \square }$

Los sistemas de tipos puros pueden considerarse como una generalización del cubo, con un conjunto arbitrario de ordenaciones, axiomas, productos y reglas de abstracción. Por el contrario, los sistemas del cubo lambda pueden expresarse como sistemas de tipos puros con dos ordenaciones , el único axioma y un conjunto de reglas tales que . ^[1] ${\displaystyle \{*,\square \}}$ ${\textstyle \{*,\square \}}$ ${\textstyle R}$ ${\displaystyle \{(*,*,*)\}\subseteq R\subseteq \{(*,*,*),(*,\square ,\square ),(\square ,*,*),(\square ,\square ,\square )\}}$

A través del isomorfismo de Curry-Howard, existe una correspondencia uno a uno entre los sistemas del cubo lambda y los sistemas lógicos, ^[1] a saber:

Todas las lógicas son implicativas (es decir, los únicos conectivos son y ), sin embargo, se pueden definir otros conectivos como o de manera impredicativa en lógicas de segundo orden y de orden superior. En las lógicas débiles de orden superior, hay variables para predicados de orden superior, pero no se puede realizar ninguna cuantificación sobre ellas. ${\textstyle \to }$ ${\textstyle \forall }$ ${\displaystyle \wedge }$ ${\displaystyle \neg }$

Propiedades comunes

Todos los sistemas del cubo disfrutan

• la propiedad de Church-Rosser : si y entonces existe tal que y ; ${\displaystyle M\to _{\beta }N}$ ${\displaystyle M\to _{\beta }N'}$ ${\displaystyle N''}$ ${\displaystyle N\to _{\beta }^{*}N''}$ ${\displaystyle N'\to _{\beta }^{*}N''}$
• la propiedad de reducción de sujeto : si y entonces ; ${\displaystyle \Gamma \vdash M:T}$ ${\displaystyle M\to _{\beta }M'}$ ${\displaystyle \Gamma \vdash M':T}$
• la unicidad de los tipos: si y entonces . ${\displaystyle \Gamma \vdash A:B}$ ${\displaystyle \Gamma \vdash A:B'}$ ${\displaystyle B=_{\beta }B'}$

Todo esto se puede demostrar en sistemas de tipos puros genéricos. ^[11]

Cualquier término bien tipificado en un sistema del cubo es fuertemente normalizante, ^[1] aunque esta propiedad no es común a todos los sistemas de tipos puros. Ningún sistema del cubo es Turing completo. ^[7]

Subtipificación

Sin embargo, la subtipificación no está representada en el cubo, aunque sistemas como , conocido como cuantificación acotada de orden superior, que combina la subtipificación y el polimorfismo, son de interés práctico y se pueden generalizar a operadores de tipo acotados. Se han realizado extensiones adicionales para permitir la definición de objetos puramente funcionales; estos sistemas se desarrollaron generalmente después de que se publicara el artículo sobre el cubo lambda. ^[12] ${\displaystyle F_{<:}^{\omega }}$ ${\displaystyle F_{<:}^{\omega }}$

La idea del cubo se debe al matemático Henk Barendregt (1991). El marco de trabajo de los sistemas de tipos puros generaliza el cubo lambda en el sentido de que todos los vértices del cubo, así como muchos otros sistemas, pueden representarse como instancias de este marco de trabajo general. ^[13] Este marco de trabajo es anterior al cubo lambda en un par de años. En su artículo de 1991, Barendregt también define los vértices del cubo en este marco de trabajo.

Véase también

• En su Habilitation à diriger les recherches , ^[14] Olivier Ridoux proporciona una plantilla recortada del cubo lambda y también una representación dual del cubo como octaedro, donde los 8 vértices son reemplazados por caras, así como una representación dual como dodecaedro, donde las 12 aristas son reemplazadas por caras.

Notas

1. 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. S2CID  44757552.
2. Nederpelt, Rob; Geuvers, Herman (2014). Teoría de tipos y demostración formal. Cambridge University Press. pág. 69. ISBN 9781107036505.
3. Nederpelt y Geuvers 2014, pág. 85
4. Nederpelt y Geuvers 2014, pág. 100
5. 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. S2CID  11598130.
6. Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). Pruebas y tipos . Cambridge Tracts in Theoretical Computer Science. Vol. 7. Cambridge University Press. ISBN 9780521371810.
7. Ridoux, Olivier (1998). Lambda-Prolog de A à Z... ou presque (PDF) . [número] OCLC  494473554.
8. Angiuli, Carlo; Gratzer, Daniel (2024). "2.1.3 ¿Quién verifica las reglas de tipificación? y 2.2 Hacia la sintaxis de la teoría de tipos dependientes". Principios de la teoría de tipos dependientes (PDF) . Universidad de Indiana y Universidad de Aarhus . Consultado el 7 de septiembre de 2024 .
9. Favier, Naïm (17 de agosto de 2023). «En la regla de inferencia de conversión del cubo lambda, ¿por qué es necesario Γ ⊢ B′:s?». Stack Exchange en Ciencias de la Computación . Consultado el 7 de septiembre de 2024 .
10. 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.
11. Sørensen, Morten Heine; Urzyczyin, Pawel (2006). "Sistemas de tipos puros y el λ-cubo". Lecciones sobre el isomorfismo de Curry-Howard . Elsevier. págs. 343–359. doi :10.1016/s0049-237x(06)80015-7. ISBN 9780444520777.
12. Pierce, Benjamin (2002). Tipos y lenguajes de programación . MIT Press. pp. 467–490. ISBN 978-0262162098.OCLC 300712077  .
13. Pierce 2002, pág. 466
14. Ridoux 1998, pág. 70

1. La suposición de la regla de conversión es una conveniencia; en su lugar, se podría demostrar un metateorema que ... ^{[8] [9]} ${\displaystyle \Gamma \vdash B':s}$ ${\displaystyle \Gamma \vdash A:B\land B=_{\beta }B'\Rightarrow \Gamma \vdash B':s}$

Lectura adicional

• Peyton Jones, Simon; Meijer, Erik (1997). "Henk: A Typed Intermediate Language" (PDF) . Microsoft . Henk se basa directamente en el cubo lambda, una familia expresiva de cálculos lambda tipados.

Enlaces externos

• El cubo Lambda de Barendregt en el contexto de los sistemas de tipos puros por Roger Bishop Jones