Théorie des types
- 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.
Voir aussi
|
Informatique théorique |
| Théorie du calcul |
|
| Logique, syntaxe et sémantique |
|
| Algorithmique, complexité et mathématiques discrètes |
|
Wikimedia Foundation.
2010.
Contenu soumis à la licence CC-BY-SA. Source : Article Théorie des types de Wikipédia en français (auteurs)
Regardez d'autres dictionnaires:
Theorie des types — 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 … Wikipédia en Français
Theorie des ensembles — Théorie des ensembles La théorie des ensembles est une branche des mathématiques, créée par le mathématicien allemand Georg Cantor à la fin du XIXe siècle. La théorie des ensembles se donne comme primitives les notions d ensemble et d… … Wikipédia en Français
Theorie des graphes — Théorie des graphes Pour la notion mathématique utilisée en Théorie des ensembles, voir Graphe d une fonction. La théorie des graphes est une branche commune à l informatique et aux mathématiques étudiant les graphes et les objets qui lui… … Wikipédia en Français
Theorie des langages — Théorie des langages La théorie des langages a pour objectif de comprendre le fonctionnement des langages, vus comme moyen de communication, d un point de vue mathématique. Un langage est un ensemble de mots. Un mot (ou lexème) est une… … Wikipédia en Français
Théorie des langages et automates — Théorie des langages La théorie des langages a pour objectif de comprendre le fonctionnement des langages, vus comme moyen de communication, d un point de vue mathématique. Un langage est un ensemble de mots. Un mot (ou lexème) est une… … Wikipédia en Français
Théorie des ensembles — La théorie des ensembles est une branche des mathématiques, créée par le mathématicien allemand Georg Cantor à la fin du XIXe siècle. La théorie des ensembles se donne comme primitives les notions d ensemble et d appartenance, à partir… … Wikipédia en Français
Théorie des expressions rationnelles — Langage rationnel Pour les articles homonymes, voir Langage, Régulier et Rationnel. Les expressions rationnelles permettent d engendrer une famille de langages appelés, suivant les auteurs, langages rationnels ou langages réguliers. Ce sont les… … Wikipédia en Français
Theorie des jeux en relations internationales — Théorie des jeux en relations internationales Les relations « entre nations » ont depuis longtemps été un objet d étude, mais les relations internationales, en tant que discipline scientifique sont nées après la Première Guerre mondiale … Wikipédia en Français
Théorie des jeux et relations internationales — Théorie des jeux en relations internationales Les relations « entre nations » ont depuis longtemps été un objet d étude, mais les relations internationales, en tant que discipline scientifique sont nées après la Première Guerre mondiale … Wikipédia en Français
Theorie des systemes sociaux — Théorie des systèmes sociaux La théorie des systèmes sociaux est une théorie sociologique développée par le sociologue et penseur allemand Niklas Luhmann à partir des bases de la théorie de Talcott Parsons dont il a suivi les cours à Harvard… … Wikipédia en Français
