Hispanopedia Wiki
Articulo de referencia

Disciplina de tipo intersección

En lógica matemática , la disciplina de tipos 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...

Hispanopedia WikiContenido en espanolLectura gratuita

En lógica matemática , la disciplina de tipos 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.(∩){\displaystyle (\cap )}asignar múltiples tipos a un solo término. [ 1 ] En particular, si un términoMETRO{\displaystyle M}Se le puede asignar ambos tipos.φ1{\displaystyle \varphi _{1}}y el tipoφ2{\displaystyle \varphi _{2}}, entoncesMETRO{\displaystyle M}Se le puede asignar el tipo de intersección.φ1∩φ2{\displaystyle \varphi _{1}\cap \varphi _{2}}(y viceversa). Por lo tanto, el constructor de tipo intersección puede usarse para expresar polimorfismo ad hoc heterogéneo finito (a diferencia del polimorfismo paramétrico ). Por ejemplo, el término λλincógnita.(incógnitaincógnita){\displaystyle \lambda x.\!(x\;x)}Se le puede asignar el tipo((α→β)∩α)→β{\displaystyle ((\alpha \to \beta )\cap \alpha )\to \beta }en la mayoría de los sistemas de tipo intersección, asumiendo para el término variableincógnita{\displaystyle x}ambos tipos de funciónα→β{\displaystyle \alpha \to \beta }y el tipo de argumento correspondienteα{\displaystyle \alpha }.

Entre los sistemas de tipos de intersección más destacados se incluyen el sistema de asignación de tipos Coppo-Dezani, [ 2 ] el sistema de asignación de tipos Barendregt-Coppo-Dezani, [ 3 ] y el sistema esencial de asignación de tipos de intersección. [ 4 ] Lo más llamativo es que los sistemas de tipos de intersección están estrechamente relacionados con (y a menudo caracterizan exactamente) las propiedades de normalización de los términos λ bajo la 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 de tipos 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 mediante la teoría de tipos . [ 9 ] Si bien el trabajo inicial de Coppo y Dezani estableció una caracterización teórica de tipos de la normalización fuerte para el λ -cálculo I, [ 2 ] Pottinger extendió esta caracterización al λ -cálculo K. [ 7 ] Además, Sallé contribuyó con la noción del tipo universal.ω{\displaystyle \omega }que se puede asignar a cualquier término λ , correspondiendo así a la intersección vacía. [ 8 ] Usando el tipo universalω{\displaystyle \omega }permitió un análisis detallado de la normalización de cabeza, la normalización y la normalización fuerte. [ 10 ] En colaboración con Henk Barendregt , se presentó un modelo λ de filtro para un sistema de tipos de intersección, vinculando los tipos de intersección cada vez más estrechamente con la semántica del cálculo λ .

Debido a la correspondencia con la normalización, la tipabilidad en sistemas de tipos de intersección infinitos es indecidible . Sin embargo, restringir los tipos de intersección a rango finito hace que su tipabilidad sea decidible para cualquier rango finito, lo cual contrasta con el sistema F , donde las restricciones (de cuantificadores) a rangos finitos superiores a 3 aún presentan tipabilidad indecidible. [ 11 ] Por otro lado, si se añaden tipos recursivos a un sistema con tipos de intersección de rango 2 o superior, la tipabilidad se vuelve indecidible en general. [ 12 ]

Complementariamente, Paweł Urzyczyn demostró la indecidibilidad del problema dual de la ocupación de tipos en sistemas de tipos de intersección prominentes. [ 13 ] Posteriormente, este resultado se refinó mostrando la completitud exponencial del espacio de ocupación de tipos de intersección de rango 2 y la indecidibilidad de la ocupación de tipos de intersección de rango 3. [ 14 ] Cabe destacar que la ocupación de tipos principales es decidible en tiempo polinomial . [ 15 ]

Para abordar las dificultades de aplicar la correspondencia de Curry-Howard a los tipos de intersección, Kamareddine y Wells reemplazaron el constructor de intersección en el sistema de deducción con declaraciones de conjuntos finitos (FSD) para el dominio de cada variable en una abstracción lambda, convirtiéndolas en tipos Π . Además, extendieron el cubo lambda a lo que denominan el f-cubo, que posee tipos de intersección codificados con FSD en todos los vértices. El término U de Urzyczyn , que no se puede tipificar en el λ-cubo, sí se puede tipificar en el f-cubo. [ 16 ]

Sistema de asignación de tipos Coppo-Dezani

