Demuestre o refute la conjetura de Barendregt-Geuvers-Klop.
En las ramas de la lógica matemática conocidas como teoría de prueba y teoría de tipos , un sistema de tipos puros ( PTS ), anteriormente conocido como sistema de tipos generalizados ( GTS ), es una forma de cálculo lambda tipificado que permite un número arbitrario de clases y dependencias entre cualquiera de estos. El marco puede ser visto como una generalización de Barendregt 's cubo lambda , en el sentido de que todas las esquinas del cubo pueden ser representados como instancias de un PTS con sólo dos clases. [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 este no es generalmente el caso, por ejemplo, el cálculo lambda simplemente tipado permite que solo los términos dependan de condiciones.
Los sistemas de tipo puro 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 L-cube por Geuvers, quien en su tesis doctoral extendió la correspondencia Curry-Howard a este escenario. [6] Basándose en estas ideas, Barthe y otros definieron los sistemas clásicos de tipo puro ( CPTS ) agregando 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 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 uno puede expresar la frase "los tipos forman un tipo".) Por otra parte, todos los ejemplos conocidos de sistemas de tipos puros que no son fuertemente normalización no son ni siquiera (débilmente) normalizadora : contienen expresiones que no tienen formas normales , al igual que el cálculo lambda sin tipo [ cita requerida ] . Es un gran problema abierto en el campo si este es siempre el caso, es decir, si un PTS que se normaliza (débilmente) siempre tiene la propiedad de normalización fuerte. Esto se conoce como la conjetura de Barendregt-Geuvers-Klop [10] (llamada así por Henk Barendregt , Herman Geuvers y Jan Willem Klop ).
Definición
Un sistema de tipo puro se define por un triple dónde es el conjunto de clases, es el conjunto de axiomas, y es el conjunto de reglas. La escritura en sistemas de tipos puros está determinada por las siguientes reglas, dondees de cualquier tipo: [4]
Implementaciones
Los siguientes lenguajes de programación tienen sistemas de tipos puros: [ cita requerida ]
Ver también
- Sistema U : un ejemplo de PTS inconsistente
- λμ-calculus utiliza un enfoque de control diferente al de CPTS
Notas
- ↑ a b Pierce, Benjamin (2002). Tipos y lenguajes de programación . Prensa del MIT. pag. 466 . ISBN 0-262-16209-1.
- ^ a b 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.
- ^ 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 .
- ^ a b 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 .
- ^ Berardi, S. (1990). Dependencia de tipo y matemática constructiva (tesis doctoral). Universidad de Torino.
- ^ Geuvers, H. (1993). Lógica y sistemas de tipos (tesis doctoral). Universidad de Nijmegen. CiteSeerX 10.1.1.56.7045 .
- ^ Barthe, G .; Hatcliff, J .; Sørensen, MH (1997). "Una noción de sistema de tipo puro 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 .
- ^ Borghuis, Tijn (1998). "Sistemas de tipo puro modal". Revista de Lógica, Lenguaje e Información . 7 (3): 265-296. doi : 10.1023 / A: 1008254612284 . S2CID 5067584 .
- ^ 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.
- ^ Sørensen, Morten Heine; Urzyczyn, Paweł (2006). "Sistemas de tipo puro y el cubo lambda § 14.7" . Conferencias sobre el isomorfismo Curry-Howard . Elsevier. pag. 358. ISBN 0-444-52077-5.
- ^ SABIO
- ^ Milenrama
- ^ Henk 2000
Referencias
- Berardi, Stefano (1988). Hacia un análisis matemático del cálculo de construcciones de Coquand-Huet y los otros sistemas en el 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 analyse van GSTTs" (en holandés). Holanda: Universidad de Nijmegen. Cite journal requiere
|journal=
( ayuda )
Otras lecturas
- Schmidt, David A. (1994). "§ 8.3 Sistemas de tipo generalizado" . 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 nLab
- Jones, Roger Bishop (1999). "Descripción general de Pure Type Systems" .