Sistema U

En lógica matemática, Sistema U y Sistema U⁻ son sistemas de tipos puros, es decir, formas especiales de un cálculo lambda tipado con un número arbitrario de géneros, axiomas y reglas (o dependencias entre los géneros). Jean-Yves Girard demostró que ambos eran inconsistentes en 1972.​ Este resultado llevó a darse cuenta de que la teoría de tipos original de Martin-Löf de 1971 era inconsistente, ya que permitía el mismo comportamiento de «Tipo en tipo» que explota la paradoja de Girard.

Definición formal

El Sistema U se define​ como un sistema de tipo puro con

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

El Sistema U⁻ se define igual con la excepción del $(\triangle ,\ast )$ regla.

los tipos $\ast$ y $\square$ se denominan convencionalmente «Tipo» y «Tipo», respectivamente; el tipo $\triangle$ no tiene un nombre especifico. Los dos axiomas describen la contención de tipos en clases ( $\ast :\square$ ) y tipos en $\triangle$ ( $\square :\triangle$ ). Intuitivamente, los géneros describen una jerarquía en la naturaleza de los términos.

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

Las reglas rigen las dependencias entre los géneros: $(\ast ,\ast )$ dice que los valores pueden depender de los valores (funciones), $(\square ,\ast )$ permite que los valores dependan de los tipos (polimorfismo), $(\square ,\square )$ permite que los tipos dependan de los tipos (operadores de tipo), y así sucesivamente.

Paradoja de Girard

Las definiciones de Sistema U y U⁻ permiten la asignación de tipos polimórficos a constructores genéricos de forma análoga a los tipos polimórficos de términos en cálculos lambda polimórficos clásicos, como Sistema F. Un ejemplo de un constructor genérico de este tipo podría ser​ (donde k denota una especie de variable)

$\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 $(\forall p:\ast ,p)$ (equivale al tipo $\bot$ ), 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.

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

Lectura adicional

• Barendregt, Henk (1992). «Lambda calculi with types». En S. Abramsky; D. Gabbay; T. Maibaum, eds. Handbook of Logic in Computer Science. Oxford Science Publications. pp. 117-309. 
• Coquand, Thierry (1986). «An analysis of Girard's paradox». Logic in Computer Science. IEEE Computer Society Press. pp. 227-236. 

• Datos: Q22909237