El sistema de asignación de tipos Coppo-Dezani(⊢CD){\displaystyle (\vdash _{\text{CD}})}Extiende el cálculo λ de tipo simple al permitir que se asuman múltiples tipos para una variable de término. [ 2 ]

Lenguaje de términos

El término lenguaje de(⊢CD){\displaystyle (\vdash _{\text{CD}})}viene dado por términos λ (o expresiones lambda ):

METRO,norte::=incógnita∣(λincógnita.METRO)∣(METROnorte) dónde incógnita abarca variables de plazo{\displaystyle {\begin{aligned}M,N&::=x\mid (\lambda x.\!M)\mid (M\;N)&&{\text{ donde }}x{\text{ varía sobre las variables del término}}\\\end{aligned}}}

Lenguaje de tipos

El lenguaje de tipos de(⊢CD){\displaystyle (\vdash _{\text{CD}})}se define inductivamente mediante la siguiente gramática:

φ::=α∣σ→φ dónde α abarca variables de tipoσ::=φ1∩⋯∩φnorte dónde norte≥1{\displaystyle {\begin{aligned}\varphi &::=\alpha \mid \sigma \to \varphi &&{\text{ donde }}\alpha {\text{ abarca variables de tipo}}\\\sigma &::=\varphi _{1}\cap \cdots \cap \varphi _{n}&&{\text{ donde }}n\geq 1\end{aligned}}}

El constructor de tipo intersección (∩{\displaystyle \cap }) se toma módulo asociatividad, conmutatividad e idempotencia .

Reglas de mecanografía

Las reglas de mecanografía(→I){\displaystyle (\to \!\!{\text{I}})},(→mi){\displaystyle (\to \!\!{\text{E}})},(∩I){\displaystyle (\cap {\text{Yo}})}, y(∩mi){\displaystyle (\cap {\text{E}})}de(⊢CD){\displaystyle (\vdash _{\text{CD}})}son:

Γ,incógnita:σ⊢CDMETRO:φΓ⊢CDλincógnita.METRO:σ→φ(→I)Γ⊢CDMETRO:σ→φΓ⊢CDnorte:σΓ⊢CDMETROnorte:φ(→mi)Γ⊢CDMETRO:φ1…Γ⊢CDMETRO:φnorteΓ⊢CDMETRO:φ1∩⋯∩φnorte(∩I)(1≤i≤norte)Γ,incógnita:φ1∩⋯∩φnorte⊢CDincógnita:φi(∩mi){\displaystyle {\begin{array}{cc}{\dfrac {\Gamma ,x:\sigma \vdash _{\text{CD}}M:\varphi }{\Gamma \vdash _{\text{CD}}\lambda x.\!M:\sigma \to \varphi }}(\to \!\!{\text{I}})&{\dfrac {\Gamma \vdash _{\text{CD}}M:\sigma \to \varphi \quad \Gamma \vdash _{\text{CD}}N:\sigma }{\Gamma \vdash _{\text{CD}}M\;N:\varphi }}(\to \!\!{\text{E}})\\\\{\dfrac {\Gamma \vdash _{\text{CD}}M:\varphi _{1}\quad \ldots \quad \Gamma \vdash _{\text{CD}}M:\varphi _{n}}{\Gamma \vdash _{\text{CD}}M:\varphi _{1}\cap \cdots \cap \varphi _{n}}}(\cap {\text{I}})&{\dfrac {(1\leq i\leq n)}{\Gamma ,x:\varphi _{1}\cap \cdots \cap \varphi _{n}\vdash _{\text{CD}}x:\varphi _{i}}}(\cap {\text{E}})\end{array}}}

Propiedades

La tipabilidad y la normalización están estrechamente relacionadas en(⊢CD){\displaystyle (\vdash _{\text{CD}})}por las siguientes propiedades: [ 2 ]

  • Reducción de sujetos : SiΓ⊢CDMETRO:σ{\displaystyle \Gamma \vdash _{\text{CD}}M:\sigma }yMETRO→βnorte{\displaystyle M\to _{\beta }N}, entoncesΓ⊢CDnorte:σ{\displaystyle \Gamma \vdash _{\text{CD}}N:\sigma }.
  • Normalización : SiΓ⊢CDMETRO:σ{\displaystyle \Gamma \vdash _{\text{CD}}M:\sigma }, entoncesMETRO{\displaystyle M}tiene una forma β -normal .
  • Tipabilidad de los términos λ fuertemente normalizadores : SiMETRO{\displaystyle M}es fuertemente normalizador , entoncesΓ⊢CDMETRO:σ{\displaystyle \Gamma \vdash _{\text{CD}}M:\sigma }para algunosΓ{\displaystyle \Gamma }yσ{\displaystyle \sigma }.
  • Caracterización de la normalización λ I :METRO{\displaystyle M}tiene una forma normal en el cálculo λ I, si y solo siΓ⊢CDMETRO:σ{\displaystyle \Gamma \vdash _{\text{CD}}M:\sigma }para algunosΓ{\displaystyle \Gamma }yσ{\displaystyle \sigma }.

