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. Le système U est défini comme un système de type pur avec trois sortes ; deux axiomes ; et cinq règles . Système U− est défini de la même manière à l'exception de la règle . Les sortes et sont classiquement appelés respectivement «Type» et « Genre »; le genre n'a pas de nom spécifique. Les deux axiomes décrivent "l'inclusion" des types dans les genres ( ) et des genres dans ( ). Intuitivement, les sortes décrivent une hiérarchie dans la nature des termes. Toutes les valeurs ont un type, tel qu'un type de base ( par exemple est lu comme « est un booléen») ou un type de fonction (par exemple est lu comme « est une fonction des nombres naturels aux booléens»). est la sorte de tous ces types ( est lu comme « est un type»). De nous pouvons créer plus de termes, tels que qui est le genre d'opérateurs de type niveau unaire (par exemple se lit : « 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. est la sorte de tous ces genres ( est lu comme « est un genre»). De même, nous pouvons construire des termes liés, selon ce que les règles permettent. est la sorte de tous ces termes. Les règles régissent les dépendances entre les sortes : dit que les valeurs peuvent dépendre de valeurs (fonctions), permet aux valeurs de dépendre des types (polymorphisme), permet aux types de dépendre des types (opérateurs de type), etc.