Sistema de tipo puro

Forma de cálculo lambda mecanografiado

Problema no resuelto 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 la prueba y teoría de tipos , un sistema de tipos puro ( PTS ), anteriormente conocido como sistema de tipos generalizado ( GTS ), es una forma de cálculo lambda tipado que permite un número arbitrario de tipos y dependencias entre cualquiera de estos. 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 sólo dos tipos. ^{[1] [2]} De hecho, Barendregt (1991) enmarcó su cubo en este escenario. ^[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 generalmente este no es el caso; por ejemplo, el cálculo lambda de tipo simple permite que sólo los términos dependan de términos.

Los sistemas de tipos puros fueron introducidos de forma independiente 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 denominada cubo L por Herman Geuvers, quien en su tesis doctoral amplió la correspondencia Curry-Howard a este entorno. ^[6] Basándose en estas ideas, G. Barthe y otros definieron los sistemas clásicos de tipo puro ( CPTS ) añadiendo un operador de doble negación . ^[7] De manera similar, en 1998, Tijn Borghuis introdujo los sistemas modales de tipo puro ( MPTS ). ^[8] Roorda ha discutido la aplicación de sistemas de tipo puro 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 se normalizan fuertemente . Los sistemas de tipo puro en general no tienen por qué 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 tipos puros 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 sin tipo ^{[ cita requerida ]} . Es un gran problema abierto en este campo si esto es siempre el caso, es decir, si un PTS (débilmente) normalizador siempre tiene la propiedad de normalización fuerte. Esto se conoce como la conjetura de Barendregt-Geuvers-Klop ^[10] (llamada así en honor a Henk Barendregt , Herman Geuvers y Jan Willem Klop ).

Definición

Un sistema de tipos puro se define por un triple donde es el conjunto de tipos, es el conjunto de axiomas y es el conjunto de reglas. La escritura 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 necesaria ]}

• SALVIA ^[11]
• milenrama ^[12]
• Henk 2000 ^[13]

Ver también

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

Notas

1. Pierce, Benjamín (2002). Tipos y Lenguajes de Programación . Prensa del MIT. pag. 466.ISBN​ 0-262-16209-1.
2. Kamareddine, Fairouz D.; Laan, Twan; Nederpelt, Rob P. (2004). "Sección 4c: Sistemas de tipo puro". Una perspectiva moderna de la teoría de tipos: desde sus orígenes hasta la actualidad . Saltador. pag. 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 . Publicaciones científicas de Oxford .
5. Berardi, S. (1990). Dependencia de tipos y Matemática Constructiva (tesis doctoral). Universidad de Turín .
6. Geuvers, H. (1993). Lógicas y Sistemas de Tipos (tesis doctoral). Universidad de Nimega . CiteSeerX 10.1.1.56.7045 . 
7. Barthe, G.; Hatcliff, J.; Sorensen, MH (1997). "Una noción del sistema de tipos puros clásico". Apuntes Electrónicos 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 modales de tipo puro". 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 tipo puro para programación funcional". Archivado desde el original el 2 de octubre de 2011 . Consultado el 29 de agosto de 2010 . La tesis de maestría de Roorda (vinculada 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 tipo puro y el cubo lambda § 14.7". Conferencias sobre el isomorfismo de Curry-Howard . Elsevier. pag. 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 construcciones de Coquand-Huet y los demás sistemas del cubo de Barendregt (Informe técnico). Departamento de Ciencias de la Computación, 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.

Otras lecturas

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

enlaces externos

• Sistema de tipo puro en el n Lab
• Jones, Roger Obispo (1999). "Descripción general de los sistemas de tipo puro".