Sistema de tipos puros

En las ramas de la lógica matemática conocidas como teoría de la demostración 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 clases y dependencias entre cualquiera de ellas. El marco puede verse como una generalización del cubo lambda de Barendregt , en el sentido de que todos los vértices del cubo pueden representarse como instancias de un PTS con solo dos clases. ^{[ 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 con el cálculo de construcciones , pero este no es el caso en general, por ejemplo, el cálculo lambda simplemente tipado permite que solo los términos dependan de otros términos.

Los sistemas de tipos puros fueron introducidos independientemente por Stefano Berardi (1988) y Jan Terlouw (1989). ^{[ 1 ] [ 2 ]} Barendregt los analizó extensamente en sus trabajos 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 extendió la correspondencia de Curry-Howard a este contexto. ^{[ 6 ]} Basándose en estas ideas, G.  Barthe y otros definieron los sistemas de tipos puros clásicos (CPTS) mediante la adición de 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 analizado 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 normalizadores . Los sistemas de tipos puros 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 frase "los tipos forman un tipo"). Además, todos los ejemplos conocidos de sistemas de tipos puros que no son fuertemente normalizadores ni siquiera son (débilmente) normalizadores : contienen expresiones que no tienen formas normales , al igual que el cálculo lambda sin tipos . Es un problema abierto importante en el campo determinar si esto siempre es así, 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 (llamada así por Henk Barendregt , Herman Geuvers y Jan Willem Klop ). ^{[ 10 ]}

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

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

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

${\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{(debilitamiento)}}}$

${\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:AB:s_{3}}}\quad {\text{(producto)}}}$

${\displaystyle {\frac {\Gamma \vdash C:\Pi x:AB\quad \Gamma \vdash a:A}{\Gamma \vdash Ca:B[x:=a]}}\quad {\text{(aplicación)}}}$

${\displaystyle {\frac {\Gamma ,x:A\vdash b:B\quad \Gamma \vdash \Pi x:AB:s}{\Gamma \vdash \lambda x:Ab:\Pi x:AB}}\quad {\text{(abstracción)}}}$

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

Los siguientes lenguajes de programación tienen sistemas de tipos puros:

• SALVIA ^{[ 11 ]}
• Milenrama ^{[ 12 ]}
• Henk 2000 ^{[ 13 ]}
• Haskell desde la versión 8 de GHC. ^{[ 14 ] [ 15 ]}

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

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

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