Sistema de tipo puro

Forma del cálculo lambda tipificado

Problema sin resolver en informática :

Pruebe o refute la conjetura de Barendregt-Geuvers-Klop.

(más problemas sin resolver en informática)

En las ramas de la lógica matemática conocidas como teoría de pruebas y teoría de tipos , un sistema de tipos puros ( PTS ), anteriormente conocido como sistema de tipos generalizado ( GTS ), es una forma de cálculo lambda tipado que permite un número arbitrario de ordenaciones y dependencias entre cualquiera de estas. El marco puede verse como una generalización del cubo lambda de Barendregt , en el sentido de que todas las esquinas del cubo pueden representarse como instancias de un PTS con solo dos ordenaciones. ^{[1] [2]} De hecho, Barendregt (1991) enmarcó su cubo en este contexto. ^[3] Los sistemas de tipos puros pueden oscurecer la distinción entre tipos y términos y colapsar la jerarquía de tipos , como es el caso del cálculo de construcciones , pero este no es generalmente el caso, por ejemplo, el cálculo lambda simplemente tipado permite que solo los términos dependan de términos.

Los sistemas de tipos puros fueron introducidos independientemente por Stefano Berardi (1988) y Jan Terlouw (1989). ^{[1] [2]} Barendregt los discutió extensamente en sus artículos posteriores. ^[4] En su tesis doctoral, ^[5] Berardi definió un cubo de lógicas constructivas similar al cubo lambda (estas especificaciones no son dependientes). Una modificación de este cubo fue posteriormente llamada el cubo L por Herman Geuvers, quien en su tesis doctoral extendió la correspondencia Curry-Howard a esta configuración. ^[6] Basándose en estas ideas, G. Barthe y otros definieron los sistemas de tipos puros clásicos ( CPTS ) añadiendo un operador de doble negación . ^[7] De manera similar, en 1998, Tijn Borghuis introdujo los sistemas de tipos puros modales ( MPTS ). ^[8] Roorda ha discutido la aplicación de los sistemas de tipos puros a la programación funcional ; y Roorda y Jeuring han propuesto un lenguaje de programación basado en sistemas de tipos puros. ^[9]

Se sabe que todos los sistemas del cubo lambda son fuertemente normalizantes . Los sistemas de tipo puro en general no necesitan serlo, por ejemplo, el Sistema U de la paradoja de Girard no lo es. (En términos generales, Girard encontró sistemas puros en los que se puede expresar la oración "los tipos forman un tipo"). Además, todos los ejemplos conocidos de sistemas de tipo puro que no son fuertemente normalizantes ni siquiera son (débilmente) normalizantes : contienen expresiones que no tienen formas normales , al igual que el cálculo lambda no tipificado ^{[ cita requerida ]} . Es un importante problema abierto en el campo si este es siempre el caso, es decir, si un PTS (débilmente) normalizante siempre tiene la propiedad de normalización fuerte. Esto se conoce como la conjetura de Barendregt–Geuvers–Klop ^[10] (nombrada en honor a Henk Barendregt , Herman Geuvers y Jan Willem Klop ).

Definición

Un sistema de tipos puros se define mediante una tripleta donde es el conjunto de tipos, es el conjunto de axiomas y es el conjunto de reglas. La tipificación en sistemas de tipos puros está determinada por las siguientes reglas, donde es cualquier tipo: ^[4] ${\textstyle ({\mathcal {S}},{\mathcal {A}},{\mathcal {R}})}$ ${\textstyle {\mathcal {S}}}$ ${\textstyle {\mathcal {A}}\subseteq {\mathcal {S}}^{2}}$ ${\textstyle {\mathcal {R}}\subseteq {\mathcal {S}}^{3}}$ ${\textstyle s}$

${\displaystyle {\frac {(s_{1},s_{2})\in {\mathcal {A}}}{\vdash s_{1}:s_{2}}}\quad {\text{(axiom)}}}$

${\displaystyle {\frac {\Gamma \vdash A:s\quad x\notin {\text{dom}}(\Gamma )}{\Gamma ,x:A\vdash x:A}}\quad {\text{(start)}}}$

${\displaystyle {\frac {\Gamma \vdash A:B\quad \Gamma \vdash C:s\quad x\notin {\text{dom}}(\Gamma )}{\Gamma ,x:C\vdash A:B}}\quad {\text{(weakening)}}}$

