Théorie des types

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

En mathématiques, logique et informatique, une théorie des types est une classe de systèmes formels, dont certains peuvent servir d'alternatives à la théorie des ensembles comme fondation des mathématiques. Grosso modo un type est une « caractérisation » des éléments qu'un terme qualifie. En théorie des types, chaque terme possède un type et les opérations décrites par le système imposent des restrictions sur le type des termes qu'elles combinent.

La théorie des types est très liée à (et recoupe parfois) l'étude des systèmes de types qui sont utilisés dans certains langages de programmation afin d'éviter certains bugs. Cependant, historiquement les théories des types ont été introduites pour empêcher des paradoxes de la logique formelle et l'expression « théorie des types » renvoie souvent à ce contexte plus large.

Deux théories des types qui émergent peuvent servir de fondations pour les mathématiques ; ce sont le λ-calcul typé d'Alonzo Church et la théorie des types intuitionniste de Per Martin-Löf. Quoi qu'il en soit, les théories des types créée par les logiciens trouvent une application majeure comme systèmes axiomatiques de la majorité des assistants de preuve du fait de la correspondance de Curry-Howard liant démonstrations et programmes.

Histoire[modifier | modifier le code]

Les types ont été pour la première fois théorisés par Bertrand Russell comme réponse à sa découverte du paradoxe ébranlant la théorie naïve des ensembles de Gottlob Frege. Cette théorie des types est développée dans l'ouvrage Principia Mathematica de Russell et Whitehead. Elle permet de contourner le paradoxe de Russell en introduisant tout d'abord une hiérarchie de types, puis en assignant un type à chaque entité mathématique. Les objets d'un certain type ne peuvent être construits qu'à partir d'objets leur pré-existant (situés plus bas dans la hiérarchie), empêchant ainsi les boucles infinies.

Dans le langage courant, « théorie des types » est à comprendre dans le contexte des systèmes de réécriture. L'exemple le plus connu est le lambda calcul d'Alonzo Church. Sa Theory of Types[1] a permis de passer du calcul non-typé originel, inconsistant du fait du paradoxe de Kleene-Rosser (en), à un calcul correct. Church a démontré que ce système pouvait servir de fondement des mathématiques ; on le décrit comme une logique d'ordre supérieur.

D'autres théories des types marquantes sont la théorie des types intuitionniste de Per Martin-Löf qui est utilisée comme fondement dans certaines branches des mathématiques constructivistes et pour des assistants de preuve tels que Agda (en) ou Idris. Le calcul des constructions de Thierry Coquand et ses extensions sont utilisés notamment par Coq et Matita (en). Le champ est un sujet de recherche actif comme le démontrent les récents développements en théorie des types homotopiques (en)[2].

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 puis supplantée par la théorie de Zermelo-Frankel en 1922 (socle axiomatique utilisé par tous les mathématiciens, l'autre théorie NF conçue par Quine en 1937 et perfectionnée en NFU en 1969 par Ronald Jensen (en) n'étant pas utilisée par les mathématiciens malgré les possibilités simplificatrices qu'elle offre, voir New Foundations[3]), 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.

Applications[modifier | modifier le code]

Le concept de type a plusieurs domaines d'applications :

Notes[modifier | modifier le code]

  1. (en) Alonzo Church, « A formulation of the simple theory of types », J. Symb. Logic, vol. 5, no 2,‎ , p. 56-68 (JSTOR 2266170).
  2. (en) Álvaro Pelayo et Michael A. Warren, « Homotopy type theory and Voevodsky's univalent foundations », Bull. Amer. Math. Soc., vol. 51,‎ , p. 597-648 (lire en ligne).
  3. La notion de type reste latente dans ZF, via la hiérarchie cumulative, et dans NF, via la notion de stratification.
  4. La définition de type par Russell, comme domaine de signifiance d'une fonction propositionnelle, était du reste linguistique.

Voir aussi[modifier | modifier le code]