Théorie des types

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. Ils ont été historiquement introduits pour résoudre le paradoxe d'un axiome de compréhension non restreint. En théorie des types, il existe des types de base et des constructeurs (comme celui des fonctions ou encore celui du produit cartésien) qui permettent de créer de nouveaux types à partir de types préexistant. Une différence notable avec la théorie des ensembles est que chaque terme possède un type, ce qui est un jugement subjectif et non pas une proposition . En d'autres termes la question de savoir si un terme appartient ou non à un type n'est pas réputée objective. Des types sont utilisés dans certains langages de programmation, ce qui permet d'éviter des bugs. Toutefois, la théorie des types fait plus souvent références à l'étude des systèmes de types qui servent de fondation alternative aux mathématiques. Le λ-calcul typé d'Alonzo Church et ses extensions permettent de faire de la logique à différents ordres ; ainsi elles servent à formaliser le système F. Dans la même ligne, la théorie des types intuitionniste de Per Martin-Löf ainsi que le calcul des constructions inductif offrent d'autres perspectives. Ceux-ci sont notamment à la base d' ou de Coq qui sont des assistants de preuve. D'un point de vue de la théorie mathématique : 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 et les paradoxes de surgir et de casser la théorie.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (131)

Cours associés (212)

Séances de cours associées (1 000)

MOOCs associés (17)

Fondements des mathématiques

Les fondements des mathématiques sont les principes de la philosophie des mathématiques sur lesquels est établie cette science. Le logicisme a été prôné notamment par Gottlob Frege et Bertrand Russell. La mathématique pure présente deux caractéristiques : la généralité de son discours et la déductibilité du discours mathématique . En ce que le discours mathématique ne prétend qu’à une vérité formelle, il est possible de réduire les mathématiques à la logique, les lois logiques étant les lois du « vrai ».

Lambda-calcul

Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930, qui fonde les concepts de fonction et d'application. On y manipule des expressions appelées λ-expressions, où la lettre grecque λ est utilisée pour lier une variable. Par exemple, si M est une λ-expression, λx.M est aussi une λ-expression et représente la fonction qui à x associe M. Le λ-calcul a été le premier formalisme pour définir et caractériser les fonctions récursives : il a donc une grande importance dans la théorie de la calculabilité, à l'égal des machines de Turing et du modèle de Herbrand-Gödel.

Théorie des types

MATH-506: Topology IV.b - cohomology rings

Singular cohomology is defined by dualizing the singular chain complex for spaces. We will study its basic properties, see how it acquires a multiplicative structure and becomes a graded commutative a

ME-437: Advanced solid mechanics

ME-331: Solid mechanics

Model the behavior of elastic, viscoelastic, and inelastic solids both in the infinitesimal and finite-deformation regimes.

Advanced Timber Plate Structural Design

A trans-disciplinary approach in structural design and digital architecture of timber structures with advanced manufacturing workflow.

Initiation à la Programmation en C++

Ce cours initie à la programmation en utilisant le langage C++. Il ne présuppose pas de connaissance préalable. Les aspects plus avancés (programmation orientée objet) sont donnés dans un cours suivan

Geographical Information Systems 1

Organisé en deux parties, ce cours présente les bases théoriques et pratiques des systèmes d’information géographique, ne nécessitant pas de connaissances préalables en informatique. En suivant cette

Gestion de la dose en microscopie électronique

Explore les défis et les solutions pour gérer la dose d'électrons en microscopie, en soulignant l'importance d'un suivi et d'une analyse précis des doses.

Chimie quantique

Couvre les valeurs propres, les fonctions propres, les opérateurs ermitiens et la mesure des observables en chimie quantique.

Tutoriel iMesh et iConc

Couvre le tutoriel pour iMesh et iConc, en se concentrant sur la création d'élément Finite Mesh pour les structures en béton.