Si el lenguaje de tipos se extiende para contener la intersección vacía, es decirσ=φ1∩⋯∩φnorte dónde norte=0{\displaystyle \sigma =\varphi _{1}\cap \cdots \cap \varphi _{n}{\text{ donde }}n=0}, entonces(⊢CD){\displaystyle (\vdash _{\text{CD}})}es cerrado bajo β -igualdad y es sólido y completo para la semántica de inferencia. [ 17 ]

Sistema de asignación de tipos Barendregt-Coppo-Dezani

El sistema de asignación de tipos Barendregt-Coppo-Dezani(⊢BCD){\displaystyle (\vdash _{\text{BCD}})}extiende el sistema de asignación de tipos Coppo-Dezani en los siguientes tres aspectos: [ 3 ]

  • (⊢BCD){\displaystyle (\vdash _{\text{BCD}})}introduce la constante de tipo universalω{\displaystyle \omega }(similar a la intersección vacía) que se puede asignar a cualquier término λ .
  • (⊢BCD){\displaystyle (\vdash _{\text{BCD}})}permite el constructor de tipo intersección(∩){\displaystyle (\cap )}para aparecer en el lado derecho del constructor de tipo flecha(→){\displaystyle (\to )}.
  • (⊢BCD){\displaystyle (\vdash _{\text{BCD}})}introduce el subtipado de tipo de intersección(≤){\displaystyle (\leq )}orden parcial en tipos junto con una regla de tipado correspondiente.

Lenguaje de términos

El término lenguaje de(⊢BCD){\displaystyle (\vdash _{\text{BCD}})}viene dado por términos λ (o expresiones lambda ):

METRO,norte::=incógnita∣(λincógnita.METRO)∣(METROnorte) dónde incógnita abarca variables de plazo{\displaystyle {\begin{aligned}M,N&::=x\mid (\lambda x.\!M)\mid (M\;N)&&{\text{ donde }}x{\text{ varía sobre las variables del término}}\\\end{aligned}}}

Lenguaje de tipos

El lenguaje de tipos de(⊢BCD){\displaystyle (\vdash _{\text{BCD}})}se define inductivamente mediante la siguiente gramática:

σ,τ::=α∣ω∣σ→τ∣σ∩τ dónde α abarca variables de tipo{\displaystyle {\begin{aligned}\sigma ,\tau &::=\alpha \mid \omega \mid \sigma \to \tau \mid \sigma \cap \tau &&{\text{ donde }}\alpha {\text{ abarca variables de tipo}}\end{aligned}}}

subtipificación del tipo de intersección

subtipificación del tipo de intersección(≤){\displaystyle (\leq )}se define como el preorden más pequeño ( relación reflexiva y transitiva ) sobre tipos de intersección que satisfacen las siguientes propiedades:

σ≤ω,ω≤ω→ω,σ∩τ≤σ,σ∩τ≤τ,(σ→τ1)∩(σ→τ2)≤σ→τ1∩τ2,si σ≤τ1 y σ≤τ2, entonces σ≤τ1∩τ2,si σ2≤σ1 y τ1≤τ2, entonces σ1→τ1≤σ2→τ2{\displaystyle {\begin{aligned}&\sigma \leq \omega ,\quad \omega \leq \omega \to \omega ,\quad \sigma \cap \tau \leq \sigma ,\quad \sigma \cap \tau \leq \tau ,\\&(\sigma \to \tau _{1})\cap (\sigma \to \tau _{2})\leq \sigma \to \tau _{1}\cap \tau _{2},\\&{\text{if }}\sigma \leq \tau _{1}{\text{ and }}\sigma \leq \tau _{2}{\text{, then }}\sigma \leq \tau _{1}\cap \tau _{2},\\&{\text{if }}\sigma _{2}\leq \sigma _{1}{\text{ and }}\tau _{1}\leq \tau _{2}{\text{, then }}\sigma _{1}\to \tau _{1}\leq \sigma _{2}\to \tau _{2}\end{aligned}}}

La subtipificación del tipo de intersección es decidible en tiempo cuadrático. [ 18 ]

Reglas de mecanografía

