Sistema U

Formas especiales de un cálculo lambda mecanografiado.

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 tipificado con un número arbitrario de tipos , axiomas y reglas (o dependencias entre los tipos). Jean-Yves Girard demostró en 1972 ^{[1] que} el Sistema U era inconsistente (y ^se formuló la cuestión de la coherencia del Sistema U ). Este resultado llevó a la comprensión 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.

Definicion 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 igual con la excepción de la regla. ${\displaystyle (\triangle ,\ast )}$

Los géneros y se denominan convencionalmente “Tipo” y “ Tipo ”, respectivamente; el género no tiene un nombre específico. Los dos axiomas describen la contención de tipos en clases ( ) y clases en ( ). Intuitivamente, los géneros 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 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 ahí podemos construir más términos, como cuál es el tipo de operadores unarios de 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 género de todos esos géneros ( se lee como “ k es un género”). De manera similar podemos construir términos relacionados, según 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 System 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 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 . Según la correspondencia Curry-Howard , esto equivale 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 teórico 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 tipo puro y el cubo lambda". Conferencias sobre el isomorfismo de Curry-Howard . Elsevier. doi :10.1016/S0049-237X(06)80015-7. ISBN 0-444-52077-5.

Otras lecturas

• Barendregt, Henk (1992). "Cálculos lambda con tipos". En S. Abramsky; D. Gabbay; T. Maibaum (eds.). Manual de lógica en informática . Publicaciones científicas de Oxford . págs. 117–309.
• Coquand, Thierry (1986). "Un análisis de la paradoja de Girard". Lógica en Informática . Prensa de la Sociedad de Computación IEEE . págs. 227-236.
• Hurkens, Antonio JC (1995). Dezani-Ciancaglini, Mariangiola; Plotkin, Gordon (eds.). Una simplificación de la paradoja de Girard. Segunda Conferencia Internacional sobre Cálculos Lambda Tipificados y Aplicaciones (TLCA '95). Edimburgo. págs. 266-278. doi :10.1007/BFb0014058.