Sistema F

Cálculo lambda tipificado

El Sistema F (también cálculo lambda polimórfico o cálculo lambda de segundo orden ) es un cálculo lambda tipado que introduce, al cálculo lambda tipado simplemente , un mecanismo de cuantificación universal sobre tipos. El Sistema F formaliza el polimorfismo paramétrico en lenguajes de programación , formando así una base teórica para lenguajes como Haskell y ML . Fue descubierto independientemente por el lógico Jean-Yves Girard (1972) y el científico informático John C. Reynolds .

Mientras que el cálculo lambda de tipos simples tiene variables que abarcan los términos y sus ligantes, el Sistema F también tiene variables que abarcan los tipos y sus ligantes. Por ejemplo, el hecho de que la función identidad pueda tener cualquier tipo de la forma A → A se formalizaría en el Sistema F como el juicio

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }$

donde es una variable de tipo . Las mayúsculas se utilizan tradicionalmente para indicar funciones de nivel de tipo, a diferencia de las minúsculas que se utilizan para funciones de nivel de valor. (El superíndice significa que el límite x es de tipo ; la expresión después de los dos puntos es el tipo de la expresión lambda que la precede). ${\displaystyle \alpha }$ ${\displaystyle \Lambda }$ ${\displaystyle \lambda }$ ${\displaystyle \alpha }$ ${\displaystyle \alpha }$

Como sistema de reescritura de términos , el Sistema F es fuertemente normalizador . Sin embargo, la inferencia de tipos en el Sistema F (sin anotaciones de tipos explícitas) es indecidible. Bajo el isomorfismo de Curry-Howard , el Sistema F corresponde al fragmento de lógica intuicionista de segundo orden que utiliza solo cuantificación universal. El Sistema F puede verse como parte del cubo lambda , junto con cálculos lambda tipados aún más expresivos, incluidos aquellos con tipos dependientes .

Según Girard, la "F" del Sistema F fue elegida por casualidad. ^[1]

Reglas de mecanografía

Las reglas de tipificación del Sistema F son las del cálculo lambda simplemente tipado con el añadido de lo siguiente:

donde son tipos, es una variable de tipo y en el contexto indica que está ligada. La primera regla es la de aplicación y la segunda es la de abstracción. ^{[2] [3]} ${\displaystyle \sigma ,\tau }$ ${\displaystyle \alpha }$ ${\displaystyle \alpha ~{\text{type}}}$ ${\displaystyle \alpha }$

Lógica y predicados

El tipo se define como: , donde es una variable de tipo . Esto significa: es el tipo de todas las funciones que toman como entrada un tipo α y dos expresiones de tipo α, y producen como salida una expresión de tipo α (nótese que consideramos que es asociativa por la derecha ). ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$ ${\displaystyle \alpha }$ ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle \to }$

Se utilizan las dos definiciones siguientes para los valores booleanos y , que extienden la definición de los valores booleanos de Church : ${\displaystyle \mathbf {T} }$ ${\displaystyle \mathbf {F} }$

${\displaystyle \mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x}$

${\displaystyle \mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y}$

(Tenga en cuenta que las dos funciones anteriores requieren tres —no dos— argumentos. Las dos últimas deberían ser expresiones lambda, pero la primera debería ser un tipo. Este hecho se refleja en el hecho de que el tipo de estas expresiones es ; el cuantificador universal que une a α corresponde a Λ que une a alfa en la expresión lambda misma. Además, tenga en cuenta que es una abreviatura conveniente de , pero no es un símbolo del Sistema F en sí, sino más bien un "meta-símbolo". Del mismo modo, y también son "meta-símbolos", abreviaturas convenientes, de "ensamblajes" del Sistema F (en el sentido de Bourbaki); de lo contrario, si tales funciones pudieran nombrarse (dentro del Sistema F), entonces no habría necesidad del aparato expresivo de lambda capaz de definir funciones anónimamente y del combinador de punto fijo , que evita esa restricción). ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$ ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$ ${\displaystyle \mathbf {T} }$ ${\displaystyle \mathbf {F} }$

Luego, con estos dos términos, podemos definir algunos operadores lógicos (que son del tipo ): ${\displaystyle \lambda }$ ${\displaystyle {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}\rightarrow {\mathsf {Boolean}}}$

${\displaystyle {\begin{aligned}\mathrm {AND} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,y\,\mathbf {F} \\\mathrm {OR} &=\lambda x^{\mathsf {Boolean}}\lambda y^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {T} \,y\\\mathrm {NOT} &=\lambda x^{\mathsf {Boolean}}{.}x\,{\mathsf {Boolean}}\,\mathbf {F} \,\mathbf {T} \end{aligned}}}$

Tenga en cuenta que en las definiciones anteriores, es un argumento de tipo para , que especifica que los otros dos parámetros que se proporcionan a son de tipo . Al igual que en las codificaciones de Church, no es necesaria una función IFTHENELSE , ya que se pueden utilizar términos tipificados como funciones de decisión. Sin embargo, si se solicita una: ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle {\mathsf {Boolean}}}$

