Ê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
Calcul des constructions
Résumé
Le calcul des constructions (CoC de l'anglais calculus of constructions) est un lambda-calcul typé d'ordre supérieur dans lequel les types sont des valeurs de première classe. Il est par conséquent possible, dans le CoC, de définir des fonctions qui vont des entiers vers les entiers, mais aussi des entiers vers les types ou des types vers les types.
Le CoC est fortement normalisant, bien que, d'après le théorème d'incomplétude de Gödel, il soit impossible de démontrer cette propriété dans le CoC lui-même, puisqu'elle implique sa cohérence.
Le CoC a été développé initialement par Thierry Coquand.
Le CoC a été à l'origine des premières versions de l'assistant de preuves Coq. Les versions suivantes ont été construites à partir du calcul des constructions inductives qui est une extension du CoC qui intègre des types de données inductives. Dans le CoC originel, les types de données inductives devaient être émulés à l'aide de leur fonction de destruction.
La façon de définir le calcul des constructions par trois types de dépendances est appelée le lambda cube et est due à Henk Barendregt.
Le calcul des constructions peut être considéré comme une extension de la correspondance de Curry-Howard. Cette dernière associe chaque terme du lambda-calcul simplement typé à une preuve en déduction naturelle dans la logique propositionnelle intuitionniste, et réciproquement. Le calcul des constructions étend cet isomorphisme aux preuves dans le calcul des prédicats intuitionniste dans son ensemble, ce qui inclut par conséquent des preuves de formules quantifiées (que l'on appellera également « propositions »).
Un terme du calcul des constructions est construit à l'aide des règles suivantes :
est un terme (également appelé Type)
est un terme (également appelé Prop, le type de toutes les propositions)
Si et sont des termes, le sont également :
()
()
Le calcul des constructions possède cinq types d'objets :
les preuves, qui sont des termes dont les types sont des propositions ;
les propositions, qui sont aussi appelées petits types ;
les prédicats, qui sont des fonctions qui retournent des propositions ;
les types larges, qui sont des types de prédicats (par exemple P est un type large) ;
T lui-même, qui est le type des types larges.
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.