Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Intuitionistic type theory
Résumé
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.
Martin-Löf designed the type theory on the principles of mathematical constructivism. Constructivism requires any existence proof to contain a "witness". So, any proof of "there exists a prime greater than 1000" must identify a specific number that is both prime and greater than 1000. Intuitionistic type theory accomplished this design goal by internalizing the BHK interpretation. An interesting consequence is that proofs become mathematical objects that can be examined, compared, and manipulated.
Intuitionistic type theory's type constructors were built to follow a one-to-one correspondence with logical connectives. For example, the logical connective called implication () corresponds to the type of a function (). This correspondence is called the Curry–Howard isomorphism. Previous type theories had also followed this isomorphism, but Martin-Löf's was the first to extend it to predicate logic by introducing dependent types.
Intuitionistic type theory has 3 finite types, which are then composed using 5 different type constructors. Unlike set theories, type theories are not built on top of a logic like Frege's. So, each feature of the type theory does double duty as a feature of both math and logic.
If you are unfamiliar with type theory and know set theory, a quick summary is: Types contain terms just like sets contain elements. Terms belong to one and only one type. Terms like and compute ("reduce") down to canonical terms like 4.
Source officielle
À 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.
Proximité ontologique
Cours associés (33)
ME-331: Solid mechanics
Model the behavior of elastic, viscoelastic, and inelastic solids both in the infinitesimal and finite-deformation regimes.
CH-310: Dynamics and kinetics
The course covers the principles of chemical kinetics, including differential rate laws, derivation of exact and approximate integral rate laws for common elementary and composite reactions, fundament
Séances de cours associées (274)
Chimie quantique
Couvre les valeurs propres, les fonctions propres, les opérateurs ermitiens et la mesure des observables en chimie quantique.
Weibull Modèle: Random Data
Explore l'application du modèle Weibull aux données aléatoires et son importance dans l'analyse de la force matérielle et de la probabilité de défaillance.
Mécanique des fractures: croissance des fissures et lien le plus faible
Explore la mécanique des fractures, la croissance des fissures et la théorie des maillons les plus faibles, en mettant l'accent sur la distribution statistique des tailles de fissures et l'importance de la plus grande fissure dans la défaillance matérielle.
Publications associées (151)
Personnes associées (31)
Unités associées (3)
Concepts associés (18)
Type dépendant
En Informatique et en Logique, un type dépendant est un type qui peut dépendre d'une valeur définie dans le langage typé. Les langages Agda et Gallina (de l'assistant de preuve Coq) sont des exemples de langages à type dépendant. Les types dépendants permettent par exemple de définir le type des listes à n éléments. Voici un exemple en Coq. Inductive Vect (A: Type): nat -> Type := | nil: Vect A 0 | cons (n: nat) (x: A) (t: Vect A n): Vect A (S n).
Extensionality
In logic, extensionality, or extensional equality, refers to principles that judge objects to be equal if they have the same external properties. It stands in contrast to the concept of intensionality, which is concerned with whether the internal definitions of objects are the same. Consider the two functions f and g mapping from and to natural numbers, defined as follows: To find f(n), first add 5 to n, then multiply by 2. To find g(n), first multiply n by 2, then add 10.
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.
MOOCs associés (14)
Advanced Timber Plate Structural Design
A trans-disciplinary approach in structural design and digital architecture of timber structures with advanced manufacturing workflow.
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
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