${\displaystyle \mathrm {IFTHENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Boolean}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz}$

Un predicado es una función que devuelve un valor tipificado. El predicado más fundamental es ISZERO , que devuelve si y solo si su argumento es el numeral de la Iglesia 0 : ${\displaystyle {\mathsf {Boolean}}}$ ${\displaystyle \mathbf {T} }$

${\displaystyle \mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\,(\lambda x^{\mathsf {Boolean}}{.}\mathbf {F} )\,\mathbf {T} }$

Estructuras del sistema F

El sistema F permite que las construcciones recursivas se incorporen de manera natural, similar a la teoría de tipos de Martin-Löf . Las estructuras abstractas ( S ) se crean utilizando constructores . Se trata de funciones tipificadas como:

${\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}$.

La recursividad se manifiesta cuando S aparece dentro de uno de los tipos . Si tienes m de estos constructores, puedes definir el tipo de S como: ${\displaystyle K_{i}}$

${\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha }$

Por ejemplo, los números naturales se pueden definir como un tipo de datos inductivo N con constructores.

${\displaystyle {\begin{aligned}{\mathit {zero}}&:\mathrm {N} \\{\mathit {succ}}&:\mathrm {N} \rightarrow \mathrm {N} \end{aligned}}}$

El tipo del Sistema F correspondiente a esta estructura es . Los términos de este tipo comprenden una versión tipificada de los numerales de Church , de los cuales los primeros son: ${\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$

${\displaystyle {\begin{aligned}0&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x\\1&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx\\2&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)\\3&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))\end{aligned}}}$

Si invertimos el orden de los argumentos currificados ( es decir, ), entonces el numeral de Church para n es una función que toma una función f como argumento y devuelve la n ^-ésima potencia de f . Es decir, un numeral de Church es una función de orden superior : toma una función de un solo argumento f y devuelve otra función de un solo argumento. ${\displaystyle \forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }$

Uso en lenguajes de programación

La versión del Sistema F utilizada en este artículo es un cálculo de tipo explícito o de tipo Church. La información de tipado contenida en los términos λ hace que la comprobación de tipos sea sencilla. Joe Wells (1994) resolvió un "problema abierto embarazoso" al demostrar que la comprobación de tipos es indecidible para una variante del Sistema F de tipo Curry, es decir, una que carece de anotaciones de tipado explícitas. ^{[4] [5]}

El resultado de Wells implica que la inferencia de tipos para el Sistema F es imposible. Una restricción del Sistema F conocida como " Hindley–Milner ", o simplemente "HM", tiene un algoritmo de inferencia de tipos fácil y se utiliza para muchos lenguajes de programación funcional de tipado estático como Haskell 98 y la familia ML . Con el tiempo, a medida que las restricciones de los sistemas de tipos de estilo HM se han vuelto evidentes, los lenguajes han ido avanzando hacia lógicas más expresivas para sus sistemas de tipos. GHC , un compilador de Haskell, va más allá de HM (a partir de 2008) y utiliza el Sistema F extendido con igualdad de tipos no sintáctica; ^[6] Las características no HM en el sistema de tipos de OCaml incluyen GADT . ^{[7] [8]}

El isomorfismo de Girard-Reynolds

En la lógica intuicionista de segundo orden , el cálculo lambda polimórfico de segundo orden (F2) fue descubierto por Girard (1972) e independientemente por Reynolds (1974). ^[9] Girard demostró el Teorema de Representación : que en la lógica de predicados intuicionista de segundo orden (P2), las funciones de los números naturales a los números naturales que pueden probarse totales, forman una proyección de P2 en F2. ^[9] Reynolds demostró el Teorema de Abstracción : que cada término en F2 satisface una relación lógica, que puede ser incorporada en las relaciones lógicas P2. ^[9] Reynolds demostró que una proyección de Girard seguida de una incorporación de Reynolds forman la identidad, es decir, el Isomorfismo de Girard-Reynolds . ^[9]

Sistema Fω

Mientras que el Sistema F corresponde al primer eje del cubo lambda de Barendregt , el Sistema F _ω o cálculo lambda polimórfico de orden superior combina el primer eje (polimorfismo) con el segundo eje ( operadores de tipo ); es un sistema diferente, más complejo.

El sistema F _ω se puede definir inductivamente en una familia de sistemas, donde la inducción se basa en los tipos permitidos en cada sistema:

• ${\displaystyle F_{n}}$permite tipos:
  • ${\displaystyle \star }$(el tipo de tipos) y
  • ${\displaystyle J\Rightarrow K}$donde y (el tipo de funciones de tipos a tipos, donde el tipo de argumento es de orden inferior) ${\displaystyle J\in F_{n-1}}$ ${\displaystyle K\in F_{n}}$

En el límite, podemos definir el sistema como ${\displaystyle F_{\omega }}$

• ${\displaystyle F_{\omega }={\underset {1\leq i}{\bigcup }}F_{i}}$

