El sistema F , también conocido como cálculo lambda polimórfico ( Girard-Reynolds ) o cálculo lambda de segundo orden , es un cálculo lambda tipificado que se diferencia del cálculo lambda simplemente tipificado por la introducción de un mecanismo de cuantificación universal sobre tipos. System F formaliza así la noción de polimorfismo paramétrico en lenguajes de programación y forma una base teórica para lenguajes como Haskell y ML . El sistema F fue descubierto de forma independiente por el lógico Jean-Yves Girard (1972) y el científico informático John C. Reynolds (1974).
Mientras que el cálculo lambda simplemente tipeado tiene variables que se extienden sobre términos y vinculantes para ellos, System F también tiene variables que varían entre tipos y vinculadores para ellos. A modo de ejemplo, el hecho de que la función identidad pueda tener cualquier tipo de la forma A → A quedaría formalizado en el Sistema F como el juicio
dónde es una variable de tipo . La mayúscula se utiliza tradicionalmente para denotar funciones a nivel de tipo, en oposición a las minúsculas que se utiliza para funciones a nivel de valor. (El superíndicesignifica que el límite x es de tipo; la expresión después de los dos puntos es el tipo de expresión lambda que la precede).
Como sistema de reescritura de términos , el Sistema F se está normalizando fuertemente . Sin embargo, la inferencia de tipo en el Sistema F (sin anotaciones de tipo 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 ú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" en el Sistema F fue elegida por casualidad. [1]
Reglas de escritura
Las reglas de tipado del Sistema F son las del cálculo lambda simplemente tipeado con la adición de lo siguiente:
(1) | (2) |
dónde son tipos, es una variable de tipo y en el contexto indica que está obligado. La primera regla es la de la aplicación y la segunda la de la abstracción. [2] [3]
Lógica y predicados
La tipo se define como: , dónde 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 ser asociativo por la derecha .)
Las siguientes dos definiciones para los valores booleanos y se utilizan, ampliando la definición de Church booleanos :
(Tenga en cuenta que las dos funciones anteriores requieren tres , no dos, argumentos. Los dos últimos deben ser expresiones lambda, pero el primero debe ser un tipo. Este hecho se refleja en el hecho de que el tipo de estas expresiones es; el cuantificador universal que une el α corresponde al Λ que une el alfa en la expresión lambda misma. 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 "meta-símbolo". Igualmente, y son también "meta-símbolos", abreviaturas convenientes, de "ensamblajes" del Sistema F (en el sentido Bourbaki ); de lo contrario, si tales funciones pudieran ser nombradas (dentro del Sistema F), entonces no habría necesidad del aparato expresivo lambda capaz de definir funciones de forma anónima y para el combinador de punto fijo , que trabaja alrededor de esa restricción).
Entonces, con estos dos -términos, podemos definir algunos operadores lógicos (que son de tipo ):
Tenga en cuenta que en las definiciones anteriores, es un argumento de tipo para , especificando que los otros dos parámetros que se dan a son de tipo . Al igual que en las codificaciones de la Iglesia, no hay necesidad de una función IFTHENELSE , ya que solo se puede usar raw-Términos tipificados como funciones de decisión. Sin embargo, si se solicita uno:
servirá. Un predicado es una función que devuelve un-valor escrito. El predicado más fundamental es ISZERO que devuelvesi y solo si su argumento es el número 0 de la Iglesia :
Estructuras del sistema F
El sistema F permite que las construcciones recursivas se incrusten de forma natural, en relación con la de la teoría de tipos de Martin-Löf . Las estructuras abstractas (S) se crean utilizando constructores . Estas son funciones escritas como:
- .
La recursividad se manifiesta cuando en sí mismo aparece dentro de uno de los tipos . Si usted tiene de estos constructores, puede definir el tipo de como:
Por ejemplo, los números naturales se pueden definir como un tipo de datos inductivo con constructores
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:
- 0: =
- 1: =
- 2: =
- 3: =
Si invertimos el orden de los argumentos al curry ( es decir, ), luego el número de la Iglesia para es una función que toma una función f como argumento y devuelve elth poder de f . Es decir, un numeral 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.
Usar en lenguajes de programación
La versión del Sistema F utilizada en este artículo es un cálculo escrito explícitamente o al estilo de la Iglesia. La información de mecanografía contenida en los términos λ hace que la verificación de tipos sea sencilla. Joe Wells (1994) resolvió un "problema abierto vergonzoso" al demostrar que la verificación de tipos es indecidible para una variante del Sistema F al estilo Curry, es decir, una que carece de anotaciones de escritura 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 tipo fácil y se usa para muchos lenguajes de programación funcional de tipo 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 hecho evidentes, los lenguajes se han movido constantemente 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 usa System F extendido con igualdad de tipos no sintáctica; [6] Las características que no son de 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 demostrarse 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 y 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:
- permite tipos:
- (el tipo de tipos) y
- dónde y (el tipo de funciones de tipos a tipos, donde el tipo de argumento es de un orden inferior)
En el límite, podemos definir el sistema ser - estar
Es decir, F ω es el sistema que permite funciones de tipos a tipos donde el argumento (y el resultado) pueden 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 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), mapeos de tipos a valores ( abstracción) y mapeos de tipos a tipos ( abstracción a nivel de tipos)
Ver también
- Tipos existenciales : las contrapartes cuantificadas existencialmente de los tipos universales.
- Sistema F <: - extiende el sistema F con subtipificación
- Sistema U
Notas
- ^ 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 de este sistema, llamadas F por azar, estaban convergiendo.
- ^ Harper R . "Fundamentos prácticos para lenguajes de programación, segunda edición" (PDF) . págs. 142–3.
- ^ Geuvers H, Nordström B, Dowek G. "Pruebas de programas y formalización de las matemáticas" (PDF) . pag. 51.
- ^ Wells, JB (20 de enero de 2005). "Intereses de investigación de Joe Wells" . Universidad Heriot-Watt.
- ^ Wells, JB (1999). "La tipificabilidad y la verificación de tipos en el Sistema F son equivalentes e indecidibles" . Ana. Pure Appl. Lógica . 98 (1-3): 111-156. doi : 10.1016 / S0168-0072 (98) 00047-5 ."The Church Project: Typability 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.
- ^ "Sistema FC: restricciones de igualdad y coacciones" . gitlab.haskell.org . Consultado el 8 de julio de 2019 .
- ^ "Notas de la versión OCaml 4.00.1" . ocaml.org . 2012-10-05 . Consultado el 23 de septiembre de 2019 .
- ^ "Manual de referencia OCaml 4.09" . 2012-09-11 . Consultado el 23 de septiembre de 2019 .
- ^ a b c d Philip Wadler (2005) El isomorfismo de Girard-Reynolds (segunda edición) Universidad de Edimburgo , lenguajes de programación y fundamentos en Edimburgo
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 . Amsterdam. págs. 63–92. doi : 10.1016 / S0049-237X (08) 70843-7 .
- Girard, Jean-Yves (1972), Interprétation fonctionnelle et élimination 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 tipográfica .
- 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 9º Simposio Anual de IEEE sobre Lógica en Ciencias de la Computación (LICS) . págs. 176-185. doi : 10.1109 / LICS.1994.316068 . ISBN 0-8186-6310-3. Versión PostScript
Otras lecturas
- Pierce, Benjamin (2002). "V Polimorfismo Cap. 23. Tipos universales, Cap. 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 por Franck Binard.
- System F ω : el caballo de batalla de los compiladores modernos por Greg Morrisett