Système F

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.