En lógica matemática , la disciplina de tipo de intersección es una rama de la teoría de tipos que abarca sistemas de tipos que utilizan el constructor de tipos de intersección. para asignar varios tipos a un solo término. [1] En particular, si un términose le puede asignar tanto el tipo y el tipo , luego se le puede asignar el tipo de intersección (y viceversa). Por lo tanto, el constructor de tipo intersección se puede utilizar para expresar polimorfismo ad hoc heterogéneo finito (en oposición al polimorfismo paramétrico ). Por ejemplo, el término λ se le puede asignar el tipo en la mayoría de los sistemas de tipo intersección, asumiendo el término variable tanto el tipo de función y el tipo de argumento correspondiente .
Los sistemas de tipo de intersección prominentes incluyen el sistema de asignación de tipo Coppo – Dezani, [2] el sistema de asignación de tipo Barendregt-Coppo – Dezani, [3] y el sistema de asignación de tipo de intersección esencial. [4] Lo más sorprendente es que los sistemas de tipo intersección están estrechamente relacionados con (y con frecuencia caracterizan exactamente) las propiedades de normalización de los términos λ bajo reducción β .
En lenguajes de programación, como TypeScript [5] y Scala, [6] los tipos de intersección se utilizan para expresar polimorfismo ad hoc .
Historia
La disciplina del tipo de intersección fue iniciada por Mario Coppo, Mariangiola Dezani-Ciancaglini , Patrick Sallé y Garrel Pottinger. [2] [7] [8] La motivación subyacente era estudiar las propiedades semánticas (como la normalización ) del cálculo λ por medio de la teoría de tipos . [9] Mientras que el trabajo inicial de Coppo y Dezani estableció una caracterización teórica de tipos de fuerte normalización para el cálculo λI, [2] Pottinger extendió esta caracterización al cálculo λK. [7] Además, Sallé aportó la noción del tipo universalque puede asignarse a cualquier término λ, correspondiente a la intersección vacía. [8] Usando el tipo universalpermitió un análisis detallado de la normalización de la cabeza, la normalización y la normalización fuerte. [10] En colaboración con Henk Barendregt , se proporcionó un modelo λ de filtro para un sistema de tipo de intersección, vinculando los tipos de intersección cada vez más estrechamente a la semántica del cálculo λ.
Debido a la correspondencia con la normalización, la tipificación en sistemas de tipo de intersección prominentes (excluyendo el tipo universal) es indecidible . Complementariamente, indecidibilidad del problema dual de tipo habitar en los sistemas de tipo de intersección prominentes fue probada por Paweł Urzyczyn. [11] Más tarde, este resultado se refinó mostrando la completitud del espacio exponencial de la ocupación del tipo de intersección de rango 2 y la indecidibilidad de la ocupación del tipo de intersección de rango 3. [12] Sorprendentemente, la ocupación del tipo principal es decidible en tiempo polinomial . [13]
Sistema de asignación de tipo Coppo – Dezani
El sistema de asignación de tipos Coppo-Dezani extiende el cálculo λ simplemente tipado al permitir que se asuman múltiples tipos para una variable de término. [2]
Idioma del término
El término lenguaje de viene dada por términos λ (o expresiones lambda ):
Tipo de idioma
El tipo de idioma de se define inductivamente por la siguiente gramática:
El constructor de tipo de intersección () se toma módulo de asociatividad, conmutatividad e idempotencia.
Reglas de tipo
Las reglas del tipo , , , y de están:
Propiedades
La tipificabilidad y la normalización están estrechamente relacionadas en por las siguientes propiedades: [2]
- Reducción de sujetos : Si y , luego .
- Normalización : Si, luego tiene una forma β-normal .
- Tipificabilidad de términos λ fuertemente normalizados : Sise está normalizando fuertemente , entonces para algunos y .
- Caracterización de la normalización λI : tiene una forma normal en el cálculo λI, si y solo si para algunos y .
Si el lenguaje de tipos se amplía para contener la intersección vacía, es decir , luego está cerrado bajo β-igualdad y es sólido y completo para la semántica de inferencia. [14]
Sistema de asignación de tipo Barendregt – Coppo – Dezani
El sistema de asignación de tipos Barendregt – Coppo – Dezani amplía el sistema de asignación de tipos Coppo-Dezani en los tres aspectos siguientes: [3]
- introduce la constante de tipo universal (similar a la intersección vacía) que se puede asignar a cualquier término λ.
- permite el constructor de tipo de intersección para aparecer en el lado derecho del constructor de tipo de flecha .
- introduce el subtipo de tipo de intersección orden parcial en los tipos junto con una regla de escritura correspondiente.
Idioma del término
El término lenguaje de viene dada por términos λ (o expresiones lambda ):
Tipo de idioma
El tipo de idioma de se define inductivamente por la siguiente gramática:
Subtipado del tipo de intersección
Subtipado del tipo de intersección se define como el preorden más pequeño (relación reflexiva y transitiva ) sobre los tipos de intersección que satisfacen las siguientes propiedades:
La subtipificación del tipo de intersección se puede decidir en tiempo cuadrático. [15]
Reglas de tipo
Las reglas del tipo , , , , , y de están:
Propiedades
- Semántica :es sano y completo wrt. un modelo λ de filtro, en el que la interpretación de un término λ coincide con el conjunto de tipos que se le pueden asignar. [3]
- Reducción de sujetos : Si y , luego . [3]
- Expansión del sujeto : Si y , luego . [3]
- Caracterización de fuerte normalización :está normalizando fuertemente el wrt. β-reducción, si y solo si es derivable sin regla para algunos y . [dieciséis]
- Pares principales : Si se está normalizando fuertemente, entonces existe un par principal tal que para cualquier escritura el par se puede obtener del par principal mediante ampliaciones de tipo, elevaciones y sustituciones. [17]
Referencias
- ^ Henk Barendregt; Wil Dekkers; Richard Statman (20 de junio de 2013). Cálculo lambda con tipos . Prensa de la Universidad de Cambridge. págs. 1–. ISBN 978-0-521-76614-2.
- ^ a b c d e Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1980). "Una extensión de la teoría de la funcionalidad básica para el cálculo λ". Diario de Notre Dame de lógica formal . 21 (4): 685–693. doi : 10.1305 / ndjfl / 1093883253 .
- ^ a b c d e Barendregt, Henk; Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1983). "Un modelo de filtro lambda y la integridad de la asignación de tipos". Revista de lógica simbólica . 48 (4): 931–940. doi : 10.2307 / 2273659 . JSTOR 2273659 .
- ^ van Bakel, Steffen (2011). "Tipos de intersección estrictos para el cálculo Lambda". Encuestas de computación ACM . 43 (3): 20: 1–20: 49. doi : 10.1145 / 1922649.1922657 .
- ^ "Tipos de intersección en TypeScript" . Consultado el 1 de agosto de 2019 .
- ^ "Tipos de compuestos en Scala" . Consultado el 1 de agosto de 2019 .
- ↑ a b Pottinger, G. (1980). Una asignación de tipo para los términos λ fuertemente normalizables. Para HB Curry: ensayos sobre lógica combinatoria, cálculo lambda y formalismo, 561-577.
- ^ a b Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Sallé, Patrick (1979). "Caracterización funcional de algunas igualdad semántica dentro de Lambda-Calculus". En Hermann A. Maurer (ed.). Autómatas, lenguajes y programación, 6º coloquio, Graz, Austria, 16 al 20 de julio de 1979, Actas . 71 . Saltador. págs. 133-146. doi : 10.1007 / 3-540-09510-1_11 . ISBN 3-540-09510-1.
- ^ Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1978). "Una nueva asignación de tipo para términos λ". Archiv für Mathische Logik und Grundlagenforschung . 19 (1): 139-156. doi : 10.1007 / BF02011875 .
- ^ Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Venneri, Betti (1981). "Caracteres funcionales de términos solubles". Trimestral de lógica matemática . 27 (2–6): 45–58. doi : 10.1002 / malq.19810270205 .
- ^ Urzyczyn, Paweł (1999). "El problema del vacío para los tipos de intersección". Revista de lógica simbólica . 64 (3): 1195-1215. doi : 10.2307 / 2586625 . JSTOR 2586625 .
- ^ Urzyczyn, Paweł (2009). "Habitacion de tipos de interseccion de rango bajo". Conferencia internacional sobre cálculos y aplicaciones Lambda tipificadas . TLCA 2009. 5608 . Saltador. págs. 356–370. doi : 10.1007 / 978-3-642-02273-9_26 . ISBN 978-3-642-02272-2.
- ^ Dudenhefner, Andrej; Rehof, Jakob (2019). "Principado y aproximación bajo cota dimensional". Actas del ACM sobre lenguajes de programación . POPL 2019. 3 . ACM. págs. 8: 1–8: 29. doi : 10.1145 / 3290321 . ISSN 2475-1421 .
- ^ Van Bakel, Steffen (1992). "Restricciones completas de la disciplina tipo intersección". Informática Teórica . 102 (1): 135-163. doi : 10.1016 / 0304-3975 (92) 90297-S .
- ^ Dudenhefner, Andrej; Martens, Moritz; Rehof, Jakob (2017). "El problema de unificación de tipo de intersección algebraica". Métodos lógicos en informática . 13 (3). doi : 10.23638 / LMCS-13 (3: 9) 2017 .
- ^ Ghilezan, Silvia (1996). "Fuerte normalización y tipificabilidad con tipos de intersección". Diario de Notre Dame de lógica formal . 37 (1): 44–52. doi : 10.1305 / ndjfl / 1040067315 .
- ^ Ronchi Della Rocca, Simona; Venneri, Betti (1983). "Esquemas de tipos principales para una teoría de tipos extendida". Informática Teórica . 28 ((1-2)): 151-169. doi : 10.1016 / 0304-3975 (83) 90069-5 .