Sistema U

Formas especiales de un cálculo lambda tipificado

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.

Definición formal

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

• tres tipos ; ${\displaystyle \{\ast ,\square ,\triangle \}}$
• 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 )}$

La paradoja de Girard

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 .

Referencias

1. Girard, Jean-Yves (1972). "Interprétation fonctionnelle et Élimination des coupures de l'arithmétique d'ordre supérieur" (PDF) .
2. Sørensen, Morten Heine; Urzyczyn, Paweł (2006). "Sistemas de tipos puros y el cubo lambda". Lecciones sobre el isomorfismo de Curry-Howard . Elsevier. doi :10.1016/S0049-237X(06)80015-7. ISBN 0-444-52077-5.

Lectura adicional

• 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.