Théorie des types
La théorie des types est une branche de la logique mathématique qui a pour principales caractéristiques que tout objet (terme, fonction, ensemble) y a un type et que les entités ne peuvent se combiner qu'en respectant des règles de "typage"[1].
Une première théorie des types (dite "ramifiée") a été créée par Bertrand Russell pour résoudre les paradoxes logiques, comme celui du menteur et ceux de la théorie des ensembles ; lourde d'emploi, elle a d'abord été simplifiée par Ramsey et ensuite supplantée par les théories de Zermelo-Frankel et NF de Quine (voir [1])[2], et aussi reconsidérée pour des objets plus élémentaires après la découverte du lambda-calcul et de la logique combinatoire. Bien que ces théories soient cohérentes dans leurs versions originelles, qui sont non typées, il est intéressant d'en étudier des formulations avec types.
Dans ces derniers cas, les entités mathématiques sont construites à l'aide de fonctions, où chaque fonction a un type qui décrit le type de ses arguments et le type de la valeur retournée. Les entités sont bien formées lorsque les fonctions sont appliquées à des entités ayant le type que la fonction attend.
Le concept de type a plusieurs domaines d'applications :
- les théories des ensembles qui, suivant l'intuition de Russell, classent les ensembles en différents types,
- la logique pour laquelle on cherche à donner un contenu calculatoire aux propositions et aux démonstrations par la correspondance de Curry Howard,
- la théorie des modèles, où un type est un ensemble de formules particulier,
- les langages de programmation, surtout les langages fonctionnels typés,
- les systèmes de démonstration sur ordinateur,
- la linguistique, à travers le concept de catégorie syntaxique[3].
Notes
- C'est un des moyens utilisés pour éviter les paradoxes.
- La notion de type reste latente dans ZF, via la hiérarchie cumulative, et dans NF, via la notion de stratification.
- La définition de type par Russell, comme domaine de signifiance d'une fonction propositionnelle, était du reste linguistique.