Las reglas de mecanografía(→I){\displaystyle (\to \!\!{\text{I}})},(→mi){\displaystyle (\to \!\!{\text{E}})},(∩I){\displaystyle (\cap {\text{I}})},(≤){\displaystyle (\leq )},(A){\displaystyle ({\text{A}})}, y(ω){\displaystyle (\omega )}de(⊢BCD){\displaystyle (\vdash _{\text{BCD}})}son:

Γ,incógnita:σ⊢BCDMETRO:τΓ⊢BCDλincógnita.METRO:σ→τ(→I)Γ⊢BCDMETRO:σ→τΓ⊢BCDnorte:σΓ⊢BCDMETROnorte:τ(→mi)Γ⊢BCDMETRO:σΓ⊢BCDMETRO:τΓ⊢BCDMETRO:σ∩τ(∩I)Γ⊢BCDMETRO:σ(σ≤τ)Γ⊢BCDMETRO:τ(≤)Γ,incógnita:σ⊢BCDincógnita:σ(A)Γ⊢BCDMETRO:ω(ω){\displaystyle {\begin{array}{cc}{\dfrac {\Gamma ,x:\sigma \vdash _{\text{BCD}}M:\tau }{\Gamma \vdash _{\text{BCD}}\lambda x.\!M:\sigma \to \tau }}(\to \!\!{\text{I}})&{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \to \tau \quad \Gamma \vdash _{\text{BCD}}N:\sigma }{\Gamma \vdash _{\text{BCD}}M\;N:\tau }}(\to \!\!{\text{E}})\\\\{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \quad \Gamma \vdash _{\text{BCD}}M:\tau }{\Gamma \vdash _{\text{BCD}}M:\sigma \cap \tau }}(\cap {\text{I}})&{\dfrac {\Gamma \vdash _{\text{BCD}}M:\sigma \quad (\sigma \leq \tau )}{\Gamma \vdash _{\text{BCD}}M:\tau }}(\leq )\\\\{\dfrac {}{\Gamma ,x:\sigma \vdash _{\text{BCD}}x:\sigma }}({\text{A}})&{\dfrac {}{\Gamma \vdash _{\text{BCD}}M:\omega }}(\omega )\end{array}}}

Propiedades

  • Semántica :(⊢BCD){\displaystyle (\vdash _{\text{BCD}})}es sólido y completo con respecto a 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Γ⊢BCDMETRO:σ{\displaystyle \Gamma \vdash _{\text{BCD}}M:\sigma }yMETRO→βnorte{\displaystyle M\to _{\beta }N}, entoncesΓ⊢BCDnorte:σ{\displaystyle \Gamma \vdash _{\text{BCD}}N:\sigma }. [ 3 ]
  • Expansión del tema : SiΓ⊢BCDnorte:σ{\displaystyle \Gamma \vdash _{\text{BCD}}N:\sigma }yMETRO→βnorte{\displaystyle M\to _{\beta }N}, entoncesΓ⊢BCDMETRO:σ{\displaystyle \Gamma \vdash _{\text{BCD}}M:\sigma }. [ 3 ]
  • Caracterización de la normalización fuerte :METRO{\displaystyle M}es fuertemente normalizador con respecto a la β- reducción, si y solo siΓ⊢BCDMETRO:σ{\displaystyle \Gamma \vdash _{\text{BCD}}M:\sigma }es derivable sin regla(ω){\displaystyle (\omega )}para algunosΓ{\displaystyle \Gamma }yσ{\displaystyle \sigma }. [ 19 ]
  • Pares principales (también conocidos como "tipificaciones principales" [ 20 ] ): SiMETRO{\displaystyle M}Si es fuertemente normalizador, entonces existe un par principal.(Γ,σ){\displaystyle (\Gamma ,\sigma )}de tal manera que para cualquier tipoΓ′⊢BCDMETRO:σ′{\displaystyle \Gamma '\vdash _{\text{BCD}}M:\sigma '}la pareja(Γ′,σ′){\displaystyle (\Gamma ',\sigma ')}se puede obtener del par principal(Γ,σ){\displaystyle (\Gamma ,\sigma )}mediante expansiones de tipos, elevaciones y sustituciones. [ 21 ]

