Système U (mathématiques)

En logique mathématique, le Système U et le Système U⁻ sont des systèmes de types purs, c'est-à-dire des formes spéciales d'un calcul lambda typé avec un nombre arbitraire de sortes, d'axiomes et de règles (ou de relations entre les sortes). Ils ont tous deux été prouvés incohérents par Jean-Yves Girard en 1972. Ce résultat conduit alors à ce que la théorie des types de Martin-Löf de 1971 est incohérente car elle permet le même comportement de «type dans le type» que le paradoxe de Girard exploite.

Définition formelle

Le système U est défini comme un système de type pur avec

• trois sortes$\{\ast ,\square ,\triangle \}$ ;
• deux axiomes$\{\ast :\square ,\square :\triangle \}$ ; et
• cinq règles$\{(\ast ,\ast ),(\square ,\ast ),(\square ,\square ),(\triangle ,\ast ),(\triangle ,\square )\}$ .

Système U⁻ est défini de la même manière à l'exception de la règle $(\triangle ,\ast )$.

Les sortes $\ast$ et $\square$ sont classiquement appelés respectivement «Type» et « Genre »; le genre $\triangle$ n'a pas de nom spécifique. Les deux axiomes décrivent "l'inclusion" des types dans les genres ($\ast :\square$ ) et des genres dans $\triangle$ ($\square :\triangle$ ). Intuitivement, les sortes décrivent une hiérarchie dans la nature des termes.

1. Toutes les valeurs ont un type, tel qu'un type de base ( par exemple $b:\mathrm {Bool}$ est lu comme «b est un booléen») ou un type de fonction (par exemple$f:\mathrm {Nat} \to \mathrm {Bool}$ est lu comme « f est une fonction des nombres naturels aux booléens»).
2. $\ast$ est la sorte de tous ces types ($t:\ast$ est lu comme « t est un type»). De $\ast$ nous pouvons créer plus de termes, tels que $\ast \to \ast$ qui est le genre d'opérateurs de type niveau unaire (par exemple $\mathrm {List} :\ast \to \ast$ se lit : «List est une fonction allant des types aux types», c'est-à-dire un type polymorphe). Les règles limitent la manière dont nous pouvons former de nouveaux genres.
3. $\square$ est la sorte de tous ces genres ($k:\square$ est lu comme « k est un genre»). De même, nous pouvons construire des termes liés, selon ce que les règles permettent.
4. $\triangle$ est la sorte de tous ces termes.

Les règles régissent les dépendances entre les sortes : $(\ast ,\ast )$ dit que les valeurs peuvent dépendre de valeurs (fonctions),$(\square ,\ast )$ permet aux valeurs de dépendre des types (polymorphisme), $(\square ,\square )$ permet aux types de dépendre des types (opérateurs de type), etc.

Le paradoxe de Girard

Les définitions des systèmes U et U⁻ permettent l'attribution de types polymorphes à des constructeurs génériques par analogie avec des types polymorphes de termes dans des calculs lambda polymorphes classiques, tels que le System F. Un exemple d'un tel constructeur générique pourrait être (où k désigne une variable de genre)

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

Ce mécanisme est suffisant pour construire un terme de type$(\forall p:\ast ,p)=\bot$, ce qui implique que chaque type est habité. Par la correspondance de Curry-Howard, cela implique (et est même équivalent à ce) que toutes les propositions logiques soient prouvables, ce qui rend le système incohérent.

Le paradoxe de Girard est l'analogue en théorie des types du paradoxe de Russell en théorie des ensembles .

Bibliographie

• Henk Barendregt, Handbook of Logic in Computer Science, Oxford Science Publications, 1992, 117–309 p., « Lambda calculi with types »
• Thierry Coquand, Logic in Computer Science, IEEE Computer Society Press, 1986, 227–236 p., « An analysis of Girard's paradox »