Ê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
Système F
Résumé
Le est un formalisme logique qui permet d'exprimer de façon très riche et très rigoureuse des fonctions et d'y démontrer formellement des propriétés difficiles. Plus précisément, le (également connu sous le nom de lambda-calcul polymorphe ou de lambda-calcul du second ordre) est une extension du lambda-calcul simplement typé introduite indépendamment par le logicien Jean-Yves Girard et par l'informaticien John C. Reynolds.
Ce système se distingue du lambda-calcul simplement typé par l'existence d'une quantification universelle sur les types qui permet d'exprimer du polymorphisme.
Le possède deux propriétés cruciales :
la réduction des termes est fortement normalisante (dit plus crûment : tous les calculs se terminent) ;
il correspond par la correspondance de Curry-Howard à la logique minimale propositionnelle du second ordre. Soit : le calcul propositionnel, sans la négation mais avec les quantificateurs.
Note liminaire : La lecture de cet article suppose la lecture préalable de l'article « lambda-calcul » et son assimilation .
Ainsi que l'atteste sa double origine, le peut être étudié dans deux contextes très différents :
Dans le domaine de la programmation fonctionnelle, où il apparaît comme une extension très expressive du noyau du langage ML. Son expressivité est illustrée par le fait que les types de données courants (booléens, entiers, listes, etc.) sont définissables dans le à partir des constructions de base ;
Dans le domaine de la logique, et plus particulièrement de la théorie de la démonstration. À travers la correspondance de Curry-Howard, le est en effet isomorphe à la logique minimale du second ordre. En outre, ce système capture très exactement la classe des fonctions numériques dont l'existence est prouvable en arithmétique intuitionniste du second ordre (parfois appelée analyse intuitionniste). C'est d'ailleurs cette propriété remarquable du qui a historiquement motivé son introduction par Jean-Yves Girard, dans la mesure où cette propriété permet de résoudre le problème de l'élimination des coupures en arithmétique du second ordre, conjecturé par Takeuti.
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.