En logique mathématique, le Système U et le Système U− sont des , c'est-à-dire des formes spéciales d'un lambda-calcul 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 ; 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.

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 Système F. Un exemple d'un tel constructeur générique pourrait être l'exemple suivant, où k désigne une variable de genre :

.

Ce mécanisme est suffisant pour construire un terme de type, 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 Burali-Forti en théorie des ensembles.

Notes et références

Bibliographie

Catégorie:Théorie des types Catégorie:Théorie de la démonstration