Sistema F

Cálculo lambda mecanografiado

El sistema F (también cálculo lambda polimórfico o cálculo lambda de segundo orden ) es un cálculo lambda tipificado que introduce, al cálculo lambda simplemente tipificado , 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 de forma independiente por el lógico Jean-Yves Girard (1972) y el informático John C. Reynolds .

Mientras que el cálculo lambda de tipo simple tiene variables que abarcan términos y carpetas para ellos, el Sistema F también tiene variables que abarcan tipos y carpetas para ellos. Como 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 se está normalizando fuertemente . Sin embargo, la inferencia de tipos en el Sistema F (sin anotaciones de tipos explícitas) es indecidible. Según el isomorfismo de Curry-Howard , el Sistema F corresponde al fragmento de la lógica intuicionista de segundo orden que utiliza únicamente la cuantificación universal. El sistema F puede verse como parte del cubo lambda , junto con cálculos lambda tipificados 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 tipificado simplemente con la adición de lo siguiente:

donde están los tipos, es una variable de tipo, y en el contexto indica que está enlazada. 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 α (tenga en cuenta que consideramos asociativa 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 , ampliando la definición de los 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 vincular α corresponde a Λ vincular al alfa en la propia expresión lambda. Además, tenga en cuenta que es una abreviatura conveniente para , pero no es un símbolo del Sistema F en sí, sino más bien un "metasímbolo". también "meta-símbolos", abreviaciones convenientes, de los "ensamblajes" del Sistema F (en el sentido Bourbaki, de lo contrario, si tales funciones pudieran nombrarse (dentro del Sistema F), entonces no habría necesidad de un aparato capaz de expresar lambda); de definir funciones de forma anónima y para el 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 de 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 hay un argumento de tipo para , que especifica que los otros dos parámetros que se dan son de tipo . Al igual que en las codificaciones de Church, no hay necesidad de una función IFTHENELSE ya que simplemente se pueden usar términos escritos sin formato como funciones de decisión. Sin embargo, si se solicita: ${\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}$

servirá. Un predicado es una función que devuelve un valor escrito. El predicado más fundamental es ISZERO que devuelve si y sólo si su argumento es el número de 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 incorporar construcciones recursivas de forma natural, similar a la de la teoría de tipos de Martin-Löf . Las estructuras abstractas ( S ) se crean utilizando constructores . Estas son funciones escritas como:

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

La recursividad se manifiesta cuando el propio S aparece dentro de uno de los tipos . Si tiene m de estos constructores, puede 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 de Sistema F correspondiente a esta estructura es . Los términos de este tipo comprenden una versión mecanografiada de los números de la Iglesia , los primeros de los cuales 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 al curry ( es decir, ), entonces el número de Church para n es una función que toma una función f como argumento y devuelve la ^enésima potencia de f . Es decir, un número de Church es una función de orden superior : toma una función f de un solo argumento 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 explícitamente escrito o estilo Church. La información de escritura contenida en los términos λ facilita la verificación de tipos . Joe Wells (1994) resolvió un "problema abierto embarazoso" al demostrar que la verificación de tipos es indecidible para una variante del Sistema F estilo Curry, es decir, una que carece de anotaciones de tipeo 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 sencillo y se utiliza para muchos lenguajes de programación funcionales tipados estáticamente , como Haskell 98 y la familia ML . Con el tiempo, a medida que las restricciones de los sistemas tipográficos de estilo HM se hicieron evidentes, los lenguajes se han movido constantemente hacia lógicas más expresivas para sus sistemas tipográficos. 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ácticos; ^[6] Las características que no son HM en el sistema de tipos de OCaml incluyen GADT . ^{[7] [8]}

El isomorfismo de Girard-Reynolds

En 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 la representación : que en la lógica de predicados intuicionista de segundo orden (P2), las funciones desde los números naturales hasta los números naturales que pueden demostrarse como totales, forman una proyección de P2 a F2. ^[9] Reynolds demostró el teorema de la abstracción : que cada término en F2 satisface una relación lógica, que puede integrarse en las relaciones lógicas P2. ^[9] Reynolds demostró que una proyección de Girard seguida de una incrustación de Reynolds forma 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 el 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 sobre 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}$dónde 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) puede ser de cualquier orden.

Tenga en cuenta que aunque F _ω no impone restricciones al 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 en el nivel de tipos). ${\displaystyle \lambda }$ ${\displaystyle \Lambda }$ ${\displaystyle \lambda }$

Sistema F

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

Ver también

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

Notas

1. Girard, Jean-Yves (1986). "El sistema F de tipos variables, quince años después". Informática Teórica . 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 casualmente F, estaban convergiendo.
2. Harper R. "Fundamentos prácticos de los 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) . pag. 51.
4. Wells, JB (20 de enero de 2005). "Intereses de investigación de Joe Wells". Universidad Heriot-Watt.
5. Wells, JB (1999). "La tipificación y la verificación de tipos en el Sistema F son equivalentes e indecidibles". Ana. Pura aplicación. Lógica . 98 (1–3): 111–156. doi : 10.1016/S0168-0072(98)00047-5 ."The Church Project: 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: limitaciones y coacciones de igualdad". gitlab.haskell.org . Consultado el 8 de julio de 2019 .
7. "Notas de la versión de OCaml 4.00.1". ocaml.org . 05/10/2012 . Consultado el 23 de septiembre de 2019 .
8. "Manual de referencia de OCaml 4.09". 2012-09-11 . Consultado el 23 de septiembre de 2019 .
9. Philip Wadler (2005) El isomorfismo de Girard-Reynolds (segunda edición) Universidad de Edimburgo , Fundamentos y lenguajes de programación en Edimburgo
10. Cardelli, Luca; Martini, Simone; Mitchell, John C.; Scedrov, André (1994). "Una extensión del sistema F con subtipos". Información y Computación, vol. 9 . Holanda Septentrional, Ámsterdam. págs. 4–56. doi : 10.1006/inco.1994.1013 .
11. Pierce, Benjamín (2002). Tipos y Lenguajes de Programación . Prensa del MIT. ISBN 978-0-262-16209-8., Capítulo 26: Cuantificación acotada

Referencias

• Girard, Jean-Yves (1971). "Una extensión de la interpretación 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, Juan (1974). Hacia una teoría de la estructura tipográfica (PDF) .
• Girard, Jean-Yves; Lafont, Yves; Taylor, Paul (1989). Pruebas y tipos. Prensa de la Universidad de Cambridge. ISBN 978-0-521-37181-0.
• Wells, JB (1994). "La tipificación y la verificación de tipos en el cálculo lambda de segundo orden son equivalentes e indecidibles". Actas del noveno simposio anual del IEEE sobre lógica en informática (LICS) . págs. 176–185. doi :10.1109/LICS.1994.316068. ISBN 0-8186-6310-3.Versión posdata

Otras lecturas

• Pierce, Benjamín (2002). "V Polimorfismo Capítulo 23. Tipos universales, Capítulo 25. Una implementación ML del sistema F". Tipos y Lenguajes de Programación . Prensa del MIT. 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