Es decir, F _ω es el sistema que permite funciones de tipos a tipos donde el argumento (y el resultado) pueden ser de cualquier orden.

Nótese que aunque F _ω no impone restricciones en el orden de los argumentos en estas asignaciones, sí restringe el universo de los argumentos para estas asignaciones: deben ser tipos en lugar de valores. El sistema F _ω no permite asignaciones de valores a tipos ( tipos dependientes ), aunque sí permite asignaciones de valores a valores ( abstracción), asignaciones de tipos a valores ( abstracción) y asignaciones de tipos a tipos ( abstracción a nivel de tipos). ${\displaystyle \lambda }$ ${\displaystyle \Lambda }$ ${\displaystyle \lambda }$

Sistema F

El sistema F _<: , que se pronuncia "F-sub", es una extensión del sistema F con subtipificación . El sistema F _<: ha sido de importancia central para la teoría de lenguajes de programación desde la década de 1980 ^{[ cita requerida ]} porque el núcleo de los lenguajes de programación funcional , como los de la familia ML , admite tanto el polimorfismo paramétrico como la subtipificación de registros , que se pueden expresar en el sistema F _<: . ^{[10] [11]}

Véase también

• Tipos existenciales : las contrapartes cuantificadas existencialmente de los tipos universales
• Sistema U
• Cubo lambda

Notas

1. Girard, Jean-Yves (1986). "El sistema F de tipos de variables, quince años después". Theoretical Computer Science . 45 : 160. doi :10.1016/0304-3975(86)90044-7. Sin embargo, en [3] se demostró que las reglas obvias de conversión para este sistema, llamado F por casualidad, eran convergentes.
2. Harper R. "Fundamentos prácticos para lenguajes de programación, segunda edición" (PDF) . págs. 142–3.
3. Geuvers H, Nordström B, Dowek G. "Pruebas de programas y formalización de las matemáticas" (PDF) . pág. 51.
4. Wells, JB (20 de enero de 2005). "Intereses de investigación de Joe Wells". Universidad Heriot-Watt.
5. Wells, JB (1999). "La tipabilidad y la comprobación de tipos en el Sistema F son equivalentes e indecidibles". Ann. Pure Appl. Logic . 98 (1–3): 111–156. doi : 10.1016/S0168-0072(98)00047-5 ."El Proyecto Iglesia: La tipificación y la verificación de tipos en {S}ystem {F} son equivalentes e indecidibles". 29 de septiembre de 2007. Archivado desde el original el 29 de septiembre de 2007.
6. "Sistema FC: restricciones de igualdad y coerciones". gitlab.haskell.org . Consultado el 8 de julio de 2019 .
7. "Notas de la versión de OCaml 4.00.1". ocaml.org . 2012-10-05 . Consultado el 2019-09-23 .
8. "Manual de referencia de OCaml 4.09". 2012-09-11 . Consultado el 2019-09-23 .
9. Philip Wadler (2005) El isomorfismo de Girard-Reynolds (segunda edición) Universidad de Edimburgo , Lenguajes de programación y fundamentos en Edimburgo
10. Cardelli, Luca; Martini, Simone; Mitchell, John C.; Scedrov, Andre (1994). "Una extensión del sistema F con subtipificación". Información y Computación, vol. 9 . Holanda Septentrional, Ámsterdam. págs. 4–56. doi : 10.1006/inco.1994.1013 .
11. Pierce, Benjamin (2002). Tipos y lenguajes de programación . MIT Press. ISBN 978-0-262-16209-8.Capítulo 26: Cuantificación acotada

Referencias

• Girard, Jean-Yves (1971). "Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types". Actas del Segundo Simposio de Lógica Escandinava . Ámsterdam. págs. 63–92. doi :10.1016/S0049-237X(08)70843-7.
• Girard, Jean-Yves (1972), Interprétation fonctionnelle et elimination des coupures de l'arithmétique d'ordre supérieur (tesis doctoral) (en francés), Université Paris 7.
• Reynolds, John (1974). Hacia una teoría de la estructura de tipos (PDF) .
• Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). Pruebas y tipos. Cambridge University Press. ISBN 978-0-521-37181-0.
• Wells, JB (1994). "La tipabilidad y la comprobación de tipos en el cálculo lambda de segundo orden son equivalentes e indecidibles". Actas del 9.º Simposio anual IEEE sobre lógica en informática (LICS) . pp. 176–185. doi :10.1109/LICS.1994.316068. ISBN. 0-8186-6310-3.Versión posdata

Lectura adicional

• Pierce, Benjamin (2002). "V Polymorphism Cap. 23. Universal Types, Cap. 25. An ML Implementation of System F". Tipos y lenguajes de programación . MIT Press. págs. 339–362, 381–388. ISBN 0-262-16209-1.

Enlaces externos

• Resumen del Sistema F de Franck Binard.
• System Fω: el caballo de batalla de los compiladores modernos por Greg Morrisett