${\displaystyle {\frac {\Gamma \vdash A:s_{1}\quad \Gamma ,x:A\vdash B:s_{2}\quad (s_{1},s_{2},s_{3})\in {\mathcal {R}}}{\Gamma \vdash \Pi x:A.B:s_{3}}}\quad {\text{(product)}}}$

${\displaystyle {\frac {\Gamma \vdash C:\Pi x:A.B\quad \Gamma \vdash a:A}{\Gamma \vdash Ca:B[x:=a]}}\quad {\text{(application)}}}$

${\displaystyle {\frac {\Gamma ,x:A\vdash b:B\quad \Gamma \vdash \Pi x:A.B:s}{\Gamma \vdash \lambda x:A.b:\Pi x:A.B}}\quad {\text{(abstraction)}}}$

${\displaystyle {\frac {\Gamma \vdash A:B\quad B=_{\beta }B'\quad \Gamma \vdash B':s}{\Gamma \vdash A:B'}}\quad {\text{(conversion)}}}$

Implementaciones

Los siguientes lenguajes de programación tienen sistemas de tipos puros: ^{[ cita requerida ]}

• SABIO ^[11]
• Milenrama ^[12]
• Henk 2000 ^[13]

Véase también

• Sistema U : un ejemplo de un PTS inconsistente
• El cálculo λμ utiliza un enfoque de control diferente al CPTS

Notas

1. Pierce, Benjamin (2002). Tipos y lenguajes de programación . MIT Press. pág. 466. ISBN 0-262-16209-1.
2. Kamareddine, Fairouz D.; Laan, Twan; Nederpelt, Rob P. (2004). "Sección 4c: Sistemas de tipos puros". Una perspectiva moderna sobre la teoría de tipos: desde sus orígenes hasta hoy . Springer. pág. 116. ISBN 1-4020-2334-0.
3. Barendregt, HP (1991). "Introducción a los sistemas de tipos generalizados". Revista de programación funcional . 1 (2): 125–154. doi :10.1017/s0956796800020025. hdl : 2066/17240 . S2CID  44757552.
4. Barendregt, H. (1992). "Cálculos lambda con tipos". En Abramsky, S.; Gabbay, D.; Maibaum, T. (eds.). Manual de lógica en informática . Oxford Science Publications .
5. Berardi, S. (1990). Dependencia de tipos y matemáticas constructivas (tesis doctoral). Universidad de Turín .
6. Geuvers, H. (1993). Lógica y sistemas de tipos (tesis doctoral). Universidad de Nijmegen . CiteSeerX 10.1.1.56.7045 . 
7. Barthe, G.; Hatcliff, J.; Sørensen, MH (1997). "Una noción de sistema de tipos puros clásico". Notas electrónicas en informática teórica . 6 : 4–59. CiteSeerX 10.1.1.32.1371 . doi :10.1016/S1571-0661(05)80170-7. 
8. Borghuis, Tijn (1998). "Sistemas de tipos puros modales". Revista de lógica, lenguaje e información . 7 (3): 265–296. doi :10.1023/A:1008254612284. S2CID  5067584.
9. Jan-Willem Roorda; Johan Jeuring. "Sistemas de tipos puros para programación funcional". Archivado desde el original el 2011-10-02 . Consultado el 2010-08-29 . La tesis de maestría de Roorda (enlazada desde la página citada) también contiene una introducción general a los sistemas de tipos puros.
10. Sørensen, Morten Heine; Urzyczyn, Paweł (2006). "Sistemas de tipos puros y el cubo lambda § 14.7". Lecciones sobre el isomorfismo de Curry-Howard . Elsevier. pág. 358. ISBN 0-444-52077-5.
11. SABIO
12. Milenrama
13. Henk 2000

Referencias

• Berardi, Stefano (1988). Hacia un análisis matemático del cálculo de Coquand-Huet de construcciones y otros sistemas en el cubo de Barendregt (informe técnico). Departamento de Informática, CMU, y Dipartimento Matematica, Universita di Torino. CMU-CS-88-131.
• Terlouw, J. (1989). "Een nadere bewijstheoretische analice van GSTT" (Documento) (en holandés). Países Bajos: Universidad de Nijmegen.

Lectura adicional

• Schmidt, David A. (1994). "§ 8.3 Sistemas de tipos generalizados". La estructura de los lenguajes de programación tipados . MIT Press. págs. 255–8. ISBN 0-262-19349-3.

Enlaces externos

• Sistema de tipos puros en el laboratorio n
• Jones, Roger Bishop (1999). "Descripción general de los sistemas de tipos puros".