En lógica matemática , System U y System U - son sistemas de tipos puros , es decir, formas especiales de un cálculo lambda tipificado con un número arbitrario de géneros , axiomas y reglas (o dependencias entre los géneros). Ambos fueron demostrados inconsistentes por Jean-Yves Girard en 1972. [1] Este resultado llevó a la comprensión de que la teoría de tipos original de 1971 de Martin-Löf 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 clases ;
- dos axiomas ; y
- cinco reglas .
Sistema U - se define de la misma manera con la excepción del regla.
Los géneros y se denominan convencionalmente "Tipo" y " Clase ", respectivamente; el tipono tiene un nombre específico. Los dos axiomas describen la contención de tipos en clases () y tipos en (). Intuitivamente, los tipos describen una jerarquía en la naturaleza de los términos.
- Todos los valores tienen un tipo , como un tipo base ( p . Ej. se lee como " b es un booleano") o un tipo de función (dependiente) ( p . ej. se lee como " f es una función de números naturales a booleanos").
- es el tipo de todos esos tipos (se lee como " t es un tipo"). De podemos construir más términos, como cuál es el tipo de operadores de nivel de tipo unario ( p . ej. 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.
- es el tipo de todos esos tipos (se lee como " k es un tipo"). De manera similar, podemos construir términos relacionados, de acuerdo con lo que permitan las reglas.
- 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 los tipos ( polimorfismo ),permite que los tipos dependan de los tipos ( operadores de tipo ), etc.
La paradoja de Girard
Las definiciones de Sistema de U y U - permiten la asignación de polimórficas tipo a constructores genéricos en analogía a tipos polimórficas de términos en cálculos lambda polimórficas clásicos, tales como System F . Un ejemplo de un constructor genérico de este tipo podría ser [2] : 353 (donde k denota una variable de tipo)
- .
Este mecanismo es suficiente para construir un término con el tipo , lo que implica que todo tipo está habitado . Según la correspondencia de Curry-Howard , esto equivale a que todas las proposiciones lógicas sean probables, lo que hace que el sistema sea inconsistente.
La paradoja de Girard es el análogo de la teoría de tipos de la paradoja de Russell en la teoría de conjuntos .
Referencias
- ^ Girard, Jean-Yves (1972). "Interprétation fonctionnelle et Élimination des coupures de l'arithmétique d'ordre supérieur" (PDF) . Cite journal requiere
|journal=
( ayuda ) - ^ a b Sørensen, Morten Heine; Urzyczyn, Paweł (2006). "Sistemas de tipo puro y el cubo lambda". Conferencias sobre el isomorfismo Curry-Howard . Elsevier. 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 Ciencias de la Computación . IEEE Computer Society Press. págs. 227-236.