Sistema U

En lógica matemática , el Sistema U y el Sistema U ⁻ son sistemas de tipos puros , es decir, formas especiales de un cálculo lambda tipado con un número arbitrario de tipos , axiomas y reglas (o dependencias entre los tipos). Jean-Yves Girard demostró la inconsistencia del Sistema U en 1972 ^[1] (y se formuló la cuestión de la consistencia del Sistema U ⁻ ). Este resultado condujo a la conclusión de que la teoría de tipos original de Martin-Löf de 1971 era inconsistencia, ya que permitía el mismo comportamiento de "Tipo en Tipo" que explota la paradoja de Girard.

El sistema U se define ^{[2] : 352} como un sistema de tipo puro con

• tres tipos ;${\displaystyle \{\ast,\cuadrado,\triángulo \}}$
• dos axiomas ; y${\displaystyle \{\ast :\square ,\square :\triangle \}}$
• cinco reglas .${\displaystyle \{(\ast ,\ast ),(\square ,\ast ),(\square ,\square ),(\triangle ,\ast ),(\triangle ,\square )\}}$

El sistema U ⁻ se define de la misma manera con excepción de la regla. ${\displaystyle (\triangle ,\ast )}$

Los tipos y se denominan convencionalmente “Tipo” y “ Clase ”, respectivamente; el tipo no tiene un nombre específico. Los dos axiomas describen la contención de tipos en tipos ( ) y tipos en ( ). Intuitivamente, los tipos describen una jerarquía en la naturaleza de los términos. ${\displaystyle \ast }$${\displaystyle \square }$${\displaystyle \triangle }$${\displaystyle \ast :\square }$${\displaystyle \triangle }$${\displaystyle \square :\triangle }$

1. Todos los valores tienen un tipo , como un tipo base ( por ejemplo, se lee como “ b es un booleano”) o un tipo de función (dependiente) ( por ejemplo, se lee como “ f es una función de números naturales a booleanos”).${\displaystyle b:\mathrm {Bool} }$ ${\displaystyle f:\mathrm {Nat} \to \mathrm {Bool} }$
2. ${\displaystyle \ast }$es el tipo de todos esos tipos ( se lee como “ t es un tipo”). A partir de esto podemos construir más términos, como que es el tipo de operadores unarios a nivel de tipo ( por ejemplo, se lee como “ La lista es una función de tipos a tipos”, es decir, un tipo polimórfico). Las reglas restringen cómo podemos formar nuevos tipos.${\displaystyle t:\ast }$${\displaystyle \ast }$${\displaystyle \ast \to \ast }$ ${\displaystyle \mathrm {List} :\ast \to \ast }$
3. ${\displaystyle \square }$es el tipo de todos los tipos ( se lee como “ k es un tipo”). De manera similar, podemos construir términos relacionados, de acuerdo con lo que permitan las reglas.${\displaystyle k:\square }$
4. ${\displaystyle \triangle }$Es el tipo de todos esos términos.

Las reglas gobiernan las dependencias entre los tipos: dice que los valores pueden depender de valores ( funciones ), permite que los valores dependan de tipos ( polimorfismo ), permite que los tipos dependan de tipos ( operadores de tipo ), etc. ${\displaystyle (\ast ,\ast )}$${\displaystyle (\square ,\ast )}$${\displaystyle (\square ,\square )}$

Las definiciones de Sistema U y U ⁻ permiten la asignación de tipos polimórficos a constructores genéricos en analogía con los tipos polimórficos de términos en cálculos lambda polimórficos clásicos, como el Sistema F. Un ejemplo de un constructor genérico de este tipo podría ser ^{[2] : 353} (donde k denota una variable de tipo)

${\displaystyle \lambda k^{\square }\lambda \alpha ^{k\to k}\lambda \beta ^{k}\!.\alpha (\alpha \beta )\;:\;\Pi k:\square .((k\to k)\to k\to k)}$.

Este mecanismo es suficiente para construir un término con el tipo (equivalente al tipo ), lo que implica que todo tipo está habitado . Por la correspondencia de Curry-Howard , esto es equivalente a que todas las proposiciones lógicas sean demostrables, lo que hace que el sistema sea inconsistente. ${\displaystyle (\forall p:\ast ,p)}$${\displaystyle \bot }$

La paradoja de Girard es el análogo en teoría de tipos de la paradoja de Russell en la teoría de conjuntos .

• Barendregt, Henk (1992). "Cálculos lambda con tipos". En S. Abramsky; D. Gabbay; T. Maibaum (eds.). Manual de lógica en informática . Oxford Science Publications . págs. 117–309.
• Coquand, Thierry (1986). "Análisis de la paradoja de Girard". Lógica en la informática . IEEE Computer Society Press. pp. 227–236.
• Hurkens, Antonius JC (1995). Dezani-Ciancaglini, Mariangiola; Plotkin, Gordon (eds.). Una simplificación de la paradoja de Girard. Segunda Conferencia Internacional sobre Cálculos Lambda Tipográficos y Aplicaciones (TLCA '95). Edimburgo. págs. 266–278. doi :10.1007/BFb0014058.