Referencias

  1. ↑ 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.
  2. 1 2 3 4 5 Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1980). "Una extensión de la teoría de la funcionalidad básica para el cálculo λ " . Notre Dame Journal of Formal Logic . 21 (4): 685– 693. doi : 10.1305/ndjfl/1093883253 . S2CID 29748788 . 
  3. 1 2 3 4 5 Barendregt, Henk; Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1983). "Un modelo lambda de filtro y la completitud de la asignación de tipos". Journal of Symbolic Logic . 48 (4): 931– 940. doi : 10.2307/2273659 . JSTOR 2273659 . S2CID 45660117 .  
  4. ↑ van Bakel, Steffen (2011). "Tipos de intersección estricta para el cálculo Lambda". ACM Computing Surveys . 43 (3): 20:1–20:49. CiteSeerX 10.1.1.310.2166 . doi : 10.1145/1922649.1922657 . S2CID 5537689 .  
  5. ↑ "Tipos de intersección en TypeScript" . Consultado el 1 de agosto de 2019 .
  6. ↑ "Tipos compuestos en Scala" . Consultado el 1 de agosto de 2019 .
  7. 1 2 Pottinger, G. (1980). Una asignación de tipos para los términos λ fuertemente normalizables . A HB Curry: ensayos sobre lógica combinatoria, cálculo lambda y formalismo, 561-577.
  8. 1 2 Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Sallé, Patrick (1979). "Caracterización funcional de algunas igualdades semánticas dentro del cálculo lambda". En Hermann A. Maurer (ed.). Autómatas, lenguajes y programación, 6.º Coloquio, Graz, Austria, 16-20 de julio de 1979, Actas . Vol. 71. Springer. pp. 133–146 . doi : 10.1007/3-540-09510-1_11 . ISBN   3-540-09510-1.
  9. ↑ Coppo, Mario; Dezani-Ciancaglini, Mariangiola (1978). "Una nueva asignación de tipo para términos λ ". Archiv für mathematische Logik und Grundlagenforschung . 19 (1): 139– 156. doi : 10.1007/BF02011875 . S2CID 206809924 . 
  10. ↑ Coppo, Mario; Dezani-Ciancaglini, Mariangiola; Venneri, Betti (1981). "Características funcionales de términos resolubles". Mathematical Logic Quarterly . 27 ( 2– 6): 45– 58. doi : 10.1002/malq.19810270205 .
  11. ↑ Kfoury, AJ; Wells, JB (enero de 2004). "Principalidad e inferencia de tipos para tipos de intersección usando variables de expansión". Theoretical Computer Science : 1–70 .
  12. ↑ Terauchi, T., Aiken, A.: Sobre la tipabilidad para tipos de intersección de rango 2 con recursión polimórfica. En: LICS, IEEE Computer Society (2006) pp. 111–122
  13. ↑ Urzyczyn, Paweł (1999). "El problema del vacío para los tipos de intersección". Journal of Symbolic Logic . 64 (3): 1195– 1215. doi : 10.2307/2586625 . JSTOR 2586625. S2CID 36979036 .  
  14. ↑ Urzyczyn, Paweł (2009). "Habitación de tipos de intersección de bajo rango". Conferencia Internacional sobre Cálculos Lambda Tipados y Aplicaciones . TLCA 2009. Vol. 5608. Springer. pp. 356–370 . doi : 10.1007/978-3-642-02273-9_26 . ISBN   978-3-642-02272-2.
  15. ↑ Dudenhefner, Andrej; Rehof, Jakob (2019). "Principalidad y aproximación bajo límites dimensionales". Actas de la ACM sobre lenguajes de programación . POPL 2019. Vol. 3. ACM. pp. 8:1–8:29. doi : 10.1145/3290321 . ISSN 2475-1421 .   
  16. ↑ Fairouz Dib Kamareddine, Joe Wells "Tipos de intersección mediante declaraciones de conjuntos finitos" https://arxiv.org/pdf/2405.00440 WoLLIC 2024
  17. ↑ Van Bakel, Steffen (1992). "Restricciones completas de la disciplina de tipo intersección". Theoretical Computer Science . 102 (1): 135– 163. CiteSeerX 10.1.1.310.903 . doi : 10.1016/0304-3975(92)90297-S . 
  18. ↑ Dudenhefner, Andrej; Martens, Moritz; Rehof, Jakob (2017). "El problema de unificación del tipo de intersección algebraica". Métodos lógicos en informática . 13 (3). arXiv : 1611.05672 . doi : 10.23638/LMCS-13(3:9)2017 . S2CID 31640337 . 
  19. ↑ Ghilezan, Silvia (1996). "Normalización fuerte y tipabilidad con tipos de intersección" . Notre Dame Journal of Formal Logic . 37 (1): 44– 52. doi : 10.1305/ndjfl/1040067315 .
  20. ↑ Wells, JB (2003). "La esencia de los tipados principales". ICALP '02: Actas del 29.º Coloquio Internacional sobre Autómatas, Lenguajes y Programación . págs. 913–925 . 
  21. ↑ 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 .