Système F

Carte Commune · n° 491391

Le système F (aussi appelé lambda-calcul polymorphe ou de lambda-calcul du second ordre) est un formalisme logique qui permet d'exprimer de façon très riche[Quoi ?] et très rigoureuse[Quoi ?] des fonctions et d'y démontrer formellement des propriétés difficiles[Quoi ?]. Plus précisément, le système F 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[pas clair] d'une quantification universelle sur les types qui permet d'exprimer du polymorphisme. Le système F possède deux propriétés cruciales : Vu comme un système de réécriture de termes, le système F est fortement normalisant (autrement dit, 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...

Lire sur Wikipédia